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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Problem: data/problems/all/SEU140+2.tptp

Goal:
(!A B. in A B ==> ~in B A) /\
(!A B. proper_subset A B ==> ~proper_subset B A) /\
(!A B. set_union2 A B = set_union2 B A) /\
(!A B. set_intersection2 A B = set_intersection2 B A) /\
(!A B. A = B <=> subset A B /\ subset B A) /\
(!A. A = empty_set <=> !B. ~in B A) /\
(!A B C. C = set_union2 A B <=> !D. in D C <=> in D A \/ in D B) /\
(!A B. subset A B <=> !C. in C A ==> in C B) /\
(!A B C. C = set_intersection2 A B <=> !D. in D C <=> in D A /\ in D B) /\
(!A B C. C = set_difference A B <=> !D. in D C <=> in D A /\ ~in D B) /\
(!A B. disjoint A B <=> set_intersection2 A B = empty_set) /\
(!A B. proper_subset A B <=> subset A B /\ ~(A = B)) /\ T /\ T /\ T /\ T /\
empty empty_set /\ (!A B. ~empty A ==> ~empty (set_union2 A B)) /\
(!A B. ~empty A ==> ~empty (set_union2 B A)) /\
(!A B. set_union2 A A = A) /\ (!A B. set_intersection2 A A = A) /\
(!A B. ~proper_subset A A) /\
(!A B. set_difference A B = empty_set <=> subset A B) /\ (?A. empty A) /\
(?A. ~empty A) /\ (!A B. subset A A) /\
(!A B. disjoint A B ==> disjoint B A) /\
(!A B. subset A B ==> set_union2 A B = B) /\
(!A B. subset (set_intersection2 A B) A) /\
(!A B C. subset A B /\ subset A C ==> subset A (set_intersection2 B C)) /\
(!A. set_union2 A empty_set = A) /\
(!A B C. subset A B /\ subset B C ==> subset A C) /\
(!A B C.
   subset A B ==>
   subset (set_intersection2 A C) (set_intersection2 B C)) /\
(!A B. subset A B ==> set_intersection2 A B = A) /\
(!A. set_intersection2 A empty_set = empty_set) /\
(!A B. (!C. in C A <=> in C B) ==> A = B) /\ (!A. subset empty_set A) /\
(!A B C.
   subset A B ==> subset (set_difference A C) (set_difference B C)) /\
(!A B. subset (set_difference A B) A) /\
(!A B. set_difference A B = empty_set <=> subset A B) /\
(!A B. set_union2 A (set_difference B A) = set_union2 A B) /\
(!A. set_difference A empty_set = A) /\
(!A B.
   ~(~disjoint A B /\ !C. ~(in C A /\ in C B)) /\
   ~((?C. in C A /\ in C B) /\ disjoint A B)) /\
(!A. subset A empty_set ==> A = empty_set) /\
(!A B. set_difference (set_union2 A B) B = set_difference A B) /\
(!A B. subset A B ==> B = set_union2 A (set_difference B A)) /\
(!A B. set_difference A (set_difference A B) = set_intersection2 A B) /\
(!A. set_difference empty_set A = empty_set) /\
(!A B.
   ~(~disjoint A B /\ !C. ~in C (set_intersection2 A B)) /\
   ~((?C. in C (set_intersection2 A B)) /\ disjoint A B)) /\
(!A B. ~(subset A B /\ proper_subset B A)) /\
(!A. empty A ==> A = empty_set) /\ (!A B. ~(in A B /\ empty B)) /\
(!A B. subset A (set_union2 A B)) /\
(!A B. ~(empty A /\ ~(A = B) /\ empty B)) /\
(!A B C. subset A B /\ subset C B ==> subset (set_union2 A C) B) ==>
!A B C. subset A B /\ disjoint B C ==> disjoint A C

Clauses:
(~in $A $B \/ ~in $B $A) /\
(~proper_subset $A $B \/ ~proper_subset $B $A) /\
set_union2 $A $B = set_union2 $B $A /\
set_intersection2 $A $B = set_intersection2 $B $A /\
(~($A = $B) \/ subset $A $B) /\ (~($A = $B) \/ subset $B $A) /\
(~subset $A $B \/ ~subset $B $A \/ $A = $B) /\
(~($A = empty_set) \/ ~in $B $A) /\
($A = empty_set \/ in (skolemFOFtoCNF_B $A) $A) /\
(~($C = set_union2 $A $B) \/ ~in $D $A \/ in $D $C) /\
(~($C = set_union2 $A $B) \/ ~in $D $B \/ in $D $C) /\
(~in (skolemFOFtoCNF_D $A $B $C) $A \/
 ~in (skolemFOFtoCNF_D $A $B $C) $C \/ $C = set_union2 $A $B) /\
(~in (skolemFOFtoCNF_D $A $B $C) $B \/
 ~in (skolemFOFtoCNF_D $A $B $C) $C \/ $C = set_union2 $A $B) /\
(~($C = set_union2 $A $B) \/ ~in $D $C \/ in $D $A \/ in $D $B) /\
($C = set_union2 $A $B \/ in (skolemFOFtoCNF_D $A $B $C) $A \/
 in (skolemFOFtoCNF_D $A $B $C) $B \/ in (skolemFOFtoCNF_D $A $B $C) $C) /\
(~in (skolemFOFtoCNF_C $A $B) $B \/ subset $A $B) /\
(in (skolemFOFtoCNF_C $A $B) $A \/ subset $A $B) /\
(~in $C $A \/ ~subset $A $B \/ in $C $B) /\
(~($C = set_intersection2 $A $B) \/ ~in $D $C \/ in $D $A) /\
(~($C = set_intersection2 $A $B) \/ ~in $D $C \/ in $D $B) /\
($C = set_intersection2 $A $B \/ in (skolemFOFtoCNF_D_1 $A $B $C) $A \/
 in (skolemFOFtoCNF_D_1 $A $B $C) $C) /\
($C = set_intersection2 $A $B \/ in (skolemFOFtoCNF_D_1 $A $B $C) $B \/
 in (skolemFOFtoCNF_D_1 $A $B $C) $C) /\
(~($C = set_intersection2 $A $B) \/ ~in $D $A \/ ~in $D $B \/ in $D $C) /\
(~in (skolemFOFtoCNF_D_1 $A $B $C) $A \/
 ~in (skolemFOFtoCNF_D_1 $A $B $C) $B \/
 ~in (skolemFOFtoCNF_D_1 $A $B $C) $C \/ $C = set_intersection2 $A $B) /\
(~($C = set_difference $A $B) \/ ~in $D $B \/ ~in $D $C) /\
(~($C = set_difference $A $B) \/ ~in $D $C \/ in $D $A) /\
(~in (skolemFOFtoCNF_D_2 $A $B $C) $B \/ $C = set_difference $A $B \/
 in (skolemFOFtoCNF_D_2 $A $B $C) $C) /\
($C = set_difference $A $B \/ in (skolemFOFtoCNF_D_2 $A $B $C) $A \/
 in (skolemFOFtoCNF_D_2 $A $B $C) $C) /\
(~($C = set_difference $A $B) \/ ~in $D $A \/ in $D $B \/ in $D $C) /\
(~in (skolemFOFtoCNF_D_2 $A $B $C) $A \/
 ~in (skolemFOFtoCNF_D_2 $A $B $C) $C \/ $C = set_difference $A $B \/
 in (skolemFOFtoCNF_D_2 $A $B $C) $B) /\
(~(set_intersection2 $A $B = empty_set) \/ disjoint $A $B) /\
(~disjoint $A $B \/ set_intersection2 $A $B = empty_set) /\
(~($A = $B) \/ ~proper_subset $A $B) /\
(~proper_subset $A $B \/ subset $A $B) /\
(~subset $A $B \/ $A = $B \/ proper_subset $A $B) /\ empty empty_set /\
(~empty (set_union2 $A $B) \/ empty $A) /\
(~empty (set_union2 $B $A) \/ empty $A) /\ set_union2 $A $A = $A /\
set_intersection2 $A $A = $A /\ ~proper_subset $A $A /\
(~(set_difference $A $B = empty_set) \/ subset $A $B) /\
(~subset $A $B \/ set_difference $A $B = empty_set) /\
empty skolemFOFtoCNF_A /\ ~empty skolemFOFtoCNF_A_1 /\ subset $A $A /\
(~disjoint $A $B \/ disjoint $B $A) /\
(~subset $A $B \/ set_union2 $A $B = $B) /\
subset (set_intersection2 $A $B) $A /\
(~subset $A $B \/ ~subset $A $C \/ subset $A (set_intersection2 $B $C)) /\
set_union2 $A empty_set = $A /\
(~subset $A $B \/ ~subset $B $C \/ subset $A $C) /\
(~subset $A $B \/
 subset (set_intersection2 $A $C) (set_intersection2 $B $C)) /\
