---------------------------------------------------------------------------

WATCH: 0.00 CPU 0.01 WC
SZS status Theorem for /CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p

SZS output start CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p
fof(pel52_1, axiom,
    (? [Z, W] : ! [X, Y] : ((Y = W & Z = X) <=> big_f(X, Y)))).

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

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

fof(negate_0_0, plain,
    (~
       ? [W] :
         ! [Y] : (? [Z] : ! [X] : (X = Z <=> big_f(X, Y)) <=> 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) <=> (Y != W | Z != X))),
    inference(canonicalize, [], [pel52_1])).

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

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

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

fof(normalize_0_9, plain,
    (! [X, Y] : (~ big_f(X, Y) | skolemFOFtoCNF_Z = X)),
    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,
    (! [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_12, plain,
    (! [X, Y] : (~ big_f(X, Y) | Y = skolemFOFtoCNF_W)),
    inference(conjunct, [], [normalize_0_8])).

fof(normalize_0_13, plain,
    (! [X, Y] :
       (Y != skolemFOFtoCNF_W | skolemFOFtoCNF_Z != X | 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) | skolemFOFtoCNF_Z = X),
    inference(canonicalize, [], [normalize_0_9])).

cnf(refute_0_7, plain,
    (~ big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11), skolemFOFtoCNF_W) |
     skolemFOFtoCNF_Z = skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11)),
    inference(subst, [],
              [refute_0_6 :
               [bind(X, $fot(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11))),
                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_10) = X_10 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_10), skolemFOFtoCNF_W)),
    inference(subst, [],
              [refute_0_10 :
               [bind(W, $fot(skolemFOFtoCNF_W)), bind(Z, $fot(X_10))]])).

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

cnf(refute_0_13, 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_12 : [bind(X, $fot(skolemFOFtoCNF_Z_1(W)))]])).

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

cnf(refute_0_15, 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_14, refute_0_13])).

cnf(refute_0_16, plain,
    (~ big_f(skolemFOFtoCNF_Z_1(X_2), skolemFOFtoCNF_Y(X_2)) |
     skolemFOFtoCNF_Z = skolemFOFtoCNF_Z_1(X_2)),
    inference(subst, [],
              [refute_0_6 :
               [bind(X, $fot(skolemFOFtoCNF_Z_1(X_2))),
                bind(Y, $fot(skolemFOFtoCNF_Y(X_2)))]])).

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

cnf(refute_0_18, plain,
    (skolemFOFtoCNF_Y(X_2) = X_2 |
     skolemFOFtoCNF_Z = skolemFOFtoCNF_Z_1(X_2)),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_Z_1(X_2),
                      skolemFOFtoCNF_Y(X_2)))],
              [refute_0_17, refute_0_16])).

cnf(refute_0_19, plain,
    (skolemFOFtoCNF_Y(W) = W | skolemFOFtoCNF_Z = skolemFOFtoCNF_Z_1(W)),
    inference(subst, [], [refute_0_18 : [bind(X_2, $fot(W))]])).

cnf(refute_0_20, plain, (X0 = X0),
    introduced(tautology, [refl, [$fot(X0)]])).

cnf(refute_0_21, plain, (X0 != X0 | X0 != Y0 | Y0 = X0),
    introduced(tautology,
               [equality, [$cnf($equal(X0, X0)), [0], $fot(Y0)]])).

cnf(refute_0_22, plain, (X0 != Y0 | Y0 = X0),
    inference(resolve, [$cnf($equal(X0, X0))],
              [refute_0_20, refute_0_21])).

cnf(refute_0_23, plain,
    (skolemFOFtoCNF_Z != skolemFOFtoCNF_Z_1(W) |
     skolemFOFtoCNF_Z_1(W) = skolemFOFtoCNF_Z),
    inference(subst, [],
              [refute_0_22 :
               [bind(X0, $fot(skolemFOFtoCNF_Z)),
                bind(Y0, $fot(skolemFOFtoCNF_Z_1(W)))]])).

cnf(refute_0_24, plain,
    (skolemFOFtoCNF_Y(W) = W | skolemFOFtoCNF_Z_1(W) = skolemFOFtoCNF_Z),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z_1(W)))],
              [refute_0_19, refute_0_23])).

cnf(refute_0_25, plain,
    (skolemFOFtoCNF_Z_1(W) != skolemFOFtoCNF_Z |
     ~ big_f(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Y(W)) |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_Y(W))),
    introduced(tautology,
               [equality,
                [$cnf(big_f(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Y(W))),
                 [0], $fot(skolemFOFtoCNF_Z)]])).

