---------------------------------------------------------------------------
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(0, plain, (X != a | Y != b | big_f(X, Y)),
    inference(cnf_normalization, [], [clause_3])).

cnf(1, plain, (a != a | b != b | big_f(a, b)),
    inference(subst, [], [0 : [bind(X, $fot(a)), bind(Y, $fot(b))]])).

cnf(2, plain, (a = a), introduced(tautology, [refl, [$fot(a)]])).

cnf(3, plain, (b != b | big_f(a, b)),
    inference(resolve, [$cnf('$equal'(a, a))], [2, 1])).

cnf(4, plain, (b = b), introduced(tautology, [refl, [$fot(b)]])).

cnf(5, plain, (big_f(a, b)),
    inference(resolve, [$cnf('$equal'(b, b))], [4, 3])).

cnf(6, plain, (f(X) != X | h(X, Z) != Z | ~ big_f(h(X, Z), f(X))),
    inference(cnf_normalization, [], [clause_10])).

cnf(7, plain, (h(X, Z) != Z | h(X, Z) = Z),
    introduced(tautology, [assume, [$cnf('$equal'(h(X, Z), Z))]])).

cnf(8, 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(9, plain, (f(X) != X | f(X) = X),
    introduced(tautology, [assume, [$cnf('$equal'(f(X), X))]])).

cnf(10, 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(11, 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)))], [10, 8])).

cnf(12, plain, (f(X) != X | h(X, Z) != Z | ~ big_f(Z, X)),
    inference(resolve, [$cnf(big_f(h(X, Z), f(X)))], [11, 6])).

cnf(13, plain, (Y != g(X) | f(X) = X | big_f(Y, f(X))),
    inference(cnf_normalization, [], [clause_6])).

cnf(14, plain, (g(X) != g(X) | f(X) = X | big_f(g(X), f(X))),
    inference(subst, [], [13 : [bind(Y, $fot(g(X)))]])).

cnf(15, plain, (g(X) = g(X)), introduced(tautology, [refl, [$fot(g(X))]])).

cnf(16, plain, (f(X) = X | big_f(g(X), f(X))),
    inference(resolve, [$cnf('$equal'(g(X), g(X)))], [15, 14])).

cnf(17, plain, (f(X2) = X2 | big_f(g(X2), f(X2))),
    inference(subst, [], [16 : [bind(X, $fot(X2))]])).

cnf(18, plain, (Y != g(X) | ~ big_f(Y, f(X)) | f(X) = X),
    inference(cnf_normalization, [], [clause_4])).

cnf(19, plain, (g(X) != g(X) | ~ big_f(g(X), f(X)) | f(X) = X),
    inference(subst, [], [18 : [bind(Y, $fot(g(X)))]])).

cnf(20, plain, (~ big_f(g(X), f(X)) | f(X) = X),
    inference(resolve, [$cnf('$equal'(g(X), g(X)))], [15, 19])).

cnf(21, plain, (~ big_f(g(X2), f(X2)) | f(X2) = X2),
    inference(subst, [], [20 : [bind(X, $fot(X2))]])).

cnf(22, plain, (f(X2) = X2),
    inference(resolve, [$cnf(big_f(g(X2), f(X2)))], [17, 21])).

cnf(23, plain, (f(X) = X),
    inference(subst, [], [22 : [bind(X2, $fot(X))]])).

cnf(24, plain, (X != X | f(X) != X | f(X) = X),
    introduced(tautology,
               [equality, [$cnf('$equal'(f(X), X)), [0, 0], $fot(X)]])).

cnf(25, plain, (X != X | f(X) = X),
    inference(resolve, [$cnf('$equal'(f(X), X))], [23, 24])).

cnf(26, plain, (X != X | h(X, Z) != Z | ~ big_f(Z, X)),
    inference(resolve, [$cnf('$equal'(f(X), X))], [25, 12])).

cnf(27, plain, (X = X), introduced(tautology, [refl, [$fot(X)]])).

cnf(28, plain, (h(X, Z) != Z | ~ big_f(Z, X)),
    inference(resolve, [$cnf('$equal'(X, X))], [27, 26])).

cnf(29, plain, (h(X, a) != a | ~ big_f(a, X)),
    inference(subst, [], [28 : [bind(Z, $fot(a))]])).

cnf(30, plain, (~ big_f(X, Y) | X = a),
    inference(cnf_normalization, [], [clause_1])).

cnf(31, plain, (~ big_f(h(X0, X1), X0) | h(X0, X1) = a),
    inference(subst, [],
              [30 : [bind(X, $fot(h(X0, X1))), bind(Y, $fot(X0))]])).

cnf(32, plain, (f(X) != X | h(X, Z) = Z | big_f(h(X, Z), f(X))),
    inference(cnf_normalization, [], [clause_9])).

cnf(33, 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(34, plain, (f(X) != X | h(X, Z) = Z | big_f(h(X, Z), X)),
    inference(resolve, [$cnf(big_f(h(X, Z), f(X)))], [32, 33])).

cnf(35, plain, (X != X | h(X, Z) = Z | big_f(h(X, Z), X)),
    inference(resolve, [$cnf('$equal'(f(X), X))], [25, 34])).

cnf(36, plain, (h(X, Z) = Z | big_f(h(X, Z), X)),
    inference(resolve, [$cnf('$equal'(X, X))], [27, 35])).

cnf(37, plain, (h(X0, X1) = X1 | big_f(h(X0, X1), X0)),
    inference(subst, [], [36 : [bind(X, $fot(X0)), bind(Z, $fot(X1))]])).

cnf(38, plain, (h(X0, X1) = X1 | h(X0, X1) = a),
    inference(resolve, [$cnf(big_f(h(X0, X1), X0))], [37, 31])).

cnf(39, plain, (h(X, a) = a),
    inference(subst, [], [38 : [bind(X0, $fot(X)), bind(X1, $fot(a))]])).

cnf(40, 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(41, plain, (a != a | h(X, a) = a),
    inference(resolve, [$cnf('$equal'(h(X, a), a))], [39, 40])).

cnf(42, plain, (a != a | ~ big_f(a, X)),
    inference(resolve, [$cnf('$equal'(h(X, a), a))], [41, 29])).

cnf(43, plain, (~ big_f(a, X)),
    inference(resolve, [$cnf('$equal'(a, a))], [2, 42])).

cnf(44, plain, (~ big_f(a, b)),
    inference(subst, [], [43 : [bind(X, $fot(b))]])).

cnf(45, plain, ($false), inference(resolve, [$cnf(big_f(a, b))], [5, 44])).
SZS output end CNFRefutation for data/problems/all/SYN075-1.tptp