---------------------------------------------------------------------------
Problem: data/problems/all/SYN075+1.tptp

Goal:
(?Z W. !X Y. big_f X Y <=> X = Z /\ Y = W) ==>
?W. !Y. (?Z. !X. big_f X Y <=> X = Z) <=> Y = W

Clauses:
(~big_f $X $Y \/ $X = skolemFOFtoCNF_Z) /\
(~big_f $X $Y \/ $Y = skolemFOFtoCNF_W) /\
(~($X = skolemFOFtoCNF_Z) \/ ~($Y = skolemFOFtoCNF_W) \/ big_f $X $Y) /\
(~($X = skolemFOFtoCNF_Z_1 $W) \/ skolemFOFtoCNF_Y $W = $W \/
 big_f $X (skolemFOFtoCNF_Y $W)) /\
(~(skolemFOFtoCNF_X $W $Z = $Z) \/ ~(skolemFOFtoCNF_Y $W = $W) \/
 ~big_f (skolemFOFtoCNF_X $W $Z) (skolemFOFtoCNF_Y $W)) /\
(~(skolemFOFtoCNF_Y $W = $W) \/ skolemFOFtoCNF_X $W $Z = $Z \/
 big_f (skolemFOFtoCNF_X $W $Z) (skolemFOFtoCNF_Y $W)) /\
(~big_f $X (skolemFOFtoCNF_Y $W) \/ $X = skolemFOFtoCNF_Z_1 $W \/
 skolemFOFtoCNF_Y $W = $W)

SZS status Theorem for data/problems/all/SYN075+1.tptp

SZS output start CNFRefutation for data/problems/all/SYN075+1.tptp
fof(pel52_1, axiom,
    (? [Z, W] : ! [X, Y] : (big_f(X, Y) <=> (X = Z & Y = W)))).

fof(pel52, conjecture,
    (? [W] : ! [Y] : (? [Z] : ! [X] : (big_f(X, Y) <=> X = Z) <=> Y = W))).

cnf(0, plain,
    (skolemFOFtoCNF_X(W, Z) != Z | skolemFOFtoCNF_Y(W) != W |
     ~ big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
    inference(cnf_normalization, [], [pel52])).

cnf(1, plain, (skolemFOFtoCNF_X(W, Z) != Z | skolemFOFtoCNF_X(W, Z) = Z),
    introduced(tautology,
               [assume, [$cnf('$equal'(skolemFOFtoCNF_X(W, Z), Z))]])).

cnf(2, plain,
    (skolemFOFtoCNF_X(W, Z) != Z | ~ big_f(Z, skolemFOFtoCNF_Y(W)) |
     big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
    introduced(tautology,
               [equality,
                [$cnf(~ big_f(skolemFOFtoCNF_X(W, Z),
                        skolemFOFtoCNF_Y(W))), [0], $fot(Z)]])).

cnf(3, plain, (skolemFOFtoCNF_Y(W) != W | skolemFOFtoCNF_Y(W) = W),
    introduced(tautology,
               [assume, [$cnf('$equal'(skolemFOFtoCNF_Y(W), W))]])).

cnf(4, plain,
    (skolemFOFtoCNF_Y(W) != W | ~ big_f(Z, W) |
     big_f(Z, skolemFOFtoCNF_Y(W))),
    introduced(tautology,
               [equality,
                [$cnf(~ big_f(Z, skolemFOFtoCNF_Y(W))), [1], $fot(W)]])).

cnf(5, plain,
    (skolemFOFtoCNF_X(W, Z) != Z | skolemFOFtoCNF_Y(W) != W |
     ~ big_f(Z, W) | big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
    inference(resolve, [$cnf(big_f(Z, skolemFOFtoCNF_Y(W)))], [4, 2])).

cnf(6, plain,
    (skolemFOFtoCNF_X(W, Z) != Z | skolemFOFtoCNF_Y(W) != W |
     ~ big_f(Z, W)),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W)))],
              [5, 0])).

cnf(7, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) !=
     skolemFOFtoCNF_Z |
     skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(subst, [],
              [6 :
               [bind(W, $fot(skolemFOFtoCNF_W)),
                bind(Z, $fot(skolemFOFtoCNF_Z))]])).

cnf(8, plain, (~ big_f(X, Y) | X = skolemFOFtoCNF_Z),
    inference(cnf_normalization, [], [pel52_1])).

cnf(9, plain,
    (~ big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1), skolemFOFtoCNF_W) |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1) = skolemFOFtoCNF_Z),
    inference(subst, [],
              [8 :
               [bind(X, $fot(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1))),
                bind(Y, $fot(skolemFOFtoCNF_W))]])).

cnf(10, plain,
    (skolemFOFtoCNF_Y(W) != W | skolemFOFtoCNF_X(W, Z) = Z |
     big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
    inference(cnf_normalization, [], [pel52])).

cnf(11, plain,
    (skolemFOFtoCNF_Y(W) != W |
     ~ big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W)) |
     big_f(skolemFOFtoCNF_X(W, Z), W)),
    introduced(tautology,
               [equality,
                [$cnf(big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
                 [1], $fot(W)]])).

cnf(12, plain,
    (skolemFOFtoCNF_Y(W) != W | skolemFOFtoCNF_X(W, Z) = Z |
     big_f(skolemFOFtoCNF_X(W, Z), W)),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W)))],
              [10, 11])).

cnf(13, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X0) = X0 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X0), skolemFOFtoCNF_W)),
    inference(subst, [],
              [12 :
               [bind(W, $fot(skolemFOFtoCNF_W)), bind(Z, $fot(X0))]])).