(~subset $A $B \/ set_intersection2 $A $B = $A) /\
set_intersection2 $A empty_set = empty_set /\
(~in (skolemFOFtoCNF_C_1 $A $B) $A \/ ~in (skolemFOFtoCNF_C_1 $A $B) $B \/
 $A = $B) /\
($A = $B \/ in (skolemFOFtoCNF_C_1 $A $B) $A \/
 in (skolemFOFtoCNF_C_1 $A $B) $B) /\ subset empty_set $A /\
(~subset $A $B \/ subset (set_difference $A $C) (set_difference $B $C)) /\
subset (set_difference $A $B) $A /\
set_union2 $A (set_difference $B $A) = set_union2 $A $B /\
set_difference $A empty_set = $A /\
(~disjoint $A $B \/ ~in $C $A \/ ~in $C $B) /\
(disjoint $A $B \/ in (skolemFOFtoCNF_C_2 $A $B) $A) /\
(disjoint $A $B \/ in (skolemFOFtoCNF_C_2 $A $B) $B) /\
(~subset $A empty_set \/ $A = empty_set) /\
set_difference (set_union2 $A $B) $B = set_difference $A $B /\
(~subset $A $B \/ $B = set_union2 $A (set_difference $B $A)) /\
set_difference $A (set_difference $A $B) = set_intersection2 $A $B /\
set_difference empty_set $A = empty_set /\
(~disjoint $A $B \/ ~in $C (set_intersection2 $A $B)) /\
(disjoint $A $B \/
 in (skolemFOFtoCNF_C_3 $A $B) (set_intersection2 $A $B)) /\
(~proper_subset $B $A \/ ~subset $A $B) /\ (~empty $A \/ $A = empty_set) /\
(~empty $B \/ ~in $A $B) /\ subset $A (set_union2 $A $B) /\
(~empty $A \/ ~empty $B \/ $A = $B) /\
(~subset $A $B \/ ~subset $C $B \/ subset (set_union2 $A $C) $B) /\
~disjoint skolemFOFtoCNF_A_2 skolemFOFtoCNF_C_4 /\
disjoint skolemFOFtoCNF_B_1 skolemFOFtoCNF_C_4 /\
subset skolemFOFtoCNF_A_2 skolemFOFtoCNF_B_1

% SZS status Theorem for data/problems/all/SEU140+2.tptp

% SZS output start CNFRefutation for data/problems/all/SEU140+2.tptp
fof(commutativity_k2_xboole_0, axiom,
    (! [A, B] : set_union2(A, B) = set_union2(B, A))).

fof(commutativity_k3_xboole_0, axiom,
    (! [A, B] : set_intersection2(A, B) = set_intersection2(B, A))).

fof(d3_xboole_0, axiom,
    (! [A, B, C] :
       (C = set_intersection2(A, B) <=>
        ! [D] : (in(D, C) <=> (in(D, A) & in(D, B)))))).

fof(d4_xboole_0, axiom,
    (! [A, B, C] :
       (C = set_difference(A, B) <=>
        ! [D] : (in(D, C) <=> (in(D, A) & ~ in(D, B)))))).

fof(d7_xboole_0, axiom,
    (! [A, B] : (disjoint(A, B) <=> set_intersection2(A, B) = empty_set))).

fof(l32_xboole_1, lemma,
    (! [A, B] : (set_difference(A, B) = empty_set <=> subset(A, B)))).

fof(symmetry_r1_xboole_0, axiom,
    (! [A, B] : (disjoint(A, B) => disjoint(B, A)))).

fof(t1_boole, axiom, (! [A] : set_union2(A, empty_set) = A)).

fof(t36_xboole_1, lemma, (! [A, B] : subset(set_difference(A, B), A))).

fof(t37_xboole_1, lemma,
    (! [A, B] : (set_difference(A, B) = empty_set <=> subset(A, B)))).

fof(t39_xboole_1, lemma,
    (! [A, B] : set_union2(A, set_difference(B, A)) = set_union2(A, B))).

fof(t3_boole, axiom, (! [A] : set_difference(A, empty_set) = A)).

fof(t3_xboole_0, lemma,
    (! [A, B] :
       (~ (~ disjoint(A, B) & ! [C] : ~ (in(C, A) & in(C, B))) &
        ~ (? [C] : (in(C, A) & in(C, B)) & disjoint(A, B))))).

fof(t48_xboole_1, lemma,
    (! [A, B] :
       set_difference(A, set_difference(A, B)) = set_intersection2(A, B))).

fof(t63_xboole_1, conjecture,
    (! [A, B, C] : ((subset(A, B) & disjoint(B, C)) => disjoint(A, C)))).

fof(subgoal_0, plain,
    (! [A, B, C] : ((subset(A, B) & disjoint(B, C)) => disjoint(A, C))),
    inference(strip, [], [t63_xboole_1])).

fof(negate_0_0, plain,
    (~ ! [A, B, C] : ((subset(A, B) & disjoint(B, C)) => disjoint(A, C))),
    inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain, (! [A, B] : (~ disjoint(A, B) | disjoint(B, A))),
    inference(canonicalize, [], [symmetry_r1_xboole_0])).

fof(normalize_0_1, plain, (! [A, B] : (~ disjoint(A, B) | disjoint(B, A))),
    inference(specialize, [], [normalize_0_0])).

fof(normalize_0_2, plain,
    (! [A, B] : (~ disjoint(A, B) | ! [C] : (~ in(C, A) | ~ in(C, B))) &
     ! [A, B] : (disjoint(A, B) | ? [C] : (in(C, A) & in(C, B)))),
    inference(canonicalize, [], [t3_xboole_0])).

fof(normalize_0_3, plain,
    (! [A, B] : (disjoint(A, B) | ? [C] : (in(C, A) & in(C, B)))),
    inference(conjunct, [], [normalize_0_2])).

fof(normalize_0_4, plain,
    (! [A, B] : (disjoint(A, B) | ? [C] : (in(C, A) & in(C, B)))),
    inference(specialize, [], [normalize_0_3])).

fof(normalize_0_5, plain,
    (! [A, B] :
       ((disjoint(A, B) | in(skolemFOFtoCNF_C_2(A, B), A)) &
        (disjoint(A, B) | in(skolemFOFtoCNF_C_2(A, B), B)))),
    inference(clausify, [], [normalize_0_4])).

fof(normalize_0_6, plain,
    (! [A, B] : (disjoint(A, B) | in(skolemFOFtoCNF_C_2(A, B), B))),
    inference(conjunct, [], [normalize_0_5])).

fof(normalize_0_7, plain,
    (! [A, B, C] :
       (C != set_intersection2(A, B) <=>
        ? [D] : (~ in(D, C) <=> (in(D, A) & in(D, B))))),
    inference(canonicalize, [], [d3_xboole_0])).

fof(normalize_0_8, plain,
    (! [A, B, C] :
       (C != set_intersection2(A, B) <=>
        ? [D] : (~ in(D, C) <=> (in(D, A) & in(D, B))))),
    inference(specialize, [], [normalize_0_7])).

fof(normalize_0_9, plain,
    (! [A, B, C, D] :
       ((C != set_intersection2(A, B) | ~ in(D, C) | in(D, A)) &
        (C != set_intersection2(A, B) | ~ in(D, C) | in(D, B)) &
        (C = set_intersection2(A, B) | in(skolemFOFtoCNF_D_1(A, B, C), A) |
         in(skolemFOFtoCNF_D_1(A, B, C), C)) &
        (C = set_intersection2(A, B) | in(skolemFOFtoCNF_D_1(A, B, C), B) |
         in(skolemFOFtoCNF_D_1(A, B, C), C)) &
        (C != set_intersection2(A, B) | ~ in(D, A) | ~ in(D, B) |
         in(D, C)) &
        (~ in(skolemFOFtoCNF_D_1(A, B, C), A) |
         ~ in(skolemFOFtoCNF_D_1(A, B, C), B) |
         ~ in(skolemFOFtoCNF_D_1(A, B, C), C) |
         C = set_intersection2(A, B)))),
    inference(clausify, [], [normalize_0_8])).

fof(normalize_0_10, plain,
    (! [A, B, C, D] :
       (C != set_intersection2(A, B) | ~ in(D, C) | in(D, B))),
    inference(conjunct, [], [normalize_0_9])).

fof(normalize_0_11, plain,
    (! [A, B] : set_union2(A, set_difference(B, A)) = set_union2(A, B)),
    inference(canonicalize, [], [t39_xboole_1])).