cnf(refute_0_26, plain,
    (~ big_f(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Y(W)) |
     skolemFOFtoCNF_Y(W) = W |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_Y(W))),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Z))],
              [refute_0_24, refute_0_25])).

cnf(refute_0_27, plain,
    (skolemFOFtoCNF_Y(W) = W |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_Y(W))),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_Z_1(W), skolemFOFtoCNF_Y(W)))],
              [refute_0_15, refute_0_26])).

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

cnf(refute_0_29, plain,
    (~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_Y(W)) |
     skolemFOFtoCNF_Y(W) = skolemFOFtoCNF_W),
    inference(subst, [],
              [refute_0_28 :
               [bind(X, $fot(skolemFOFtoCNF_Z)),
                bind(Y, $fot(skolemFOFtoCNF_Y(W)))]])).

cnf(refute_0_30, plain,
    (skolemFOFtoCNF_Y(W) = W | skolemFOFtoCNF_Y(W) = skolemFOFtoCNF_W),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_Y(W)))],
              [refute_0_27, refute_0_29])).

cnf(refute_0_31, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) = skolemFOFtoCNF_W),
    inference(subst, [],
              [refute_0_30 : [bind(W, $fot(skolemFOFtoCNF_W))]])).

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

cnf(refute_0_34, plain,
    (skolemFOFtoCNF_W != skolemFOFtoCNF_W |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_10) = X_10 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_10), skolemFOFtoCNF_W)),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Y(skolemFOFtoCNF_W),
                      skolemFOFtoCNF_W))], [refute_0_33, refute_0_11])).

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

cnf(refute_0_36, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_10) = X_10 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_10), skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [refute_0_35, refute_0_34])).

cnf(refute_0_37, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11) = X_11 |
     big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11), skolemFOFtoCNF_W)),
    inference(subst, [], [refute_0_36 : [bind(X_10, $fot(X_11))]])).

cnf(refute_0_38, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11) = X_11 |
     skolemFOFtoCNF_Z = skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11)),
    inference(resolve,
              [$cnf(big_f(skolemFOFtoCNF_X(skolemFOFtoCNF_W, X_11),
                      skolemFOFtoCNF_W))], [refute_0_37, refute_0_7])).

cnf(refute_0_39, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z |
     skolemFOFtoCNF_Z =
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z)),
    inference(subst, [],
              [refute_0_38 : [bind(X_11, $fot(skolemFOFtoCNF_Z))]])).

cnf(refute_0_40, plain,
    (skolemFOFtoCNF_Z !=
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) |
     skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z),
    inference(subst, [],
              [refute_0_22 :
               [bind(X0, $fot(skolemFOFtoCNF_Z)),
                bind(Y0,
                     $fot(skolemFOFtoCNF_X(skolemFOFtoCNF_W,
                            skolemFOFtoCNF_Z)))]])).

cnf(refute_0_41, plain,
    (skolemFOFtoCNF_X(skolemFOFtoCNF_W, skolemFOFtoCNF_Z) =
     skolemFOFtoCNF_Z),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_Z,
                      skolemFOFtoCNF_X(skolemFOFtoCNF_W,
                        skolemFOFtoCNF_Z)))], [refute_0_39, refute_0_40])).

cnf(refute_0_42, 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_43, 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_41, refute_0_42])).

cnf(refute_0_44, 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_43, refute_0_5])).

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

cnf(refute_0_46, plain,
    (skolemFOFtoCNF_Y(skolemFOFtoCNF_W) != skolemFOFtoCNF_W |
     ~ big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z))],
              [refute_0_45, refute_0_44])).

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

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

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

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

cnf(refute_0_51, plain,
    (skolemFOFtoCNF_Z != skolemFOFtoCNF_Z |
     big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_W, skolemFOFtoCNF_W))],
              [refute_0_35, refute_0_50])).

cnf(refute_0_52, plain, (big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W)),
    inference(resolve, [$cnf($equal(skolemFOFtoCNF_Z, skolemFOFtoCNF_Z))],
              [refute_0_45, refute_0_51])).

cnf(refute_0_53, plain, ($false),
    inference(resolve, [$cnf(big_f(skolemFOFtoCNF_Z, skolemFOFtoCNF_W))],
              [refute_0_52, refute_0_48])).
SZS output end CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p


WATCH: 0.01 CPU 0.07 WC

FINAL WATCH: 0.01 CPU 0.07 WC