%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Problem: data/problems/all/SYN075-1.tptp Clauses: (~big_f \$X \$Y \/ \$X = a) /\ (~big_f \$X \$Y \/ \$Y = b) /\ (~(\$X = a) \/ ~(\$Y = b) \/ big_f \$X \$Y) /\ (~(\$Y = g \$X) \/ ~big_f \$Y (f \$X) \/ f \$X = \$X) /\ (~big_f \$Y (f \$X) \/ ~big_f (h \$X \$Z) (f \$X) \/ \$Y = g \$X \/ big_f (h \$X \$Z) (f \$X)) /\ (~(\$Y = g \$X) \/ f \$X = \$X \/ big_f \$Y (f \$X)) /\ (~(\$Y = g \$X) \/ h \$X \$Z = \$Z \/ big_f \$Y (f \$X) \/ big_f (h \$X \$Z) (f \$X)) /\ (~(\$Y = g \$X) \/ ~(h \$X \$Z = \$Z) \/ ~big_f (h \$X \$Z) (f \$X) \/ big_f \$Y (f \$X)) /\ (~(f \$X = \$X) \/ h \$X \$Z = \$Z \/ big_f (h \$X \$Z) (f \$X)) /\ (~(f \$X = \$X) \/ ~(h \$X \$Z = \$Z) \/ ~big_f (h \$X \$Z) (f \$X)) % SZS status Unsatisfiable for data/problems/all/SYN075-1.tptp % SZS output start CNFRefutation for data/problems/all/SYN075-1.tptp cnf(clause_1, axiom, (~ big_f(X, Y) | X = a)). cnf(clause_3, axiom, (X != a | Y != b | big_f(X, Y))). cnf(clause_4, negated_conjecture, (~ big_f(Y, f(X)) | Y != g(X) | f(X) = X)). cnf(clause_6, negated_conjecture, (Y != g(X) | big_f(Y, f(X)) | f(X) = X)). cnf(clause_9, negated_conjecture, (f(X) != X | big_f(h(X, Z), f(X)) | h(X, Z) = Z)). cnf(clause_10, negated_conjecture, (f(X) != X | h(X, Z) != Z | ~ big_f(h(X, Z), f(X)))). cnf(refute_0_0, plain, (a != a | b != b | big_f(a, b)), inference(subst, [], [clause_3 : [bind(X, \$fot(a)), bind(Y, \$fot(b))]])). cnf(refute_0_1, plain, (a = a), introduced(tautology, [refl, [\$fot(a)]])). cnf(refute_0_2, plain, (b != b | big_f(a, b)), inference(resolve, [\$cnf(\$equal(a, a))], [refute_0_1, refute_0_0])). cnf(refute_0_3, plain, (b = b), introduced(tautology, [refl, [\$fot(b)]])). cnf(refute_0_4, plain, (big_f(a, b)), inference(resolve, [\$cnf(\$equal(b, b))], [refute_0_3, refute_0_2])). cnf(refute_0_5, plain, (h(X, Z) != Z | ~ big_f(Z, f(X)) | big_f(h(X, Z), f(X))), introduced(tautology, [equality, [\$cnf(~ big_f(h(X, Z), f(X))), [0], \$fot(Z)]])). cnf(refute_0_6, plain, (f(X) != X | ~ big_f(Z, X) | big_f(Z, f(X))), introduced(tautology, [equality, [\$cnf(~ big_f(Z, f(X))), [1], \$fot(X)]])). cnf(refute_0_7, plain, (f(X) != X | h(X, Z) != Z | ~ big_f(Z, X) | big_f(h(X, Z), f(X))), inference(resolve, [\$cnf(big_f(Z, f(X)))], [refute_0_6, refute_0_5])). cnf(refute_0_8, plain, (f(X) != X | h(X, Z) != Z | ~ big_f(Z, X)), inference(resolve, [\$cnf(big_f(h(X, Z), f(X)))], [refute_0_7, clause_10])). cnf(refute_0_9, plain, (g(X) != g(X) | ~ big_f(g(X), f(X)) | f(X) = X), inference(subst, [], [clause_4 : [bind(Y, \$fot(g(X)))]])). cnf(refute_0_10, plain, (g(X) = g(X)), introduced(tautology, [refl, [\$fot(g(X))]])). cnf(refute_0_11, plain, (~ big_f(g(X), f(X)) | f(X) = X), inference(resolve, [\$cnf(\$equal(g(X), g(X)))], [refute_0_10, refute_0_9])). cnf(refute_0_12, plain, (~ big_f(g(X_3), f(X_3)) | f(X_3) = X_3), inference(subst, [], [refute_0_11 : [bind(X, \$fot(X_3))]])). cnf(refute_0_13, plain, (g(X) != g(X) | f(X) = X | big_f(g(X), f(X))), inference(subst, [], [clause_6 : [bind(Y, \$fot(g(X)))]])). cnf(refute_0_14, plain, (f(X) = X | big_f(g(X), f(X))), inference(resolve, [\$cnf(\$equal(g(X), g(X)))], [refute_0_10, refute_0_13])). cnf(refute_0_15, plain, (f(X_3) = X_3 | big_f(g(X_3), f(X_3))), inference(subst, [], [refute_0_14 : [bind(X, \$fot(X_3))]])). cnf(refute_0_16, plain, (f(X_3) = X_3), inference(resolve, [\$cnf(big_f(g(X_3), f(X_3)))], [refute_0_15, refute_0_12])). cnf(refute_0_17, plain, (f(X) = X), inference(subst, [], [refute_0_16 : [bind(X_3, \$fot(X))]])). cnf(refute_0_18, plain, (X != X | f(X) != X | f(X) = X), introduced(tautology, [equality, [\$cnf(\$equal(f(X), X)), [0, 0], \$fot(X)]])). cnf(refute_0_19, plain, (X != X | f(X) = X), inference(resolve, [\$cnf(\$equal(f(X), X))], [refute_0_17, refute_0_18])). cnf(refute_0_20, plain, (X != X | h(X, Z) != Z | ~ big_f(Z, X)), inference(resolve, [\$cnf(\$equal(f(X), X))], [refute_0_19, refute_0_8])). cnf(refute_0_21, plain, (X = X), introduced(tautology, [refl, [\$fot(X)]])). cnf(refute_0_22, plain, (h(X, Z) != Z | ~ big_f(Z, X)), inference(resolve, [\$cnf(\$equal(X, X))], [refute_0_21, refute_0_20])). cnf(refute_0_23, plain, (h(X, a) != a | ~ big_f(a, X)), inference(subst, [], [refute_0_22 : [bind(Z, \$fot(a))]])). cnf(refute_0_24, plain, (~ big_f(h(X_9, X_10), X_9) | h(X_9, X_10) = a), inference(subst, [], [clause_1 : [bind(X, \$fot(h(X_9, X_10))), bind(Y, \$fot(X_9))]])). cnf(refute_0_25, plain, (f(X) != X | ~ big_f(h(X, Z), f(X)) | big_f(h(X, Z), X)), introduced(tautology, [equality, [\$cnf(big_f(h(X, Z), f(X))), [1], \$fot(X)]])). cnf(refute_0_26, plain, (f(X) != X | h(X, Z) = Z | big_f(h(X, Z), X)), inference(resolve, [\$cnf(big_f(h(X, Z), f(X)))], [clause_9, refute_0_25])). cnf(refute_0_27, plain, (X != X | h(X, Z) = Z | big_f(h(X, Z), X)), inference(resolve, [\$cnf(\$equal(f(X), X))], [refute_0_19, refute_0_26])). cnf(refute_0_28, plain, (h(X, Z) = Z | big_f(h(X, Z), X)), inference(resolve, [\$cnf(\$equal(X, X))], [refute_0_21, refute_0_27])). cnf(refute_0_29, plain, (h(X_9, X_10) = X_10 | big_f(h(X_9, X_10), X_9)), inference(subst, [], [refute_0_28 : [bind(X, \$fot(X_9)), bind(Z, \$fot(X_10))]])). cnf(refute_0_30, plain, (h(X_9, X_10) = X_10 | h(X_9, X_10) = a), inference(resolve, [\$cnf(big_f(h(X_9, X_10), X_9))], [refute_0_29, refute_0_24])). cnf(refute_0_31, plain, (h(X, a) = a), inference(subst, [], [refute_0_30 : [bind(X_10, \$fot(a)), bind(X_9, \$fot(X))]])). cnf(refute_0_32, plain, (a != a | h(X, a) != a | h(X, a) = a), introduced(tautology, [equality, [\$cnf(\$equal(h(X, a), a)), [0, 1], \$fot(a)]])). cnf(refute_0_33, plain, (a != a | h(X, a) = a), inference(resolve, [\$cnf(\$equal(h(X, a), a))], [refute_0_31, refute_0_32])). cnf(refute_0_34, plain, (a != a | ~ big_f(a, X)), inference(resolve, [\$cnf(\$equal(h(X, a), a))], [refute_0_33, refute_0_23])). cnf(refute_0_35, plain, (~ big_f(a, X)), inference(resolve, [\$cnf(\$equal(a, a))], [refute_0_1, refute_0_34])). cnf(refute_0_36, plain, (~ big_f(a, b)), inference(subst, [], [refute_0_35 : [bind(X, \$fot(b))]])). cnf(refute_0_37, plain, (\$false), inference(resolve, [\$cnf(big_f(a, b))], [refute_0_4, refute_0_36])). % SZS output end CNFRefutation for data/problems/all/SYN075-1.tptp