diff --git a/smt/0016_sol.tex b/smt/0016_sol.tex index 3899f63..e8a5623 100644 --- a/smt/0016_sol.tex +++ b/smt/0016_sol.tex @@ -6,5 +6,5 @@ &\{x,f(y),u,v,z,v\},\{y,f(u)\}, \{f(x),f(z)\} \end{align*} -Checking the disequality $f(x) \neq f(z)$ leads to the result that the assignment is UNSAT, since $f(x)$ and $f(z)$ -are in the same congruence class. \ No newline at end of file +Checking the inequalities $f(x) \neq f(z)$ leads to the result that the assignment is UNSAT, since $f(x)$ and $f(z)$ +are in the same congruence class. diff --git a/smt/1032_sol.tex b/smt/1032_sol.tex index aa9961c..2eed9b5 100644 --- a/smt/1032_sol.tex +++ b/smt/1032_sol.tex @@ -1,8 +1,8 @@ \begin{align*} & \{f(b),a\}, \{e,b\}, \{c,f(c)\}, \{f(e)\}, \{\underline{f(a)},f(d)\}, \{d,\underline{f(a)}\} \\ & \{\underline{f(b)},a\}, \{\underline{e,b}\}, \{c,f(c)\}, \{\underline{f(e)}\}, \{f(a),f(d),d\} \\ - & \{f(b),a,f(e)\}, \{e,b\}, \{c,f(c)\}, \{f(a),f(d),d\} + & \{f(b),a,f(e)\}, \{e,b\}, \{c,f(c)\}, \{f(a),f(d),d\} \end{align*} -Checking the disequalities $d \neq f(e)$ and $a \neq f(c)$ leads to the result that the assignment is SAT, since neither $d$ and $f(e)$ nor $a$ and $f(c)$ -are in the same congruence class. \ No newline at end of file +Checking the inequalities $d \neq f(e)$ and $a \neq f(c)$ leads to the result that the assignment is SAT, since neither $d$ and $f(e)$ nor $a$ and $f(c)$ +are in the same congruence class. diff --git a/smt/1033_sol.tex b/smt/1033_sol.tex index 124d7ad..078db79 100644 --- a/smt/1033_sol.tex +++ b/smt/1033_sol.tex @@ -7,5 +7,5 @@ & \{k,m,n,o,f(k),f(m),f(n),f(o)\}, \{l\} \\ \end{align*} -Checking the disequalities $o \neq k$, $f(m) \neq k$, $m \neq f(m)$ leads to the result that the assignment is UNSAT, since $o$ and $k$, $f(m)$ and $k$, $m$ and $f(m)$ +Checking the inequalities $o \neq k$, $f(m) \neq k$, $m \neq f(m)$ leads to the result that the assignment is UNSAT, since $o$ and $k$, $f(m)$ and $k$, $m$ and $f(m)$ are in the same congruence class.