fof(normalize_0_12, plain,
    (! [A, B] : set_union2(A, set_difference(B, A)) = set_union2(A, B)),
    inference(specialize, [], [normalize_0_11])).

fof(normalize_0_13, plain,
    (! [A, B] :
       set_difference(A, set_difference(A, B)) = set_intersection2(A, B)),
    inference(canonicalize, [], [t48_xboole_1])).

fof(normalize_0_14, plain,
    (! [A, B] :
       set_difference(A, set_difference(A, B)) = set_intersection2(A, B)),
    inference(specialize, [], [normalize_0_13])).

fof(normalize_0_15, plain,
    (! [A, B] : set_union2(A, B) = set_union2(B, A)),
    inference(canonicalize, [], [commutativity_k2_xboole_0])).

fof(normalize_0_16, plain,
    (! [A, B] : set_union2(A, B) = set_union2(B, A)),
    inference(specialize, [], [normalize_0_15])).

fof(normalize_0_17, plain,
    (! [A, B] : set_intersection2(A, B) = set_intersection2(B, A)),
    inference(canonicalize, [], [commutativity_k3_xboole_0])).

fof(normalize_0_18, plain,
    (! [A, B] : set_intersection2(A, B) = set_intersection2(B, A)),
    inference(specialize, [], [normalize_0_17])).

fof(normalize_0_19, plain,
    (? [A, B, C] : (~ disjoint(A, C) & disjoint(B, C) & subset(A, B))),
    inference(canonicalize, [], [negate_0_0])).

fof(normalize_0_20, plain,
    (~ disjoint(skolemFOFtoCNF_A_2, skolemFOFtoCNF_C_4) &
     disjoint(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) &
     subset(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(skolemize, [], [normalize_0_19])).

fof(normalize_0_21, plain,
    (subset(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(conjunct, [], [normalize_0_20])).

fof(normalize_0_22, plain,
    (! [A, B] : (set_difference(A, B) != empty_set <=> ~ subset(A, B))),
    inference(canonicalize, [], [t37_xboole_1])).

fof(normalize_0_23, plain,
    (! [A, B] : (set_difference(A, B) != empty_set <=> ~ subset(A, B))),
    inference(specialize, [], [normalize_0_22])).

fof(normalize_0_24, plain,
    (! [A, B] :
       ((set_difference(A, B) != empty_set | subset(A, B)) &
        (~ subset(A, B) | set_difference(A, B) = empty_set))),
    inference(clausify, [], [normalize_0_23])).

fof(normalize_0_25, plain,
    (! [A, B] : (~ subset(A, B) | set_difference(A, B) = empty_set)),
    inference(conjunct, [], [normalize_0_24])).

fof(normalize_0_26, plain, (! [A] : set_union2(A, empty_set) = A),
    inference(canonicalize, [], [t1_boole])).

fof(normalize_0_27, plain, (! [A] : set_union2(A, empty_set) = A),
    inference(specialize, [], [normalize_0_26])).

fof(normalize_0_28, plain,
    (! [A, B] : (disjoint(A, B) | in(skolemFOFtoCNF_C_2(A, B), A))),
    inference(conjunct, [], [normalize_0_5])).

fof(normalize_0_29, plain,
    (! [A, B, C] :
       (C != set_difference(A, B) <=>
        ? [D] : (~ in(D, C) <=> (~ in(D, B) & in(D, A))))),
    inference(canonicalize, [], [d4_xboole_0])).

fof(normalize_0_30, plain,
    (! [A, B, C] :
       (C != set_difference(A, B) <=>
        ? [D] : (~ in(D, C) <=> (~ in(D, B) & in(D, A))))),
    inference(specialize, [], [normalize_0_29])).

fof(normalize_0_31, plain,
    (! [A, B, C, D] :
       ((C != set_difference(A, B) | ~ in(D, B) | ~ in(D, C)) &
        (C != set_difference(A, B) | ~ in(D, C) | in(D, A)) &
        (~ in(skolemFOFtoCNF_D_2(A, B, C), B) | C = set_difference(A, B) |
         in(skolemFOFtoCNF_D_2(A, B, C), C)) &
        (C = set_difference(A, B) | in(skolemFOFtoCNF_D_2(A, B, C), A) |
         in(skolemFOFtoCNF_D_2(A, B, C), C)) &
        (C != set_difference(A, B) | ~ in(D, A) | in(D, B) | in(D, C)) &
        (~ in(skolemFOFtoCNF_D_2(A, B, C), A) |
         ~ in(skolemFOFtoCNF_D_2(A, B, C), C) | C = set_difference(A, B) |
         in(skolemFOFtoCNF_D_2(A, B, C), B)))),
    inference(clausify, [], [normalize_0_30])).

fof(normalize_0_32, plain,
    (! [A, B, C, D] :
       (C != set_difference(A, B) | ~ in(D, B) | ~ in(D, C))),
    inference(conjunct, [], [normalize_0_31])).

fof(normalize_0_33, plain, (! [A, B] : subset(set_difference(A, B), A)),
    inference(canonicalize, [], [t36_xboole_1])).

fof(normalize_0_34, plain, (! [A, B] : subset(set_difference(A, B), A)),
    inference(specialize, [], [normalize_0_33])).

fof(normalize_0_35, plain,
    (disjoint(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(conjunct, [], [normalize_0_20])).

fof(normalize_0_36, plain,
    (! [A, B] :
       (set_intersection2(A, B) != empty_set <=> ~ disjoint(A, B))),
    inference(canonicalize, [], [d7_xboole_0])).

fof(normalize_0_37, plain,
    (! [A, B] :
       (set_intersection2(A, B) != empty_set <=> ~ disjoint(A, B))),
    inference(specialize, [], [normalize_0_36])).

fof(normalize_0_38, plain,
    (! [A, B] :
       ((set_intersection2(A, B) != empty_set | disjoint(A, B)) &
        (~ disjoint(A, B) | set_intersection2(A, B) = empty_set))),
    inference(clausify, [], [normalize_0_37])).

fof(normalize_0_39, plain,
    (! [A, B] : (~ disjoint(A, B) | set_intersection2(A, B) = empty_set)),
    inference(conjunct, [], [normalize_0_38])).

fof(normalize_0_40, plain, (! [A] : set_difference(A, empty_set) = A),
    inference(canonicalize, [], [t3_boole])).

fof(normalize_0_41, plain, (! [A] : set_difference(A, empty_set) = A),
    inference(specialize, [], [normalize_0_40])).

fof(normalize_0_42, plain,
    (~ disjoint(skolemFOFtoCNF_A_2, skolemFOFtoCNF_C_4)),
    inference(conjunct, [], [normalize_0_20])).

cnf(refute_0_0, plain, (~ disjoint(A, B) | disjoint(B, A)),
    inference(canonicalize, [], [normalize_0_1])).

cnf(refute_0_1, plain,
    (~ disjoint(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2) |
     disjoint(skolemFOFtoCNF_A_2, skolemFOFtoCNF_C_4)),
    inference(subst, [],
              [refute_0_0 :
               [bind(A, $fot(skolemFOFtoCNF_C_4)),
                bind(B, $fot(skolemFOFtoCNF_A_2))]])).

cnf(refute_0_2, plain, (disjoint(A, B) | in(skolemFOFtoCNF_C_2(A, B), B)),
    inference(canonicalize, [], [normalize_0_6])).

cnf(refute_0_3, plain,
    (disjoint(A, skolemFOFtoCNF_A_2) |
     in(skolemFOFtoCNF_C_2(A, skolemFOFtoCNF_A_2), skolemFOFtoCNF_A_2)),
    inference(subst, [],
              [refute_0_2 : [bind(B, $fot(skolemFOFtoCNF_A_2))]])).

cnf(refute_0_4, plain,
    (C != set_intersection2(A, B) | ~ in(D, C) | in(D, B)),
    inference(canonicalize, [], [normalize_0_10])).

cnf(refute_0_5, plain,
    (set_intersection2(A, B) != set_intersection2(A, B) |
     ~ in(D, set_intersection2(A, B)) | in(D, B)),
    inference(subst, [],
              [refute_0_4 : [bind(C, $fot(set_intersection2(A, B)))]])).

cnf(refute_0_6, plain, (set_intersection2(A, B) = set_intersection2(A, B)),
    introduced(tautology, [refl, [$fot(set_intersection2(A, B))]])).

cnf(refute_0_7, plain, (~ in(D, set_intersection2(A, B)) | in(D, B)),
    inference(resolve,
              [$cnf($equal(set_intersection2(A, B),
                      set_intersection2(A, B)))],
              [refute_0_6, refute_0_5])).

cnf(refute_0_8, plain,
    (~
       in(X_291,
         set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     in(X_291, skolemFOFtoCNF_B_1)),
    inference(subst, [],
              [refute_0_7 :
               [bind(A, $fot(skolemFOFtoCNF_A_2)),
                bind(B, $fot(skolemFOFtoCNF_B_1)),
                bind(D, $fot(X_291))]])).

cnf(refute_0_9, plain,
    (set_union2(A, set_difference(B, A)) = set_union2(A, B)),
    inference(canonicalize, [], [normalize_0_12])).

cnf(refute_0_10, plain,
    (set_union2(set_difference(B, X_68),
       set_difference(B, set_difference(B, X_68))) =
     set_union2(set_difference(B, X_68), B)),
    inference(subst, [],
              [refute_0_9 : [bind(A, $fot(set_difference(B, X_68)))]])).

cnf(refute_0_11, plain,
    (set_difference(A, set_difference(A, B)) = set_intersection2(A, B)),
    inference(canonicalize, [], [normalize_0_14])).

cnf(refute_0_12, plain,
    (set_difference(B, set_difference(B, X_68)) =
     set_intersection2(B, X_68)),
    inference(subst, [],
              [refute_0_11 : [bind(A, $fot(B)), bind(B, $fot(X_68))]])).

cnf(refute_0_13, plain,
    (set_difference(B, set_difference(B, X_68)) !=
     set_intersection2(B, X_68) |
     set_union2(set_difference(B, X_68),
       set_difference(B, set_difference(B, X_68))) !=
     set_union2(set_difference(B, X_68), B) |
     set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) =
     set_union2(set_difference(B, X_68), B)),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(set_difference(B, X_68),
                          set_difference(B, set_difference(B, X_68))),
                        set_union2(set_difference(B, X_68), B))), [0, 1],
                 $fot(set_intersection2(B, X_68))]])).

cnf(refute_0_14, plain,
    (set_union2(set_difference(B, X_68),
       set_difference(B, set_difference(B, X_68))) !=
     set_union2(set_difference(B, X_68), B) |
     set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) =
     set_union2(set_difference(B, X_68), B)),
    inference(resolve,
              [$cnf($equal(set_difference(B, set_difference(B, X_68)),
                      set_intersection2(B, X_68)))],
              [refute_0_12, refute_0_13])).

