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