Closed wo closed 1 month ago
∃x∀y((¬Rxx∨Rxy∨Ryx∨Ryy)∧(Rxx∨¬Rxy∨Ryx∨Ryy)∧(¬Rxx∨¬Rxy∨Ryx∨Ryy))) presents a "countermodel" with domain {0, 1, 2} and relation {(1,2), (2,0), (0,1), (0,0)}, which is not a countermodel. {(1,2), (2,0), (0,1) } is one.
If the first two conjuncts are swapped, no countermodel is found at all!
The problem seems to lie in the tseitin transformation. If that is turned off, the right model is found immediately.
∃x∀y((¬Rxx∨Rxy∨Ryx∨Ryy)∧(Rxx∨¬Rxy∨Ryx∨Ryy)∧(¬Rxx∨¬Rxy∨Ryx∨Ryy))) presents a "countermodel" with domain {0, 1, 2} and relation {(1,2), (2,0), (0,1), (0,0)}, which is not a countermodel. {(1,2), (2,0), (0,1) } is one.
If the first two conjuncts are swapped, no countermodel is found at all!
The problem seems to lie in the tseitin transformation. If that is turned off, the right model is found immediately.