cnf(refute_0_15, plain,
    (set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) =
     set_union2(set_difference(B, X_68), B)),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(B, X_68),
                        set_difference(B, set_difference(B, X_68))),
                      set_union2(set_difference(B, X_68), B)))],
              [refute_0_10, refute_0_14])).

cnf(refute_0_16, plain, (set_union2(A, B) = set_union2(B, A)),
    inference(canonicalize, [], [normalize_0_16])).

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

cnf(refute_0_18, plain, (X != X | X != Y | Y = X),
    introduced(tautology, [equality, [$cnf($equal(X, X)), [0], $fot(Y)]])).

cnf(refute_0_19, plain, (X != Y | Y = X),
    inference(resolve, [$cnf($equal(X, X))], [refute_0_17, refute_0_18])).

cnf(refute_0_20, plain,
    (set_union2(A, B) != set_union2(B, A) |
     set_union2(B, A) = set_union2(A, B)),
    inference(subst, [],
              [refute_0_19 :
               [bind(X, $fot(set_union2(A, B))),
                bind(Y, $fot(set_union2(B, A)))]])).

cnf(refute_0_21, plain, (set_union2(B, A) = set_union2(A, B)),
    inference(resolve, [$cnf($equal(set_union2(A, B), set_union2(B, A)))],
              [refute_0_16, refute_0_20])).

cnf(refute_0_22, plain,
    (set_union2(set_difference(B, X_68), B) =
     set_union2(B, set_difference(B, X_68))),
    inference(subst, [],
              [refute_0_21 :
               [bind(A, $fot(B)),
                bind(B, $fot(set_difference(B, X_68)))]])).

cnf(refute_0_23, plain,
    (set_union2(set_difference(B, X_68), B) !=
     set_union2(B, set_difference(B, X_68)) |
     set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) !=
     set_union2(set_difference(B, X_68), B) |
     set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) =
     set_union2(B, set_difference(B, X_68))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(set_difference(B, X_68),
                          set_intersection2(B, X_68)),
                        set_union2(set_difference(B, X_68), B))), [1],
                 $fot(set_union2(B, set_difference(B, X_68)))]])).

cnf(refute_0_24, plain,
    (set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) !=
     set_union2(set_difference(B, X_68), B) |
     set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) =
     set_union2(B, set_difference(B, X_68))),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(B, X_68), B),
                      set_union2(B, set_difference(B, X_68))))],
              [refute_0_22, refute_0_23])).

cnf(refute_0_25, plain,
    (set_union2(set_difference(B, X_68), set_intersection2(B, X_68)) =
     set_union2(B, set_difference(B, X_68))),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(B, X_68),
                        set_intersection2(B, X_68)),
                      set_union2(set_difference(B, X_68), B)))],
              [refute_0_15, refute_0_24])).

cnf(refute_0_26, plain,
    (set_union2(set_difference(X_69, X_70),
       set_intersection2(X_69, X_70)) =
     set_union2(X_69, set_difference(X_69, X_70))),
    inference(subst, [],
              [refute_0_25 :
               [bind(B, $fot(X_69)), bind(X_68, $fot(X_70))]])).

cnf(refute_0_27, plain,
    (set_intersection2(A, B) = set_intersection2(B, A)),
    inference(canonicalize, [], [normalize_0_18])).

cnf(refute_0_28, plain,
    (set_intersection2(X_70, X_69) = set_intersection2(X_69, X_70)),
    inference(subst, [],
              [refute_0_27 : [bind(A, $fot(X_70)), bind(B, $fot(X_69))]])).

cnf(refute_0_29, plain,
    (set_intersection2(X_70, X_69) != set_intersection2(X_69, X_70) |
     set_intersection2(X_69, X_70) = set_intersection2(X_70, X_69)),
    inference(subst, [],
              [refute_0_19 :
               [bind(X, $fot(set_intersection2(X_70, X_69))),
                bind(Y, $fot(set_intersection2(X_69, X_70)))]])).

cnf(refute_0_30, plain,
    (set_intersection2(X_69, X_70) = set_intersection2(X_70, X_69)),
    inference(resolve,
              [$cnf($equal(set_intersection2(X_70, X_69),
                      set_intersection2(X_69, X_70)))],
              [refute_0_28, refute_0_29])).

cnf(refute_0_31, plain,
    (set_intersection2(X_69, X_70) != set_intersection2(X_70, X_69) |
     set_union2(set_difference(X_69, X_70),
       set_intersection2(X_69, X_70)) !=
     set_union2(X_69, set_difference(X_69, X_70)) |
     set_union2(set_difference(X_69, X_70),
       set_intersection2(X_70, X_69)) =
     set_union2(X_69, set_difference(X_69, X_70))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(set_difference(X_69, X_70),
                          set_intersection2(X_69, X_70)),
                        set_union2(X_69, set_difference(X_69, X_70)))),
                 [0, 1], $fot(set_intersection2(X_70, X_69))]])).

cnf(refute_0_32, plain,
    (set_union2(set_difference(X_69, X_70),
       set_intersection2(X_69, X_70)) !=
     set_union2(X_69, set_difference(X_69, X_70)) |
     set_union2(set_difference(X_69, X_70),
       set_intersection2(X_70, X_69)) =
     set_union2(X_69, set_difference(X_69, X_70))),
    inference(resolve,
              [$cnf($equal(set_intersection2(X_69, X_70),
                      set_intersection2(X_70, X_69)))],
              [refute_0_30, refute_0_31])).

cnf(refute_0_33, plain,
    (set_union2(set_difference(X_69, X_70),
       set_intersection2(X_70, X_69)) =
     set_union2(X_69, set_difference(X_69, X_70))),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(X_69, X_70),
                        set_intersection2(X_69, X_70)),
                      set_union2(X_69, set_difference(X_69, X_70))))],
              [refute_0_26, refute_0_32])).

