Running in basic DEBUG mode.
Running in metis DEBUG mode.
---------------------------------------------------------------------------
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))).

fof(subgoal_0, plain,
    (? [W] : ! [Y] : (? [Z] : ! [X] : (big_f(X, Y) <=> X = Z) <=> Y = W)),
    inference(strip, [], [pel52])).

fof(negate_0_0, plain,
    (~
       ? [W] :
         ! [Y] : (? [Z] : ! [X] : (big_f(X, Y) <=> X = Z) <=> Y = W)),
    inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain,
    (! [W] :
       ? [Y] : (Y != W <=> ? [Z] : ! [X] : (X != Z <=> ~ big_f(X, Y)))),
    inference(canonicalize, [], [negate_0_0])).

fof(normalize_0_1, plain,
    (! [W] :
       ? [Y] : (Y != W <=> ? [Z] : ! [X] : (X != Z <=> ~ big_f(X, Y)))),
    inference(specialize, [], [normalize_0_0])).

fof(normalize_0_2, plain,
    (! [W] :
       (skolemFOFtoCNF_Y(W) != W <=>
        ? [Z] : ! [X] : (X != Z <=> ~ big_f(X, skolemFOFtoCNF_Y(W))))),
    inference(skolemize, [], [normalize_0_1])).

fof(normalize_0_3, plain,
    (! [W, X, Z] :
       ((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))),
    inference(clausify, [], [normalize_0_2])).

fof(normalize_0_4, plain,
    (! [W, Z] :
       (skolemFOFtoCNF_X(W, Z) != Z | skolemFOFtoCNF_Y(W) != W |
        ~ big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W)))),
    inference(conjunct, [], [normalize_0_3])).

fof(normalize_0_5, plain,
    (? [W, Z] : ! [X, Y] : (~ big_f(X, Y) <=> (X != Z | Y != W))),
    inference(canonicalize, [], [pel52_1])).

fof(normalize_0_6, plain,
    (! [X, Y] :
       (~ big_f(X, Y) <=>
        (X != skolemFOFtoCNF_Z | Y != skolemFOFtoCNF_W))),
    inference(skolemize, [], [normalize_0_5])).

fof(normalize_0_7, plain,
    (! [X, Y] :
       (~ big_f(X, Y) <=>
        (X != skolemFOFtoCNF_Z | Y != skolemFOFtoCNF_W))),
    inference(specialize, [], [normalize_0_6])).

fof(normalize_0_8, plain,
    (! [X, Y] :
       ((~ big_f(X, Y) | X = skolemFOFtoCNF_Z) &
        (~ big_f(X, Y) | Y = skolemFOFtoCNF_W) &
        (X != skolemFOFtoCNF_Z | Y != skolemFOFtoCNF_W | big_f(X, Y)))),
    inference(clausify, [], [normalize_0_7])).

fof(normalize_0_9, plain,
    (! [X, Y] : (~ big_f(X, Y) | X = skolemFOFtoCNF_Z)),
    inference(conjunct, [], [normalize_0_8])).

fof(normalize_0_10, plain,
    (! [W, Z] :
       (skolemFOFtoCNF_Y(W) != W | skolemFOFtoCNF_X(W, Z) = Z |
        big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W)))),
    inference(conjunct, [], [normalize_0_3])).

fof(normalize_0_11, plain,
    (! [X, Y] : (~ big_f(X, Y) | Y = skolemFOFtoCNF_W)),
    inference(conjunct, [], [normalize_0_8])).

fof(normalize_0_12, plain,
    (! [W, X] :
       (X != skolemFOFtoCNF_Z_1(W) | skolemFOFtoCNF_Y(W) = W |
        big_f(X, skolemFOFtoCNF_Y(W)))),
    inference(conjunct, [], [normalize_0_3])).

fof(normalize_0_13, plain,
    (! [X, Y] :
       (X != skolemFOFtoCNF_Z | Y != skolemFOFtoCNF_W | big_f(X, Y))),
    inference(conjunct, [], [normalize_0_8])).

cnf(refute_0_0, plain,
    (skolemFOFtoCNF_X(W, Z) != Z | skolemFOFtoCNF_Y(W) != W |
     ~ big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
    inference(canonicalize, [], [normalize_0_4])).

cnf(refute_0_1, 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(refute_0_2, 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(refute_0_3, 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)))],
              [refute_0_2, refute_0_1])).

cnf(refute_0_4, 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)))],
              [refute_0_3, refute_0_0])).

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

cnf(refute_0_6, plain, (~ big_f(X, Y) | X = skolemFOFtoCNF_Z),
    inference(canonicalize, [], [normalize_0_9])).

