%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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