cnf(refute_0_34, plain,
    (set_union2(set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1),
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    inference(subst, [],
              [refute_0_33 :
               [bind(X_69, $fot(skolemFOFtoCNF_A_2)),
                bind(X_70, $fot(skolemFOFtoCNF_B_1))]])).

cnf(refute_0_35, plain, (subset(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(canonicalize, [], [normalize_0_21])).

cnf(refute_0_36, plain,
    (~ subset(A, B) | set_difference(A, B) = empty_set),
    inference(canonicalize, [], [normalize_0_25])).

cnf(refute_0_37, plain,
    (~ subset(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) |
     set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) = empty_set),
    inference(subst, [],
              [refute_0_36 :
               [bind(A, $fot(skolemFOFtoCNF_A_2)),
                bind(B, $fot(skolemFOFtoCNF_B_1))]])).

cnf(refute_0_38, plain,
    (set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) = empty_set),
    inference(resolve,
              [$cnf(subset(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))],
              [refute_0_35, refute_0_37])).

cnf(refute_0_39, plain,
    (set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) != empty_set |
     set_union2(set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1),
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(set_difference(skolemFOFtoCNF_A_2,
                            skolemFOFtoCNF_B_1),
                          set_intersection2(skolemFOFtoCNF_B_1,
                            skolemFOFtoCNF_A_2)),
                        set_union2(skolemFOFtoCNF_A_2,
                          set_difference(skolemFOFtoCNF_A_2,
                            skolemFOFtoCNF_B_1)))), [0, 0],
                 $fot(empty_set)]])).

cnf(refute_0_40, plain,
    (set_union2(set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1),
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    inference(resolve,
              [$cnf($equal(set_difference(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1), empty_set))],
              [refute_0_38, refute_0_39])).

cnf(refute_0_41, plain,
    (set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1),
                        set_intersection2(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_A_2)),
                      set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1))))],
              [refute_0_34, refute_0_40])).

cnf(refute_0_42, plain,
    (set_intersection2(A, B) != set_intersection2(B, A) |
     set_intersection2(B, A) = set_intersection2(A, B)),
    inference(subst, [],
              [refute_0_19 :
               [bind(X, $fot(set_intersection2(A, B))),
                bind(Y, $fot(set_intersection2(B, A)))]])).

cnf(refute_0_43, plain,
    (set_intersection2(B, A) = set_intersection2(A, B)),
    inference(resolve,
              [$cnf($equal(set_intersection2(A, B),
                      set_intersection2(B, A)))],
              [refute_0_27, refute_0_42])).

cnf(refute_0_44, plain,
    (set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2) =
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(subst, [],
              [refute_0_43 :
               [bind(A, $fot(skolemFOFtoCNF_A_2)),
                bind(B, $fot(skolemFOFtoCNF_B_1))]])).

cnf(refute_0_45, plain, (set_union2(A, empty_set) = A),
    inference(canonicalize, [], [normalize_0_27])).

cnf(refute_0_46, plain,
    (set_union2(A, empty_set) = set_union2(empty_set, A)),
    inference(subst, [], [refute_0_16 : [bind(B, $fot(empty_set))]])).

cnf(refute_0_47, plain,
    (set_union2(A, empty_set) != A |
     set_union2(A, empty_set) != set_union2(empty_set, A) |
     set_union2(empty_set, A) = A),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(A, empty_set), A)), [0],
                 $fot(set_union2(empty_set, A))]])).

cnf(refute_0_48, plain,
    (set_union2(A, empty_set) != A | set_union2(empty_set, A) = A),
    inference(resolve,
              [$cnf($equal(set_union2(A, empty_set),
                      set_union2(empty_set, A)))],
              [refute_0_46, refute_0_47])).

cnf(refute_0_49, plain, (set_union2(empty_set, A) = A),
    inference(resolve, [$cnf($equal(set_union2(A, empty_set), A))],
              [refute_0_45, refute_0_48])).

cnf(refute_0_50, plain,
    (set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)),
    inference(subst, [],
              [refute_0_49 :
               [bind(A,
                     $fot(set_intersection2(skolemFOFtoCNF_B_1,
                            skolemFOFtoCNF_A_2)))]])).

cnf(refute_0_51, plain, (Y != X | Y != Z | X = Z),
    introduced(tautology, [equality, [$cnf($equal(Y, Z)), [0], $fot(X)]])).

cnf(refute_0_52, plain, (X != Y | Y != Z | X = Z),
    inference(resolve, [$cnf($equal(Y, X))], [refute_0_19, refute_0_51])).

cnf(refute_0_53, plain,
    (set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2) !=
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) |
     set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2) |
     set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(subst, [],
              [refute_0_52 :
               [bind(X,
                     $fot(set_union2(empty_set,
                            set_intersection2(skolemFOFtoCNF_B_1,
                              skolemFOFtoCNF_A_2)))),
                bind(Y,
                     $fot(set_intersection2(skolemFOFtoCNF_B_1,
                            skolemFOFtoCNF_A_2))),
                bind(Z,
                     $fot(set_intersection2(skolemFOFtoCNF_A_2,
                            skolemFOFtoCNF_B_1)))]])).

cnf(refute_0_54, plain,
    (set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2) !=
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) |
     set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(resolve,
              [$cnf($equal(set_union2(empty_set,
                        set_intersection2(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_A_2)),
                      set_intersection2(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_A_2)))],
              [refute_0_50, refute_0_53])).

cnf(refute_0_55, plain,
    (set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) =
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)),
    inference(resolve,
              [$cnf($equal(set_intersection2(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_A_2),
                      set_intersection2(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1)))],
              [refute_0_44, refute_0_54])).

cnf(refute_0_56, plain,
    (set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) |
     set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(empty_set,
                          set_intersection2(skolemFOFtoCNF_B_1,
                            skolemFOFtoCNF_A_2)),
                        set_union2(skolemFOFtoCNF_A_2,
                          set_difference(skolemFOFtoCNF_A_2,
                            skolemFOFtoCNF_B_1)))), [0],
                 $fot(set_intersection2(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1))]])).

cnf(refute_0_57, plain,
    (set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    inference(resolve,
              [$cnf($equal(set_union2(empty_set,
                        set_intersection2(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_A_2)),
                      set_intersection2(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1)))],
              [refute_0_55, refute_0_56])).

cnf(refute_0_58, plain,
    (set_union2(skolemFOFtoCNF_A_2, empty_set) = skolemFOFtoCNF_A_2),
    inference(subst, [],
              [refute_0_45 : [bind(A, $fot(skolemFOFtoCNF_A_2))]])).

cnf(refute_0_59, plain,
    (set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    introduced(tautology,
               [refl,
                [$fot(set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1)))]])).

cnf(refute_0_60, plain,
    (set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) != empty_set |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     set_union2(skolemFOFtoCNF_A_2, empty_set)),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(skolemFOFtoCNF_A_2,
                          set_difference(skolemFOFtoCNF_A_2,
                            skolemFOFtoCNF_B_1)),
                        set_union2(skolemFOFtoCNF_A_2,
                          set_difference(skolemFOFtoCNF_A_2,
                            skolemFOFtoCNF_B_1)))), [1, 1],
                 $fot(empty_set)]])).

cnf(refute_0_61, plain,
    (set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) != empty_set |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     set_union2(skolemFOFtoCNF_A_2, empty_set)),
    inference(resolve,
              [$cnf($equal(set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1)),
                      set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1))))],
              [refute_0_59, refute_0_60])).

cnf(refute_0_62, plain,
    (set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     set_union2(skolemFOFtoCNF_A_2, empty_set)),
    inference(resolve,
              [$cnf($equal(set_difference(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1), empty_set))],
              [refute_0_38, refute_0_61])).

cnf(refute_0_63, plain,
    (set_union2(skolemFOFtoCNF_A_2, empty_set) != skolemFOFtoCNF_A_2 |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) !=
     set_union2(skolemFOFtoCNF_A_2, empty_set) |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     skolemFOFtoCNF_A_2),
    inference(subst, [],
              [refute_0_52 :
               [bind(X,
                     $fot(set_union2(skolemFOFtoCNF_A_2,
                            set_difference(skolemFOFtoCNF_A_2,
                              skolemFOFtoCNF_B_1)))),
                bind(Y, $fot(set_union2(skolemFOFtoCNF_A_2, empty_set))),
                bind(Z, $fot(skolemFOFtoCNF_A_2))]])).

cnf(refute_0_64, plain,
    (set_union2(skolemFOFtoCNF_A_2, empty_set) != skolemFOFtoCNF_A_2 |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     skolemFOFtoCNF_A_2),
    inference(resolve,
              [$cnf($equal(set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1)),
                      set_union2(skolemFOFtoCNF_A_2, empty_set)))],
              [refute_0_62, refute_0_63])).

cnf(refute_0_65, plain,
    (set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) =
     skolemFOFtoCNF_A_2),
    inference(resolve,
              [$cnf($equal(set_union2(skolemFOFtoCNF_A_2, empty_set),
                      skolemFOFtoCNF_A_2))], [refute_0_58, refute_0_64])).