cnf(refute_0_7, plain,
    (~ big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21), skolemFOFtoCNF_W) |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21) = skolemFOFtoCNF_Z),
    inference(subst, [],
              [refute_0_6 :
               [bind(X, $fot(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21))),
                bind(Y, $fot(skolemFOFtoCNF_W))]])).

cnf(refute_0_8, plain,
    (skolemFOFtoCNF_Y(W) != W | skolemFOFtoCNF_X(W, Z) = Z |
     big_f(skolemFOFtoCNF_X(W, Z), skolemFOFtoCNF_Y(W))),
    inference(canonicalize, [], [normalize_0_10])).

cnf(refute_0_9, 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(refute_0_10, 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)))],
              [refute_0_8, refute_0_9])).

cnf(refute_0_11, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_20) = X_20 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_20), skolemFOFtoCNF_W)),
    inference(subst, [],
              [refute_0_10 :
               [bind(W, $fot(skolemFOFtoCNF_W)), bind(Z, $fot(X_20))]])).

cnf(refute_0_12, plain, (~ big_f(X, Y) | Y = skolemFOFtoCNF_W),
    inference(canonicalize, [], [normalize_0_11])).

cnf(refute_0_13, plain,
    (~ big_f(skolemFOFtoCNF_Z_1(X_4), skolemFOFtoCNF_Y(X_4)) |
     skolemFOFtoCNF_Y(X_4) = skolemFOFtoCNF_W),
    inference(subst, [],
              [refute_0_12 :
               [bind(X, $fot(skolemFOFtoCNF_Z_1(X_4))),
                bind(Y, $fot(skolemFOFtoCNF_Y(X_4)))]])).

cnf(refute_0_14, plain,
    (X != skolemFOFtoCNF_Z_1(W) | skolemFOFtoCNF_Y(W) = W |
     big_f(X, skolemFOFtoCNF_Y(W))),
    inference(canonicalize, [], [normalize_0_12])).

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

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

cnf(refute_0_17, 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)))],
              [refute_0_16, refute_0_15])).

cnf(refute_0_18, plain,
    (skolemFOFtoCNF_Y(X_4) = X_4 |
     big_f(skolemFOFtoCNF_Z_1(X_4), skolemFOFtoCNF_Y(X_4))),
    inference(subst, [], [refute_0_17 : [bind(W, $fot(X_4))]])).

cnf(refute_0_19, plain,
    (skolemFOFtoCNF_Y(X_4) = X_4 |
     skolemFOFtoCNF_Y(X_4) = skolemFOFtoCNF_W),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_Z_1(X_4),
                      skolemFOFtoCNF_Y(X_4)))],
              [refute_0_18, refute_0_13])).

cnf(refute_0_20, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) = skolemFOFtoCNF_W),
    inference(subst, [],
              [refute_0_19 : [bind(X_4, $fot(skolemFOFtoCNF_W))]])).

cnf(refute_0_21, 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(refute_0_22, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_Y(skolemFOFtoCNF_W) = skolemFOFtoCNF_W),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [refute_0_20, refute_0_21])).

cnf(refute_0_23, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_20) = X_20 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_20), skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [refute_0_22, refute_0_11])).

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

cnf(refute_0_25, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_20) = X_20 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_20), skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [refute_0_24, refute_0_23])).

cnf(refute_0_26, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21) = X_21 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21), skolemFOFtoCNF_W)),
    inference(subst, [], [refute_0_25 : [bind(X_20, $fot(X_21))]])).

cnf(refute_0_27, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21) = X_21 |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21) = skolemFOFtoCNF_Z),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_21),
                      skolemFOFtoCNF_W))], [refute_0_26, refute_0_7])).

cnf(refute_0_28, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z),
    inference(subst, [],
              [refute_0_27 : [bind(X_21, $fot(skolemFOFtoCNF_Z))]])).

cnf(refute_0_29, 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(refute_0_30, 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))],
              [refute_0_28, refute_0_29])).

cnf(refute_0_31, 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))],
              [refute_0_30, refute_0_5])).

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

cnf(refute_0_33, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z))],
              [refute_0_32, refute_0_31])).

cnf(refute_0_34, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [refute_0_22, refute_0_33])).

cnf(refute_0_35, plain, (~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [refute_0_24, refute_0_34])).

cnf(refute_0_36, plain,
    (X != skolemFOFtoCNF_Z | Y != skolemFOFtoCNF_W | big_f(X, Y)),
    inference(canonicalize, [], [normalize_0_13])).

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

cnf(refute_0_38, plain,
    (skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [refute_0_24, refute_0_37])).

cnf(refute_0_39, plain, (big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z))],
              [refute_0_32, refute_0_38])).

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