%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU157+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:21:50 PM UTC 2026
% Result : Theorem 123.17s 15.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU157+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n006.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 05:53:12 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 123.17/15.93 % Refutation found
% 123.17/15.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 123.17/15.93 % SZS output start CNFRefutation for theBenchmark
% 123.17/15.93 fof(f1,axiom,(
% 123.17/15.93 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f3,axiom,(
% 123.17/15.93 (! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f7,axiom,(
% 123.17/15.93 (! [A,B] :( B = singleton(A)<=> (! [C] :( in(C,B)<=> C = A ) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f8,axiom,(
% 123.17/15.93 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f9,axiom,(
% 123.17/15.93 (! [A,B] :( B = powerset(A)<=> (! [C] :( in(C,B)<=> subset(C,A) ) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f10,axiom,(
% 123.17/15.93 (! [A,B,C] :( C = unordered_pair(A,B)<=> (! [D] :( in(D,C)<=> ( D = A| D = B ) ) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f11,axiom,(
% 123.17/15.93 (! [A,B,C] :( C = set_union2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)| in(D,B) ) ) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f12,axiom,(
% 123.17/15.93 (! [A,B,C] :( C = cartesian_product2(A,B)<=> (! [D] :( in(D,C)<=> (? [E,F] :( in(E,A)& in(F,B)& D = ordered_pair(E,F) ) )) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f14,axiom,(
% 123.17/15.93 (! [A,B,C] :( C = set_intersection2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& in(D,B) ) ) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f15,axiom,(
% 123.17/15.93 (! [A,B] :( B = union(A)<=> (! [C] :( in(C,B)<=> (? [D] :( in(C,D)& in(D,A) ) )) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f16,axiom,(
% 123.17/15.93 (! [A,B,C] :( C = set_difference(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& ~ in(D,B) ) ) )) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f17,axiom,(
% 123.17/15.93 (! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f30,axiom,(
% 123.17/15.93 empty(empty_set) ),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f33,axiom,(
% 123.17/15.93 (! [A,B] :( ~ empty(A)=> ~ empty(set_union2(B,A)) ) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f34,axiom,(
% 123.17/15.93 (! [A,B] : set_union2(A,A) = A )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f37,lemma,(
% 123.17/15.93 (! [A] : singleton(A) != empty_set )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f46,conjecture,(
% 123.17/15.93 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f47,negated_conjecture,(
% 123.17/15.93 ~((! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) ))),
% 123.17/15.93 inference(negated_conjecture,[status(cth)],[f46])).
% 123.17/15.93 fof(f56,axiom,(
% 123.17/15.93 (! [A] : set_union2(A,empty_set) = A )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f58,lemma,(
% 123.17/15.93 powerset(empty_set) = singleton(empty_set) ),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f61,axiom,(
% 123.17/15.93 (! [A] : set_intersection2(A,empty_set) = empty_set )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f63,lemma,(
% 123.17/15.93 (! [A] : subset(empty_set,A) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f65,lemma,(
% 123.17/15.93 (! [A,B,C,D] :( ordered_pair(A,B) = ordered_pair(C,D)=> ( A = C& B = D ) ) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f82,axiom,(
% 123.17/15.93 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 123.17/15.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 123.17/15.93 fof(f89,plain,(
% 123.17/15.93 ![A,B]: (~in(A,B)|~in(B,A))),
% 123.17/15.93 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 123.17/15.93 fof(f90,plain,(
% 123.17/15.93 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f89])).
% 123.17/15.93 fof(f93,plain,(
% 123.17/15.93 ![X0,X1]: (unordered_pair(X0,X1)=unordered_pair(X1,X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f3])).
% 123.17/15.93 fof(f101,plain,(
% 123.17/15.93 ![A,B]: ((~B=singleton(A)|(![C]: ((~in(C,B)|C=A)&(in(C,B)|~C=A))))&(B=singleton(A)|(?[C]: ((~in(C,B)|~C=A)&(in(C,B)|C=A)))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f7])).
% 123.17/15.93 fof(f102,plain,(
% 123.17/15.93 (![A,B]: (~B=singleton(A)|((![C]: (~in(C,B)|C=A))&(![C]: (in(C,B)|~C=A)))))&(![A,B]: (B=singleton(A)|(?[C]: ((~in(C,B)|~C=A)&(in(C,B)|C=A)))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f101])).
% 123.17/15.93 fof(f103,plain,(
% 123.17/15.93 (![A,B]: (~B=singleton(A)|((![C]: (~in(C,B)|C=A))&(![C]: (in(C,B)|~C=A)))))&(![A,B]: (B=singleton(A)|((~in(sK0_skl(B,A),B)|~sK0_skl(B,A)=A)&(in(sK0_skl(B,A),B)|sK0_skl(B,A)=A))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f102])).
% 123.17/15.93 fof(f106,plain,(
% 123.17/15.93 ![X0,X1]: (X0=singleton(X1)|~in(sK0_skl(X0,X1),X0)|~sK0_skl(X0,X1)=X1)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f103])).
% 123.17/15.93 fof(f107,plain,(
% 123.17/15.93 ![X0,X1]: (X0=singleton(X1)|in(sK0_skl(X0,X1),X0)|sK0_skl(X0,X1)=X1)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f103])).
% 123.17/15.93 fof(f108,plain,(
% 123.17/15.93 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f8])).
% 123.17/15.93 fof(f109,plain,(
% 123.17/15.93 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f108])).
% 123.17/15.93 fof(f110,plain,(
% 123.17/15.93 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK1_skl(A),A)))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f109])).
% 123.17/15.93 fof(f111,plain,(
% 123.17/15.93 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f110])).
% 123.17/15.93 fof(f112,plain,(
% 123.17/15.93 ![X0]: (X0=empty_set|in(sK1_skl(X0),X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f110])).
% 123.17/15.93 fof(f113,plain,(
% 123.17/15.93 ![A,B]: ((~B=powerset(A)|(![C]: ((~in(C,B)|subset(C,A))&(in(C,B)|~subset(C,A)))))&(B=powerset(A)|(?[C]: ((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f9])).
% 123.17/15.93 fof(f114,plain,(
% 123.17/15.93 (![A,B]: (~B=powerset(A)|((![C]: (~in(C,B)|subset(C,A)))&(![C]: (in(C,B)|~subset(C,A))))))&(![A,B]: (B=powerset(A)|(?[C]: ((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f113])).
% 123.17/15.93 fof(f115,plain,(
% 123.17/15.93 (![A,B]: (~B=powerset(A)|((![C]: (~in(C,B)|subset(C,A)))&(![C]: (in(C,B)|~subset(C,A))))))&(![A,B]: (B=powerset(A)|((~in(sK2_skl(B,A),B)|~subset(sK2_skl(B,A),A))&(in(sK2_skl(B,A),B)|subset(sK2_skl(B,A),A)))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f114])).
% 123.17/15.93 fof(f116,plain,(
% 123.17/15.93 ![X0,X1,X2]: (~X0=powerset(X1)|~in(X2,X0)|subset(X2,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f115])).
% 123.17/15.93 fof(f117,plain,(
% 123.17/15.93 ![X0,X1,X2]: (~X0=powerset(X1)|in(X2,X0)|~subset(X2,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f115])).
% 123.17/15.93 fof(f120,plain,(
% 123.17/15.93 ![A,B,C]: ((~C=unordered_pair(A,B)|(![D]: ((~in(D,C)|(D=A|D=B))&(in(D,C)|(~D=A&~D=B)))))&(C=unordered_pair(A,B)|(?[D]: ((~in(D,C)|(~D=A&~D=B))&(in(D,C)|(D=A|D=B))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f10])).
% 123.17/15.93 fof(f121,plain,(
% 123.17/15.93 (![A,B,C]: (~C=unordered_pair(A,B)|((![D]: (~in(D,C)|(D=A|D=B)))&(![D]: (in(D,C)|(~D=A&~D=B))))))&(![A,B,C]: (C=unordered_pair(A,B)|(?[D]: ((~in(D,C)|(~D=A&~D=B))&(in(D,C)|(D=A|D=B))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f120])).
% 123.17/15.93 fof(f122,plain,(
% 123.17/15.93 (![A,B,C]: (~C=unordered_pair(A,B)|((![D]: (~in(D,C)|(D=A|D=B)))&(![D]: (in(D,C)|(~D=A&~D=B))))))&(![A,B,C]: (C=unordered_pair(A,B)|((~in(sK3_skl(C,B,A),C)|(~sK3_skl(C,B,A)=A&~sK3_skl(C,B,A)=B))&(in(sK3_skl(C,B,A),C)|(sK3_skl(C,B,A)=A|sK3_skl(C,B,A)=B)))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(D,sK3_skl(C,B,A))],[f121])).
% 123.17/15.93 fof(f124,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=unordered_pair(X1,X2)|in(X3,X0)|~X3=X1)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f122])).
% 123.17/15.93 fof(f125,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=unordered_pair(X1,X2)|in(X3,X0)|~X3=X2)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f122])).
% 123.17/15.93 fof(f129,plain,(
% 123.17/15.93 ![A,B,C]: ((~C=set_union2(A,B)|(![D]: ((~in(D,C)|(in(D,A)|in(D,B)))&(in(D,C)|(~in(D,A)&~in(D,B))))))&(C=set_union2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f11])).
% 123.17/15.93 fof(f130,plain,(
% 123.17/15.93 (![A,B,C]: (~C=set_union2(A,B)|((![D]: (~in(D,C)|(in(D,A)|in(D,B))))&(![D]: (in(D,C)|(~in(D,A)&~in(D,B)))))))&(![A,B,C]: (C=set_union2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f129])).
% 123.17/15.93 fof(f131,plain,(
% 123.17/15.93 (![A,B,C]: (~C=set_union2(A,B)|((![D]: (~in(D,C)|(in(D,A)|in(D,B))))&(![D]: (in(D,C)|(~in(D,A)&~in(D,B)))))))&(![A,B,C]: (C=set_union2(A,B)|((~in(sK4_skl(C,B,A),C)|(~in(sK4_skl(C,B,A),A)&~in(sK4_skl(C,B,A),B)))&(in(sK4_skl(C,B,A),C)|(in(sK4_skl(C,B,A),A)|in(sK4_skl(C,B,A),B))))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(D,sK4_skl(C,B,A))],[f130])).
% 123.17/15.93 fof(f132,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=set_union2(X1,X2)|~in(X3,X0)|in(X3,X1)|in(X3,X2))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f131])).
% 123.17/15.93 fof(f133,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=set_union2(X1,X2)|in(X3,X0)|~in(X3,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f131])).
% 123.17/15.93 fof(f137,plain,(
% 123.17/15.93 ![X0,X1,X2]: (X0=set_union2(X1,X2)|in(sK4_skl(X0,X2,X1),X0)|in(sK4_skl(X0,X2,X1),X1)|in(sK4_skl(X0,X2,X1),X2))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f131])).
% 123.17/15.93 fof(f138,definition,(
% 123.17/15.93 ![A,B,D,E,F]: (sP0_prd(F,E,D,B,A)<=>((in(E,A)&in(F,B))&D=ordered_pair(E,F)))),
% 123.17/15.93 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 123.17/15.93 fof(f139,plain,(
% 123.17/15.93 ![A,B,C]: (C=cartesian_product2(A,B)<=>(![D]: (in(D,C)<=>(?[E,F]: sP0_prd(F,E,D,B,A)))))),
% 123.17/15.93 inference(formula_renaming,[status(thm)],[f12,f138])).
% 123.17/15.93 fof(f140,plain,(
% 123.17/15.93 ![A,B,C]: ((~C=cartesian_product2(A,B)|(![D]: ((~in(D,C)|(?[E,F]: sP0_prd(F,E,D,B,A)))&(in(D,C)|(![E,F]: ~sP0_prd(F,E,D,B,A))))))&(C=cartesian_product2(A,B)|(?[D]: ((~in(D,C)|(![E,F]: ~sP0_prd(F,E,D,B,A)))&(in(D,C)|(?[E,F]: sP0_prd(F,E,D,B,A)))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f139])).
% 123.17/15.93 fof(f141,plain,(
% 123.17/15.93 (![A,B,C]: (~C=cartesian_product2(A,B)|((![D]: (~in(D,C)|(?[E,F]: sP0_prd(F,E,D,B,A))))&(![D]: (in(D,C)|(![E,F]: ~sP0_prd(F,E,D,B,A)))))))&(![A,B,C]: (C=cartesian_product2(A,B)|(?[D]: ((~in(D,C)|(![E,F]: ~sP0_prd(F,E,D,B,A)))&(in(D,C)|(?[E,F]: sP0_prd(F,E,D,B,A)))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f140])).
% 123.17/15.93 fof(f142,plain,(
% 123.17/15.93 (![A,B,C]: (~C=cartesian_product2(A,B)|((![D]: (~in(D,C)|sP0_prd(sK6_skl(D,C,B,A),sK5_skl(D,C,B,A),D,B,A)))&(![D]: (in(D,C)|(![E,F]: ~sP0_prd(F,E,D,B,A)))))))&(![A,B,C]: (C=cartesian_product2(A,B)|((~in(sK7_skl(C,B,A),C)|(![E,F]: ~sP0_prd(F,E,sK7_skl(C,B,A),B,A)))&(in(sK7_skl(C,B,A),C)|sP0_prd(sK9_skl(C,B,A),sK8_skl(C,B,A),sK7_skl(C,B,A),B,A)))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(E,sK5_skl(D,C,B,A)),skolemize(F,sK6_skl(D,C,B,A)),skolemize(D,sK7_skl(C,B,A)),skolemize(E,sK8_skl(C,B,A)),skolemize(F,sK9_skl(C,B,A))],[f141])).
% 123.17/15.93 fof(f143,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=cartesian_product2(X1,X2)|~in(X3,X0)|sP0_prd(sK6_skl(X3,X0,X2,X1),sK5_skl(X3,X0,X2,X1),X3,X2,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f142])).
% 123.17/15.93 fof(f144,plain,(
% 123.17/15.93 ![X0,X1,X2,X3,X4,X5]: (~X0=cartesian_product2(X1,X2)|in(X3,X0)|~sP0_prd(X4,X5,X3,X2,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f142])).
% 123.17/15.93 fof(f146,plain,(
% 123.17/15.93 ![X0,X1,X2]: (X0=cartesian_product2(X1,X2)|in(sK7_skl(X0,X2,X1),X0)|sP0_prd(sK9_skl(X0,X2,X1),sK8_skl(X0,X2,X1),sK7_skl(X0,X2,X1),X2,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f142])).
% 123.17/15.93 fof(f154,plain,(
% 123.17/15.93 ![A,B,C]: ((~C=set_intersection2(A,B)|(![D]: ((~in(D,C)|(in(D,A)&in(D,B)))&(in(D,C)|(~in(D,A)|~in(D,B))))))&(C=set_intersection2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f14])).
% 123.17/15.93 fof(f155,plain,(
% 123.17/15.93 (![A,B,C]: (~C=set_intersection2(A,B)|((![D]: (~in(D,C)|(in(D,A)&in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|~in(D,B)))))))&(![A,B,C]: (C=set_intersection2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f154])).
% 123.17/15.93 fof(f156,plain,(
% 123.17/15.93 (![A,B,C]: (~C=set_intersection2(A,B)|((![D]: (~in(D,C)|(in(D,A)&in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|~in(D,B)))))))&(![A,B,C]: (C=set_intersection2(A,B)|((~in(sK11_skl(C,B,A),C)|(~in(sK11_skl(C,B,A),A)|~in(sK11_skl(C,B,A),B)))&(in(sK11_skl(C,B,A),C)|(in(sK11_skl(C,B,A),A)&in(sK11_skl(C,B,A),B))))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(D,sK11_skl(C,B,A))],[f155])).
% 123.17/15.93 fof(f157,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f156])).
% 123.17/15.93 fof(f158,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X2))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f156])).
% 123.17/15.93 fof(f161,plain,(
% 123.17/15.93 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK11_skl(X0,X2,X1),X0)|in(sK11_skl(X0,X2,X1),X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f156])).
% 123.17/15.93 fof(f162,plain,(
% 123.17/15.93 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK11_skl(X0,X2,X1),X0)|in(sK11_skl(X0,X2,X1),X2))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f156])).
% 123.17/15.93 fof(f163,plain,(
% 123.17/15.93 ![A,B]: ((~B=union(A)|(![C]: ((~in(C,B)|(?[D]: (in(C,D)&in(D,A))))&(in(C,B)|(![D]: (~in(C,D)|~in(D,A)))))))&(B=union(A)|(?[C]: ((~in(C,B)|(![D]: (~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]: (in(C,D)&in(D,A))))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f15])).
% 123.17/15.93 fof(f164,plain,(
% 123.17/15.93 (![A,B]: (~B=union(A)|((![C]: (~in(C,B)|(?[D]: (in(C,D)&in(D,A)))))&(![C]: (in(C,B)|(![D]: (~in(C,D)|~in(D,A))))))))&(![A,B]: (B=union(A)|(?[C]: ((~in(C,B)|(![D]: (~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]: (in(C,D)&in(D,A))))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f163])).
% 123.17/15.93 fof(f165,plain,(
% 123.17/15.93 (![A,B]: (~B=union(A)|((![C]: (~in(C,B)|(in(C,sK12_skl(C,B,A))&in(sK12_skl(C,B,A),A))))&(![C]: (in(C,B)|(![D]: (~in(C,D)|~in(D,A))))))))&(![A,B]: (B=union(A)|((~in(sK13_skl(B,A),B)|(![D]: (~in(sK13_skl(B,A),D)|~in(D,A))))&(in(sK13_skl(B,A),B)|(in(sK13_skl(B,A),sK14_skl(B,A))&in(sK14_skl(B,A),A))))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(D,sK12_skl(C,B,A)),skolemize(C,sK13_skl(B,A)),skolemize(D,sK14_skl(B,A))],[f164])).
% 123.17/15.93 fof(f167,plain,(
% 123.17/15.93 ![X0,X1,X2]: (~X0=union(X1)|~in(X2,X0)|in(sK12_skl(X2,X0,X1),X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f165])).
% 123.17/15.93 fof(f168,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=union(X1)|in(X2,X0)|~in(X2,X3)|~in(X3,X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f165])).
% 123.17/15.93 fof(f172,plain,(
% 123.17/15.93 ![A,B,C]: ((~C=set_difference(A,B)|(![D]: ((~in(D,C)|(in(D,A)&~in(D,B)))&(in(D,C)|(~in(D,A)|in(D,B))))))&(C=set_difference(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|in(D,B)))&(in(D,C)|(in(D,A)&~in(D,B)))))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f16])).
% 123.17/15.93 fof(f173,plain,(
% 123.17/15.93 (![A,B,C]: (~C=set_difference(A,B)|((![D]: (~in(D,C)|(in(D,A)&~in(D,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)))&(in(D,C)|(in(D,A)&~in(D,B)))))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f172])).
% 123.17/15.93 fof(f174,plain,(
% 123.17/15.93 (![A,B,C]: (~C=set_difference(A,B)|((![D]: (~in(D,C)|(in(D,A)&~in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|in(D,B)))))))&(![A,B,C]: (C=set_difference(A,B)|((~in(sK15_skl(C,B,A),C)|(~in(sK15_skl(C,B,A),A)|in(sK15_skl(C,B,A),B)))&(in(sK15_skl(C,B,A),C)|(in(sK15_skl(C,B,A),A)&~in(sK15_skl(C,B,A),B))))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(D,sK15_skl(C,B,A))],[f173])).
% 123.17/15.93 fof(f176,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~X0=set_difference(X1,X2)|~in(X3,X0)|~in(X3,X2))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f174])).
% 123.17/15.93 fof(f181,plain,(
% 123.17/15.93 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X0,X1),singleton(X0)))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f17])).
% 123.17/15.93 fof(f191,plain,(
% 123.17/15.93 empty(empty_set)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f30])).
% 123.17/15.93 fof(f196,plain,(
% 123.17/15.93 ![A,B]: (empty(A)|~empty(set_union2(B,A)))),
% 123.17/15.93 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 123.17/15.93 fof(f197,plain,(
% 123.17/15.93 ![A]: (empty(A)|(![B]: ~empty(set_union2(B,A))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f196])).
% 123.17/15.93 fof(f198,plain,(
% 123.17/15.93 ![X0,X1]: (empty(X0)|~empty(set_union2(X1,X0)))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f197])).
% 123.17/15.93 fof(f199,plain,(
% 123.17/15.93 ![A]: set_union2(A,A)=A),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f34])).
% 123.17/15.93 fof(f200,plain,(
% 123.17/15.93 ![X0]: (set_union2(X0,X0)=X0)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f199])).
% 123.17/15.93 fof(f205,plain,(
% 123.17/15.93 ![X0]: (~singleton(X0)=empty_set)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f37])).
% 123.17/15.93 fof(f230,plain,(
% 123.17/15.93 (?[A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))<~>(in(A,C)&in(B,D))))),
% 123.17/15.93 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 123.17/15.93 fof(f231,plain,(
% 123.17/15.93 ?[A,B,C,D]: ((in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(~in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f230])).
% 123.17/15.93 fof(f232,plain,(
% 123.17/15.93 ((in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|(in(sK16_skl,sK18_skl)&in(sK17_skl,sK19_skl)))&(~in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|(~in(sK16_skl,sK18_skl)|~in(sK17_skl,sK19_skl))))),
% 123.17/15.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(A,sK16_skl),skolemize(B,sK17_skl),skolemize(C,sK18_skl),skolemize(D,sK19_skl)],[f231])).
% 123.17/15.93 fof(f233,plain,(
% 123.17/15.93 in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|in(sK16_skl,sK18_skl)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f232])).
% 123.17/15.93 fof(f234,plain,(
% 123.17/15.93 in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|in(sK17_skl,sK19_skl)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f232])).
% 123.17/15.93 fof(f235,plain,(
% 123.17/15.93 ~in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|~in(sK16_skl,sK18_skl)|~in(sK17_skl,sK19_skl)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f232])).
% 123.17/15.93 fof(f252,plain,(
% 123.17/15.93 ![X0]: (set_union2(X0,empty_set)=X0)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f56])).
% 123.17/15.93 fof(f256,plain,(
% 123.17/15.93 powerset(empty_set)=singleton(empty_set)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f58])).
% 123.17/15.93 fof(f262,plain,(
% 123.17/15.93 ![X0]: (set_intersection2(X0,empty_set)=empty_set)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f61])).
% 123.17/15.93 fof(f268,plain,(
% 123.17/15.93 ![X0]: (subset(empty_set,X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f63])).
% 123.17/15.93 fof(f272,plain,(
% 123.17/15.93 ![A,B,C,D]: (~ordered_pair(A,B)=ordered_pair(C,D)|(A=C&B=D))),
% 123.17/15.93 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 123.17/15.93 fof(f273,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~ordered_pair(X0,X1)=ordered_pair(X2,X3)|X0=X2)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f272])).
% 123.17/15.93 fof(f274,plain,(
% 123.17/15.93 ![X0,X1,X2,X3]: (~ordered_pair(X0,X1)=ordered_pair(X2,X3)|X1=X3)),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f272])).
% 123.17/15.93 fof(f310,plain,(
% 123.17/15.93 ![A,B]: (~in(A,B)|~empty(B))),
% 123.17/15.93 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 123.17/15.93 fof(f311,plain,(
% 123.17/15.93 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f310])).
% 123.17/15.93 fof(f312,plain,(
% 123.17/15.93 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f311])).
% 123.17/15.93 fof(f329,plain,(
% 123.17/15.93 ![A,B,D,E,F]: ((~sP0_prd(F,E,D,B,A)|((in(E,A)&in(F,B))&D=ordered_pair(E,F)))&(sP0_prd(F,E,D,B,A)|((~in(E,A)|~in(F,B))|~D=ordered_pair(E,F))))),
% 123.17/15.93 inference(NNF_transformation,[status(thm)],[f138])).
% 123.17/15.93 fof(f330,plain,(
% 123.17/15.93 (![A,B,D,E,F]: (~sP0_prd(F,E,D,B,A)|((in(E,A)&in(F,B))&D=ordered_pair(E,F))))&(![A,B,D,E,F]: (sP0_prd(F,E,D,B,A)|((~in(E,A)|~in(F,B))|~D=ordered_pair(E,F))))),
% 123.17/15.93 inference(miniscoping,[status(thm)],[f329])).
% 123.17/15.93 fof(f331,plain,(
% 123.17/15.93 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|in(X1,X4))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f330])).
% 123.17/15.93 fof(f332,plain,(
% 123.17/15.93 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|in(X0,X3))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f330])).
% 123.17/15.93 fof(f333,plain,(
% 123.17/15.93 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=ordered_pair(X1,X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f330])).
% 123.17/15.93 fof(f334,plain,(
% 123.17/15.93 ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2,X3,X4)|~in(X1,X4)|~in(X0,X3)|~X2=ordered_pair(X1,X0))),
% 123.17/15.93 inference(cnf_transformation,[status(thm)],[f330])).
% 123.17/15.93 fof(f335,definition,(
% 123.17/15.93 sQ0_spl <=> (in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)))),
% 123.17/15.93 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 123.17/15.93 fof(f336,plain,(
% 123.17/15.93 in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|~sQ0_spl),
% 123.17/15.93 inference(component_clause,[status(thm)],[f335])).
% 123.17/15.93 fof(f337,plain,(
% 123.17/15.93 ~in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl))|sQ0_spl),
% 123.17/15.93 inference(component_clause,[status(thm)],[f335])).
% 123.17/15.93 fof(f338,definition,(
% 123.17/15.93 sQ1_spl <=> (in(sK16_skl,sK18_skl))),
% 123.17/15.93 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 123.17/15.93 fof(f341,plain,(
% 123.17/15.93 sQ0_spl|sQ1_spl),
% 123.17/15.93 inference(split_clause,[status(thm)],[f233,f335,f338])).
% 123.17/15.93 fof(f342,definition,(
% 123.17/15.93 sQ2_spl <=> (in(sK17_skl,sK19_skl))),
% 123.17/15.93 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 123.17/15.93 fof(f345,plain,(
% 123.17/15.93 sQ0_spl|sQ2_spl),
% 123.17/15.93 inference(split_clause,[status(thm)],[f234,f335,f342])).
% 123.17/15.93 fof(f346,plain,(
% 123.17/15.93 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 123.17/15.93 inference(split_clause,[status(thm)],[f235,f335,f338,f342])).
% 123.17/15.93 fof(f351,plain,(
% 123.17/15.93 ![X0]: (~in(X0,empty_set))),
% 123.17/15.93 inference(destructive_equality_resolution,[status(thm)],[f111])).
% 123.17/15.93 fof(f352,plain,(
% 123.17/15.93 ![X0,X1]: (~in(X0,powerset(X1))|subset(X0,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f116])).
% 123.17/15.94 fof(f353,plain,(
% 123.17/15.94 ![X0,X1]: (in(X0,powerset(X1))|~subset(X0,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f117])).
% 123.17/15.94 fof(f355,plain,(
% 123.17/15.94 ![X0,X1]: (in(X0,unordered_pair(X0,X1)))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 123.17/15.94 fof(f356,plain,(
% 123.17/15.94 ![X0,X1]: (in(X0,unordered_pair(X1,X0)))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f125])).
% 123.17/15.94 fof(f357,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(X0,set_union2(X1,X2))|in(X0,X1)|in(X0,X2))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f132])).
% 123.17/15.94 fof(f358,plain,(
% 123.17/15.94 ![X0,X1,X2]: (in(X0,set_union2(X1,X2))|~in(X0,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f133])).
% 123.17/15.94 fof(f360,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(X0,cartesian_product2(X1,X2))|sP0_prd(sK6_skl(X0,cartesian_product2(X1,X2),X2,X1),sK5_skl(X0,cartesian_product2(X1,X2),X2,X1),X0,X2,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 123.17/15.94 fof(f361,plain,(
% 123.17/15.94 ![X0,X1,X2,X3,X4]: (in(X0,cartesian_product2(X1,X2))|~sP0_prd(X3,X4,X0,X2,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f144])).
% 123.17/15.94 fof(f362,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f157])).
% 123.17/15.94 fof(f363,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X2))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f158])).
% 123.17/15.94 fof(f366,plain,(
% 123.17/15.94 ![X0,X1]: (~in(X0,union(X1))|in(sK12_skl(X0,union(X1),X1),X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f167])).
% 123.17/15.94 fof(f367,plain,(
% 123.17/15.94 ![X0,X1,X2]: (in(X0,union(X1))|~in(X0,X2)|~in(X2,X1))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f168])).
% 123.17/15.94 fof(f369,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(X0,set_difference(X1,X2))|~in(X0,X2))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f176])).
% 123.17/15.94 fof(f374,plain,(
% 123.17/15.94 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,ordered_pair(X1,X0),X2,X3)|~in(X1,X3)|~in(X0,X2))),
% 123.17/15.94 inference(destructive_equality_resolution,[status(thm)],[f334])).
% 123.17/15.94 fof(f386,plain,(
% 123.17/15.94 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X1,X0),singleton(X0)))),
% 123.17/15.94 inference(paramodulation,[status(thm)],[f93,f181])).
% 123.17/15.94 fof(f612,plain,(
% 123.17/15.94 ![X0,X1]: (in(unordered_pair(X0,X1),ordered_pair(X1,X0)))),
% 123.17/15.94 inference(paramodulation,[status(thm)],[f386,f355])).
% 123.17/15.94 fof(f613,plain,(
% 123.17/15.94 ![X0,X1]: (in(unordered_pair(X0,X1),ordered_pair(X0,X1)))),
% 123.17/15.94 inference(paramodulation,[status(thm)],[f181,f355])).
% 123.17/15.94 fof(f616,plain,(
% 123.17/15.94 ![X0,X1]: (~in(unordered_pair(X0,X1),X1))),
% 123.17/15.94 inference(resolution,[status(thm)],[f356,f90])).
% 123.17/15.94 fof(f633,plain,(
% 123.17/15.94 ![X0]: (empty_set=singleton(X0)|sK0_skl(empty_set,X0)=X0)),
% 123.17/15.94 inference(resolution,[status(thm)],[f107,f351])).
% 123.17/15.94 fof(f635,plain,(
% 123.17/15.94 ![X0]: (sK0_skl(empty_set,X0)=X0)),
% 123.17/15.94 inference(forward_subsumption_resolution,[status(thm)],[f633,f205])).
% 123.17/15.94 fof(f697,plain,(
% 123.17/15.94 ![X0]: (in(empty_set,powerset(X0)))),
% 123.17/15.94 inference(resolution,[status(thm)],[f353,f268])).
% 123.17/15.94 fof(f925,plain,(
% 123.17/15.94 ![X0,X1]: (in(sK1_skl(set_union2(X0,X1)),X0)|in(sK1_skl(set_union2(X0,X1)),X1)|set_union2(X0,X1)=empty_set)),
% 123.17/15.94 inference(resolution,[status(thm)],[f357,f112])).
% 123.17/15.94 fof(f992,plain,(
% 123.17/15.94 ![X0,X1,X2,X3]: (~in(X0,X1)|~in(X2,X3)|in(ordered_pair(X0,X2),cartesian_product2(X1,X3)))),
% 123.17/15.94 inference(resolution,[status(thm)],[f374,f361])).
% 123.17/15.94 fof(f1027,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(sK0_skl(set_union2(X0,X1),X2),X0)|set_union2(X0,X1)=singleton(X2)|~sK0_skl(set_union2(X0,X1),X2)=X2)),
% 123.17/15.94 inference(resolution,[status(thm)],[f358,f106])).
% 123.17/15.94 fof(f1107,plain,(
% 123.17/15.94 ![X0,X1]: (empty_set=set_union2(X0,X1)|in(sK4_skl(empty_set,X1,X0),X0)|in(sK4_skl(empty_set,X1,X0),X1))),
% 123.17/15.94 inference(resolution,[status(thm)],[f137,f351])).
% 123.17/15.94 fof(f1124,plain,(
% 123.17/15.94 ![X0]: (X0=set_union2(empty_set,empty_set)|in(sK4_skl(X0,empty_set,empty_set),X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f137,f351])).
% 123.17/15.94 fof(f1140,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(X0,cartesian_product2(X1,X2))|X0=ordered_pair(sK5_skl(X0,cartesian_product2(X1,X2),X2,X1),sK6_skl(X0,cartesian_product2(X1,X2),X2,X1)))),
% 123.17/15.94 inference(resolution,[status(thm)],[f360,f333])).
% 123.17/15.94 fof(f1554,plain,(
% 123.17/15.94 ![X0,X1]: (in(sK1_skl(set_intersection2(X0,X1)),X0)|set_intersection2(X0,X1)=empty_set)),
% 123.17/15.94 inference(resolution,[status(thm)],[f362,f112])).
% 123.17/15.94 fof(f1619,plain,(
% 123.17/15.94 ![X0,X1]: (in(sK1_skl(set_intersection2(X0,X1)),X1)|set_intersection2(X0,X1)=empty_set)),
% 123.17/15.94 inference(resolution,[status(thm)],[f363,f112])).
% 123.17/15.94 fof(f1817,plain,(
% 123.17/15.94 ![X0]: (empty_set=set_intersection2(empty_set,X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f161,f351])).
% 123.17/15.94 fof(f1832,plain,(
% 123.17/15.94 ![X0,X1]: (X0=set_intersection2(empty_set,X1)|in(sK11_skl(X0,X1,empty_set),X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f161,f351])).
% 123.17/15.94 fof(f1870,plain,(
% 123.17/15.94 ![X0,X1]: (X0=set_intersection2(X1,empty_set)|in(sK11_skl(X0,empty_set,X1),X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f162,f351])).
% 123.17/15.94 fof(f1886,plain,(
% 123.17/15.94 ![X0]: (~in(X0,union(empty_set)))),
% 123.17/15.94 inference(resolution,[status(thm)],[f366,f351])).
% 123.17/15.94 fof(f1900,plain,(
% 123.17/15.94 ![X0,X1,X2]: (~in(unordered_pair(X0,union(X1)),X2)|~in(X2,X1))),
% 123.17/15.94 inference(resolution,[status(thm)],[f367,f616])).
% 123.17/15.94 fof(f3059,definition,(
% 123.17/15.94 sQ4_spl <=> (empty(singleton(ordered_pair(sK16_skl,sK17_skl))))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f3060,plain,(
% 123.17/15.94 empty(singleton(ordered_pair(sK16_skl,sK17_skl)))|~sQ4_spl),
% 123.17/15.94 inference(component_clause,[status(thm)],[f3059])).
% 123.17/15.94 fof(f3183,definition,(
% 123.17/15.94 sQ8_spl <=> (singleton(ordered_pair(sK16_skl,sK17_skl))=empty_set)),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f3184,plain,(
% 123.17/15.94 singleton(ordered_pair(sK16_skl,sK17_skl))=empty_set|~sQ8_spl),
% 123.17/15.94 inference(component_clause,[status(thm)],[f3183])).
% 123.17/15.94 fof(f3216,plain,(
% 123.17/15.94 ~in(sK16_skl,sK18_skl)|~in(sK17_skl,sK19_skl)|sQ0_spl),
% 123.17/15.94 inference(resolution,[status(thm)],[f337,f992])).
% 123.17/15.94 fof(f3217,plain,(
% 123.17/15.94 ~sQ1_spl|~sQ2_spl|sQ0_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f3216,f338,f342,f335])).
% 123.17/15.94 fof(f3423,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|~sQ4_spl)),
% 123.17/15.94 inference(resolution,[status(thm)],[f3060,f312])).
% 123.17/15.94 fof(f3449,plain,(
% 123.17/15.94 singleton(ordered_pair(sK16_skl,sK17_skl))=empty_set|~sQ4_spl),
% 123.17/15.94 inference(resolution,[status(thm)],[f3423,f112])).
% 123.17/15.94 fof(f3452,plain,(
% 123.17/15.94 $false|~sQ4_spl),
% 123.17/15.94 inference(forward_subsumption_resolution,[status(thm)],[f3449,f205])).
% 123.17/15.94 fof(f3453,plain,(
% 123.17/15.94 ~sQ4_spl),
% 123.17/15.94 inference(contradiction_clause,[status(thm)],[f3452])).
% 123.17/15.94 fof(f3940,plain,(
% 123.17/15.94 ![X0]: (empty(empty_set)|~empty(X0))),
% 123.17/15.94 inference(paramodulation,[status(thm)],[f252,f198])).
% 123.17/15.94 fof(f3949,definition,(
% 123.17/15.94 ![X0]: (sQ13_spl <=> (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f3950,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|~sQ13_spl)),
% 123.17/15.94 inference(component_clause,[status(thm)],[f3949])).
% 123.17/15.94 fof(f3956,definition,(
% 123.17/15.94 sQ15_spl <=> (empty(empty_set))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f3959,definition,(
% 123.17/15.94 ![X0]: (sQ16_spl <=> (~empty(X0)))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f3960,plain,(
% 123.17/15.94 ![X0]: (~empty(X0)|~sQ16_spl)),
% 123.17/15.94 inference(component_clause,[status(thm)],[f3959])).
% 123.17/15.94 fof(f3962,plain,(
% 123.17/15.94 sQ15_spl|sQ16_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f3940,f3956,f3959])).
% 123.17/15.94 fof(f3995,plain,(
% 123.17/15.94 singleton(ordered_pair(sK16_skl,sK17_skl))=empty_set|~sQ13_spl),
% 123.17/15.94 inference(resolution,[status(thm)],[f3950,f112])).
% 123.17/15.94 fof(f3998,plain,(
% 123.17/15.94 $false|~sQ13_spl),
% 123.17/15.94 inference(forward_subsumption_resolution,[status(thm)],[f3995,f205])).
% 123.17/15.94 fof(f3999,plain,(
% 123.17/15.94 ~sQ13_spl),
% 123.17/15.94 inference(contradiction_clause,[status(thm)],[f3998])).
% 123.17/15.94 fof(f4115,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(empty_set))|subset(X0,empty_set))),
% 123.17/15.94 inference(paramodulation,[status(thm)],[f256,f352])).
% 123.17/15.94 fof(f4213,plain,(
% 123.17/15.94 subset(sK1_skl(singleton(empty_set)),empty_set)|singleton(empty_set)=empty_set),
% 123.17/15.94 inference(resolution,[status(thm)],[f4115,f112])).
% 123.17/15.94 fof(f4225,definition,(
% 123.17/15.94 sQ19_spl <=> (subset(sK1_skl(singleton(empty_set)),empty_set))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f4228,definition,(
% 123.17/15.94 sQ20_spl <=> (singleton(empty_set)=empty_set)),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f4229,plain,(
% 123.17/15.94 singleton(empty_set)=empty_set|~sQ20_spl),
% 123.17/15.94 inference(component_clause,[status(thm)],[f4228])).
% 123.17/15.94 fof(f4231,plain,(
% 123.17/15.94 sQ19_spl|sQ20_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f4213,f4225,f4228])).
% 123.17/15.94 fof(f6053,plain,(
% 123.17/15.94 ![X0,X1,X2]: (in(sK8_skl(X0,X1,X2),X2)|X0=cartesian_product2(X2,X1)|in(sK7_skl(X0,X1,X2),X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f331,f146])).
% 123.17/15.94 fof(f6055,plain,(
% 123.17/15.94 ![X0,X1,X2,X3]: (in(X0,X1)|~in(X0,X1)|~in(X2,X3))),
% 123.17/15.94 inference(resolution,[status(thm)],[f331,f374])).
% 123.17/15.94 fof(f6056,definition,(
% 123.17/15.94 ![X0,X1]: (sQ39_spl <=> (in(X0,X1)|~in(X0,X1)))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f6059,definition,(
% 123.17/15.94 ![X2,X3]: (sQ40_spl <=> (~in(X2,X3)))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f6060,plain,(
% 123.17/15.94 ![X0,X1]: (~in(X0,X1)|~sQ40_spl)),
% 123.17/15.94 inference(component_clause,[status(thm)],[f6059])).
% 123.17/15.94 fof(f6062,plain,(
% 123.17/15.94 sQ39_spl|sQ40_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f6055,f6056,f6059])).
% 123.17/15.94 fof(f8793,plain,(
% 123.17/15.94 set_union2(singleton(empty_set),singleton(empty_set))=empty_set|subset(sK1_skl(set_union2(singleton(empty_set),singleton(empty_set))),empty_set)),
% 123.17/15.94 inference(resolution,[status(thm)],[f925,f4115])).
% 123.17/15.94 fof(f8894,definition,(
% 123.17/15.94 sQ52_spl <=> (set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),singleton(ordered_pair(sK16_skl,sK17_skl)))=empty_set)),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f8895,plain,(
% 123.17/15.94 set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),singleton(ordered_pair(sK16_skl,sK17_skl)))=empty_set|~sQ52_spl),
% 123.17/15.94 inference(component_clause,[status(thm)],[f8894])).
% 123.17/15.94 fof(f8901,definition,(
% 123.17/15.94 sQ54_spl <=> (set_union2(singleton(empty_set),singleton(empty_set))=empty_set)),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f8902,plain,(
% 123.17/15.94 set_union2(singleton(empty_set),singleton(empty_set))=empty_set|~sQ54_spl),
% 123.17/15.94 inference(component_clause,[status(thm)],[f8901])).
% 123.17/15.94 fof(f8904,definition,(
% 123.17/15.94 sQ55_spl <=> (subset(sK1_skl(set_union2(singleton(empty_set),singleton(empty_set))),empty_set))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f8907,plain,(
% 123.17/15.94 sQ54_spl|sQ55_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f8793,f8901,f8904])).
% 123.17/15.94 fof(f8939,definition,(
% 123.17/15.94 sQ61_spl <=> (set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl))=empty_set)),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f8940,plain,(
% 123.17/15.94 set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl))=empty_set|~sQ61_spl),
% 123.17/15.94 inference(component_clause,[status(thm)],[f8939])).
% 123.17/15.94 fof(f8967,plain,(
% 123.17/15.94 singleton(ordered_pair(sK16_skl,sK17_skl))=empty_set|~sQ52_spl),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f200,f8895])).
% 123.17/15.94 fof(f8968,plain,(
% 123.17/15.94 $false|~sQ52_spl),
% 123.17/15.94 inference(forward_subsumption_resolution,[status(thm)],[f8967,f205])).
% 123.17/15.94 fof(f8969,plain,(
% 123.17/15.94 ~sQ52_spl),
% 123.17/15.94 inference(contradiction_clause,[status(thm)],[f8968])).
% 123.17/15.94 fof(f8970,plain,(
% 123.17/15.94 singleton(empty_set)=empty_set|~sQ54_spl),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f200,f8902])).
% 123.17/15.94 fof(f8971,plain,(
% 123.17/15.94 $false|~sQ54_spl),
% 123.17/15.94 inference(forward_subsumption_resolution,[status(thm)],[f8970,f205])).
% 123.17/15.94 fof(f8972,plain,(
% 123.17/15.94 ~sQ54_spl),
% 123.17/15.94 inference(contradiction_clause,[status(thm)],[f8971])).
% 123.17/15.94 fof(f10221,plain,(
% 123.17/15.94 ![X0,X1]: (X0=cartesian_product2(empty_set,X1)|in(sK7_skl(X0,X1,empty_set),X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f6053,f351])).
% 123.17/15.94 fof(f10248,plain,(
% 123.17/15.94 ![X0,X1]: (in(sK8_skl(empty_set,X0,X1),X1)|empty_set=cartesian_product2(X1,X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f6053,f351])).
% 123.17/15.94 fof(f11259,plain,(
% 123.17/15.94 ![X0]: (~in(sK0_skl(empty_set,X0),singleton(ordered_pair(sK16_skl,sK17_skl)))|set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl))=singleton(X0)|~sK0_skl(set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl)),X0)=X0|~sQ61_spl)),
% 123.17/15.94 inference(paramodulation,[status(thm)],[f8940,f1027])).
% 123.17/15.94 fof(f11340,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl))=singleton(X0)|~sK0_skl(set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl)),X0)=X0|~sQ61_spl)),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f635,f11259])).
% 123.17/15.94 fof(f11341,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|empty_set=singleton(X0)|~sK0_skl(set_union2(singleton(ordered_pair(sK16_skl,sK17_skl)),cartesian_product2(sK18_skl,sK19_skl)),X0)=X0|~sQ61_spl)),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f8940,f11340])).
% 123.17/15.94 fof(f11342,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|empty_set=singleton(X0)|~sK0_skl(empty_set,X0)=X0|~sQ61_spl)),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f8940,f11341])).
% 123.17/15.94 fof(f11343,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|empty_set=singleton(X0)|~X0=X0|~sQ61_spl)),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f635,f11342])).
% 123.17/15.94 fof(f11344,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|empty_set=singleton(X0)|~sQ61_spl)),
% 123.17/15.94 inference(trivial_equality_resolution,[status(thm)],[f11343])).
% 123.17/15.94 fof(f11345,plain,(
% 123.17/15.94 ![X0]: (~in(X0,singleton(ordered_pair(sK16_skl,sK17_skl)))|~sQ61_spl)),
% 123.17/15.94 inference(forward_subsumption_resolution,[status(thm)],[f11344,f205])).
% 123.17/15.94 fof(f11587,plain,(
% 123.17/15.94 ![X0]: (empty_set=cartesian_product2(empty_set,X0))),
% 123.17/15.94 inference(resolution,[status(thm)],[f10221,f351])).
% 123.17/15.94 fof(f12287,plain,(
% 123.17/15.94 empty_set=set_union2(singleton(empty_set),singleton(empty_set))|subset(sK4_skl(empty_set,singleton(empty_set),singleton(empty_set)),empty_set)),
% 123.17/15.94 inference(resolution,[status(thm)],[f1107,f4115])).
% 123.17/15.94 fof(f12376,definition,(
% 123.17/15.94 sQ73_spl <=> (subset(sK4_skl(empty_set,singleton(empty_set),singleton(empty_set)),empty_set))),
% 123.17/15.94 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 123.17/15.94 fof(f12379,plain,(
% 123.17/15.94 sQ54_spl|sQ73_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f12287,f8901,f12376])).
% 123.17/15.94 fof(f14561,plain,(
% 123.17/15.94 sQ13_spl|~sQ61_spl),
% 123.17/15.94 inference(split_clause,[status(thm)],[f11345,f3949,f8939])).
% 123.17/15.94 fof(f14640,plain,(
% 123.17/15.94 $false|~sQ16_spl),
% 123.17/15.94 inference(backward_subsumption_resolution,[status(thm)],[f191,f3960])).
% 123.17/15.94 fof(f14641,plain,(
% 123.17/15.94 ~sQ16_spl),
% 123.17/15.94 inference(contradiction_clause,[status(thm)],[f14640])).
% 123.17/15.94 fof(f15143,plain,(
% 123.17/15.94 ![X0]: (X0=empty_set|in(sK4_skl(X0,empty_set,empty_set),X0))),
% 123.17/15.94 inference(forward_demodulation,[status(thm)],[f252,f1124])).
% 123.17/15.94 fof(f15165,plain,(
% 123.17/15.94 singleton(empty_set)=empty_set|subset(sK4_skl(singleton(empty_set),empty_set,empty_set),empty_set)),
% 123.17/15.94 inference(resolution,[status(thm)],[f15143,f4115])).
% 123.17/15.94 fof(f15192,definition,(
% 123.17/15.94 sQ104_spl <=> (subset(sK4_skl(singleton(empty_set),empty_set,empty_set),empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f15195,plain,(
% 123.17/15.95 sQ20_spl|sQ104_spl),
% 123.17/15.95 inference(split_clause,[status(thm)],[f15165,f4228,f15192])).
% 123.17/15.95 fof(f15200,plain,(
% 123.17/15.95 $false|~sQ8_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f3184,f205])).
% 123.17/15.95 fof(f15201,plain,(
% 123.17/15.95 ~sQ8_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f15200])).
% 123.17/15.95 fof(f15202,plain,(
% 123.17/15.95 $false|~sQ20_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f4229,f205])).
% 123.17/15.95 fof(f15203,plain,(
% 123.17/15.95 ~sQ20_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f15202])).
% 123.17/15.95 fof(f17044,definition,(
% 123.17/15.95 sQ143_spl <=> (in(ordered_pair(sK16_skl,sK17_skl),empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f17045,plain,(
% 123.17/15.95 in(ordered_pair(sK16_skl,sK17_skl),empty_set)|~sQ143_spl),
% 123.17/15.95 inference(component_clause,[status(thm)],[f17044])).
% 123.17/15.95 fof(f17073,plain,(
% 123.17/15.95 $false|~sQ143_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f17045,f351])).
% 123.17/15.95 fof(f17074,plain,(
% 123.17/15.95 ~sQ143_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f17073])).
% 123.17/15.95 fof(f17883,plain,(
% 123.17/15.95 ordered_pair(sK16_skl,sK17_skl)=ordered_pair(sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl))|~sQ0_spl),
% 123.17/15.95 inference(resolution,[status(thm)],[f1140,f336])).
% 123.17/15.95 fof(f18049,definition,(
% 123.17/15.95 sQ159_spl <=> (in(sK4_skl(singleton(ordered_pair(sK16_skl,sK17_skl)),empty_set,cartesian_product2(sK18_skl,sK19_skl)),empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f18050,plain,(
% 123.17/15.95 in(sK4_skl(singleton(ordered_pair(sK16_skl,sK17_skl)),empty_set,cartesian_product2(sK18_skl,sK19_skl)),empty_set)|~sQ159_spl),
% 123.17/15.95 inference(component_clause,[status(thm)],[f18049])).
% 123.17/15.95 fof(f18053,plain,(
% 123.17/15.95 $false|~sQ159_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f18050,f351])).
% 123.17/15.95 fof(f18054,plain,(
% 123.17/15.95 ~sQ159_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f18053])).
% 123.17/15.95 fof(f18090,plain,(
% 123.17/15.95 ![X0,X1]: (~in(ordered_pair(union(X0),X1),X0))),
% 123.17/15.95 inference(resolution,[status(thm)],[f1900,f612])).
% 123.17/15.95 fof(f18107,plain,(
% 123.17/15.95 ![X0,X1,X2]: (~in(union(cartesian_product2(X0,X1)),X0)|~in(X2,X1))),
% 123.17/15.95 inference(resolution,[status(thm)],[f18090,f992])).
% 123.17/15.95 fof(f18130,plain,(
% 123.17/15.95 ![X0,X1]: (~in(union(empty_set),empty_set)|~in(X0,X1))),
% 123.17/15.95 inference(paramodulation,[status(thm)],[f11587,f18107])).
% 123.17/15.95 fof(f18132,definition,(
% 123.17/15.95 sQ160_spl <=> (in(union(empty_set),empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f18135,plain,(
% 123.17/15.95 ~sQ160_spl|sQ40_spl),
% 123.17/15.95 inference(split_clause,[status(thm)],[f18130,f18132,f6059])).
% 123.17/15.95 fof(f18157,plain,(
% 123.17/15.95 $false|~sQ40_spl),
% 123.17/15.95 inference(backward_subsumption_resolution,[status(thm)],[f697,f6060])).
% 123.17/15.95 fof(f18230,plain,(
% 123.17/15.95 ~sQ40_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f18157])).
% 123.17/15.95 fof(f18421,plain,(
% 123.17/15.95 sP0_prd(sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/15.95 inference(resolution,[status(thm)],[f360,f336])).
% 123.17/15.95 fof(f21371,definition,(
% 123.17/15.95 sQ197_spl <=> (ordered_pair(sK16_skl,sK17_skl)=empty_set)),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f21372,plain,(
% 123.17/15.95 ordered_pair(sK16_skl,sK17_skl)=empty_set|~sQ197_spl),
% 123.17/15.95 inference(component_clause,[status(thm)],[f21371])).
% 123.17/15.95 fof(f21510,plain,(
% 123.17/15.95 in(unordered_pair(sK16_skl,sK17_skl),empty_set)|~sQ197_spl),
% 123.17/15.95 inference(paramodulation,[status(thm)],[f21372,f613])).
% 123.17/15.95 fof(f25221,plain,(
% 123.17/15.95 ![X0]: (in(sK1_skl(empty_set),empty_set)|set_intersection2(X0,empty_set)=empty_set)),
% 123.17/15.95 inference(paramodulation,[status(thm)],[f262,f1619])).
% 123.17/15.95 fof(f25225,definition,(
% 123.17/15.95 sQ199_spl <=> (in(sK1_skl(empty_set),empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f25226,plain,(
% 123.17/15.95 in(sK1_skl(empty_set),empty_set)|~sQ199_spl),
% 123.17/15.95 inference(component_clause,[status(thm)],[f25225])).
% 123.17/15.95 fof(f25228,definition,(
% 123.17/15.95 ![X0]: (sQ200_spl <=> (set_intersection2(X0,empty_set)=empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f25231,plain,(
% 123.17/15.95 sQ199_spl|sQ200_spl),
% 123.17/15.95 inference(split_clause,[status(thm)],[f25221,f25225,f25228])).
% 123.17/15.95 fof(f25233,plain,(
% 123.17/15.95 $false|~sQ199_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f25226,f351])).
% 123.17/15.95 fof(f25234,plain,(
% 123.17/15.95 ~sQ199_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f25233])).
% 123.17/15.95 fof(f28806,plain,(
% 123.17/15.95 ![X0]: (in(sK1_skl(empty_set),empty_set)|set_intersection2(empty_set,X0)=empty_set)),
% 123.17/15.95 inference(paramodulation,[status(thm)],[f1817,f1554])).
% 123.17/15.95 fof(f28934,definition,(
% 123.17/15.95 ![X0]: (sQ201_spl <=> (set_intersection2(empty_set,X0)=empty_set))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f28937,plain,(
% 123.17/15.95 sQ199_spl|sQ201_spl),
% 123.17/15.95 inference(split_clause,[status(thm)],[f28806,f25225,f28934])).
% 123.17/15.95 fof(f29250,plain,(
% 123.17/15.95 sK17_skl=sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/15.95 inference(resolution,[status(thm)],[f17883,f274])).
% 123.17/15.95 fof(f29251,plain,(
% 123.17/15.95 sK16_skl=sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/15.95 inference(resolution,[status(thm)],[f17883,f273])).
% 123.17/15.95 fof(f29256,plain,(
% 123.17/15.95 sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl)=sK17_skl|~sQ0_spl),
% 123.17/15.95 inference(resolution,[status(thm)],[f17883,f274])).
% 123.17/15.95 fof(f30698,plain,(
% 123.17/15.95 ![X0,X1]: (X0=empty_set|in(sK11_skl(X0,X1,empty_set),X0))),
% 123.17/15.95 inference(forward_demodulation,[status(thm)],[f1817,f1832])).
% 123.17/15.95 fof(f30718,plain,(
% 123.17/15.95 ![X0]: (singleton(empty_set)=empty_set|subset(sK11_skl(singleton(empty_set),X0,empty_set),empty_set))),
% 123.17/15.95 inference(resolution,[status(thm)],[f30698,f4115])).
% 123.17/15.95 fof(f30770,definition,(
% 123.17/15.95 ![X0]: (sQ221_spl <=> (subset(sK11_skl(singleton(empty_set),X0,empty_set),empty_set)))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f30773,plain,(
% 123.17/15.95 sQ20_spl|sQ221_spl),
% 123.17/15.95 inference(split_clause,[status(thm)],[f30718,f4228,f30770])).
% 123.17/15.95 fof(f30804,plain,(
% 123.17/15.95 $false|~sQ197_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f21510,f351])).
% 123.17/15.95 fof(f30805,plain,(
% 123.17/15.95 ~sQ197_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f30804])).
% 123.17/15.95 fof(f33731,plain,(
% 123.17/15.95 sP0_prd(sK17_skl,sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/15.95 inference(backward_demodulation,[status(thm)],[f29250,f18421])).
% 123.17/15.95 fof(f33733,plain,(
% 123.17/15.95 in(sK17_skl,sK19_skl)|~sQ0_spl),
% 123.17/15.95 inference(resolution,[status(thm)],[f33731,f332])).
% 123.17/15.95 fof(f33737,plain,(
% 123.17/15.95 ![X0]: (in(sK17_skl,set_union2(sK19_skl,X0))|~sQ0_spl)),
% 123.17/15.95 inference(resolution,[status(thm)],[f33733,f358])).
% 123.17/15.95 fof(f33751,plain,(
% 123.17/15.95 ![X0]: (in(sK17_skl,sK19_skl)|in(sK17_skl,X0)|~sQ0_spl)),
% 123.17/15.95 inference(resolution,[status(thm)],[f33737,f357])).
% 123.17/15.95 fof(f33772,definition,(
% 123.17/15.95 ![X0]: (sQ231_spl <=> (in(sK17_skl,X0)))),
% 123.17/15.95 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 123.17/15.95 fof(f33773,plain,(
% 123.17/15.95 ![X0]: (in(sK17_skl,X0)|~sQ231_spl)),
% 123.17/15.95 inference(component_clause,[status(thm)],[f33772])).
% 123.17/15.95 fof(f33775,plain,(
% 123.17/15.95 sQ2_spl|sQ231_spl|~sQ0_spl),
% 123.17/15.95 inference(split_clause,[status(thm)],[f33751,f342,f33772,f335])).
% 123.17/15.95 fof(f33807,plain,(
% 123.17/15.95 ![X0]: (~in(sK17_skl,X0)|~sQ231_spl)),
% 123.17/15.95 inference(resolution,[status(thm)],[f33773,f369])).
% 123.17/15.95 fof(f33867,plain,(
% 123.17/15.95 $false|~sQ231_spl),
% 123.17/15.95 inference(forward_subsumption_resolution,[status(thm)],[f33807,f33773])).
% 123.17/15.95 fof(f33868,plain,(
% 123.17/15.95 ~sQ231_spl),
% 123.17/15.95 inference(contradiction_clause,[status(thm)],[f33867])).
% 123.17/15.95 fof(f34187,plain,(
% 123.17/15.95 sP0_prd(sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/16.02 inference(resolution,[status(thm)],[f336,f360])).
% 123.17/16.02 fof(f36553,plain,(
% 123.17/16.02 ![X0,X1]: (X0=empty_set|in(sK11_skl(X0,empty_set,X1),X0))),
% 123.17/16.02 inference(forward_demodulation,[status(thm)],[f262,f1870])).
% 123.17/16.02 fof(f36573,plain,(
% 123.17/16.02 ![X0]: (singleton(empty_set)=empty_set|subset(sK11_skl(singleton(empty_set),empty_set,X0),empty_set))),
% 123.17/16.02 inference(resolution,[status(thm)],[f36553,f4115])).
% 123.17/16.02 fof(f36619,definition,(
% 123.17/16.02 ![X0]: (sQ251_spl <=> (subset(sK11_skl(singleton(empty_set),empty_set,X0),empty_set)))),
% 123.17/16.02 introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 123.17/16.02 fof(f36622,plain,(
% 123.17/16.02 sQ20_spl|sQ251_spl),
% 123.17/16.02 inference(split_clause,[status(thm)],[f36573,f4228,f36619])).
% 123.17/16.02 fof(f37833,plain,(
% 123.17/16.02 ![X0]: (empty_set=cartesian_product2(union(empty_set),X0))),
% 123.17/16.02 inference(resolution,[status(thm)],[f1886,f10248])).
% 123.17/16.02 fof(f38666,plain,(
% 123.17/16.02 ![X0,X1]: (~in(union(empty_set),union(empty_set))|~in(X0,X1))),
% 123.17/16.02 inference(paramodulation,[status(thm)],[f37833,f18107])).
% 123.17/16.02 fof(f38673,definition,(
% 123.17/16.02 sQ252_spl <=> (in(union(empty_set),union(empty_set)))),
% 123.17/16.02 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 123.17/16.02 fof(f38676,plain,(
% 123.17/16.02 ~sQ252_spl|sQ40_spl),
% 123.17/16.02 inference(split_clause,[status(thm)],[f38666,f38673,f6059])).
% 123.17/16.02 fof(f41353,plain,(
% 123.17/16.02 sP0_prd(sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),sK16_skl,ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/16.02 inference(backward_demodulation,[status(thm)],[f29251,f34187])).
% 123.17/16.02 fof(f41355,plain,(
% 123.17/16.02 sP0_prd(sK17_skl,sK16_skl,ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl)|~sQ0_spl),
% 123.17/16.02 inference(forward_demodulation,[status(thm)],[f29256,f41353])).
% 123.17/16.02 fof(f41356,plain,(
% 123.17/16.02 in(sK16_skl,sK18_skl)|~sQ0_spl),
% 123.17/16.02 inference(resolution,[status(thm)],[f41355,f331])).
% 123.17/16.02 fof(f41360,plain,(
% 123.17/16.02 sQ1_spl|~sQ0_spl),
% 123.17/16.02 inference(split_clause,[status(thm)],[f41356,f338,f335])).
% 123.17/16.02 fof(f41361,plain,(
% 123.17/16.02 $false),
% 123.17/16.02 inference(sat_refutation,[status(thm)],[f341,f345,f346,f3217,f3453,f3962,f3999,f4231,f6062,f8907,f8969,f8972,f12379,f14561,f14641,f15195,f15201,f15203,f17074,f18054,f18135,f18230,f25231,f25234,f28937,f30773,f30805,f33775,f33868,f36622,f38676,f41360])).
% 123.17/16.02 % SZS output end CNFRefutation for theBenchmark.p
% 46.60/16.06 % Elapsed time: 15.696797 seconds
% 46.60/16.06 % CPU time: 124.219313 seconds
% 46.60/16.06 % Total memory used: 1.215 GB
% 46.60/16.06 % Net memory used: 1.146 GB
%------------------------------------------------------------------------------