cnf(refute_0_66, plain,
    (set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) !=
     skolemFOFtoCNF_A_2 |
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) =
     skolemFOFtoCNF_A_2),
    introduced(tautology,
               [equality,
                [$cnf(~ $equal(set_intersection2(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1), skolemFOFtoCNF_A_2)), [0],
                 $fot(set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1)))]])).

cnf(refute_0_67, plain,
    (set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) =
     skolemFOFtoCNF_A_2),
    inference(resolve,
              [$cnf($equal(set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1)), skolemFOFtoCNF_A_2))],
              [refute_0_65, refute_0_66])).

cnf(refute_0_68, plain,
    (set_union2(empty_set,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_A_2)) !=
     set_union2(skolemFOFtoCNF_A_2,
       set_difference(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1)) |
     set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) =
     skolemFOFtoCNF_A_2),
    inference(resolve,
              [$cnf($equal(set_intersection2(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1),
                      set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1))))],
              [refute_0_57, refute_0_67])).

cnf(refute_0_69, plain,
    (set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) =
     skolemFOFtoCNF_A_2),
    inference(resolve,
              [$cnf($equal(set_union2(empty_set,
                        set_intersection2(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_A_2)),
                      set_union2(skolemFOFtoCNF_A_2,
                        set_difference(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1))))],
              [refute_0_41, refute_0_68])).

cnf(refute_0_70, plain,
    (set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1) !=
     skolemFOFtoCNF_A_2 | ~ in(X_291, skolemFOFtoCNF_A_2) |
     in(X_291, set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    introduced(tautology,
               [equality,
                [$cnf(~ in(X_291,
                        set_intersection2(skolemFOFtoCNF_A_2,
                          skolemFOFtoCNF_B_1))), [1],
                 $fot(skolemFOFtoCNF_A_2)]])).

cnf(refute_0_71, plain,
    (~ in(X_291, skolemFOFtoCNF_A_2) |
     in(X_291, set_intersection2(skolemFOFtoCNF_A_2, skolemFOFtoCNF_B_1))),
    inference(resolve,
              [$cnf($equal(set_intersection2(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1), skolemFOFtoCNF_A_2))],
              [refute_0_69, refute_0_70])).

cnf(refute_0_72, plain,
    (~ in(X_291, skolemFOFtoCNF_A_2) | in(X_291, skolemFOFtoCNF_B_1)),
    inference(resolve,
              [$cnf(in(X_291,
                      set_intersection2(skolemFOFtoCNF_A_2,
                        skolemFOFtoCNF_B_1)))],
              [refute_0_71, refute_0_8])).

cnf(refute_0_73, plain,
    (~ in(skolemFOFtoCNF_C_2(A, skolemFOFtoCNF_A_2), skolemFOFtoCNF_A_2) |
     in(skolemFOFtoCNF_C_2(A, skolemFOFtoCNF_A_2), skolemFOFtoCNF_B_1)),
    inference(subst, [],
              [refute_0_72 :
               [bind(X_291,
                     $fot(skolemFOFtoCNF_C_2(A, skolemFOFtoCNF_A_2)))]])).

cnf(refute_0_74, plain,
    (disjoint(A, skolemFOFtoCNF_A_2) |
     in(skolemFOFtoCNF_C_2(A, skolemFOFtoCNF_A_2), skolemFOFtoCNF_B_1)),
    inference(resolve,
              [$cnf(in(skolemFOFtoCNF_C_2(A, skolemFOFtoCNF_A_2),
                      skolemFOFtoCNF_A_2))], [refute_0_3, refute_0_73])).

cnf(refute_0_75, plain,
    (disjoint(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2) |
     in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2),
       skolemFOFtoCNF_B_1)),
    inference(subst, [],
              [refute_0_74 : [bind(A, $fot(skolemFOFtoCNF_C_4))]])).

cnf(refute_0_76, plain, (disjoint(A, B) | in(skolemFOFtoCNF_C_2(A, B), A)),
    inference(canonicalize, [], [normalize_0_28])).

cnf(refute_0_77, plain,
    (disjoint(skolemFOFtoCNF_C_4, B) |
     in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, B), skolemFOFtoCNF_C_4)),
    inference(subst, [],
              [refute_0_76 : [bind(A, $fot(skolemFOFtoCNF_C_4))]])).

cnf(refute_0_78, plain,
    (C != set_difference(A, B) | ~ in(D, B) | ~ in(D, C)),
    inference(canonicalize, [], [normalize_0_32])).

cnf(refute_0_79, plain,
    (set_difference(A, B) != set_difference(A, B) | ~ in(D, B) |
     ~ in(D, set_difference(A, B))),
    inference(subst, [],
              [refute_0_78 : [bind(C, $fot(set_difference(A, B)))]])).

cnf(refute_0_80, plain, (set_difference(A, B) = set_difference(A, B)),
    introduced(tautology, [refl, [$fot(set_difference(A, B))]])).

cnf(refute_0_81, plain, (~ in(D, B) | ~ in(D, set_difference(A, B))),
    inference(resolve,
              [$cnf($equal(set_difference(A, B), set_difference(A, B)))],
              [refute_0_80, refute_0_79])).

cnf(refute_0_82, plain,
    (~ in(X_307, set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)) |
     ~ in(X_307, skolemFOFtoCNF_C_4)),
    inference(subst, [],
              [refute_0_81 :
               [bind(A, $fot(skolemFOFtoCNF_B_1)),
                bind(B, $fot(skolemFOFtoCNF_C_4)),
                bind(D, $fot(X_307))]])).

cnf(refute_0_83, plain,
    (set_union2(set_difference(set_difference(X_70, X_110), X_70),
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    inference(subst, [],
              [refute_0_33 :
               [bind(X_69, $fot(set_difference(X_70, X_110)))]])).

cnf(refute_0_84, plain, (subset(set_difference(A, B), A)),
    inference(canonicalize, [], [normalize_0_34])).

cnf(refute_0_85, plain, (subset(set_difference(X_109, B), X_109)),
    inference(subst, [], [refute_0_84 : [bind(A, $fot(X_109))]])).

cnf(refute_0_86, plain,
    (~ subset(set_difference(X_109, B), X_109) |
     set_difference(set_difference(X_109, B), X_109) = empty_set),
    inference(subst, [],
              [refute_0_36 :
               [bind(A, $fot(set_difference(X_109, B))),
                bind(B, $fot(X_109))]])).

cnf(refute_0_87, plain,
    (set_difference(set_difference(X_109, B), X_109) = empty_set),
    inference(resolve, [$cnf(subset(set_difference(X_109, B), X_109))],
              [refute_0_85, refute_0_86])).

cnf(refute_0_88, plain,
    (set_difference(set_difference(X_70, X_110), X_70) = empty_set),
    inference(subst, [],
              [refute_0_87 :
               [bind(B, $fot(X_110)), bind(X_109, $fot(X_70))]])).

cnf(refute_0_89, plain,
    (set_difference(set_difference(X_70, X_110), X_70) != empty_set |
     set_union2(set_difference(set_difference(X_70, X_110), X_70),
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(set_difference(set_difference(X_70,
                              X_110), X_70),
                          set_intersection2(X_70,
                            set_difference(X_70, X_110))),
                        set_union2(set_difference(X_70, X_110),
                          set_difference(set_difference(X_70, X_110),
                            X_70)))), [0, 0], $fot(empty_set)]])).

cnf(refute_0_90, plain,
    (set_union2(set_difference(set_difference(X_70, X_110), X_70),
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    inference(resolve,
              [$cnf($equal(set_difference(set_difference(X_70, X_110),
                        X_70), empty_set))], [refute_0_88, refute_0_89])).

cnf(refute_0_91, plain,
    (set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(set_difference(X_70,
                            X_110), X_70),
                        set_intersection2(X_70,
                          set_difference(X_70, X_110))),
                      set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110),
                          X_70))))], [refute_0_83, refute_0_90])).

cnf(refute_0_92, plain,
    (set_difference(A, set_difference(A, set_difference(A, X_68))) =
     set_intersection2(A, set_difference(A, X_68))),
    inference(subst, [],
              [refute_0_11 : [bind(B, $fot(set_difference(A, X_68)))]])).

cnf(refute_0_93, plain,
    (set_difference(A, set_difference(A, X_68)) =
     set_intersection2(A, X_68)),
    inference(subst, [], [refute_0_11 : [bind(B, $fot(X_68))]])).

cnf(refute_0_94, plain,
    (set_difference(A, set_difference(A, X_68)) !=
     set_intersection2(A, X_68) |
     set_difference(A, set_difference(A, set_difference(A, X_68))) !=
     set_intersection2(A, set_difference(A, X_68)) |
     set_difference(A, set_intersection2(A, X_68)) =
     set_intersection2(A, set_difference(A, X_68))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_difference(A,
                          set_difference(A, set_difference(A, X_68))),
                        set_intersection2(A, set_difference(A, X_68)))),
                 [0, 1], $fot(set_intersection2(A, X_68))]])).

