%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU290+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 : n008.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:22:14 PM UTC 2026
% Result : Theorem 235.16s 35.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU290+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.42 % Computer : n008.cluster.edu
% 0.14/5.42 % Model : x86_64 x86_64
% 0.14/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.42 % Memory : 8046.5625MB
% 0.14/5.42 % OS : Linux 6.8.0-71-generic
% 0.14/5.42 % CPULimit : 300
% 0.14/5.42 % WCLimit : 300
% 0.14/5.42 % DateTime : Mon Sep 21 06:09:02 UTC 2026
% 0.14/5.43 % CPUTime :
% 0.14/5.47 % Drodi V4.1.1
% 235.16/35.22 % Refutation found
% 235.16/35.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 235.16/35.22 % SZS output start CNFRefutation for theBenchmark
% 235.16/35.22 fof(f5,axiom,(
% 235.16/35.22 (! [A] :( empty(A)=> relation(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f6,axiom,(
% 235.16/35.22 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f12,axiom,(
% 235.16/35.22 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f27,axiom,(
% 235.16/35.22 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> ( ( ( B = empty_set=> A = empty_set )=> ( quasi_total(C,A,B)<=> A = relation_dom_as_subset(A,B,C) ) )& ( B = empty_set=> ( A = empty_set| ( quasi_total(C,A,B)<=> C = empty_set ) ) ) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f33,axiom,(
% 235.16/35.22 (! [A,B] :( ( A != empty_set=> ( B = set_meet(A)<=> (! [C] :( in(C,B)<=> (! [D] :( in(D,A)=> in(C,D) ) )) )) )& ( A = empty_set=> ( B = set_meet(A)<=> B = empty_set ) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f37,axiom,(
% 235.16/35.22 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f38,axiom,(
% 235.16/35.22 (! [A,B] :( B = powerset(A)<=> (! [C] :( in(C,B)<=> subset(C,A) ) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f42,axiom,(
% 235.16/35.22 (! [A,B] :( ( ~ empty(A)=> ( element(B,A)<=> in(B,A) ) )& ( empty(A)=> ( element(B,A)<=> empty(B) ) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f45,axiom,(
% 235.16/35.22 (! [A,B,C] :( C = set_union2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)| in(D,B) ) ) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f55,axiom,(
% 235.16/35.22 (! [A] :( relation(A)=> (! [B] :( is_antisymmetric_in(A,B)<=> (! [C,D] :( ( in(C,B)& in(D,B)& in(ordered_pair(C,D),A)& in(ordered_pair(D,C),A) )=> C = D ) )) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f60,axiom,(
% 235.16/35.22 (! [A,B,C] :( C = set_difference(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& ~ in(D,B) ) ) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f61,axiom,(
% 235.16/35.22 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] :( in(D,relation_dom(A))& C = apply(A,D) ) )) )) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f75,axiom,(
% 235.16/35.22 (! [A] :( relation(A)=> (! [B] :( is_transitive_in(A,B)<=> (! [C,D,E] :( ( in(C,B)& in(D,B)& in(E,B)& in(ordered_pair(C,D),A)& in(ordered_pair(D,E),A) )=> in(ordered_pair(C,E),A) ) )) )) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f111,axiom,(
% 235.16/35.22 (! [A] : relation(identity_relation(A)) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f120,axiom,(
% 235.16/35.22 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f122,axiom,(
% 235.16/35.22 (! [A] :(? [B] : element(B,A) ))),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f125,axiom,(
% 235.16/35.22 (! [A] :( empty(A)=> ( empty(relation_inverse(A))& relation(relation_inverse(A)) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f126,axiom,(
% 235.16/35.22 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f131,axiom,(
% 235.16/35.22 (! [A] : ~ empty(powerset(A)) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f134,axiom,(
% 235.16/35.22 (! [A] :( relation(identity_relation(A))& function(identity_relation(A)) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f135,axiom,(
% 235.16/35.22 ( relation(empty_set)& relation_empty_yielding(empty_set)& function(empty_set)& one_to_one(empty_set)& empty(empty_set)& epsilon_transitive(empty_set)& epsilon_connected(empty_set)& ordinal(empty_set) ) ),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f137,axiom,(
% 235.16/35.22 (! [A] : ~ empty(singleton(A)) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f152,axiom,(
% 235.16/35.22 (! [A] :( empty(A)=> ( empty(relation_rng(A))& relation(relation_rng(A)) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f161,lemma,(
% 235.16/35.22 (! [A] : singleton(A) != empty_set )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f181,axiom,(
% 235.16/35.22 (? [A] :( epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f182,axiom,(
% 235.16/35.22 (? [A] :( relation(A)& function(A)& one_to_one(A)& empty(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f183,axiom,(
% 235.16/35.22 (? [A] :( empty(A)& relation(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f186,axiom,(
% 235.16/35.22 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f187,axiom,(
% 235.16/35.22 (? [A] :( relation(A)& function(A)& one_to_one(A)& empty(A)& epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f189,axiom,(
% 235.16/35.22 (? [A] :( ~ empty(A)& relation(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f190,axiom,(
% 235.16/35.22 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f192,axiom,(
% 235.16/35.22 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f193,axiom,(
% 235.16/35.22 (? [A] :( ~ empty(A)& epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f195,axiom,(
% 235.16/35.22 (? [A] :( relation(A)& relation_empty_yielding(A)& function(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f238,lemma,(
% 235.16/35.22 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> ( subset(relation_dom(C),A)& subset(relation_rng(C),B) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f247,lemma,(
% 235.16/35.22 (! [A] :( relation(A)=> relation_image(A,relation_dom(A)) = relation_rng(A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f266,lemma,(
% 235.16/35.22 (! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_dom(C))& in(B,relation_rng(C)) ) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f273,lemma,(
% 235.16/35.22 (! [A,B,C] :( relation_of2_as_subset(C,B,A)=> ( (! [D] :~ ( in(D,B)& (! [E] : ~ in(ordered_pair(D,E),C) )))<=> relation_dom_as_subset(B,A,C) = B ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f288,axiom,(
% 235.16/35.22 (! [A] : set_intersection2(A,empty_set) = empty_set )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f292,lemma,(
% 235.16/35.22 (! [A] : subset(empty_set,A) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f305,lemma,(
% 235.16/35.22 (! [A,B] :( set_difference(A,B) = empty_set<=> subset(A,B) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f312,lemma,(
% 235.16/35.22 (! [A,B,C] :~ ( in(A,B)& in(B,C)& in(C,A) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f347,lemma,(
% 235.16/35.22 ( relation_dom(empty_set) = empty_set& relation_rng(empty_set) = empty_set ) ),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f356,axiom,(
% 235.16/35.22 (! [A] :( empty(A)=> A = empty_set ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f357,conjecture,(
% 235.16/35.22 (! [A,B,C,D] :( ( function(D)& quasi_total(D,A,B)& relation_of2_as_subset(D,A,B) )=> ( in(C,A)=> ( B = empty_set| in(apply(D,C),relation_rng(D)) ) ) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f358,negated_conjecture,(
% 235.16/35.22 ~((! [A,B,C,D] :( ( function(D)& quasi_total(D,A,B)& relation_of2_as_subset(D,A,B) )=> ( in(C,A)=> ( B = empty_set| in(apply(D,C),relation_rng(D)) ) ) ) ))),
% 235.16/35.22 inference(negated_conjecture,[status(cth)],[f357])).
% 235.16/35.22 fof(f365,axiom,(
% 235.16/35.22 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 235.16/35.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 235.16/35.22 fof(f394,plain,(
% 235.16/35.22 ![A]: (~empty(A)|relation(A))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 235.16/35.22 fof(f395,plain,(
% 235.16/35.22 ![X0]: (~empty(X0)|relation(X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f394])).
% 235.16/35.22 fof(f396,plain,(
% 235.16/35.22 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 235.16/35.22 fof(f397,plain,(
% 235.16/35.22 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f396])).
% 235.16/35.22 fof(f398,plain,(
% 235.16/35.22 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f397])).
% 235.16/35.22 fof(f411,plain,(
% 235.16/35.22 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f12])).
% 235.16/35.22 fof(f519,plain,(
% 235.16/35.22 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|(((B=empty_set&~A=empty_set)|(quasi_total(C,A,B)<=>A=relation_dom_as_subset(A,B,C)))&(~B=empty_set|(A=empty_set|(quasi_total(C,A,B)<=>C=empty_set)))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 235.16/35.22 fof(f520,definition,(
% 235.16/35.22 ![A,B]: (sP2_prd(B,A)<=>(B=empty_set&~A=empty_set))),
% 235.16/35.22 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 235.16/35.22 fof(f521,plain,(
% 235.16/35.22 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|((sP2_prd(B,A)|(quasi_total(C,A,B)<=>A=relation_dom_as_subset(A,B,C)))&(~B=empty_set|(A=empty_set|(quasi_total(C,A,B)<=>C=empty_set)))))),
% 235.16/35.22 inference(formula_renaming,[status(thm)],[f519,f520])).
% 235.16/35.22 fof(f522,plain,(
% 235.16/35.22 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|((sP2_prd(B,A)|((~quasi_total(C,A,B)|A=relation_dom_as_subset(A,B,C))&(quasi_total(C,A,B)|~A=relation_dom_as_subset(A,B,C))))&(~B=empty_set|(A=empty_set|((~quasi_total(C,A,B)|C=empty_set)&(quasi_total(C,A,B)|~C=empty_set))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f521])).
% 235.16/35.22 fof(f523,plain,(
% 235.16/35.22 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|sP2_prd(X2,X1)|~quasi_total(X0,X1,X2)|X1=relation_dom_as_subset(X1,X2,X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f522])).
% 235.16/35.22 fof(f553,plain,(
% 235.16/35.22 ![A,B]: ((A=empty_set|(B=set_meet(A)<=>(![C]: (in(C,B)<=>(![D]: (~in(D,A)|in(C,D)))))))&(~A=empty_set|(B=set_meet(A)<=>B=empty_set)))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 235.16/35.22 fof(f554,plain,(
% 235.16/35.22 ![A,B]: ((A=empty_set|((~B=set_meet(A)|(![C]: ((~in(C,B)|(![D]: (~in(D,A)|in(C,D))))&(in(C,B)|(?[D]: (in(D,A)&~in(C,D)))))))&(B=set_meet(A)|(?[C]: ((~in(C,B)|(?[D]: (in(D,A)&~in(C,D))))&(in(C,B)|(![D]: (~in(D,A)|in(C,D)))))))))&(~A=empty_set|((~B=set_meet(A)|B=empty_set)&(B=set_meet(A)|~B=empty_set))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f553])).
% 235.16/35.22 fof(f555,plain,(
% 235.16/35.22 (![A]: (A=empty_set|((![B]: (~B=set_meet(A)|((![C]: (~in(C,B)|(![D]: (~in(D,A)|in(C,D)))))&(![C]: (in(C,B)|(?[D]: (in(D,A)&~in(C,D))))))))&(![B]: (B=set_meet(A)|(?[C]: ((~in(C,B)|(?[D]: (in(D,A)&~in(C,D))))&(in(C,B)|(![D]: (~in(D,A)|in(C,D)))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f554])).
% 235.16/35.22 fof(f556,plain,(
% 235.16/35.22 (![A]: (A=empty_set|((![B]: (~B=set_meet(A)|((![C]: (~in(C,B)|(![D]: (~in(D,A)|in(C,D)))))&(![C]: (in(C,B)|(in(sK26_skl(C,B,A),A)&~in(C,sK26_skl(C,B,A))))))))&(![B]: (B=set_meet(A)|((~in(sK27_skl(B,A),B)|(in(sK28_skl(B,A),A)&~in(sK27_skl(B,A),sK28_skl(B,A))))&(in(sK27_skl(B,A),B)|(![D]: (~in(D,A)|in(sK27_skl(B,A),D))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl]),skolemize(D,sK26_skl(C,B,A)),skolemize(C,sK27_skl(B,A)),skolemize(D,sK28_skl(B,A))],[f555])).
% 235.16/35.22 fof(f563,plain,(
% 235.16/35.22 ![X0,X1]: (~X0=empty_set|~X1=set_meet(X0)|X1=empty_set)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f556])).
% 235.16/35.22 fof(f593,plain,(
% 235.16/35.22 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f37])).
% 235.16/35.22 fof(f594,plain,(
% 235.16/35.22 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f593])).
% 235.16/35.22 fof(f595,plain,(
% 235.16/35.22 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK33_skl(A),A)))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(B,sK33_skl(A))],[f594])).
% 235.16/35.22 fof(f596,plain,(
% 235.16/35.22 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f595])).
% 235.16/35.22 fof(f598,plain,(
% 235.16/35.22 ![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))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f38])).
% 235.16/35.22 fof(f599,plain,(
% 235.16/35.22 (![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))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f598])).
% 235.16/35.22 fof(f600,plain,(
% 235.16/35.22 (![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(sK34_skl(B,A),B)|~subset(sK34_skl(B,A),A))&(in(sK34_skl(B,A),B)|subset(sK34_skl(B,A),A)))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(C,sK34_skl(B,A))],[f599])).
% 235.16/35.22 fof(f601,plain,(
% 235.16/35.22 ![X0,X1,X2]: (~X0=powerset(X1)|~in(X2,X0)|subset(X2,X1))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f600])).
% 235.16/35.22 fof(f602,plain,(
% 235.16/35.22 ![X0,X1,X2]: (~X0=powerset(X1)|in(X2,X0)|~subset(X2,X1))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f600])).
% 235.16/35.22 fof(f627,plain,(
% 235.16/35.22 ![A,B]: ((empty(A)|(element(B,A)<=>in(B,A)))&(~empty(A)|(element(B,A)<=>empty(B))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 235.16/35.22 fof(f628,plain,(
% 235.16/35.22 ![A,B]: ((empty(A)|((~element(B,A)|in(B,A))&(element(B,A)|~in(B,A))))&(~empty(A)|((~element(B,A)|empty(B))&(element(B,A)|~empty(B)))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f627])).
% 235.16/35.22 fof(f629,plain,(
% 235.16/35.22 (![A]: (empty(A)|((![B]: (~element(B,A)|in(B,A)))&(![B]: (element(B,A)|~in(B,A))))))&(![A]: (~empty(A)|((![B]: (~element(B,A)|empty(B)))&(![B]: (element(B,A)|~empty(B))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f628])).
% 235.16/35.22 fof(f632,plain,(
% 235.16/35.22 ![X0,X1]: (~empty(X0)|~element(X1,X0)|empty(X1))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f629])).
% 235.16/35.22 fof(f651,plain,(
% 235.16/35.22 ![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)))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f45])).
% 235.16/35.22 fof(f652,plain,(
% 235.16/35.22 (![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)))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f651])).
% 235.16/35.22 fof(f653,plain,(
% 235.16/35.22 (![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(sK43_skl(C,B,A),C)|(~in(sK43_skl(C,B,A),A)&~in(sK43_skl(C,B,A),B)))&(in(sK43_skl(C,B,A),C)|(in(sK43_skl(C,B,A),A)|in(sK43_skl(C,B,A),B))))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl]),skolemize(D,sK43_skl(C,B,A))],[f652])).
% 235.16/35.22 fof(f655,plain,(
% 235.16/35.22 ![X0,X1,X2,X3]: (~X0=set_union2(X1,X2)|in(X3,X0)|~in(X3,X1))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f653])).
% 235.16/35.22 fof(f730,plain,(
% 235.16/35.22 ![A]: (~relation(A)|(![B]: (is_antisymmetric_in(A,B)<=>(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D)))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 235.16/35.22 fof(f731,plain,(
% 235.16/35.22 ![A]: (~relation(A)|(![B]: ((~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D)))&(is_antisymmetric_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,C),A))&~C=D))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f730])).
% 235.16/35.22 fof(f732,plain,(
% 235.16/35.22 ![A]: (~relation(A)|((![B]: (~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D))))&(![B]: (is_antisymmetric_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,C),A))&~C=D))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f731])).
% 235.16/35.22 fof(f733,plain,(
% 235.16/35.22 ![A]: (~relation(A)|((![B]: (~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D))))&(![B]: (is_antisymmetric_in(A,B)|((((in(sK60_skl(B,A),B)&in(sK61_skl(B,A),B))&in(ordered_pair(sK60_skl(B,A),sK61_skl(B,A)),A))&in(ordered_pair(sK61_skl(B,A),sK60_skl(B,A)),A))&~sK60_skl(B,A)=sK61_skl(B,A))))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK60_skl,sK61_skl]),skolemize(C,sK60_skl(B,A)),skolemize(D,sK61_skl(B,A))],[f732])).
% 235.16/35.22 fof(f737,plain,(
% 235.16/35.22 ![X0,X1]: (~relation(X0)|is_antisymmetric_in(X0,X1)|in(ordered_pair(sK60_skl(X1,X0),sK61_skl(X1,X0)),X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f733])).
% 235.16/35.22 fof(f767,plain,(
% 235.16/35.22 ![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)))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f60])).
% 235.16/35.22 fof(f768,plain,(
% 235.16/35.22 (![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)))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f767])).
% 235.16/35.22 fof(f769,plain,(
% 235.16/35.22 (![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(sK66_skl(C,B,A),C)|(~in(sK66_skl(C,B,A),A)|in(sK66_skl(C,B,A),B)))&(in(sK66_skl(C,B,A),C)|(in(sK66_skl(C,B,A),A)&~in(sK66_skl(C,B,A),B))))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK66_skl]),skolemize(D,sK66_skl(C,B,A))],[f768])).
% 235.16/35.22 fof(f771,plain,(
% 235.16/35.22 ![X0,X1,X2,X3]: (~X0=set_difference(X1,X2)|~in(X3,X0)|~in(X3,X2))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f769])).
% 235.16/35.22 fof(f772,plain,(
% 235.16/35.22 ![X0,X1,X2,X3]: (~X0=set_difference(X1,X2)|in(X3,X0)|~in(X3,X1)|in(X3,X2))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f769])).
% 235.16/35.22 fof(f776,plain,(
% 235.16/35.22 ![A]: ((~relation(A)|~function(A))|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 235.16/35.22 fof(f777,plain,(
% 235.16/35.22 ![A]: ((~relation(A)|~function(A))|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))&(in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D)))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))&(in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f776])).
% 235.16/35.22 fof(f778,plain,(
% 235.16/35.22 ![A]: ((~relation(A)|~function(A))|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D)))))&(![C]: (in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))&(in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f777])).
% 235.16/35.22 fof(f779,plain,(
% 235.16/35.22 ![A]: ((~relation(A)|~function(A))|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(in(sK67_skl(C,B,A),relation_dom(A))&C=apply(A,sK67_skl(C,B,A)))))&(![C]: (in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))))))&(![B]: (B=relation_rng(A)|((~in(sK68_skl(B,A),B)|(![D]: (~in(D,relation_dom(A))|~sK68_skl(B,A)=apply(A,D))))&(in(sK68_skl(B,A),B)|(in(sK69_skl(B,A),relation_dom(A))&sK68_skl(B,A)=apply(A,sK69_skl(B,A)))))))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl,sK68_skl,sK69_skl]),skolemize(D,sK67_skl(C,B,A)),skolemize(C,sK68_skl(B,A)),skolemize(D,sK69_skl(B,A))],[f778])).
% 235.16/35.22 fof(f782,plain,(
% 235.16/35.22 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(X3,relation_dom(X0))|~X2=apply(X0,X3))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f779])).
% 235.16/35.22 fof(f867,plain,(
% 235.16/35.22 ![A]: (~relation(A)|(![B]: (is_transitive_in(A,B)<=>(![C,D,E]: (((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A))|in(ordered_pair(C,E),A))))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 235.16/35.22 fof(f868,plain,(
% 235.16/35.22 ![A]: (~relation(A)|(![B]: ((~is_transitive_in(A,B)|(![C,D,E]: (((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A))|in(ordered_pair(C,E),A))))&(is_transitive_in(A,B)|(?[C,D,E]: (((((in(C,B)&in(D,B))&in(E,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,E),A))&~in(ordered_pair(C,E),A)))))))),
% 235.16/35.22 inference(NNF_transformation,[status(thm)],[f867])).
% 235.16/35.22 fof(f869,plain,(
% 235.16/35.22 ![A]: (~relation(A)|((![B]: (~is_transitive_in(A,B)|(![C,E]: ((![D]: ((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A)))|in(ordered_pair(C,E),A)))))&(![B]: (is_transitive_in(A,B)|(?[C,E]: ((?[D]: ((((in(C,B)&in(D,B))&in(E,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,E),A)))&~in(ordered_pair(C,E),A)))))))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f868])).
% 235.16/35.22 fof(f870,plain,(
% 235.16/35.22 ![A]: (~relation(A)|((![B]: (~is_transitive_in(A,B)|(![C,E]: ((![D]: ((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A)))|in(ordered_pair(C,E),A)))))&(![B]: (is_transitive_in(A,B)|(((((in(sK85_skl(B,A),B)&in(sK87_skl(B,A),B))&in(sK86_skl(B,A),B))&in(ordered_pair(sK85_skl(B,A),sK87_skl(B,A)),A))&in(ordered_pair(sK87_skl(B,A),sK86_skl(B,A)),A))&~in(ordered_pair(sK85_skl(B,A),sK86_skl(B,A)),A))))))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK85_skl,sK86_skl,sK87_skl]),skolemize(C,sK85_skl(B,A)),skolemize(E,sK86_skl(B,A)),skolemize(D,sK87_skl(B,A))],[f869])).
% 235.16/35.22 fof(f875,plain,(
% 235.16/35.22 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(ordered_pair(sK85_skl(X1,X0),sK87_skl(X1,X0)),X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f870])).
% 235.16/35.22 fof(f917,plain,(
% 235.16/35.22 ![X0]: (relation(identity_relation(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f111])).
% 235.16/35.22 fof(f930,plain,(
% 235.16/35.22 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 235.16/35.22 fof(f931,plain,(
% 235.16/35.22 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f930])).
% 235.16/35.22 fof(f934,plain,(
% 235.16/35.22 ![A]: element(sK90_skl(A),A)),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK90_skl]),skolemize(B,sK90_skl(A))],[f122])).
% 235.16/35.22 fof(f935,plain,(
% 235.16/35.22 ![X0]: (element(sK90_skl(X0),X0))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f934])).
% 235.16/35.22 fof(f941,plain,(
% 235.16/35.22 ![A]: (~empty(A)|(empty(relation_inverse(A))&relation(relation_inverse(A))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 235.16/35.22 fof(f942,plain,(
% 235.16/35.22 ![X0]: (~empty(X0)|empty(relation_inverse(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f941])).
% 235.16/35.22 fof(f943,plain,(
% 235.16/35.22 ![X0]: (~empty(X0)|relation(relation_inverse(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f941])).
% 235.16/35.22 fof(f944,plain,(
% 235.16/35.22 empty(empty_set)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f126])).
% 235.16/35.22 fof(f945,plain,(
% 235.16/35.22 relation(empty_set)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f126])).
% 235.16/35.22 fof(f957,plain,(
% 235.16/35.22 ![X0]: (~empty(powerset(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f131])).
% 235.16/35.22 fof(f960,plain,(
% 235.16/35.22 (![A]: relation(identity_relation(A)))&(![A]: function(identity_relation(A)))),
% 235.16/35.22 inference(miniscoping,[status(thm)],[f134])).
% 235.16/35.22 fof(f962,plain,(
% 235.16/35.22 ![X0]: (function(identity_relation(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f960])).
% 235.16/35.22 fof(f965,plain,(
% 235.16/35.22 function(empty_set)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f135])).
% 235.16/35.22 fof(f968,plain,(
% 235.16/35.22 epsilon_transitive(empty_set)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f135])).
% 235.16/35.22 fof(f973,plain,(
% 235.16/35.22 ![X0]: (~empty(singleton(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f137])).
% 235.16/35.22 fof(f1014,plain,(
% 235.16/35.22 ![A]: (~empty(A)|(empty(relation_rng(A))&relation(relation_rng(A))))),
% 235.16/35.22 inference(pre_NNF_transformation,[status(thm)],[f152])).
% 235.16/35.22 fof(f1015,plain,(
% 235.16/35.22 ![X0]: (~empty(X0)|empty(relation_rng(X0)))),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f1014])).
% 235.16/35.22 fof(f1038,plain,(
% 235.16/35.22 ![X0]: (~singleton(X0)=empty_set)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f161])).
% 235.16/35.22 fof(f1120,plain,(
% 235.16/35.22 ((epsilon_transitive(sK104_skl)&epsilon_connected(sK104_skl))&ordinal(sK104_skl))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK104_skl]),skolemize(A,sK104_skl)],[f181])).
% 235.16/35.22 fof(f1121,plain,(
% 235.16/35.22 epsilon_transitive(sK104_skl)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f1120])).
% 235.16/35.22 fof(f1124,plain,(
% 235.16/35.22 (((relation(sK105_skl)&function(sK105_skl))&one_to_one(sK105_skl))&empty(sK105_skl))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK105_skl]),skolemize(A,sK105_skl)],[f182])).
% 235.16/35.22 fof(f1128,plain,(
% 235.16/35.22 empty(sK105_skl)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f1124])).
% 235.16/35.22 fof(f1129,plain,(
% 235.16/35.22 (empty(sK106_skl)&relation(sK106_skl))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK106_skl]),skolemize(A,sK106_skl)],[f183])).
% 235.16/35.22 fof(f1130,plain,(
% 235.16/35.22 empty(sK106_skl)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f1129])).
% 235.16/35.22 fof(f1138,plain,(
% 235.16/35.22 ((relation(sK109_skl)&empty(sK109_skl))&function(sK109_skl))),
% 235.16/35.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK109_skl]),skolemize(A,sK109_skl)],[f186])).
% 235.16/35.22 fof(f1140,plain,(
% 235.16/35.22 empty(sK109_skl)),
% 235.16/35.22 inference(cnf_transformation,[status(thm)],[f1138])).
% 235.16/35.22 fof(f1142,plain,(
% 235.16/35.22 ((((((relation(sK110_skl)&function(sK110_skl))&one_to_one(sK110_skl))&empty(sK110_skl))&epsilon_transitive(sK110_skl))&epsilon_connected(sK110_skl))&ordinal(sK110_skl))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK110_skl]),skolemize(A,sK110_skl)],[f187])).
% 235.16/35.23 fof(f1146,plain,(
% 235.16/35.23 empty(sK110_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1142])).
% 235.16/35.23 fof(f1154,plain,(
% 235.16/35.23 (~empty(sK112_skl)&relation(sK112_skl))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK112_skl]),skolemize(A,sK112_skl)],[f189])).
% 235.16/35.23 fof(f1156,plain,(
% 235.16/35.23 relation(sK112_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1154])).
% 235.16/35.23 fof(f1157,plain,(
% 235.16/35.23 ![A]: (element(sK113_skl(A),powerset(A))&empty(sK113_skl(A)))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK113_skl]),skolemize(B,sK113_skl(A))],[f190])).
% 235.16/35.23 fof(f1159,plain,(
% 235.16/35.23 ![X0]: (empty(sK113_skl(X0)))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1157])).
% 235.16/35.23 fof(f1162,plain,(
% 235.16/35.23 ((relation(sK115_skl)&function(sK115_skl))&one_to_one(sK115_skl))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(A,sK115_skl)],[f192])).
% 235.16/35.23 fof(f1163,plain,(
% 235.16/35.23 relation(sK115_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1162])).
% 235.16/35.23 fof(f1166,plain,(
% 235.16/35.23 (((~empty(sK116_skl)&epsilon_transitive(sK116_skl))&epsilon_connected(sK116_skl))&ordinal(sK116_skl))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl]),skolemize(A,sK116_skl)],[f193])).
% 235.16/35.23 fof(f1168,plain,(
% 235.16/35.23 epsilon_transitive(sK116_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1166])).
% 235.16/35.23 fof(f1174,plain,(
% 235.16/35.23 ((relation(sK118_skl)&relation_empty_yielding(sK118_skl))&function(sK118_skl))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK118_skl]),skolemize(A,sK118_skl)],[f195])).
% 235.16/35.23 fof(f1175,plain,(
% 235.16/35.23 relation(sK118_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1174])).
% 235.16/35.23 fof(f1435,plain,(
% 235.16/35.23 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|(subset(relation_dom(C),A)&subset(relation_rng(C),B)))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f238])).
% 235.16/35.23 fof(f1437,plain,(
% 235.16/35.23 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|subset(relation_rng(X0),X2))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1435])).
% 235.16/35.23 fof(f1470,plain,(
% 235.16/35.23 ![A]: (~relation(A)|relation_image(A,relation_dom(A))=relation_rng(A))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f247])).
% 235.16/35.23 fof(f1471,plain,(
% 235.16/35.23 ![X0]: (~relation(X0)|relation_image(X0,relation_dom(X0))=relation_rng(X0))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1470])).
% 235.16/35.23 fof(f1526,plain,(
% 235.16/35.23 ![A,B,C]: (~relation(C)|(~in(ordered_pair(A,B),C)|(in(A,relation_dom(C))&in(B,relation_rng(C)))))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f266])).
% 235.16/35.23 fof(f1527,plain,(
% 235.16/35.23 ![C]: (~relation(C)|(![A,B]: (~in(ordered_pair(A,B),C)|(in(A,relation_dom(C))&in(B,relation_rng(C))))))),
% 235.16/35.23 inference(miniscoping,[status(thm)],[f1526])).
% 235.16/35.23 fof(f1528,plain,(
% 235.16/35.23 ![X0,X1,X2]: (~relation(X0)|~in(ordered_pair(X1,X2),X0)|in(X1,relation_dom(X0)))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1527])).
% 235.16/35.23 fof(f1550,plain,(
% 235.16/35.23 ![A,B,C]: (~relation_of2_as_subset(C,B,A)|((![D]: (~in(D,B)|(?[E]: in(ordered_pair(D,E),C))))<=>relation_dom_as_subset(B,A,C)=B))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f273])).
% 235.16/35.23 fof(f1551,plain,(
% 235.16/35.23 ![A,B,C]: (~relation_of2_as_subset(C,B,A)|(((?[D]: (in(D,B)&(![E]: ~in(ordered_pair(D,E),C))))|relation_dom_as_subset(B,A,C)=B)&((![D]: (~in(D,B)|(?[E]: in(ordered_pair(D,E),C))))|~relation_dom_as_subset(B,A,C)=B)))),
% 235.16/35.23 inference(NNF_transformation,[status(thm)],[f1550])).
% 235.16/35.23 fof(f1552,plain,(
% 235.16/35.23 ![A,B,C]: (~relation_of2_as_subset(C,B,A)|(((in(sK198_skl(C,B,A),B)&(![E]: ~in(ordered_pair(sK198_skl(C,B,A),E),C)))|relation_dom_as_subset(B,A,C)=B)&((![D]: (~in(D,B)|in(ordered_pair(D,sK199_skl(D,C,B,A)),C)))|~relation_dom_as_subset(B,A,C)=B)))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK198_skl,sK199_skl]),skolemize(D,sK198_skl(C,B,A)),skolemize(E,sK199_skl(D,C,B,A))],[f1551])).
% 235.16/35.23 fof(f1555,plain,(
% 235.16/35.23 ![X0,X1,X2,X3]: (~relation_of2_as_subset(X0,X1,X2)|~in(X3,X1)|in(ordered_pair(X3,sK199_skl(X3,X0,X1,X2)),X0)|~relation_dom_as_subset(X1,X2,X0)=X1)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1552])).
% 235.16/35.23 fof(f1605,plain,(
% 235.16/35.23 ![X0]: (set_intersection2(X0,empty_set)=empty_set)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f288])).
% 235.16/35.23 fof(f1614,plain,(
% 235.16/35.23 ![X0]: (subset(empty_set,X0))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f292])).
% 235.16/35.23 fof(f1659,plain,(
% 235.16/35.23 ![A,B]: ((~set_difference(A,B)=empty_set|subset(A,B))&(set_difference(A,B)=empty_set|~subset(A,B)))),
% 235.16/35.23 inference(NNF_transformation,[status(thm)],[f305])).
% 235.16/35.23 fof(f1660,plain,(
% 235.16/35.23 (![A,B]: (~set_difference(A,B)=empty_set|subset(A,B)))&(![A,B]: (set_difference(A,B)=empty_set|~subset(A,B)))),
% 235.16/35.23 inference(miniscoping,[status(thm)],[f1659])).
% 235.16/35.23 fof(f1662,plain,(
% 235.16/35.23 ![X0,X1]: (set_difference(X0,X1)=empty_set|~subset(X0,X1))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1660])).
% 235.16/35.23 fof(f1682,plain,(
% 235.16/35.23 ![A,B,C]: ((~in(A,B)|~in(B,C))|~in(C,A))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f312])).
% 235.16/35.23 fof(f1683,plain,(
% 235.16/35.23 ![A,C]: ((![B]: (~in(A,B)|~in(B,C)))|~in(C,A))),
% 235.16/35.23 inference(miniscoping,[status(thm)],[f1682])).
% 235.16/35.23 fof(f1684,plain,(
% 235.16/35.23 ![X0,X1,X2]: (~in(X0,X1)|~in(X1,X2)|~in(X2,X0))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1683])).
% 235.16/35.23 fof(f1791,plain,(
% 235.16/35.23 relation_dom(empty_set)=empty_set),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f347])).
% 235.16/35.23 fof(f1792,plain,(
% 235.16/35.23 relation_rng(empty_set)=empty_set),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f347])).
% 235.16/35.23 fof(f1820,plain,(
% 235.16/35.23 ![A]: (~empty(A)|A=empty_set)),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f356])).
% 235.16/35.23 fof(f1821,plain,(
% 235.16/35.23 ![X0]: (~empty(X0)|X0=empty_set)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1820])).
% 235.16/35.23 fof(f1822,plain,(
% 235.16/35.23 (?[A,B,C,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(in(C,A)&(~B=empty_set&~in(apply(D,C),relation_rng(D))))))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f358])).
% 235.16/35.23 fof(f1823,plain,(
% 235.16/35.23 ?[A,B,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(?[C]: (in(C,A)&(~B=empty_set&~in(apply(D,C),relation_rng(D))))))),
% 235.16/35.23 inference(miniscoping,[status(thm)],[f1822])).
% 235.16/35.23 fof(f1824,plain,(
% 235.16/35.23 (((function(sK222_skl)&quasi_total(sK222_skl,sK220_skl,sK221_skl))&relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl))&(in(sK223_skl,sK220_skl)&(~sK221_skl=empty_set&~in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl)))))),
% 235.16/35.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK220_skl,sK221_skl,sK222_skl,sK223_skl]),skolemize(A,sK220_skl),skolemize(B,sK221_skl),skolemize(D,sK222_skl),skolemize(C,sK223_skl)],[f1823])).
% 235.16/35.23 fof(f1825,plain,(
% 235.16/35.23 function(sK222_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1824])).
% 235.16/35.23 fof(f1826,plain,(
% 235.16/35.23 quasi_total(sK222_skl,sK220_skl,sK221_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1824])).
% 235.16/35.23 fof(f1827,plain,(
% 235.16/35.23 relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1824])).
% 235.16/35.23 fof(f1828,plain,(
% 235.16/35.23 in(sK223_skl,sK220_skl)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1824])).
% 235.16/35.23 fof(f1829,plain,(
% 235.16/35.23 ~sK221_skl=empty_set),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1824])).
% 235.16/35.23 fof(f1830,plain,(
% 235.16/35.23 ~in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1824])).
% 235.16/35.23 fof(f1850,plain,(
% 235.16/35.23 ![A,B]: (~in(A,B)|~empty(B))),
% 235.16/35.23 inference(pre_NNF_transformation,[status(thm)],[f365])).
% 235.16/35.23 fof(f1851,plain,(
% 235.16/35.23 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 235.16/35.23 inference(miniscoping,[status(thm)],[f1850])).
% 235.16/35.23 fof(f1852,plain,(
% 235.16/35.23 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1851])).
% 235.16/35.23 fof(f1930,plain,(
% 235.16/35.23 ![A,B]: ((~sP2_prd(B,A)|(B=empty_set&~A=empty_set))&(sP2_prd(B,A)|(~B=empty_set|A=empty_set)))),
% 235.16/35.23 inference(NNF_transformation,[status(thm)],[f520])).
% 235.16/35.23 fof(f1931,plain,(
% 235.16/35.23 (![A,B]: (~sP2_prd(B,A)|(B=empty_set&~A=empty_set)))&(![A,B]: (sP2_prd(B,A)|(~B=empty_set|A=empty_set)))),
% 235.16/35.23 inference(miniscoping,[status(thm)],[f1930])).
% 235.16/35.23 fof(f1932,plain,(
% 235.16/35.23 ![X0,X1]: (~sP2_prd(X0,X1)|X0=empty_set)),
% 235.16/35.23 inference(cnf_transformation,[status(thm)],[f1931])).
% 235.16/35.23 fof(f2173,plain,(
% 235.16/35.23 set_meet(empty_set)=empty_set),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f563])).
% 235.16/35.23 fof(f2187,plain,(
% 235.16/35.23 ![X0]: (~in(X0,empty_set))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f596])).
% 235.16/35.23 fof(f2188,plain,(
% 235.16/35.23 ![X0,X1]: (~in(X0,powerset(X1))|subset(X0,X1))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f601])).
% 235.16/35.23 fof(f2189,plain,(
% 235.16/35.23 ![X0,X1]: (in(X0,powerset(X1))|~subset(X0,X1))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f602])).
% 235.16/35.23 fof(f2197,plain,(
% 235.16/35.23 ![X0,X1,X2]: (in(X0,set_union2(X1,X2))|~in(X0,X1))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f655])).
% 235.16/35.23 fof(f2214,plain,(
% 235.16/35.23 ![X0,X1,X2]: (~in(X0,set_difference(X1,X2))|~in(X0,X2))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f771])).
% 235.16/35.23 fof(f2215,plain,(
% 235.16/35.23 ![X0,X1,X2]: (in(X0,set_difference(X1,X2))|~in(X0,X1)|in(X0,X2))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f772])).
% 235.16/35.23 fof(f2218,plain,(
% 235.16/35.23 ![X0,X1]: (~relation(X0)|~function(X0)|in(apply(X0,X1),relation_rng(X0))|~in(X1,relation_dom(X0)))),
% 235.16/35.23 inference(destructive_equality_resolution,[status(thm)],[f782])).
% 235.16/35.23 fof(f2368,definition,(
% 235.16/35.23 sQ18_spl <=> (function(relation_dom(sK105_skl)))),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f2370,plain,(
% 235.16/35.23 ~function(relation_dom(sK105_skl))|sQ18_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f2368])).
% 235.16/35.23 fof(f2475,plain,(
% 235.16/35.23 ~relation(sK222_skl)|~function(sK222_skl)|~in(sK223_skl,relation_dom(sK222_skl))),
% 235.16/35.23 inference(resolution,[status(thm)],[f2218,f1830])).
% 235.16/35.23 fof(f2478,definition,(
% 235.16/35.23 sQ37_spl <=> (relation(sK222_skl))),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f2480,plain,(
% 235.16/35.23 ~relation(sK222_skl)|sQ37_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f2478])).
% 235.16/35.23 fof(f2481,definition,(
% 235.16/35.23 sQ38_spl <=> (function(sK222_skl))),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f2483,plain,(
% 235.16/35.23 ~function(sK222_skl)|sQ38_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f2481])).
% 235.16/35.23 fof(f2484,definition,(
% 235.16/35.23 sQ39_spl <=> (in(sK223_skl,relation_dom(sK222_skl)))),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f2486,plain,(
% 235.16/35.23 ~in(sK223_skl,relation_dom(sK222_skl))|sQ39_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f2484])).
% 235.16/35.23 fof(f2487,plain,(
% 235.16/35.23 ~sQ37_spl|~sQ38_spl|~sQ39_spl),
% 235.16/35.23 inference(split_clause,[status(thm)],[f2475,f2478,f2481,f2484])).
% 235.16/35.23 fof(f2554,plain,(
% 235.16/35.23 $false|sQ38_spl),
% 235.16/35.23 inference(forward_subsumption_resolution,[status(thm)],[f2483,f1825])).
% 235.16/35.23 fof(f2555,plain,(
% 235.16/35.23 sQ38_spl),
% 235.16/35.23 inference(contradiction_clause,[status(thm)],[f2554])).
% 235.16/35.23 fof(f2570,plain,(
% 235.16/35.23 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|relation(X0))),
% 235.16/35.23 inference(resolution,[status(thm)],[f931,f398])).
% 235.16/35.23 fof(f2789,plain,(
% 235.16/35.23 ![X0]: (~in(X0,X0)|~in(X0,X0))),
% 235.16/35.23 inference(factoring,[status(thm)],[f1684])).
% 235.16/35.23 fof(f2825,plain,(
% 235.16/35.23 ![X0]: (~in(X0,X0))),
% 235.16/35.23 inference(duplicate_literals_removal,[status(thm)],[f2789])).
% 235.16/35.23 fof(f2987,definition,(
% 235.16/35.23 sQ120_spl <=> (relation_dom(sK110_skl)=empty_set)),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f2989,plain,(
% 235.16/35.23 ~relation_dom(sK110_skl)=empty_set|sQ120_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f2987])).
% 235.16/35.23 fof(f2994,definition,(
% 235.16/35.23 sQ122_spl <=> (relation_dom(sK109_skl)=empty_set)),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f2996,plain,(
% 235.16/35.23 ~relation_dom(sK109_skl)=empty_set|sQ122_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f2994])).
% 235.16/35.23 fof(f3001,definition,(
% 235.16/35.23 sQ124_spl <=> (relation_dom(sK106_skl)=empty_set)),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f3003,plain,(
% 235.16/35.23 ~relation_dom(sK106_skl)=empty_set|sQ124_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f3001])).
% 235.16/35.23 fof(f3008,definition,(
% 235.16/35.23 sQ126_spl <=> (relation_dom(sK105_skl)=empty_set)),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f3010,plain,(
% 235.16/35.23 ~relation_dom(sK105_skl)=empty_set|sQ126_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f3008])).
% 235.16/35.23 fof(f3060,definition,(
% 235.16/35.23 sQ136_spl <=> (relation_rng(sK110_skl)=empty_set)),
% 235.16/35.23 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 235.16/35.23 fof(f3062,plain,(
% 235.16/35.23 ~relation_rng(sK110_skl)=empty_set|sQ136_spl),
% 235.16/35.23 inference(component_clause,[status(thm)],[f3060])).
% 235.16/35.23 fof(f3244,plain,(
% 235.16/35.23 sK105_skl=empty_set),
% 235.16/35.23 inference(resolution,[status(thm)],[f1821,f1128])).
% 235.16/35.23 fof(f3245,plain,(
% 235.16/35.23 ![X0]: (relation_rng(X0)=empty_set|~empty(X0))),
% 235.16/35.23 inference(resolution,[status(thm)],[f1821,f1015])).
% 235.16/35.23 fof(f3282,plain,(
% 235.16/35.23 sK106_skl=empty_set),
% 235.16/35.23 inference(resolution,[status(thm)],[f1130,f1821])).
% 235.16/35.23 fof(f3285,plain,(
% 235.16/35.23 sK109_skl=empty_set),
% 235.16/35.23 inference(resolution,[status(thm)],[f1140,f1821])).
% 235.16/35.23 fof(f3305,plain,(
% 235.16/35.23 sK110_skl=empty_set),
% 235.16/35.23 inference(resolution,[status(thm)],[f1146,f1821])).
% 235.16/35.23 fof(f3577,plain,(
% 235.16/35.23 relation(sK222_skl)),
% 235.16/35.23 inference(resolution,[status(thm)],[f2570,f1827])).
% 235.16/35.23 fof(f3580,plain,(
% 235.16/35.23 $false|sQ37_spl),
% 235.16/35.23 inference(forward_subsumption_resolution,[status(thm)],[f3577,f2480])).
% 235.16/35.23 fof(f3581,plain,(
% 235.16/35.23 sQ37_spl),
% 235.16/35.23 inference(contradiction_clause,[status(thm)],[f3580])).
% 235.16/35.24 fof(f3757,plain,(
% 235.16/35.24 ![X0,X1,X2]: (in(relation_rng(X0),powerset(X1))|~relation_of2_as_subset(X0,X2,X1))),
% 235.16/35.24 inference(resolution,[status(thm)],[f2189,f1437])).
% 235.16/35.24 fof(f4208,definition,(
% 235.16/35.24 sQ214_spl <=> (relation(identity_relation(sK220_skl)))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f4210,plain,(
% 235.16/35.24 ~relation(identity_relation(sK220_skl))|sQ214_spl),
% 235.16/35.24 inference(component_clause,[status(thm)],[f4208])).
% 235.16/35.24 fof(f4211,definition,(
% 235.16/35.24 sQ215_spl <=> (function(identity_relation(sK220_skl)))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f4213,plain,(
% 235.16/35.24 ~function(identity_relation(sK220_skl))|sQ215_spl),
% 235.16/35.24 inference(component_clause,[status(thm)],[f4211])).
% 235.16/35.24 fof(f4253,plain,(
% 235.16/35.24 in(relation_rng(sK222_skl),powerset(sK221_skl))),
% 235.16/35.24 inference(resolution,[status(thm)],[f3757,f1827])).
% 235.16/35.24 fof(f4272,plain,(
% 235.16/35.24 subset(relation_rng(sK222_skl),sK221_skl)),
% 235.16/35.24 inference(resolution,[status(thm)],[f4253,f2188])).
% 235.16/35.24 fof(f4362,definition,(
% 235.16/35.24 sQ238_spl <=> (sK221_skl=empty_set)),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f4363,plain,(
% 235.16/35.24 sK221_skl=empty_set|~sQ238_spl),
% 235.16/35.24 inference(component_clause,[status(thm)],[f4362])).
% 235.16/35.24 fof(f4371,plain,(
% 235.16/35.24 $false|~sQ238_spl),
% 235.16/35.24 inference(forward_subsumption_resolution,[status(thm)],[f4363,f1829])).
% 235.16/35.24 fof(f4372,plain,(
% 235.16/35.24 ~sQ238_spl),
% 235.16/35.24 inference(contradiction_clause,[status(thm)],[f4371])).
% 235.16/35.24 fof(f4604,definition,(
% 235.16/35.24 sQ250_spl <=> (sP2_prd(sK221_skl,sK220_skl))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f4605,plain,(
% 235.16/35.24 sP2_prd(sK221_skl,sK220_skl)|~sQ250_spl),
% 235.16/35.24 inference(component_clause,[status(thm)],[f4604])).
% 235.16/35.24 fof(f4672,plain,(
% 235.16/35.24 ~relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl)|sP2_prd(sK221_skl,sK220_skl)|sK220_skl=relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl)),
% 235.16/35.24 inference(resolution,[status(thm)],[f1826,f523])).
% 235.16/35.24 fof(f4673,definition,(
% 235.16/35.24 sQ255_spl <=> (relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f4675,plain,(
% 235.16/35.24 ~relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl)|sQ255_spl),
% 235.16/35.24 inference(component_clause,[status(thm)],[f4673])).
% 235.16/35.24 fof(f4676,definition,(
% 235.16/35.24 sQ256_spl <=> (sK220_skl=relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f4679,plain,(
% 235.16/35.24 ~sQ255_spl|sQ250_spl|sQ256_spl),
% 235.16/35.24 inference(split_clause,[status(thm)],[f4672,f4673,f4604,f4676])).
% 235.16/35.24 fof(f4685,plain,(
% 235.16/35.24 $false|sQ255_spl),
% 235.16/35.24 inference(forward_subsumption_resolution,[status(thm)],[f4675,f1827])).
% 235.16/35.24 fof(f4686,plain,(
% 235.16/35.24 sQ255_spl),
% 235.16/35.24 inference(contradiction_clause,[status(thm)],[f4685])).
% 235.16/35.24 fof(f5225,definition,(
% 235.16/35.24 ![X0]: (sQ293_spl <=> (in(X0,set_meet(empty_set))))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f5226,plain,(
% 235.16/35.24 ![X0]: (in(X0,set_meet(empty_set))|~sQ293_spl)),
% 235.16/35.24 inference(component_clause,[status(thm)],[f5225])).
% 235.16/35.24 fof(f5366,plain,(
% 235.16/35.24 ~function(relation_dom(empty_set))|sQ18_spl),
% 235.16/35.24 inference(forward_demodulation,[status(thm)],[f3244,f2370])).
% 235.16/35.24 fof(f5367,plain,(
% 235.16/35.24 ~function(empty_set)|sQ18_spl),
% 235.16/35.24 inference(forward_demodulation,[status(thm)],[f1791,f5366])).
% 235.16/35.24 fof(f5368,plain,(
% 235.16/35.24 $false|sQ18_spl),
% 235.16/35.24 inference(forward_subsumption_resolution,[status(thm)],[f5367,f965])).
% 235.16/35.24 fof(f5369,plain,(
% 235.16/35.24 sQ18_spl),
% 235.16/35.24 inference(contradiction_clause,[status(thm)],[f5368])).
% 235.16/35.24 fof(f5376,definition,(
% 235.16/35.24 sQ314_spl <=> (relation(sK115_skl))),
% 235.16/35.24 introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 235.16/35.24 fof(f5378,plain,(
% 235.16/35.24 ~relation(sK115_skl)|sQ314_spl),
% 235.16/35.24 inference(component_clause,[status(thm)],[f5376])).
% 235.16/35.24 fof(f5431,plain,(
% 235.16/35.24 $false|sQ314_spl),
% 235.16/35.24 inference(forward_subsumption_resolution,[status(thm)],[f5378,f1163])).
% 235.16/35.24 fof(f5432,plain,(
% 235.16/35.24 sQ314_spl),
% 235.16/35.24 inference(contradiction_clause,[status(thm)],[f5431])).
% 235.16/35.24 fof(f5494,definition,(
% 235.16/35.24 sQ321_spl <=> (sK220_skl=empty_set)),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f5495,plain,(
% 235.93/35.25 sK220_skl=empty_set|~sQ321_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f5494])).
% 235.93/35.25 fof(f5514,definition,(
% 235.93/35.25 sQ326_spl <=> (powerset(sK220_skl)=empty_set)),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f5515,plain,(
% 235.93/35.25 powerset(sK220_skl)=empty_set|~sQ326_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f5514])).
% 235.93/35.25 fof(f5521,definition,(
% 235.93/35.25 sQ328_spl <=> (powerset(sK221_skl)=empty_set)),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f5522,plain,(
% 235.93/35.25 powerset(sK221_skl)=empty_set|~sQ328_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f5521])).
% 235.93/35.25 fof(f5545,definition,(
% 235.93/35.25 ![X0]: (sQ333_spl <=> (in(X0,set_meet(empty_set))|in(sK26_skl(X0,empty_set,empty_set),empty_set)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f5546,plain,(
% 235.93/35.25 ![X0]: (in(X0,set_meet(empty_set))|in(sK26_skl(X0,empty_set,empty_set),empty_set)|~sQ333_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f5545])).
% 235.93/35.25 fof(f5553,plain,(
% 235.93/35.25 ![X0]: (in(X0,empty_set)|in(sK26_skl(X0,empty_set,empty_set),empty_set)|~sQ333_spl)),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f2173,f5546])).
% 235.93/35.25 fof(f5554,plain,(
% 235.93/35.25 ![X0]: (in(sK26_skl(X0,empty_set,empty_set),empty_set)|~sQ333_spl)),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f5553,f2187])).
% 235.93/35.25 fof(f5567,plain,(
% 235.93/35.25 in(sK223_skl,empty_set)|~sQ321_spl),
% 235.93/35.25 inference(backward_demodulation,[status(thm)],[f5495,f1828])).
% 235.93/35.25 fof(f5762,plain,(
% 235.93/35.25 $false|~sQ321_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f5567,f2187])).
% 235.93/35.25 fof(f5763,plain,(
% 235.93/35.25 ~sQ321_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f5762])).
% 235.93/35.25 fof(f6196,definition,(
% 235.93/35.25 sQ383_spl <=> (sK221_skl=relation_rng(empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f6197,plain,(
% 235.93/35.25 sK221_skl=relation_rng(empty_set)|~sQ383_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f6196])).
% 235.93/35.25 fof(f6206,plain,(
% 235.93/35.25 sK221_skl=empty_set|~sQ383_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1792,f6197])).
% 235.93/35.25 fof(f6207,plain,(
% 235.93/35.25 $false|~sQ383_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f6206,f1829])).
% 235.93/35.25 fof(f6208,plain,(
% 235.93/35.25 ~sQ383_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f6207])).
% 235.93/35.25 fof(f6301,definition,(
% 235.93/35.25 sQ401_spl <=> (in(ordered_pair(sK31_skl(relation_field(empty_set),empty_set),sK32_skl(relation_field(empty_set),empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f6302,plain,(
% 235.93/35.25 in(ordered_pair(sK31_skl(relation_field(empty_set),empty_set),sK32_skl(relation_field(empty_set),empty_set)),empty_set)|~sQ401_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f6301])).
% 235.93/35.25 fof(f6309,plain,(
% 235.93/35.25 $false|~sQ401_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f6302,f2187])).
% 235.93/35.25 fof(f6310,plain,(
% 235.93/35.25 ~sQ401_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f6309])).
% 235.93/35.25 fof(f6827,plain,(
% 235.93/35.25 ~relation_dom(empty_set)=empty_set|sQ126_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f3244,f3010])).
% 235.93/35.25 fof(f6828,plain,(
% 235.93/35.25 ~empty_set=empty_set|sQ126_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f6827])).
% 235.93/35.25 fof(f6829,plain,(
% 235.93/35.25 $false|sQ126_spl),
% 235.93/35.25 inference(trivial_equality_resolution,[status(thm)],[f6828])).
% 235.93/35.25 fof(f6830,plain,(
% 235.93/35.25 sQ126_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f6829])).
% 235.93/35.25 fof(f6837,plain,(
% 235.93/35.25 ~relation_dom(empty_set)=empty_set|sQ124_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f3282,f3003])).
% 235.93/35.25 fof(f6838,plain,(
% 235.93/35.25 ~empty_set=empty_set|sQ124_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f6837])).
% 235.93/35.25 fof(f6839,plain,(
% 235.93/35.25 $false|sQ124_spl),
% 235.93/35.25 inference(trivial_equality_resolution,[status(thm)],[f6838])).
% 235.93/35.25 fof(f6840,plain,(
% 235.93/35.25 sQ124_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f6839])).
% 235.93/35.25 fof(f6922,plain,(
% 235.93/35.25 ~relation_dom(empty_set)=empty_set|sQ122_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f3285,f2996])).
% 235.93/35.25 fof(f6923,plain,(
% 235.93/35.25 ~empty_set=empty_set|sQ122_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f6922])).
% 235.93/35.25 fof(f6924,plain,(
% 235.93/35.25 $false|sQ122_spl),
% 235.93/35.25 inference(trivial_equality_resolution,[status(thm)],[f6923])).
% 235.93/35.25 fof(f6925,plain,(
% 235.93/35.25 sQ122_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f6924])).
% 235.93/35.25 fof(f6932,plain,(
% 235.93/35.25 ~relation_dom(empty_set)=empty_set|sQ120_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f3305,f2989])).
% 235.93/35.25 fof(f6933,plain,(
% 235.93/35.25 ~empty_set=empty_set|sQ120_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f6932])).
% 235.93/35.25 fof(f6934,plain,(
% 235.93/35.25 $false|sQ120_spl),
% 235.93/35.25 inference(trivial_equality_resolution,[status(thm)],[f6933])).
% 235.93/35.25 fof(f6935,plain,(
% 235.93/35.25 sQ120_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f6934])).
% 235.93/35.25 fof(f7049,plain,(
% 235.93/35.25 ![X0]: (~element(X0,empty_set)|empty(X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f632,f944])).
% 235.93/35.25 fof(f7127,definition,(
% 235.93/35.25 sQ470_spl <=> (relation(sK112_skl))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ470_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f7129,plain,(
% 235.93/35.25 ~relation(sK112_skl)|sQ470_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f7127])).
% 235.93/35.25 fof(f7139,plain,(
% 235.93/35.25 $false|sQ470_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f7129,f1156])).
% 235.93/35.25 fof(f7140,plain,(
% 235.93/35.25 sQ470_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f7139])).
% 235.93/35.25 fof(f7441,plain,(
% 235.93/35.25 ~relation_rng(empty_set)=empty_set|sQ136_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f3305,f3062])).
% 235.93/35.25 fof(f7442,plain,(
% 235.93/35.25 ~empty_set=empty_set|sQ136_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1792,f7441])).
% 235.93/35.25 fof(f7443,plain,(
% 235.93/35.25 $false|sQ136_spl),
% 235.93/35.25 inference(trivial_equality_resolution,[status(thm)],[f7442])).
% 235.93/35.25 fof(f7444,plain,(
% 235.93/35.25 sQ136_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f7443])).
% 235.93/35.25 fof(f7723,plain,(
% 235.93/35.25 ![X0]: (in(sK223_skl,set_union2(sK220_skl,X0)))),
% 235.93/35.25 inference(resolution,[status(thm)],[f2197,f1828])).
% 235.93/35.25 fof(f8320,definition,(
% 235.93/35.25 sQ549_spl <=> (relation_dom(relation_rng(empty_set))=empty_set)),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f8322,plain,(
% 235.93/35.25 ~relation_dom(relation_rng(empty_set))=empty_set|sQ549_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f8320])).
% 235.93/35.25 fof(f8327,plain,(
% 235.93/35.25 ~relation_dom(empty_set)=empty_set|sQ549_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1792,f8322])).
% 235.93/35.25 fof(f8328,plain,(
% 235.93/35.25 ~empty_set=empty_set|sQ549_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f8327])).
% 235.93/35.25 fof(f8329,plain,(
% 235.93/35.25 $false|sQ549_spl),
% 235.93/35.25 inference(trivial_equality_resolution,[status(thm)],[f8328])).
% 235.93/35.25 fof(f8330,plain,(
% 235.93/35.25 sQ549_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f8329])).
% 235.93/35.25 fof(f9675,definition,(
% 235.93/35.25 ![X0]: (sQ643_spl <=> (~in(sK223_skl,X0)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f9676,plain,(
% 235.93/35.25 ![X0]: (~in(sK223_skl,X0)|~sQ643_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f9675])).
% 235.93/35.25 fof(f9679,definition,(
% 235.93/35.25 sQ644_spl <=> (in(sK223_skl,empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f9680,plain,(
% 235.93/35.25 in(sK223_skl,empty_set)|~sQ644_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f9679])).
% 235.93/35.25 fof(f9683,plain,(
% 235.93/35.25 $false|~sQ643_spl),
% 235.93/35.25 inference(backward_subsumption_resolution,[status(thm)],[f7723,f9676])).
% 235.93/35.25 fof(f9700,plain,(
% 235.93/35.25 ~sQ643_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f9683])).
% 235.93/35.25 fof(f10433,plain,(
% 235.93/35.25 ![X0,X1]: (is_antisymmetric_in(X0,X1)|in(ordered_pair(sK60_skl(X1,X0),sK61_skl(X1,X0)),X0)|~empty(X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f737,f395])).
% 235.93/35.25 fof(f10436,plain,(
% 235.93/35.25 ![X0,X1]: (is_antisymmetric_in(X0,X1)|~empty(X0))),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f10433,f1852])).
% 235.93/35.25 fof(f12064,plain,(
% 235.93/35.25 ![X0]: (in(sK223_skl,set_difference(sK220_skl,X0))|in(sK223_skl,X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f2215,f1828])).
% 235.93/35.25 fof(f12160,definition,(
% 235.93/35.25 ![X0]: (sQ793_spl <=> (in(relation_rng(sK222_skl),X0)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ793_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f12161,plain,(
% 235.93/35.25 ![X0]: (in(relation_rng(sK222_skl),X0)|~sQ793_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f12160])).
% 235.93/35.25 fof(f12170,plain,(
% 235.93/35.25 ![X0]: (~in(relation_rng(sK222_skl),X0)|~sQ793_spl)),
% 235.93/35.25 inference(resolution,[status(thm)],[f12161,f2214])).
% 235.93/35.25 fof(f12222,plain,(
% 235.93/35.25 $false|~sQ793_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f12170,f12161])).
% 235.93/35.25 fof(f12223,plain,(
% 235.93/35.25 ~sQ793_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f12222])).
% 235.93/35.25 fof(f12239,plain,(
% 235.93/35.25 $false|~sQ644_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f9680,f2187])).
% 235.93/35.25 fof(f12240,plain,(
% 235.93/35.25 ~sQ644_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f12239])).
% 235.93/35.25 fof(f15161,definition,(
% 235.93/35.25 sQ977_spl <=> (function(set_meet(empty_set)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ977_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f15163,plain,(
% 235.93/35.25 ~function(set_meet(empty_set))|sQ977_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f15161])).
% 235.93/35.25 fof(f15165,plain,(
% 235.93/35.25 ~function(empty_set)|sQ977_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f2173,f15163])).
% 235.93/35.25 fof(f15166,plain,(
% 235.93/35.25 $false|sQ977_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f15165,f965])).
% 235.93/35.25 fof(f15167,plain,(
% 235.93/35.25 sQ977_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f15166])).
% 235.93/35.25 fof(f15616,definition,(
% 235.93/35.25 sQ999_spl <=> (subset(empty_set,relation_dom(relation_composition(empty_set,empty_set))))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ999_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f15618,plain,(
% 235.93/35.25 ~subset(empty_set,relation_dom(relation_composition(empty_set,empty_set)))|sQ999_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f15616])).
% 235.93/35.25 fof(f15620,plain,(
% 235.93/35.25 $false|sQ999_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f15618,f1614])).
% 235.93/35.25 fof(f15621,plain,(
% 235.93/35.25 sQ999_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f15620])).
% 235.93/35.25 fof(f15745,definition,(
% 235.93/35.25 sQ1015_spl <=> (in(sK79_skl(empty_set),relation_dom(empty_set)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1015_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f15746,plain,(
% 235.93/35.25 in(sK79_skl(empty_set),relation_dom(empty_set))|~sQ1015_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f15745])).
% 235.93/35.25 fof(f15749,plain,(
% 235.93/35.25 in(sK79_skl(empty_set),empty_set)|~sQ1015_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f15746])).
% 235.93/35.25 fof(f15750,plain,(
% 235.93/35.25 $false|~sQ1015_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f15749,f2187])).
% 235.93/35.25 fof(f15751,plain,(
% 235.93/35.25 ~sQ1015_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f15750])).
% 235.93/35.25 fof(f15892,plain,(
% 235.93/35.25 ![X0]: (in(X0,empty_set)|~sQ293_spl)),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f2173,f5226])).
% 235.93/35.25 fof(f15893,plain,(
% 235.93/35.25 $false|~sQ293_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f15892,f2187])).
% 235.93/35.25 fof(f15894,plain,(
% 235.93/35.25 ~sQ293_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f15893])).
% 235.93/35.25 fof(f16044,definition,(
% 235.93/35.25 sQ1035_spl <=> (relation(sK118_skl))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1035_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f16046,plain,(
% 235.93/35.25 ~relation(sK118_skl)|sQ1035_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f16044])).
% 235.93/35.25 fof(f16059,plain,(
% 235.93/35.25 $false|sQ1035_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f16046,f1175])).
% 235.93/35.25 fof(f16060,plain,(
% 235.93/35.25 sQ1035_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f16059])).
% 235.93/35.25 fof(f16325,definition,(
% 235.93/35.25 sQ1070_spl <=> (in(sK80_skl(empty_set),relation_dom(empty_set)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1070_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f16326,plain,(
% 235.93/35.25 in(sK80_skl(empty_set),relation_dom(empty_set))|~sQ1070_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f16325])).
% 235.93/35.25 fof(f16329,plain,(
% 235.93/35.25 in(sK80_skl(empty_set),empty_set)|~sQ1070_spl),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f1791,f16326])).
% 235.93/35.25 fof(f16330,plain,(
% 235.93/35.25 $false|~sQ1070_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f16329,f2187])).
% 235.93/35.25 fof(f16331,plain,(
% 235.93/35.25 ~sQ1070_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f16330])).
% 235.93/35.25 fof(f16966,plain,(
% 235.93/35.25 $false|~sQ333_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f5554,f2187])).
% 235.93/35.25 fof(f16967,plain,(
% 235.93/35.25 ~sQ333_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f16966])).
% 235.93/35.25 fof(f17339,plain,(
% 235.93/35.25 ![X0,X1]: (is_transitive_in(X0,X1)|in(ordered_pair(sK85_skl(X1,X0),sK87_skl(X1,X0)),X0)|~empty(X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f875,f395])).
% 235.93/35.25 fof(f17342,plain,(
% 235.93/35.25 ![X0,X1]: (is_transitive_in(X0,X1)|~empty(X0))),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f17339,f1852])).
% 235.93/35.25 fof(f17907,definition,(
% 235.93/35.25 ![X0,X1]: (sQ1170_spl <=> (~in(X0,X1)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1170_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f17908,plain,(
% 235.93/35.25 ![X0,X1]: (~in(X0,X1)|~sQ1170_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f17907])).
% 235.93/35.25 fof(f18499,plain,(
% 235.93/35.25 ![X0]: (in(sK223_skl,set_difference(sK220_skl,X0))|~sQ1170_spl)),
% 235.93/35.25 inference(backward_subsumption_resolution,[status(thm)],[f12064,f17908])).
% 235.93/35.25 fof(f18647,plain,(
% 235.93/35.25 $false|~sQ1170_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f18499,f17908])).
% 235.93/35.25 fof(f18648,plain,(
% 235.93/35.25 ~sQ1170_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f18647])).
% 235.93/35.25 fof(f18952,plain,(
% 235.93/35.25 ![X0]: (~subset(powerset(X0),X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f2189,f2825])).
% 235.93/35.25 fof(f19069,plain,(
% 235.93/35.25 empty(relation_inverse(empty_set))),
% 235.93/35.25 inference(resolution,[status(thm)],[f942,f944])).
% 235.93/35.25 fof(f19071,plain,(
% 235.93/35.25 relation(relation_inverse(empty_set))),
% 235.93/35.25 inference(resolution,[status(thm)],[f943,f944])).
% 235.93/35.25 fof(f19140,plain,(
% 235.93/35.25 relation_rng(relation_inverse(empty_set))=empty_set),
% 235.93/35.25 inference(resolution,[status(thm)],[f19069,f3245])).
% 235.93/35.25 fof(f19189,definition,(
% 235.93/35.25 sQ1264_spl <=> (relation(relation_inverse(empty_set)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1264_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f19191,plain,(
% 235.93/35.25 ~relation(relation_inverse(empty_set))|sQ1264_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f19189])).
% 235.93/35.25 fof(f19216,plain,(
% 235.93/35.25 $false|sQ1264_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f19191,f19071])).
% 235.93/35.25 fof(f19217,plain,(
% 235.93/35.25 sQ1264_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f19216])).
% 235.93/35.25 fof(f19385,definition,(
% 235.93/35.25 ![X0]: (sQ1271_spl <=> (~relation(X0)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1271_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f19386,plain,(
% 235.93/35.25 ![X0]: (~relation(X0)|~sQ1271_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f19385])).
% 235.93/35.25 fof(f19875,definition,(
% 235.93/35.25 sQ1289_spl <=> (epsilon_transitive(empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1289_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f19877,plain,(
% 235.93/35.25 ~epsilon_transitive(empty_set)|sQ1289_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f19875])).
% 235.93/35.25 fof(f19882,plain,(
% 235.93/35.25 $false|sQ1289_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f19877,f968])).
% 235.93/35.25 fof(f19883,plain,(
% 235.93/35.25 sQ1289_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f19882])).
% 235.93/35.25 fof(f19949,definition,(
% 235.93/35.25 ![X0]: (sQ1293_spl <=> (~empty(X0)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1293_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f19950,plain,(
% 235.93/35.25 ![X0]: (~empty(X0)|~sQ1293_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f19949])).
% 235.93/35.25 fof(f20159,definition,(
% 235.93/35.25 sQ1295_spl <=> (in(empty_set,empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1295_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f20160,plain,(
% 235.93/35.25 in(empty_set,empty_set)|~sQ1295_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f20159])).
% 235.93/35.25 fof(f20163,plain,(
% 235.93/35.25 $false|~sQ1295_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f20160,f2187])).
% 235.93/35.25 fof(f20164,plain,(
% 235.93/35.25 ~sQ1295_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f20163])).
% 235.93/35.25 fof(f20605,definition,(
% 235.93/35.25 ![X0]: (sQ1314_spl <=> (~subset(empty_set,X0)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1314_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f20606,plain,(
% 235.93/35.25 ![X0]: (~subset(empty_set,X0)|~sQ1314_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f20605])).
% 235.93/35.25 fof(f20609,plain,(
% 235.93/35.25 $false|~sQ1314_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f20606,f1614])).
% 235.93/35.25 fof(f20610,plain,(
% 235.93/35.25 ~sQ1314_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f20609])).
% 235.93/35.25 fof(f20694,definition,(
% 235.93/35.25 sQ1320_spl <=> (in(ordered_pair(sK38_skl(empty_set,empty_set),sK39_skl(empty_set,empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1320_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f20695,plain,(
% 235.93/35.25 in(ordered_pair(sK38_skl(empty_set,empty_set),sK39_skl(empty_set,empty_set)),empty_set)|~sQ1320_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f20694])).
% 235.93/35.25 fof(f20698,plain,(
% 235.93/35.25 $false|~sQ1320_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f20695,f2187])).
% 235.93/35.25 fof(f20699,plain,(
% 235.93/35.25 ~sQ1320_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f20698])).
% 235.93/35.25 fof(f21551,definition,(
% 235.93/35.25 sQ1325_spl <=> (empty(singleton(empty_set)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1325_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f21552,plain,(
% 235.93/35.25 empty(singleton(empty_set))|~sQ1325_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f21551])).
% 235.93/35.25 fof(f21562,plain,(
% 235.93/35.25 $false|~sQ1325_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f21552,f973])).
% 235.93/35.25 fof(f21563,plain,(
% 235.93/35.25 ~sQ1325_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f21562])).
% 235.93/35.25 fof(f21610,plain,(
% 235.93/35.25 empty(sK90_skl(empty_set))),
% 235.93/35.25 inference(resolution,[status(thm)],[f7049,f935])).
% 235.93/35.25 fof(f21632,plain,(
% 235.93/35.25 ![X0]: (is_transitive_in(sK90_skl(empty_set),X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f21610,f17342])).
% 235.93/35.25 fof(f21633,plain,(
% 235.93/35.25 ![X0]: (is_antisymmetric_in(sK90_skl(empty_set),X0))),
% 235.93/35.25 inference(resolution,[status(thm)],[f21610,f10436])).
% 235.93/35.25 fof(f21642,plain,(
% 235.93/35.25 sK90_skl(empty_set)=empty_set),
% 235.93/35.25 inference(resolution,[status(thm)],[f21610,f1821])).
% 235.93/35.25 fof(f21660,plain,(
% 235.93/35.25 ![X0]: (is_transitive_in(empty_set,X0))),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f21642,f21632])).
% 235.93/35.25 fof(f21670,plain,(
% 235.93/35.25 ![X0]: (is_antisymmetric_in(empty_set,X0))),
% 235.93/35.25 inference(forward_demodulation,[status(thm)],[f21642,f21633])).
% 235.93/35.25 fof(f21733,definition,(
% 235.93/35.25 sQ1344_spl <=> (in(ordered_pair(sK93_skl(empty_set),sK95_skl(empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1344_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f21734,plain,(
% 235.93/35.25 in(ordered_pair(sK93_skl(empty_set),sK95_skl(empty_set)),empty_set)|~sQ1344_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f21733])).
% 235.93/35.25 fof(f21738,plain,(
% 235.93/35.25 $false|~sQ1344_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f21734,f2187])).
% 235.93/35.25 fof(f21739,plain,(
% 235.93/35.25 ~sQ1344_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f21738])).
% 235.93/35.25 fof(f21780,definition,(
% 235.93/35.25 sQ1350_spl <=> (in(ordered_pair(sK95_skl(empty_set),sK94_skl(empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1350_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f21781,plain,(
% 235.93/35.25 in(ordered_pair(sK95_skl(empty_set),sK94_skl(empty_set)),empty_set)|~sQ1350_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f21780])).
% 235.93/35.25 fof(f21785,plain,(
% 235.93/35.25 $false|~sQ1350_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f21781,f2187])).
% 235.93/35.25 fof(f21786,plain,(
% 235.93/35.25 ~sQ1350_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f21785])).
% 235.93/35.25 fof(f22218,definition,(
% 235.93/35.25 sQ1362_spl <=> (in(ordered_pair(sK97_skl(empty_set),sK98_skl(empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1362_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f22219,plain,(
% 235.93/35.25 in(ordered_pair(sK97_skl(empty_set),sK98_skl(empty_set)),empty_set)|~sQ1362_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f22218])).
% 235.93/35.25 fof(f22223,plain,(
% 235.93/35.25 $false|~sQ1362_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f22219,f2187])).
% 235.93/35.25 fof(f22224,plain,(
% 235.93/35.25 ~sQ1362_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f22223])).
% 235.93/35.25 fof(f22333,definition,(
% 235.93/35.25 sQ1368_spl <=> (in(ordered_pair(sK98_skl(empty_set),sK97_skl(empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1368_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f22334,plain,(
% 235.93/35.25 in(ordered_pair(sK98_skl(empty_set),sK97_skl(empty_set)),empty_set)|~sQ1368_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f22333])).
% 235.93/35.25 fof(f22338,plain,(
% 235.93/35.25 $false|~sQ1368_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f22334,f2187])).
% 235.93/35.25 fof(f22339,plain,(
% 235.93/35.25 ~sQ1368_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f22338])).
% 235.93/35.25 fof(f22773,definition,(
% 235.93/35.25 ![X0]: (sQ1381_spl <=> (empty_set=singleton(X0)))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1381_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f22774,plain,(
% 235.93/35.25 ![X0]: (empty_set=singleton(X0)|~sQ1381_spl)),
% 235.93/35.25 inference(component_clause,[status(thm)],[f22773])).
% 235.93/35.25 fof(f22777,plain,(
% 235.93/35.25 $false|~sQ1381_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f22774,f1038])).
% 235.93/35.25 fof(f22778,plain,(
% 235.93/35.25 ~sQ1381_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f22777])).
% 235.93/35.25 fof(f23081,definition,(
% 235.93/35.25 sQ1397_spl <=> (empty(singleton(sK39_skl(empty_set,sK221_skl))))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1397_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f23082,plain,(
% 235.93/35.25 empty(singleton(sK39_skl(empty_set,sK221_skl)))|~sQ1397_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f23081])).
% 235.93/35.25 fof(f23092,plain,(
% 235.93/35.25 $false|~sQ1397_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f23082,f973])).
% 235.93/35.25 fof(f23093,plain,(
% 235.93/35.25 ~sQ1397_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f23092])).
% 235.93/35.25 fof(f23250,definition,(
% 235.93/35.25 sQ1406_spl <=> (epsilon_transitive(sK104_skl))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1406_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f23252,plain,(
% 235.93/35.25 ~epsilon_transitive(sK104_skl)|sQ1406_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f23250])).
% 235.93/35.25 fof(f23257,plain,(
% 235.93/35.25 $false|sQ1406_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f23252,f1121])).
% 235.93/35.25 fof(f23258,plain,(
% 235.93/35.25 sQ1406_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f23257])).
% 235.93/35.25 fof(f24221,definition,(
% 235.93/35.25 sQ1421_spl <=> (epsilon_transitive(sK116_skl))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1421_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f24223,plain,(
% 235.93/35.25 ~epsilon_transitive(sK116_skl)|sQ1421_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f24221])).
% 235.93/35.25 fof(f24228,plain,(
% 235.93/35.25 $false|sQ1421_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f24223,f1168])).
% 235.93/35.25 fof(f24229,plain,(
% 235.93/35.25 sQ1421_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f24228])).
% 235.93/35.25 fof(f26565,definition,(
% 235.93/35.25 sQ1524_spl <=> (in(ordered_pair(sK51_skl(empty_set,empty_set),sK52_skl(empty_set,empty_set)),empty_set))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1524_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f26566,plain,(
% 235.93/35.25 in(ordered_pair(sK51_skl(empty_set,empty_set),sK52_skl(empty_set,empty_set)),empty_set)|~sQ1524_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f26565])).
% 235.93/35.25 fof(f26570,plain,(
% 235.93/35.25 $false|~sQ1524_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f26566,f2187])).
% 235.93/35.25 fof(f26571,plain,(
% 235.93/35.25 ~sQ1524_spl),
% 235.93/35.25 inference(contradiction_clause,[status(thm)],[f26570])).
% 235.93/35.25 fof(f27078,definition,(
% 235.93/35.25 sQ1554_spl <=> (empty(singleton(sK52_skl(empty_set,sK221_skl))))),
% 235.93/35.25 introduced(definition,[new_symbols(definition,[sQ1554_spl])],[split_symbol_definition])).
% 235.93/35.25 fof(f27079,plain,(
% 235.93/35.25 empty(singleton(sK52_skl(empty_set,sK221_skl)))|~sQ1554_spl),
% 235.93/35.25 inference(component_clause,[status(thm)],[f27078])).
% 235.93/35.25 fof(f27086,plain,(
% 235.93/35.25 $false|~sQ1554_spl),
% 235.93/35.25 inference(forward_subsumption_resolution,[status(thm)],[f27079,f973])).
% 235.93/35.27 fof(f27087,plain,(
% 235.93/35.27 ~sQ1554_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f27086])).
% 235.93/35.27 fof(f27345,plain,(
% 235.93/35.27 $false|sQ215_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f4213,f962])).
% 235.93/35.27 fof(f27346,plain,(
% 235.93/35.27 sQ215_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f27345])).
% 235.93/35.27 fof(f27505,plain,(
% 235.93/35.27 $false|sQ214_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f4210,f917])).
% 235.93/35.27 fof(f27506,plain,(
% 235.93/35.27 sQ214_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f27505])).
% 235.93/35.27 fof(f27922,definition,(
% 235.93/35.27 sQ1580_spl <=> (subset(empty_set,relation_dom(relation_composition(empty_set,relation_inverse(empty_set)))))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1580_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f27924,plain,(
% 235.93/35.27 ~subset(empty_set,relation_dom(relation_composition(empty_set,relation_inverse(empty_set))))|sQ1580_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f27922])).
% 235.93/35.27 fof(f27926,plain,(
% 235.93/35.27 $false|sQ1580_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f27924,f1614])).
% 235.93/35.27 fof(f27927,plain,(
% 235.93/35.27 sQ1580_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f27926])).
% 235.93/35.27 fof(f29505,definition,(
% 235.93/35.27 ![X0]: (sQ1655_spl <=> (empty_set=X0))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1655_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f29506,plain,(
% 235.93/35.27 ![X0]: (empty_set=X0|~sQ1655_spl)),
% 235.93/35.27 inference(component_clause,[status(thm)],[f29505])).
% 235.93/35.27 fof(f30105,plain,(
% 235.93/35.27 $false|~sQ1655_spl),
% 235.93/35.27 inference(backward_subsumption_resolution,[status(thm)],[f1038,f29506])).
% 235.93/35.27 fof(f30207,plain,(
% 235.93/35.27 ~sQ1655_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f30105])).
% 235.93/35.27 fof(f31819,plain,(
% 235.93/35.27 ~subset(empty_set,sK221_skl)|~sQ328_spl),
% 235.93/35.27 inference(paramodulation,[status(thm)],[f5522,f18952])).
% 235.93/35.27 fof(f31893,definition,(
% 235.93/35.27 sQ1700_spl <=> (in(sK55_skl(sK221_skl,sK115_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1700_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f31894,plain,(
% 235.93/35.27 in(sK55_skl(sK221_skl,sK115_skl),empty_set)|~sQ1700_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f31893])).
% 235.93/35.27 fof(f31900,definition,(
% 235.93/35.27 sQ1702_spl <=> (in(sK55_skl(sK221_skl,sK102_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1702_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f31901,plain,(
% 235.93/35.27 in(sK55_skl(sK221_skl,sK102_skl),empty_set)|~sQ1702_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f31900])).
% 235.93/35.27 fof(f31914,definition,(
% 235.93/35.27 sQ1704_spl <=> (in(sK55_skl(sK221_skl,sK117_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1704_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f31915,plain,(
% 235.93/35.27 in(sK55_skl(sK221_skl,sK117_skl),empty_set)|~sQ1704_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f31914])).
% 235.93/35.27 fof(f31921,definition,(
% 235.93/35.27 sQ1706_spl <=> (in(sK55_skl(sK221_skl,sK112_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1706_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f31922,plain,(
% 235.93/35.27 in(sK55_skl(sK221_skl,sK112_skl),empty_set)|~sQ1706_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f31921])).
% 235.93/35.27 fof(f31928,definition,(
% 235.93/35.27 sQ1708_spl <=> (in(sK55_skl(sK221_skl,sK118_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1708_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f31929,plain,(
% 235.93/35.27 in(sK55_skl(sK221_skl,sK118_skl),empty_set)|~sQ1708_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f31928])).
% 235.93/35.27 fof(f31946,definition,(
% 235.93/35.27 sQ1711_spl <=> (in(sK55_skl(sK221_skl,empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1711_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f31947,plain,(
% 235.93/35.27 in(sK55_skl(sK221_skl,empty_set),empty_set)|~sQ1711_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f31946])).
% 235.93/35.27 fof(f31971,plain,(
% 235.93/35.27 $false|~sQ328_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31819,f1614])).
% 235.93/35.27 fof(f31972,plain,(
% 235.93/35.27 ~sQ328_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31971])).
% 235.93/35.27 fof(f31973,plain,(
% 235.93/35.27 $false|~sQ1711_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31947,f2187])).
% 235.93/35.27 fof(f31974,plain,(
% 235.93/35.27 ~sQ1711_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31973])).
% 235.93/35.27 fof(f31975,plain,(
% 235.93/35.27 $false|~sQ1708_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31929,f2187])).
% 235.93/35.27 fof(f31976,plain,(
% 235.93/35.27 ~sQ1708_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31975])).
% 235.93/35.27 fof(f31977,plain,(
% 235.93/35.27 $false|~sQ1706_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31922,f2187])).
% 235.93/35.27 fof(f31978,plain,(
% 235.93/35.27 ~sQ1706_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31977])).
% 235.93/35.27 fof(f31979,plain,(
% 235.93/35.27 $false|~sQ1704_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31915,f2187])).
% 235.93/35.27 fof(f31980,plain,(
% 235.93/35.27 ~sQ1704_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31979])).
% 235.93/35.27 fof(f31981,plain,(
% 235.93/35.27 $false|~sQ1702_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31901,f2187])).
% 235.93/35.27 fof(f31982,plain,(
% 235.93/35.27 ~sQ1702_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31981])).
% 235.93/35.27 fof(f31983,plain,(
% 235.93/35.27 $false|~sQ1700_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f31894,f2187])).
% 235.93/35.27 fof(f31984,plain,(
% 235.93/35.27 ~sQ1700_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f31983])).
% 235.93/35.27 fof(f32149,plain,(
% 235.93/35.27 ~subset(empty_set,sK220_skl)|~sQ326_spl),
% 235.93/35.27 inference(paramodulation,[status(thm)],[f5515,f18952])).
% 235.93/35.27 fof(f32223,definition,(
% 235.93/35.27 sQ1713_spl <=> (in(sK55_skl(sK220_skl,sK115_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1713_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f32224,plain,(
% 235.93/35.27 in(sK55_skl(sK220_skl,sK115_skl),empty_set)|~sQ1713_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f32223])).
% 235.93/35.27 fof(f32230,definition,(
% 235.93/35.27 sQ1715_spl <=> (in(sK55_skl(sK220_skl,sK102_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1715_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f32231,plain,(
% 235.93/35.27 in(sK55_skl(sK220_skl,sK102_skl),empty_set)|~sQ1715_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f32230])).
% 235.93/35.27 fof(f32244,definition,(
% 235.93/35.27 sQ1717_spl <=> (in(sK55_skl(sK220_skl,sK117_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1717_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f32245,plain,(
% 235.93/35.27 in(sK55_skl(sK220_skl,sK117_skl),empty_set)|~sQ1717_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f32244])).
% 235.93/35.27 fof(f32251,definition,(
% 235.93/35.27 sQ1719_spl <=> (in(sK55_skl(sK220_skl,sK112_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1719_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f32252,plain,(
% 235.93/35.27 in(sK55_skl(sK220_skl,sK112_skl),empty_set)|~sQ1719_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f32251])).
% 235.93/35.27 fof(f32258,definition,(
% 235.93/35.27 sQ1721_spl <=> (in(sK55_skl(sK220_skl,sK118_skl),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1721_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f32259,plain,(
% 235.93/35.27 in(sK55_skl(sK220_skl,sK118_skl),empty_set)|~sQ1721_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f32258])).
% 235.93/35.27 fof(f32276,definition,(
% 235.93/35.27 sQ1724_spl <=> (in(sK55_skl(sK220_skl,empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1724_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f32277,plain,(
% 235.93/35.27 in(sK55_skl(sK220_skl,empty_set),empty_set)|~sQ1724_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f32276])).
% 235.93/35.27 fof(f32301,plain,(
% 235.93/35.27 $false|~sQ326_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32149,f1614])).
% 235.93/35.27 fof(f32302,plain,(
% 235.93/35.27 ~sQ326_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32301])).
% 235.93/35.27 fof(f32303,plain,(
% 235.93/35.27 $false|~sQ1724_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32277,f2187])).
% 235.93/35.27 fof(f32304,plain,(
% 235.93/35.27 ~sQ1724_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32303])).
% 235.93/35.27 fof(f32305,plain,(
% 235.93/35.27 $false|~sQ1721_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32259,f2187])).
% 235.93/35.27 fof(f32306,plain,(
% 235.93/35.27 ~sQ1721_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32305])).
% 235.93/35.27 fof(f32307,plain,(
% 235.93/35.27 $false|~sQ1719_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32252,f2187])).
% 235.93/35.27 fof(f32308,plain,(
% 235.93/35.27 ~sQ1719_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32307])).
% 235.93/35.27 fof(f32309,plain,(
% 235.93/35.27 $false|~sQ1717_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32245,f2187])).
% 235.93/35.27 fof(f32310,plain,(
% 235.93/35.27 ~sQ1717_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32309])).
% 235.93/35.27 fof(f32311,plain,(
% 235.93/35.27 $false|~sQ1715_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32231,f2187])).
% 235.93/35.27 fof(f32312,plain,(
% 235.93/35.27 ~sQ1715_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32311])).
% 235.93/35.27 fof(f32313,plain,(
% 235.93/35.27 $false|~sQ1713_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f32224,f2187])).
% 235.93/35.27 fof(f32314,plain,(
% 235.93/35.27 ~sQ1713_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f32313])).
% 235.93/35.27 fof(f33858,definition,(
% 235.93/35.27 sQ1791_spl <=> (is_transitive_in(empty_set,empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1791_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f33860,plain,(
% 235.93/35.27 ~is_transitive_in(empty_set,empty_set)|sQ1791_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f33858])).
% 235.93/35.27 fof(f33861,definition,(
% 235.93/35.27 sQ1792_spl <=> (is_antisymmetric_in(empty_set,empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1792_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f33863,plain,(
% 235.93/35.27 ~is_antisymmetric_in(empty_set,empty_set)|sQ1792_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f33861])).
% 235.93/35.27 fof(f33868,plain,(
% 235.93/35.27 $false|sQ1792_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f33863,f21670])).
% 235.93/35.27 fof(f33869,plain,(
% 235.93/35.27 sQ1792_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f33868])).
% 235.93/35.27 fof(f33870,plain,(
% 235.93/35.27 $false|sQ1791_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f33860,f21660])).
% 235.93/35.27 fof(f33871,plain,(
% 235.93/35.27 sQ1791_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f33870])).
% 235.93/35.27 fof(f34478,plain,(
% 235.93/35.27 relation_image(empty_set,relation_dom(empty_set))=relation_rng(empty_set)),
% 235.93/35.27 inference(resolution,[status(thm)],[f1471,f945])).
% 235.93/35.27 fof(f34482,plain,(
% 235.93/35.27 relation_image(empty_set,empty_set)=relation_rng(empty_set)),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f1791,f34478])).
% 235.93/35.27 fof(f34483,plain,(
% 235.93/35.27 relation_image(empty_set,empty_set)=empty_set),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f1792,f34482])).
% 235.93/35.27 fof(f36265,definition,(
% 235.93/35.27 sQ1889_spl <=> (in(empty_set,relation_dom(empty_set)))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1889_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f36266,plain,(
% 235.93/35.27 in(empty_set,relation_dom(empty_set))|~sQ1889_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f36265])).
% 235.93/35.27 fof(f36270,plain,(
% 235.93/35.27 in(empty_set,empty_set)|~sQ1889_spl),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f1791,f36266])).
% 235.93/35.27 fof(f36271,plain,(
% 235.93/35.27 $false|~sQ1889_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f36270,f2187])).
% 235.93/35.27 fof(f36272,plain,(
% 235.93/35.27 ~sQ1889_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f36271])).
% 235.93/35.27 fof(f36970,definition,(
% 235.93/35.27 sQ1949_spl <=> (empty(singleton(apply(sK118_skl,empty_set))))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1949_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f36971,plain,(
% 235.93/35.27 empty(singleton(apply(sK118_skl,empty_set)))|~sQ1949_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f36970])).
% 235.93/35.27 fof(f36978,plain,(
% 235.93/35.27 $false|~sQ1949_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f36971,f973])).
% 235.93/35.27 fof(f36979,plain,(
% 235.93/35.27 ~sQ1949_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f36978])).
% 235.93/35.27 fof(f37492,definition,(
% 235.93/35.27 sQ1955_spl <=> (empty(powerset(empty_set)))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ1955_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f37493,plain,(
% 235.93/35.27 empty(powerset(empty_set))|~sQ1955_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f37492])).
% 235.93/35.27 fof(f37498,plain,(
% 235.93/35.27 $false|~sQ1955_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f37493,f957])).
% 235.93/35.27 fof(f37499,plain,(
% 235.93/35.27 ~sQ1955_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f37498])).
% 235.93/35.27 fof(f39486,definition,(
% 235.93/35.27 sQ2080_spl <=> (function(relation_rng(relation_inverse(empty_set))))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2080_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f39488,plain,(
% 235.93/35.27 ~function(relation_rng(relation_inverse(empty_set)))|sQ2080_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f39486])).
% 235.93/35.27 fof(f39493,definition,(
% 235.93/35.27 sQ2082_spl <=> (function(relation_rng(empty_set)))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2082_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f39495,plain,(
% 235.93/35.27 ~function(relation_rng(empty_set))|sQ2082_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f39493])).
% 235.93/35.27 fof(f39500,plain,(
% 235.93/35.27 ~function(empty_set)|sQ2082_spl),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f1792,f39495])).
% 235.93/35.27 fof(f39501,plain,(
% 235.93/35.27 $false|sQ2082_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f39500,f965])).
% 235.93/35.27 fof(f39502,plain,(
% 235.93/35.27 sQ2082_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f39501])).
% 235.93/35.27 fof(f39503,plain,(
% 235.93/35.27 ~function(empty_set)|sQ2080_spl),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f19140,f39488])).
% 235.93/35.27 fof(f39504,plain,(
% 235.93/35.27 $false|sQ2080_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f39503,f965])).
% 235.93/35.27 fof(f39505,plain,(
% 235.93/35.27 sQ2080_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f39504])).
% 235.93/35.27 fof(f39821,plain,(
% 235.93/35.27 ![X0]: (~in(X0,sK220_skl)|in(ordered_pair(X0,sK199_skl(X0,sK222_skl,sK220_skl,sK221_skl)),sK222_skl)|~relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl)=sK220_skl)),
% 235.93/35.27 inference(resolution,[status(thm)],[f1827,f1555])).
% 235.93/35.27 fof(f39845,definition,(
% 235.93/35.27 ![X0]: (sQ2098_spl <=> (~in(X0,sK220_skl)|in(ordered_pair(X0,sK199_skl(X0,sK222_skl,sK220_skl,sK221_skl)),sK222_skl)))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2098_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f39846,plain,(
% 235.93/35.27 ![X0]: (~in(X0,sK220_skl)|in(ordered_pair(X0,sK199_skl(X0,sK222_skl,sK220_skl,sK221_skl)),sK222_skl)|~sQ2098_spl)),
% 235.93/35.27 inference(component_clause,[status(thm)],[f39845])).
% 235.93/35.27 fof(f39848,plain,(
% 235.93/35.27 sQ2098_spl|~sQ256_spl),
% 235.93/35.27 inference(split_clause,[status(thm)],[f39821,f39845,f4676])).
% 235.93/35.27 fof(f40010,definition,(
% 235.93/35.27 sQ2101_spl <=> (in(apply(sK204_skl(sK220_skl),empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2101_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f40011,plain,(
% 235.93/35.27 in(apply(sK204_skl(sK220_skl),empty_set),empty_set)|~sQ2101_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f40010])).
% 235.93/35.27 fof(f40022,plain,(
% 235.93/35.27 $false|~sQ2101_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f40011,f2187])).
% 235.93/35.27 fof(f40023,plain,(
% 235.93/35.27 ~sQ2101_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f40022])).
% 235.93/35.27 fof(f41035,definition,(
% 235.93/35.27 sQ2109_spl <=> (in(sK100_skl(empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2109_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41036,plain,(
% 235.93/35.27 in(sK100_skl(empty_set),empty_set)|~sQ2109_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41035])).
% 235.93/35.27 fof(f41039,definition,(
% 235.93/35.27 sQ2110_spl <=> (in(sK99_skl(empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2110_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41040,plain,(
% 235.93/35.27 in(sK99_skl(empty_set),empty_set)|~sQ2110_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41039])).
% 235.93/35.27 fof(f41046,definition,(
% 235.93/35.27 sQ2112_spl <=> (in(sK92_skl(empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2112_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41047,plain,(
% 235.93/35.27 in(sK92_skl(empty_set),empty_set)|~sQ2112_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41046])).
% 235.93/35.27 fof(f41094,plain,(
% 235.93/35.27 $false|~sQ2112_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41047,f2187])).
% 235.93/35.27 fof(f41095,plain,(
% 235.93/35.27 ~sQ2112_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41094])).
% 235.93/35.27 fof(f41096,plain,(
% 235.93/35.27 $false|~sQ2110_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41040,f2187])).
% 235.93/35.27 fof(f41097,plain,(
% 235.93/35.27 ~sQ2110_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41096])).
% 235.93/35.27 fof(f41098,plain,(
% 235.93/35.27 $false|~sQ2109_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41036,f2187])).
% 235.93/35.27 fof(f41099,plain,(
% 235.93/35.27 ~sQ2109_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41098])).
% 235.93/35.27 fof(f41142,definition,(
% 235.93/35.27 sQ2122_spl <=> (in(apply(sK204_skl(relation_dom(sK118_skl)),empty_set),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2122_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41143,plain,(
% 235.93/35.27 in(apply(sK204_skl(relation_dom(sK118_skl)),empty_set),empty_set)|~sQ2122_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41142])).
% 235.93/35.27 fof(f41149,plain,(
% 235.93/35.27 $false|~sQ2122_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41143,f2187])).
% 235.93/35.27 fof(f41150,plain,(
% 235.93/35.27 ~sQ2122_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41149])).
% 235.93/35.27 fof(f41676,definition,(
% 235.93/35.27 sQ2141_spl <=> (in(sK208_skl(relation_dom(empty_set),empty_set),relation_dom(empty_set)))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2141_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41677,plain,(
% 235.93/35.27 in(sK208_skl(relation_dom(empty_set),empty_set),relation_dom(empty_set))|~sQ2141_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41676])).
% 235.93/35.27 fof(f41682,plain,(
% 235.93/35.27 in(sK208_skl(empty_set,empty_set),relation_dom(empty_set))|~sQ2141_spl),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f1791,f41677])).
% 235.93/35.27 fof(f41683,plain,(
% 235.93/35.27 in(sK208_skl(empty_set,empty_set),empty_set)|~sQ2141_spl),
% 235.93/35.27 inference(forward_demodulation,[status(thm)],[f1791,f41682])).
% 235.93/35.27 fof(f41684,plain,(
% 235.93/35.27 $false|~sQ2141_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41683,f2187])).
% 235.93/35.27 fof(f41685,plain,(
% 235.93/35.27 ~sQ2141_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41684])).
% 235.93/35.27 fof(f41825,definition,(
% 235.93/35.27 sQ2150_spl <=> (empty(singleton(sK223_skl)))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2150_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41826,plain,(
% 235.93/35.27 empty(singleton(sK223_skl))|~sQ2150_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41825])).
% 235.93/35.27 fof(f41833,plain,(
% 235.93/35.27 $false|~sQ2150_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41826,f973])).
% 235.93/35.27 fof(f41834,plain,(
% 235.93/35.27 ~sQ2150_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41833])).
% 235.93/35.27 fof(f41923,definition,(
% 235.93/35.27 sQ2166_spl <=> (in(ordered_pair(sK76_skl(empty_set,empty_set),sK75_skl(empty_set,empty_set)),empty_set))),
% 235.93/35.27 introduced(definition,[new_symbols(definition,[sQ2166_spl])],[split_symbol_definition])).
% 235.93/35.27 fof(f41924,plain,(
% 235.93/35.27 in(ordered_pair(sK76_skl(empty_set,empty_set),sK75_skl(empty_set,empty_set)),empty_set)|~sQ2166_spl),
% 235.93/35.27 inference(component_clause,[status(thm)],[f41923])).
% 235.93/35.27 fof(f41928,plain,(
% 235.93/35.27 $false|~sQ2166_spl),
% 235.93/35.27 inference(forward_subsumption_resolution,[status(thm)],[f41924,f2187])).
% 235.93/35.27 fof(f41929,plain,(
% 235.93/35.27 ~sQ2166_spl),
% 235.93/35.27 inference(contradiction_clause,[status(thm)],[f41928])).
% 235.93/35.27 fof(f43023,plain,(
% 235.93/35.27 $false|~sQ1293_spl),
% 235.93/35.28 inference(backward_subsumption_resolution,[status(thm)],[f1159,f19950])).
% 235.93/35.28 fof(f44621,definition,(
% 235.93/35.28 sQ2237_spl <=> (in(ordered_pair(sK82_skl(empty_set,empty_set,empty_set),sK84_skl(empty_set,empty_set,empty_set)),empty_set))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2237_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f44622,plain,(
% 235.93/35.28 in(ordered_pair(sK82_skl(empty_set,empty_set,empty_set),sK84_skl(empty_set,empty_set,empty_set)),empty_set)|~sQ2237_spl),
% 235.93/35.28 inference(component_clause,[status(thm)],[f44621])).
% 235.93/35.28 fof(f44625,plain,(
% 235.93/35.28 $false|~sQ2237_spl),
% 235.93/35.28 inference(forward_subsumption_resolution,[status(thm)],[f44622,f2187])).
% 235.93/35.28 fof(f44626,plain,(
% 235.93/35.28 ~sQ2237_spl),
% 235.93/35.28 inference(contradiction_clause,[status(thm)],[f44625])).
% 235.93/35.28 fof(f44925,definition,(
% 235.93/35.28 sQ2249_spl <=> (in(sK210_skl(empty_set),empty_set))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2249_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f44926,plain,(
% 235.93/35.28 in(sK210_skl(empty_set),empty_set)|~sQ2249_spl),
% 235.93/35.28 inference(component_clause,[status(thm)],[f44925])).
% 235.93/35.28 fof(f44929,plain,(
% 235.93/35.28 $false|~sQ2249_spl),
% 235.93/35.28 inference(forward_subsumption_resolution,[status(thm)],[f44926,f2187])).
% 235.93/35.28 fof(f44930,plain,(
% 235.93/35.28 ~sQ2249_spl),
% 235.93/35.28 inference(contradiction_clause,[status(thm)],[f44929])).
% 235.93/35.28 fof(f45862,plain,(
% 235.93/35.28 set_difference(relation_rng(sK222_skl),sK221_skl)=empty_set),
% 235.93/35.28 inference(resolution,[status(thm)],[f4272,f1662])).
% 235.93/35.28 fof(f47802,definition,(
% 235.93/35.28 sQ2348_spl <=> (relation(set_difference(relation_rng(sK222_skl),sK221_skl)))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2348_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f47804,plain,(
% 235.93/35.28 ~relation(set_difference(relation_rng(sK222_skl),sK221_skl))|sQ2348_spl),
% 235.93/35.28 inference(component_clause,[status(thm)],[f47802])).
% 235.93/35.28 fof(f47815,plain,(
% 235.93/35.28 ~relation(empty_set)|sQ2348_spl),
% 235.93/35.28 inference(forward_demodulation,[status(thm)],[f45862,f47804])).
% 235.93/35.28 fof(f47816,plain,(
% 235.93/35.28 $false|sQ2348_spl),
% 235.93/35.28 inference(forward_subsumption_resolution,[status(thm)],[f47815,f945])).
% 235.93/35.28 fof(f47817,plain,(
% 235.93/35.28 sQ2348_spl),
% 235.93/35.28 inference(contradiction_clause,[status(thm)],[f47816])).
% 235.93/35.28 fof(f48389,definition,(
% 235.93/35.28 sQ2369_spl <=> (in(ordered_pair(sK217_skl(empty_set),sK218_skl(empty_set)),empty_set))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2369_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f48390,plain,(
% 235.93/35.28 in(ordered_pair(sK217_skl(empty_set),sK218_skl(empty_set)),empty_set)|~sQ2369_spl),
% 235.93/35.28 inference(component_clause,[status(thm)],[f48389])).
% 235.93/35.28 fof(f48393,plain,(
% 235.93/35.28 $false|~sQ2369_spl),
% 235.93/35.28 inference(forward_subsumption_resolution,[status(thm)],[f48390,f2187])).
% 235.93/35.28 fof(f48394,plain,(
% 235.93/35.28 ~sQ2369_spl),
% 235.93/35.28 inference(contradiction_clause,[status(thm)],[f48393])).
% 235.93/35.28 fof(f48444,plain,(
% 235.93/35.28 ![X0]: (~in(X0,sK220_skl)|~relation(sK222_skl)|in(X0,relation_dom(sK222_skl))|~sQ2098_spl)),
% 235.93/35.28 inference(resolution,[status(thm)],[f39846,f1528])).
% 235.93/35.28 fof(f48469,definition,(
% 235.93/35.28 ![X0]: (sQ2373_spl <=> (~in(X0,sK220_skl)|in(X0,relation_dom(sK222_skl))))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2373_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f48470,plain,(
% 235.93/35.28 ![X0]: (~in(X0,sK220_skl)|in(X0,relation_dom(sK222_skl))|~sQ2373_spl)),
% 235.93/35.28 inference(component_clause,[status(thm)],[f48469])).
% 235.93/35.28 fof(f48472,plain,(
% 235.93/35.28 sQ2373_spl|~sQ37_spl|~sQ2098_spl),
% 235.93/35.28 inference(split_clause,[status(thm)],[f48444,f48469,f2478,f39845])).
% 235.93/35.28 fof(f48477,definition,(
% 235.93/35.28 ![X0]: (sQ2375_spl <=> (~in(X0,sK220_skl)))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2375_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f48478,plain,(
% 235.93/35.28 ![X0]: (~in(X0,sK220_skl)|~sQ2375_spl)),
% 235.93/35.28 inference(component_clause,[status(thm)],[f48477])).
% 235.93/35.28 fof(f48522,plain,(
% 235.93/35.28 $false|~sQ2375_spl),
% 235.93/35.28 inference(backward_subsumption_resolution,[status(thm)],[f1828,f48478])).
% 235.93/35.28 fof(f50591,definition,(
% 235.93/35.28 ![X0]: (sQ2482_spl <=> (in(empty_set,set_intersection2(empty_set,X0))))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2482_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f50592,plain,(
% 235.93/35.28 ![X0]: (in(empty_set,set_intersection2(empty_set,X0))|~sQ2482_spl)),
% 235.93/35.28 inference(component_clause,[status(thm)],[f50591])).
% 235.93/35.28 fof(f50623,definition,(
% 235.93/35.28 ![X0]: (sQ2486_spl <=> (in(sK197_skl(X0,empty_set,empty_set),X0)))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2486_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f50624,plain,(
% 235.93/35.28 ![X0]: (in(sK197_skl(X0,empty_set,empty_set),X0)|~sQ2486_spl)),
% 235.93/35.28 inference(component_clause,[status(thm)],[f50623])).
% 235.93/35.28 fof(f50627,definition,(
% 235.93/35.28 ![X0]: (sQ2487_spl <=> (in(ordered_pair(empty_set,sK197_skl(X0,empty_set,empty_set)),empty_set)))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2487_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f50628,plain,(
% 235.93/35.28 ![X0]: (in(ordered_pair(empty_set,sK197_skl(X0,empty_set,empty_set)),empty_set)|~sQ2487_spl)),
% 235.93/35.28 inference(component_clause,[status(thm)],[f50627])).
% 235.93/35.28 fof(f50631,definition,(
% 235.93/35.28 ![X0]: (sQ2488_spl <=> (in(sK197_skl(X0,empty_set,empty_set),relation_rng(empty_set))))),
% 235.93/35.28 introduced(definition,[new_symbols(definition,[sQ2488_spl])],[split_symbol_definition])).
% 235.93/35.28 fof(f50632,plain,(
% 235.93/35.28 ![X0]: (in(sK197_skl(X0,empty_set,empty_set),relation_rng(empty_set))|~sQ2488_spl)),
% 235.93/35.28 inference(component_clause,[status(thm)],[f50631])).
% 235.93/35.28 fof(f50637,plain,(
% 235.93/35.29 ![X0]: (in(sK197_skl(X0,empty_set,empty_set),empty_set)|~sQ2488_spl)),
% 235.93/35.29 inference(forward_demodulation,[status(thm)],[f1792,f50632])).
% 235.93/35.29 fof(f50638,plain,(
% 235.93/35.29 $false|~sQ2488_spl),
% 235.93/35.29 inference(forward_subsumption_resolution,[status(thm)],[f50637,f2187])).
% 235.93/35.29 fof(f50639,plain,(
% 235.93/35.29 ~sQ2488_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f50638])).
% 235.93/35.29 fof(f50640,plain,(
% 235.93/35.29 $false|~sQ2487_spl),
% 235.93/35.29 inference(forward_subsumption_resolution,[status(thm)],[f50628,f2187])).
% 235.93/35.29 fof(f50641,plain,(
% 235.93/35.29 ~sQ2487_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f50640])).
% 235.93/35.29 fof(f50672,definition,(
% 235.93/35.29 ![X0]: (sQ2489_spl <=> (in(sK196_skl(X0,empty_set,empty_set),X0)))),
% 235.93/35.29 introduced(definition,[new_symbols(definition,[sQ2489_spl])],[split_symbol_definition])).
% 235.93/35.29 fof(f50673,plain,(
% 235.93/35.29 ![X0]: (in(sK196_skl(X0,empty_set,empty_set),X0)|~sQ2489_spl)),
% 235.93/35.29 inference(component_clause,[status(thm)],[f50672])).
% 235.93/35.29 fof(f50676,definition,(
% 235.93/35.29 ![X0]: (sQ2490_spl <=> (in(ordered_pair(sK196_skl(X0,empty_set,empty_set),empty_set),empty_set)))),
% 235.93/35.29 introduced(definition,[new_symbols(definition,[sQ2490_spl])],[split_symbol_definition])).
% 235.93/35.29 fof(f50677,plain,(
% 235.93/35.29 ![X0]: (in(ordered_pair(sK196_skl(X0,empty_set,empty_set),empty_set),empty_set)|~sQ2490_spl)),
% 235.93/35.29 inference(component_clause,[status(thm)],[f50676])).
% 235.93/35.29 fof(f50680,definition,(
% 235.93/35.29 ![X0]: (sQ2491_spl <=> (in(sK196_skl(X0,empty_set,empty_set),relation_dom(empty_set))))),
% 235.93/35.29 introduced(definition,[new_symbols(definition,[sQ2491_spl])],[split_symbol_definition])).
% 235.93/35.29 fof(f50681,plain,(
% 235.93/35.29 ![X0]: (in(sK196_skl(X0,empty_set,empty_set),relation_dom(empty_set))|~sQ2491_spl)),
% 235.93/35.29 inference(component_clause,[status(thm)],[f50680])).
% 235.93/35.29 fof(f50687,plain,(
% 235.93/35.29 ![X0]: (in(sK196_skl(X0,empty_set,empty_set),empty_set)|~sQ2491_spl)),
% 235.93/35.29 inference(forward_demodulation,[status(thm)],[f1791,f50681])).
% 235.93/35.29 fof(f50688,plain,(
% 235.93/35.29 $false|~sQ2491_spl),
% 235.93/35.29 inference(forward_subsumption_resolution,[status(thm)],[f50687,f2187])).
% 235.93/35.29 fof(f50689,plain,(
% 235.93/35.29 ~sQ2491_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f50688])).
% 235.93/35.29 fof(f50690,plain,(
% 235.93/35.29 $false|~sQ2490_spl),
% 235.93/35.29 inference(forward_subsumption_resolution,[status(thm)],[f50677,f2187])).
% 235.93/35.29 fof(f50691,plain,(
% 235.93/35.29 ~sQ2490_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f50690])).
% 235.93/35.29 fof(f50733,plain,(
% 235.93/35.29 ![X0]: (in(empty_set,set_intersection2(X0,empty_set))|~sQ2482_spl)),
% 235.93/35.29 inference(paramodulation,[status(thm)],[f411,f50592])).
% 235.93/35.29 fof(f50739,plain,(
% 235.93/35.29 in(empty_set,empty_set)|~sQ2482_spl),
% 235.93/35.29 inference(forward_demodulation,[status(thm)],[f1605,f50733])).
% 235.93/35.29 fof(f50740,plain,(
% 235.93/35.29 $false|~sQ2482_spl),
% 235.93/35.29 inference(forward_subsumption_resolution,[status(thm)],[f50739,f2187])).
% 235.93/35.29 fof(f50741,plain,(
% 235.93/35.29 ~sQ2482_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f50740])).
% 235.93/35.29 fof(f51066,plain,(
% 235.93/35.29 $false|~sQ2486_spl),
% 235.93/35.29 inference(resolution,[status(thm)],[f50624,f2187])).
% 235.93/35.29 fof(f51102,plain,(
% 235.93/35.29 ~sQ2486_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f51066])).
% 235.93/35.29 fof(f51164,plain,(
% 235.93/35.29 $false|~sQ2489_spl),
% 235.93/35.29 inference(resolution,[status(thm)],[f50673,f2187])).
% 235.93/35.29 fof(f51200,plain,(
% 235.93/35.29 ~sQ2489_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f51164])).
% 235.93/35.29 fof(f51887,definition,(
% 235.93/35.29 sQ2505_spl <=> (function(relation_image(empty_set,empty_set)))),
% 235.93/35.29 introduced(definition,[new_symbols(definition,[sQ2505_spl])],[split_symbol_definition])).
% 235.93/35.29 fof(f51889,plain,(
% 235.93/35.29 ~function(relation_image(empty_set,empty_set))|sQ2505_spl),
% 235.93/35.29 inference(component_clause,[status(thm)],[f51887])).
% 235.93/35.29 fof(f51896,plain,(
% 235.93/35.29 ~function(empty_set)|sQ2505_spl),
% 235.93/35.29 inference(forward_demodulation,[status(thm)],[f34483,f51889])).
% 235.93/35.29 fof(f51897,plain,(
% 235.93/35.29 $false|sQ2505_spl),
% 235.93/35.29 inference(forward_subsumption_resolution,[status(thm)],[f51896,f965])).
% 235.93/35.29 fof(f51898,plain,(
% 235.93/35.29 sQ2505_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f51897])).
% 235.93/35.29 fof(f52091,plain,(
% 235.93/35.29 ~sQ1293_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f43023])).
% 235.93/35.29 fof(f54791,plain,(
% 235.93/35.29 sK221_skl=empty_set|~sQ250_spl),
% 235.93/35.29 inference(resolution,[status(thm)],[f1932,f4605])).
% 235.93/35.29 fof(f54792,plain,(
% 235.93/35.29 sQ238_spl|~sQ250_spl),
% 235.93/35.29 inference(split_clause,[status(thm)],[f54791,f4362,f4604])).
% 235.93/35.29 fof(f54793,plain,(
% 235.93/35.29 ~sQ2375_spl),
% 235.93/35.29 inference(contradiction_clause,[status(thm)],[f48522])).
% 207.24/35.38 fof(f55482,plain,(
% 207.24/35.38 $false|~sQ1271_spl),
% 207.24/35.38 inference(backward_subsumption_resolution,[status(thm)],[f3577,f19386])).
% 207.24/35.38 fof(f55498,plain,(
% 207.24/35.38 ~sQ1271_spl),
% 207.24/35.38 inference(contradiction_clause,[status(thm)],[f55482])).
% 207.24/35.38 fof(f55566,definition,(
% 207.24/35.38 sQ2631_spl <=> (empty(relation_rng(relation_inverse(empty_set))))),
% 207.24/35.38 introduced(definition,[new_symbols(definition,[sQ2631_spl])],[split_symbol_definition])).
% 207.24/35.38 fof(f55568,plain,(
% 207.24/35.38 ~empty(relation_rng(relation_inverse(empty_set)))|sQ2631_spl),
% 207.24/35.38 inference(component_clause,[status(thm)],[f55566])).
% 207.24/35.38 fof(f55570,plain,(
% 207.24/35.38 ~empty(empty_set)|sQ2631_spl),
% 207.24/35.38 inference(forward_demodulation,[status(thm)],[f19140,f55568])).
% 207.24/35.38 fof(f55571,plain,(
% 207.24/35.38 $false|sQ2631_spl),
% 207.24/35.38 inference(forward_subsumption_resolution,[status(thm)],[f55570,f944])).
% 207.24/35.38 fof(f55572,plain,(
% 207.24/35.38 sQ2631_spl),
% 207.24/35.38 inference(contradiction_clause,[status(thm)],[f55571])).
% 207.24/35.38 fof(f55853,definition,(
% 207.24/35.38 sQ2647_spl <=> (in(apply(sK204_skl(relation_rng(sK118_skl)),empty_set),empty_set))),
% 207.24/35.38 introduced(definition,[new_symbols(definition,[sQ2647_spl])],[split_symbol_definition])).
% 207.24/35.38 fof(f55854,plain,(
% 207.24/35.38 in(apply(sK204_skl(relation_rng(sK118_skl)),empty_set),empty_set)|~sQ2647_spl),
% 207.24/35.38 inference(component_clause,[status(thm)],[f55853])).
% 207.24/35.38 fof(f55869,plain,(
% 207.24/35.38 $false|~sQ2647_spl),
% 207.24/35.38 inference(forward_subsumption_resolution,[status(thm)],[f55854,f2187])).
% 207.24/35.38 fof(f55870,plain,(
% 207.24/35.38 ~sQ2647_spl),
% 207.24/35.38 inference(contradiction_clause,[status(thm)],[f55869])).
% 207.24/35.38 fof(f56930,plain,(
% 207.24/35.38 in(sK223_skl,relation_dom(sK222_skl))|~sQ2373_spl),
% 207.24/35.38 inference(resolution,[status(thm)],[f1828,f48470])).
% 207.24/35.38 fof(f57024,plain,(
% 207.24/35.38 $false|sQ39_spl|~sQ2373_spl),
% 207.24/35.38 inference(forward_subsumption_resolution,[status(thm)],[f56930,f2486])).
% 207.24/35.38 fof(f57025,plain,(
% 207.24/35.38 sQ39_spl|~sQ2373_spl),
% 207.24/35.38 inference(contradiction_clause,[status(thm)],[f57024])).
% 207.24/35.38 fof(f57026,plain,(
% 207.24/35.38 $false),
% 207.24/35.38 inference(sat_refutation,[status(thm)],[f2487,f2555,f3581,f4372,f4679,f4686,f5369,f5432,f5763,f6208,f6310,f6830,f6840,f6925,f6935,f7140,f7444,f8330,f9700,f12223,f12240,f15167,f15621,f15751,f15894,f16060,f16331,f16967,f18648,f19217,f19883,f20164,f20610,f20699,f21563,f21739,f21786,f22224,f22339,f22778,f23093,f23258,f24229,f26571,f27087,f27346,f27506,f27927,f30207,f31972,f31974,f31976,f31978,f31980,f31982,f31984,f32302,f32304,f32306,f32308,f32310,f32312,f32314,f33869,f33871,f36272,f36979,f37499,f39502,f39505,f39848,f40023,f41095,f41097,f41099,f41150,f41685,f41834,f41929,f44626,f44930,f47817,f48394,f48472,f50639,f50641,f50689,f50691,f50741,f51102,f51200,f51898,f52091,f54792,f54793,f55498,f55572,f55870,f57025])).
% 207.24/35.38 % SZS output end CNFRefutation for theBenchmark.p
% 15.16/35.44 % Elapsed time: 29.995108 seconds
% 15.16/35.44 % CPU time: 237.114224 seconds
% 15.16/35.44 % Total memory used: 1.110 GB
% 15.16/35.44 % Net memory used: 1.003 GB
%------------------------------------------------------------------------------