cnf(14, plain, (~ big_f(X, Y) | Y = skolemFOFtoCNF_W),
    inference(cnf_normalization, [], [pel52_1])).

cnf(15, plain,
    (~ big_f(skolemFOFtoCNF_Z_1(X2), skolemFOFtoCNF_Y(X2)) |
     skolemFOFtoCNF_Y(X2) = skolemFOFtoCNF_W),
    inference(subst, [],
              [14 :
               [bind(X, $fot(skolemFOFtoCNF_Z_1(X2))),
                bind(Y, $fot(skolemFOFtoCNF_Y(X2)))]])).

cnf(16, plain,
    (X != skolemFOFtoCNF_Z_1(W) | skolemFOFtoCNF_Y(W) = W |
     big_f(X, skolemFOFtoCNF_Y(W))),
    inference(cnf_normalization, [], [pel52])).

cnf(17, plain,
    (skolemFOFtoCNF_Z_1(W) != skolemFOFtoCNF_Z_1(W) |
     skolemFOFtoCNF_Y(W) = W |
     big_f(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Y(W))),
    inference(subst, [], [16 : [bind(X, $fot(skolemFOFtoCNF_Z_1(W)))]])).

cnf(18, plain, (skolemFOFtoCNF_Z_1(W) = skolemFOFtoCNF_Z_1(W)),
    introduced(tautology, [refl, [$fot(skolemFOFtoCNF_Z_1(W))]])).

cnf(19, plain,
    (skolemFOFtoCNF_Y(W) = W |
     big_f(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Y(W))),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_Z_1(W),
                      skolemFOFtoCNF_Z_1(W)))], [18, 17])).

cnf(20, plain,
    (skolemFOFtoCNF_Y(X2) = X2 |
     big_f(skolemFOFtoCNF_Z_1(X2), skolemFOFtoCNF_Y(X2))),
    inference(subst, [], [19 : [bind(W, $fot(X2))]])).

cnf(21, plain,
    (skolemFOFtoCNF_Y(X2) = X2 | skolemFOFtoCNF_Y(X2) = skolemFOFtoCNF_W),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_Z_1(X2), skolemFOFtoCNF_Y(X2)))],
              [20, 15])).

cnf(22, plain, (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) = skolemFOFtoCNF_W),
    inference(subst, [], [21 : [bind(X2, $fot(skolemFOFtoCNF_W))]])).

cnf(23, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     skolemFOFtoCNF_Y(skolemFOFtoCNF_W) = skolemFOFtoCNF_W),
    introduced(tautology,
               [equality,
                [$cnf('$equal'(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                        skolemFOFtoCNF_W)), [0, 0],
                 $fot(skolemFOFtoCNF_W)]])).

cnf(24, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_Y(skolemFOFtoCNF_W) = skolemFOFtoCNF_W),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [22, 23])).

cnf(25, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X0) = X0 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X0), skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [24, 13])).

cnf(26, plain, (skolemFOFtoCNF_W = skolemFOFtoCNF_W),
    introduced(tautology, [refl, [$fot(skolemFOFtoCNF_W)]])).

cnf(27, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X0) = X0 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X0), skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [26, 25])).

cnf(28, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1) = X1 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1), skolemFOFtoCNF_W)),
    inference(subst, [], [27 : [bind(X0, $fot(X1))]])).

cnf(29, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1) = X1 |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1) = skolemFOFtoCNF_Z),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X1),
                      skolemFOFtoCNF_W))], [28, 9])).

cnf(30, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z),
    inference(subst, [], [29 : [bind(X1, $fot(skolemFOFtoCNF_Z))]])).

cnf(31, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) !=
     skolemFOFtoCNF_Z | skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z),
    introduced(tautology,
               [equality,
                [$cnf(~ '$equal'(skolemFOFtoCNF_X(skolemFOFtoCNF_W,
                          skolemFOFtoCNF_Z), skolemFOFtoCNF_Z)), [0],
                 $fot(skolemFOFtoCNF_Z)]])).

cnf(32, plain,
    (skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_X(skolemFOFtoCNF_W,
                        skolemFOFtoCNF_Z), skolemFOFtoCNF_Z))], [30, 31])).

cnf(33, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_X(skolemFOFtoCNF_W,
                        skolemFOFtoCNF_Z), skolemFOFtoCNF_Z))], [32, 7])).

cnf(34, plain, (skolemFOFtoCNF_Z = skolemFOFtoCNF_Z),
    introduced(tautology, [refl, [$fot(skolemFOFtoCNF_Z)]])).

cnf(35, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z))],
              [34, 33])).

cnf(36, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [24, 35])).

cnf(37, plain, (~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [26, 36])).

cnf(38, plain,
    (X != skolemFOFtoCNF_Z | Y != skolemFOFtoCNF_W | big_f(X, Y)),
    inference(cnf_normalization, [], [pel52_1])).

cnf(39, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(subst, [],
              [38 :
               [bind(X, $fot(skolemFOFtoCNF_Z)),
                bind(Y, $fot(skolemFOFtoCNF_W))]])).

cnf(40, plain,
    (skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [26, 39])).

cnf(41, plain, (big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf('$equal'(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z))],
              [34, 40])).

cnf(42, plain, ($false),
    inference(resolve, [$cnf(big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W))],
              [41, 37])).
SZS output end CNFRefutation for data/problems/all/SYN075+1.tptp