cnf(refute_0_95, plain,
    (set_difference(A, set_difference(A, set_difference(A, X_68))) !=
     set_intersection2(A, set_difference(A, X_68)) |
     set_difference(A, set_intersection2(A, X_68)) =
     set_intersection2(A, set_difference(A, X_68))),
    inference(resolve,
              [$cnf($equal(set_difference(A, set_difference(A, X_68)),
                      set_intersection2(A, X_68)))],
              [refute_0_93, refute_0_94])).

cnf(refute_0_96, plain,
    (set_difference(A, set_intersection2(A, X_68)) =
     set_intersection2(A, set_difference(A, X_68))),
    inference(resolve,
              [$cnf($equal(set_difference(A,
                        set_difference(A, set_difference(A, X_68))),
                      set_intersection2(A, set_difference(A, X_68))))],
              [refute_0_92, refute_0_95])).

cnf(refute_0_97, plain,
    (set_difference(A, set_intersection2(A, X_68)) !=
     set_intersection2(A, set_difference(A, X_68)) |
     set_intersection2(A, set_difference(A, X_68)) =
     set_difference(A, set_intersection2(A, X_68))),
    inference(subst, [],
              [refute_0_19 :
               [bind(X,
                     $fot(set_difference(A, set_intersection2(A, X_68)))),
                bind(Y,
                     $fot(set_intersection2(A,
                            set_difference(A, X_68))))]])).

cnf(refute_0_98, plain,
    (set_intersection2(A, set_difference(A, X_68)) =
     set_difference(A, set_intersection2(A, X_68))),
    inference(resolve,
              [$cnf($equal(set_difference(A, set_intersection2(A, X_68)),
                      set_intersection2(A, set_difference(A, X_68))))],
              [refute_0_96, refute_0_97])).

cnf(refute_0_99, plain,
    (set_intersection2(X_70, set_difference(X_70, X_110)) =
     set_difference(X_70, set_intersection2(X_70, X_110))),
    inference(subst, [],
              [refute_0_98 :
               [bind(A, $fot(X_70)), bind(X_68, $fot(X_110))]])).

cnf(refute_0_100, plain,
    (set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_intersection2(X_70, set_difference(X_70, X_110))),
    inference(subst, [],
              [refute_0_49 :
               [bind(A,
                     $fot(set_intersection2(X_70,
                            set_difference(X_70, X_110))))]])).

cnf(refute_0_101, plain,
    (set_intersection2(X_70, set_difference(X_70, X_110)) !=
     set_difference(X_70, set_intersection2(X_70, X_110)) |
     set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_intersection2(X_70, set_difference(X_70, X_110)) |
     set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_difference(X_70, set_intersection2(X_70, X_110))),
    inference(subst, [],
              [refute_0_52 :
               [bind(X,
                     $fot(set_union2(empty_set,
                            set_intersection2(X_70,
                              set_difference(X_70, X_110))))),
                bind(Y,
                     $fot(set_intersection2(X_70,
                            set_difference(X_70, X_110)))),
                bind(Z,
                     $fot(set_difference(X_70,
                            set_intersection2(X_70, X_110))))]])).

cnf(refute_0_102, plain,
    (set_intersection2(X_70, set_difference(X_70, X_110)) !=
     set_difference(X_70, set_intersection2(X_70, X_110)) |
     set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_difference(X_70, set_intersection2(X_70, X_110))),
    inference(resolve,
              [$cnf($equal(set_union2(empty_set,
                        set_intersection2(X_70,
                          set_difference(X_70, X_110))),
                      set_intersection2(X_70,
                        set_difference(X_70, X_110))))],
              [refute_0_100, refute_0_101])).

cnf(refute_0_103, plain,
    (set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) =
     set_difference(X_70, set_intersection2(X_70, X_110))),
    inference(resolve,
              [$cnf($equal(set_intersection2(X_70,
                        set_difference(X_70, X_110)),
                      set_difference(X_70,
                        set_intersection2(X_70, X_110))))],
              [refute_0_99, refute_0_102])).

cnf(refute_0_104, plain,
    (set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_difference(X_70, set_intersection2(X_70, X_110)) |
     set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_difference(X_70, set_intersection2(X_70, X_110)) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(empty_set,
                          set_intersection2(X_70,
                            set_difference(X_70, X_110))),
                        set_union2(set_difference(X_70, X_110),
                          set_difference(set_difference(X_70, X_110),
                            X_70)))), [0],
                 $fot(set_difference(X_70,
                        set_intersection2(X_70, X_110)))]])).

cnf(refute_0_105, plain,
    (set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_difference(X_70, set_intersection2(X_70, X_110)) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    inference(resolve,
              [$cnf($equal(set_union2(empty_set,
                        set_intersection2(X_70,
                          set_difference(X_70, X_110))),
                      set_difference(X_70,
                        set_intersection2(X_70, X_110))))],
              [refute_0_103, refute_0_104])).

cnf(refute_0_106, plain,
    (set_union2(set_difference(X_70, X_110), empty_set) =
     set_difference(X_70, X_110)),
    inference(subst, [],
              [refute_0_45 :
               [bind(A, $fot(set_difference(X_70, X_110)))]])).

cnf(refute_0_107, plain,
    (set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70))),
    introduced(tautology,
               [refl,
                [$fot(set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110),
                          X_70)))]])).

cnf(refute_0_108, plain,
    (set_difference(set_difference(X_70, X_110), X_70) != empty_set |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_union2(set_difference(X_70, X_110), empty_set)),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_union2(set_difference(X_70, X_110),
                          set_difference(set_difference(X_70, X_110),
                            X_70)),
                        set_union2(set_difference(X_70, X_110),
                          set_difference(set_difference(X_70, X_110),
                            X_70)))), [1, 1], $fot(empty_set)]])).

cnf(refute_0_109, plain,
    (set_difference(set_difference(X_70, X_110), X_70) != empty_set |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_union2(set_difference(X_70, X_110), empty_set)),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110), X_70)),
                      set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110),
                          X_70))))], [refute_0_107, refute_0_108])).

cnf(refute_0_110, plain,
    (set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_union2(set_difference(X_70, X_110), empty_set)),
    inference(resolve,
              [$cnf($equal(set_difference(set_difference(X_70, X_110),
                        X_70), empty_set))], [refute_0_88, refute_0_109])).

cnf(refute_0_111, plain,
    (set_union2(set_difference(X_70, X_110), empty_set) !=
     set_difference(X_70, X_110) |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) !=
     set_union2(set_difference(X_70, X_110), empty_set) |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_difference(X_70, X_110)),
    inference(subst, [],
              [refute_0_52 :
               [bind(X,
                     $fot(set_union2(set_difference(X_70, X_110),
                            set_difference(set_difference(X_70, X_110),
                              X_70)))),
                bind(Y,
                     $fot(set_union2(set_difference(X_70, X_110),
                            empty_set))),
                bind(Z, $fot(set_difference(X_70, X_110)))]])).

cnf(refute_0_112, plain,
    (set_union2(set_difference(X_70, X_110), empty_set) !=
     set_difference(X_70, X_110) |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_difference(X_70, X_110)),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110), X_70)),
                      set_union2(set_difference(X_70, X_110),
                        empty_set)))], [refute_0_110, refute_0_111])).

cnf(refute_0_113, plain,
    (set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) =
     set_difference(X_70, X_110)),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(X_70, X_110),
                        empty_set), set_difference(X_70, X_110)))],
              [refute_0_106, refute_0_112])).

cnf(refute_0_114, plain,
    (set_difference(X_70, set_intersection2(X_70, X_110)) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) !=
     set_difference(X_70, X_110) |
     set_difference(X_70, set_intersection2(X_70, X_110)) =
     set_difference(X_70, X_110)),
    introduced(tautology,
               [equality,
                [$cnf(~ $equal(set_difference(X_70,
                          set_intersection2(X_70, X_110)),
                        set_difference(X_70, X_110))), [0],
                 $fot(set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110),
                          X_70)))]])).

cnf(refute_0_115, plain,
    (set_difference(X_70, set_intersection2(X_70, X_110)) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_difference(X_70, set_intersection2(X_70, X_110)) =
     set_difference(X_70, X_110)),
    inference(resolve,
              [$cnf($equal(set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110), X_70)),
                      set_difference(X_70, X_110)))],
              [refute_0_113, refute_0_114])).

cnf(refute_0_116, plain,
    (set_union2(empty_set,
       set_intersection2(X_70, set_difference(X_70, X_110))) !=
     set_union2(set_difference(X_70, X_110),
       set_difference(set_difference(X_70, X_110), X_70)) |
     set_difference(X_70, set_intersection2(X_70, X_110)) =
     set_difference(X_70, X_110)),
    inference(resolve,
              [$cnf($equal(set_difference(X_70,
                        set_intersection2(X_70, X_110)),
                      set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110),
                          X_70))))], [refute_0_105, refute_0_115])).

cnf(refute_0_117, plain,
    (set_difference(X_70, set_intersection2(X_70, X_110)) =
     set_difference(X_70, X_110)),
    inference(resolve,
              [$cnf($equal(set_union2(empty_set,
                        set_intersection2(X_70,
                          set_difference(X_70, X_110))),
                      set_union2(set_difference(X_70, X_110),
                        set_difference(set_difference(X_70, X_110),
                          X_70))))], [refute_0_91, refute_0_116])).

cnf(refute_0_118, plain,
    (set_difference(skolemFOFtoCNF_B_1,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)) =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(subst, [],
              [refute_0_117 :
               [bind(X_110, $fot(skolemFOFtoCNF_C_4)),
                bind(X_70, $fot(skolemFOFtoCNF_B_1))]])).

cnf(refute_0_119, plain,
    (disjoint(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(canonicalize, [], [normalize_0_35])).

cnf(refute_0_120, plain,
    (~ disjoint(A, B) | set_intersection2(A, B) = empty_set),
    inference(canonicalize, [], [normalize_0_39])).

cnf(refute_0_121, plain,
    (~ disjoint(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) |
     set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) =
     empty_set),
    inference(subst, [],
              [refute_0_120 :
               [bind(A, $fot(skolemFOFtoCNF_B_1)),
                bind(B, $fot(skolemFOFtoCNF_C_4))]])).

cnf(refute_0_122, plain,
    (set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) =
     empty_set),
    inference(resolve,
              [$cnf(disjoint(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4))],
              [refute_0_119, refute_0_121])).

cnf(refute_0_123, plain,
    (set_difference(skolemFOFtoCNF_B_1,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)) !=
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) |
     set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) !=
     empty_set |
     set_difference(skolemFOFtoCNF_B_1, empty_set) =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_difference(skolemFOFtoCNF_B_1,
                          set_intersection2(skolemFOFtoCNF_B_1,
                            skolemFOFtoCNF_C_4)),
                        set_difference(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_C_4))), [0, 1],
                 $fot(empty_set)]])).

cnf(refute_0_124, plain,
    (set_difference(skolemFOFtoCNF_B_1,
       set_intersection2(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)) !=
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) |
     set_difference(skolemFOFtoCNF_B_1, empty_set) =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(resolve,
              [$cnf($equal(set_intersection2(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_C_4), empty_set))],
              [refute_0_122, refute_0_123])).

cnf(refute_0_125, plain,
    (set_difference(skolemFOFtoCNF_B_1, empty_set) =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(resolve,
              [$cnf($equal(set_difference(skolemFOFtoCNF_B_1,
                        set_intersection2(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_C_4)),
                      set_difference(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_C_4)))],
              [refute_0_118, refute_0_124])).

cnf(refute_0_126, plain, (set_difference(A, empty_set) = A),
    inference(canonicalize, [], [normalize_0_41])).

cnf(refute_0_127, plain,
    (set_difference(skolemFOFtoCNF_B_1, empty_set) = skolemFOFtoCNF_B_1),
    inference(subst, [],
              [refute_0_126 : [bind(A, $fot(skolemFOFtoCNF_B_1))]])).

cnf(refute_0_128, plain,
    (set_difference(skolemFOFtoCNF_B_1, empty_set) !=
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) |
     set_difference(skolemFOFtoCNF_B_1, empty_set) != skolemFOFtoCNF_B_1 |
     skolemFOFtoCNF_B_1 =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    introduced(tautology,
               [equality,
                [$cnf($equal(set_difference(skolemFOFtoCNF_B_1, empty_set),
                        set_difference(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_C_4))), [0],
                 $fot(skolemFOFtoCNF_B_1)]])).

cnf(refute_0_129, plain,
    (set_difference(skolemFOFtoCNF_B_1, empty_set) !=
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) |
     skolemFOFtoCNF_B_1 =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(resolve,
              [$cnf($equal(set_difference(skolemFOFtoCNF_B_1, empty_set),
                      skolemFOFtoCNF_B_1))],
              [refute_0_127, refute_0_128])).

cnf(refute_0_130, plain,
    (skolemFOFtoCNF_B_1 =
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4)),
    inference(resolve,
              [$cnf($equal(set_difference(skolemFOFtoCNF_B_1, empty_set),
                      set_difference(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_C_4)))],
              [refute_0_125, refute_0_129])).

cnf(refute_0_131, plain,
    (skolemFOFtoCNF_B_1 !=
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) |
     set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) =
     skolemFOFtoCNF_B_1),
    inference(subst, [],
              [refute_0_19 :
               [bind(X, $fot(skolemFOFtoCNF_B_1)),
                bind(Y,
                     $fot(set_difference(skolemFOFtoCNF_B_1,
                            skolemFOFtoCNF_C_4)))]])).

cnf(refute_0_132, plain,
    (set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) =
     skolemFOFtoCNF_B_1),
    inference(resolve,
              [$cnf($equal(skolemFOFtoCNF_B_1,
                      set_difference(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_C_4)))],
              [refute_0_130, refute_0_131])).

cnf(refute_0_133, plain,
    (set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4) !=
     skolemFOFtoCNF_B_1 | ~ in(X_307, skolemFOFtoCNF_B_1) |
     in(X_307, set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4))),
    introduced(tautology,
               [equality,
                [$cnf(~ in(X_307,
                        set_difference(skolemFOFtoCNF_B_1,
                          skolemFOFtoCNF_C_4))), [1],
                 $fot(skolemFOFtoCNF_B_1)]])).

cnf(refute_0_134, plain,
    (~ in(X_307, skolemFOFtoCNF_B_1) |
     in(X_307, set_difference(skolemFOFtoCNF_B_1, skolemFOFtoCNF_C_4))),
    inference(resolve,
              [$cnf($equal(set_difference(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_C_4), skolemFOFtoCNF_B_1))],
              [refute_0_132, refute_0_133])).

cnf(refute_0_135, plain,
    (~ in(X_307, skolemFOFtoCNF_B_1) | ~ in(X_307, skolemFOFtoCNF_C_4)),
    inference(resolve,
              [$cnf(in(X_307,
                      set_difference(skolemFOFtoCNF_B_1,
                        skolemFOFtoCNF_C_4)))],
              [refute_0_134, refute_0_82])).

cnf(refute_0_136, plain,
    (~ in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, B), skolemFOFtoCNF_B_1) |
     ~ in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, B), skolemFOFtoCNF_C_4)),
    inference(subst, [],
              [refute_0_135 :
               [bind(X_307,
                     $fot(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, B)))]])).

cnf(refute_0_137, plain,
    (~ in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, B), skolemFOFtoCNF_B_1) |
     disjoint(skolemFOFtoCNF_C_4, B)),
    inference(resolve,
              [$cnf(in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, B),
                      skolemFOFtoCNF_C_4))], [refute_0_77, refute_0_136])).

cnf(refute_0_138, plain,
    (~
       in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2),
         skolemFOFtoCNF_B_1) |
     disjoint(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2)),
    inference(subst, [],
              [refute_0_137 : [bind(B, $fot(skolemFOFtoCNF_A_2))]])).

cnf(refute_0_139, plain,
    (disjoint(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2)),
    inference(resolve,
              [$cnf(in(skolemFOFtoCNF_C_2(skolemFOFtoCNF_C_4,
                        skolemFOFtoCNF_A_2), skolemFOFtoCNF_B_1))],
              [refute_0_75, refute_0_138])).

cnf(refute_0_140, plain,
    (disjoint(skolemFOFtoCNF_A_2, skolemFOFtoCNF_C_4)),
    inference(resolve,
              [$cnf(disjoint(skolemFOFtoCNF_C_4, skolemFOFtoCNF_A_2))],
              [refute_0_139, refute_0_1])).

cnf(refute_0_141, plain,
    (~ disjoint(skolemFOFtoCNF_A_2, skolemFOFtoCNF_C_4)),
    inference(canonicalize, [], [normalize_0_42])).

cnf(refute_0_142, plain, ($false),
    inference(resolve,
              [$cnf(disjoint(skolemFOFtoCNF_A_2, skolemFOFtoCNF_C_4))],
              [refute_0_140, refute_0_141])).
% SZS output end CNFRefutation for data/problems/all/SEU140+2.tptp