%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU225+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:22:03 PM UTC 2026
% Result : Theorem 111.06s 14.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU225+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:00:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 111.06/14.50 % Refutation found
% 111.06/14.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 111.06/14.50 % SZS output start CNFRefutation for theBenchmark
% 111.06/14.50 fof(f3,axiom,(
% 111.06/14.50 (! [A] :( empty(A)=> function(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f4,axiom,(
% 111.06/14.50 (! [A] :( empty(A)=> relation(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f16,axiom,(
% 111.06/14.50 (! [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 ) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f18,axiom,(
% 111.06/14.50 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f21,axiom,(
% 111.06/14.50 (! [A,B] :( ( ~ empty(A)=> ( element(B,A)<=> in(B,A) ) )& ( empty(A)=> ( element(B,A)<=> empty(B) ) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f28,axiom,(
% 111.06/14.50 (! [A] :( ( relation(A)& function(A) )=> (! [B,C] :( ( in(B,relation_dom(A))=> ( C = apply(A,B)<=> in(ordered_pair(B,C),A) ) )& ( ~ in(B,relation_dom(A))=> ( C = apply(A,B)<=> C = empty_set ) ) ) )) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f30,axiom,(
% 111.06/14.50 (! [A] : cast_to_subset(A) = A )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f53,axiom,(
% 111.06/14.50 (! [A] : element(cast_to_subset(A),powerset(A)) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f61,axiom,(
% 111.06/14.50 (! [A] :( relation(A)=> relation(relation_inverse(A)) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f66,axiom,(
% 111.06/14.50 (! [A] : relation(identity_relation(A)) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f69,axiom,(
% 111.06/14.50 (! [A,B] :( relation(A)=> relation(relation_dom_restriction(A,B)) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f76,axiom,(
% 111.06/14.50 (! [A] :( empty(A)=> ( empty(relation_inverse(A))& relation(relation_inverse(A)) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f77,axiom,(
% 111.06/14.50 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f81,axiom,(
% 111.06/14.50 (! [A] : ~ empty(powerset(A)) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f91,axiom,(
% 111.06/14.50 (! [A,B] :( ( relation(A)& function(A) )=> ( relation(relation_dom_restriction(A,B))& function(relation_dom_restriction(A,B)) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f105,lemma,(
% 111.06/14.50 (! [A] : singleton(A) != empty_set )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f118,axiom,(
% 111.06/14.50 (? [A] :( relation(A)& function(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f119,axiom,(
% 111.06/14.50 (? [A] :( empty(A)& relation(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f121,axiom,(
% 111.06/14.50 (? [A] : empty(A) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f122,axiom,(
% 111.06/14.50 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f123,axiom,(
% 111.06/14.50 (? [A] :( ~ empty(A)& relation(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f126,axiom,(
% 111.06/14.50 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f127,axiom,(
% 111.06/14.50 (? [A] :( relation(A)& relation_empty_yielding(A) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f171,lemma,(
% 111.06/14.50 (! [A] : subset(empty_set,A) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f210,lemma,(
% 111.06/14.50 ( relation_dom(empty_set) = empty_set& relation_rng(empty_set) = empty_set ) ),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f219,axiom,(
% 111.06/14.50 (! [A] :( empty(A)=> A = empty_set ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f221,lemma,(
% 111.06/14.50 (! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,relation_dom(relation_dom_restriction(C,A)))=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f223,conjecture,(
% 111.06/14.50 (! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,A)=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f224,negated_conjecture,(
% 111.06/14.50 ~((! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,A)=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) ))),
% 111.06/14.50 inference(negated_conjecture,[status(cth)],[f223])).
% 111.06/14.50 fof(f229,lemma,(
% 111.06/14.50 (! [A,B,C] :( relation(C)=> ( in(A,relation_dom(relation_dom_restriction(C,B)))<=> ( in(A,B)& in(A,relation_dom(C)) ) ) ) )),
% 111.06/14.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 111.06/14.50 fof(f246,plain,(
% 111.06/14.50 ![A]: (~empty(A)|function(A))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 111.06/14.50 fof(f247,plain,(
% 111.06/14.50 ![X0]: (~empty(X0)|function(X0))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f246])).
% 111.06/14.50 fof(f248,plain,(
% 111.06/14.50 ![A]: (~empty(A)|relation(A))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 111.06/14.50 fof(f249,plain,(
% 111.06/14.50 ![X0]: (~empty(X0)|relation(X0))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f248])).
% 111.06/14.50 fof(f319,plain,(
% 111.06/14.50 ![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)))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 111.06/14.50 fof(f320,plain,(
% 111.06/14.50 ![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))))),
% 111.06/14.50 inference(NNF_transformation,[status(thm)],[f319])).
% 111.06/14.50 fof(f321,plain,(
% 111.06/14.50 (![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)))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f320])).
% 111.06/14.50 fof(f322,plain,(
% 111.06/14.50 (![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(sK15_skl(C,B,A),A)&~in(C,sK15_skl(C,B,A))))))))&(![B]: (B=set_meet(A)|((~in(sK16_skl(B,A),B)|(in(sK17_skl(B,A),A)&~in(sK16_skl(B,A),sK17_skl(B,A))))&(in(sK16_skl(B,A),B)|(![D]: (~in(D,A)|in(sK16_skl(B,A),D))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(D,sK15_skl(C,B,A)),skolemize(C,sK16_skl(B,A)),skolemize(D,sK17_skl(B,A))],[f321])).
% 111.06/14.50 fof(f329,plain,(
% 111.06/14.50 ![X0,X1]: (~X0=empty_set|~X1=set_meet(X0)|X1=empty_set)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f322])).
% 111.06/14.50 fof(f338,plain,(
% 111.06/14.50 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 111.06/14.50 inference(NNF_transformation,[status(thm)],[f18])).
% 111.06/14.50 fof(f339,plain,(
% 111.06/14.50 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f338])).
% 111.06/14.50 fof(f340,plain,(
% 111.06/14.50 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK19_skl(A),A)))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(B,sK19_skl(A))],[f339])).
% 111.06/14.50 fof(f341,plain,(
% 111.06/14.50 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f340])).
% 111.06/14.50 fof(f358,plain,(
% 111.06/14.50 ![A,B]: ((empty(A)|(element(B,A)<=>in(B,A)))&(~empty(A)|(element(B,A)<=>empty(B))))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 111.06/14.50 fof(f359,plain,(
% 111.06/14.50 ![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)))))),
% 111.06/14.50 inference(NNF_transformation,[status(thm)],[f358])).
% 111.06/14.50 fof(f360,plain,(
% 111.06/14.50 (![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))))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f359])).
% 111.06/14.50 fof(f361,plain,(
% 111.06/14.50 ![X0,X1]: (empty(X0)|~element(X1,X0)|in(X1,X0))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f360])).
% 111.06/14.50 fof(f414,plain,(
% 111.06/14.50 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|(C=apply(A,B)<=>in(ordered_pair(B,C),A)))&(in(B,relation_dom(A))|(C=apply(A,B)<=>C=empty_set)))))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 111.06/14.50 fof(f415,plain,(
% 111.06/14.50 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|((~C=apply(A,B)|in(ordered_pair(B,C),A))&(C=apply(A,B)|~in(ordered_pair(B,C),A))))&(in(B,relation_dom(A))|((~C=apply(A,B)|C=empty_set)&(C=apply(A,B)|~C=empty_set))))))),
% 111.06/14.50 inference(NNF_transformation,[status(thm)],[f414])).
% 111.06/14.50 fof(f416,plain,(
% 111.06/14.50 ![A]: ((~relation(A)|~function(A))|((![B]: (~in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|in(ordered_pair(B,C),A)))&(![C]: (C=apply(A,B)|~in(ordered_pair(B,C),A))))))&(![B]: (in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|C=empty_set))&(![C]: (C=apply(A,B)|~C=empty_set)))))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f415])).
% 111.06/14.50 fof(f419,plain,(
% 111.06/14.50 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|~X2=apply(X0,X1)|X2=empty_set)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f416])).
% 111.06/14.50 fof(f429,plain,(
% 111.06/14.50 ![X0]: (cast_to_subset(X0)=X0)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f30])).
% 111.06/14.50 fof(f509,plain,(
% 111.06/14.50 ![X0]: (element(cast_to_subset(X0),powerset(X0)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f53])).
% 111.06/14.50 fof(f512,plain,(
% 111.06/14.50 ![A]: (~relation(A)|relation(relation_inverse(A)))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 111.06/14.50 fof(f513,plain,(
% 111.06/14.50 ![X0]: (~relation(X0)|relation(relation_inverse(X0)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f512])).
% 111.06/14.50 fof(f518,plain,(
% 111.06/14.50 ![X0]: (relation(identity_relation(X0)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f66])).
% 111.06/14.50 fof(f523,plain,(
% 111.06/14.50 ![A,B]: (~relation(A)|relation(relation_dom_restriction(A,B)))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 111.06/14.50 fof(f524,plain,(
% 111.06/14.50 ![A]: (~relation(A)|(![B]: relation(relation_dom_restriction(A,B))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f523])).
% 111.06/14.50 fof(f525,plain,(
% 111.06/14.50 ![X0,X1]: (~relation(X0)|relation(relation_dom_restriction(X0,X1)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f524])).
% 111.06/14.50 fof(f536,plain,(
% 111.06/14.50 ![A]: (~empty(A)|(empty(relation_inverse(A))&relation(relation_inverse(A))))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 111.06/14.50 fof(f537,plain,(
% 111.06/14.50 ![X0]: (~empty(X0)|empty(relation_inverse(X0)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f536])).
% 111.06/14.50 fof(f539,plain,(
% 111.06/14.50 empty(empty_set)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f77])).
% 111.06/14.50 fof(f540,plain,(
% 111.06/14.50 relation(empty_set)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f77])).
% 111.06/14.50 fof(f551,plain,(
% 111.06/14.50 ![X0]: (~empty(powerset(X0)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f81])).
% 111.06/14.50 fof(f570,plain,(
% 111.06/14.50 ![A,B]: ((~relation(A)|~function(A))|(relation(relation_dom_restriction(A,B))&function(relation_dom_restriction(A,B))))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 111.06/14.50 fof(f571,plain,(
% 111.06/14.50 ![A]: ((~relation(A)|~function(A))|((![B]: relation(relation_dom_restriction(A,B)))&(![B]: function(relation_dom_restriction(A,B)))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f570])).
% 111.06/14.50 fof(f573,plain,(
% 111.06/14.50 ![X0,X1]: (~relation(X0)|~function(X0)|function(relation_dom_restriction(X0,X1)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f571])).
% 111.06/14.50 fof(f603,plain,(
% 111.06/14.50 ![X0]: (~singleton(X0)=empty_set)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f105])).
% 111.06/14.50 fof(f645,plain,(
% 111.06/14.50 (relation(sK55_skl)&function(sK55_skl))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(A,sK55_skl)],[f118])).
% 111.06/14.50 fof(f646,plain,(
% 111.06/14.50 relation(sK55_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f645])).
% 111.06/14.50 fof(f648,plain,(
% 111.06/14.50 (empty(sK56_skl)&relation(sK56_skl))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl]),skolemize(A,sK56_skl)],[f119])).
% 111.06/14.50 fof(f649,plain,(
% 111.06/14.50 empty(sK56_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f648])).
% 111.06/14.50 fof(f650,plain,(
% 111.06/14.50 relation(sK56_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f648])).
% 111.06/14.50 fof(f655,plain,(
% 111.06/14.50 empty(sK58_skl)),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK58_skl]),skolemize(A,sK58_skl)],[f121])).
% 111.06/14.50 fof(f656,plain,(
% 111.06/14.50 empty(sK58_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f655])).
% 111.06/14.50 fof(f657,plain,(
% 111.06/14.50 ((relation(sK59_skl)&empty(sK59_skl))&function(sK59_skl))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK59_skl]),skolemize(A,sK59_skl)],[f122])).
% 111.06/14.50 fof(f659,plain,(
% 111.06/14.50 empty(sK59_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f657])).
% 111.06/14.50 fof(f661,plain,(
% 111.06/14.50 (~empty(sK60_skl)&relation(sK60_skl))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK60_skl]),skolemize(A,sK60_skl)],[f123])).
% 111.06/14.50 fof(f663,plain,(
% 111.06/14.50 relation(sK60_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f661])).
% 111.06/14.50 fof(f669,plain,(
% 111.06/14.50 ((relation(sK63_skl)&function(sK63_skl))&one_to_one(sK63_skl))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK63_skl]),skolemize(A,sK63_skl)],[f126])).
% 111.06/14.50 fof(f670,plain,(
% 111.06/14.50 relation(sK63_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f669])).
% 111.06/14.50 fof(f673,plain,(
% 111.06/14.50 (relation(sK64_skl)&relation_empty_yielding(sK64_skl))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK64_skl]),skolemize(A,sK64_skl)],[f127])).
% 111.06/14.50 fof(f674,plain,(
% 111.06/14.50 relation(sK64_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f673])).
% 111.06/14.50 fof(f809,plain,(
% 111.06/14.50 ![X0]: (subset(empty_set,X0))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f171])).
% 111.06/14.50 fof(f930,plain,(
% 111.06/14.50 relation_dom(empty_set)=empty_set),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f210])).
% 111.06/14.50 fof(f931,plain,(
% 111.06/14.50 relation_rng(empty_set)=empty_set),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f210])).
% 111.06/14.50 fof(f959,plain,(
% 111.06/14.50 ![A]: (~empty(A)|A=empty_set)),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f219])).
% 111.06/14.50 fof(f960,plain,(
% 111.06/14.50 ![X0]: (~empty(X0)|X0=empty_set)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f959])).
% 111.06/14.50 fof(f963,plain,(
% 111.06/14.50 ![A,B,C]: ((~relation(C)|~function(C))|(~in(B,relation_dom(relation_dom_restriction(C,A)))|apply(relation_dom_restriction(C,A),B)=apply(C,B)))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f221])).
% 111.06/14.50 fof(f964,plain,(
% 111.06/14.50 ![C]: ((~relation(C)|~function(C))|(![A,B]: (~in(B,relation_dom(relation_dom_restriction(C,A)))|apply(relation_dom_restriction(C,A),B)=apply(C,B))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f963])).
% 111.06/14.50 fof(f965,plain,(
% 111.06/14.50 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(relation_dom_restriction(X0,X2)))|apply(relation_dom_restriction(X0,X2),X1)=apply(X0,X1))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f964])).
% 111.06/14.50 fof(f969,plain,(
% 111.06/14.50 (?[A,B,C]: ((relation(C)&function(C))&(in(B,A)&~apply(relation_dom_restriction(C,A),B)=apply(C,B))))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f224])).
% 111.06/14.50 fof(f970,plain,(
% 111.06/14.50 ?[C]: ((relation(C)&function(C))&(?[A,B]: (in(B,A)&~apply(relation_dom_restriction(C,A),B)=apply(C,B))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f969])).
% 111.06/14.50 fof(f971,plain,(
% 111.06/14.50 ((relation(sK79_skl)&function(sK79_skl))&(in(sK81_skl,sK80_skl)&~apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=apply(sK79_skl,sK81_skl)))),
% 111.06/14.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK79_skl,sK80_skl,sK81_skl]),skolemize(C,sK79_skl),skolemize(A,sK80_skl),skolemize(B,sK81_skl)],[f970])).
% 111.06/14.50 fof(f972,plain,(
% 111.06/14.50 relation(sK79_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f971])).
% 111.06/14.50 fof(f973,plain,(
% 111.06/14.50 function(sK79_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f971])).
% 111.06/14.50 fof(f974,plain,(
% 111.06/14.50 in(sK81_skl,sK80_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f971])).
% 111.06/14.50 fof(f975,plain,(
% 111.06/14.50 ~apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=apply(sK79_skl,sK81_skl)),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f971])).
% 111.06/14.50 fof(f990,plain,(
% 111.06/14.50 ![A,B,C]: (~relation(C)|(in(A,relation_dom(relation_dom_restriction(C,B)))<=>(in(A,B)&in(A,relation_dom(C)))))),
% 111.06/14.50 inference(pre_NNF_transformation,[status(thm)],[f229])).
% 111.06/14.50 fof(f991,plain,(
% 111.06/14.50 ![A,B,C]: (~relation(C)|((~in(A,relation_dom(relation_dom_restriction(C,B)))|(in(A,B)&in(A,relation_dom(C))))&(in(A,relation_dom(relation_dom_restriction(C,B)))|(~in(A,B)|~in(A,relation_dom(C))))))),
% 111.06/14.50 inference(NNF_transformation,[status(thm)],[f990])).
% 111.06/14.50 fof(f992,plain,(
% 111.06/14.50 ![C]: (~relation(C)|((![A,B]: (~in(A,relation_dom(relation_dom_restriction(C,B)))|(in(A,B)&in(A,relation_dom(C)))))&(![A,B]: (in(A,relation_dom(relation_dom_restriction(C,B)))|(~in(A,B)|~in(A,relation_dom(C)))))))),
% 111.06/14.50 inference(miniscoping,[status(thm)],[f991])).
% 111.06/14.50 fof(f995,plain,(
% 111.06/14.50 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(relation_dom_restriction(X0,X2)))|~in(X1,X2)|~in(X1,relation_dom(X0)))),
% 111.06/14.50 inference(cnf_transformation,[status(thm)],[f992])).
% 111.06/14.50 fof(f1069,plain,(
% 111.06/14.50 set_meet(empty_set)=empty_set),
% 111.06/14.50 inference(destructive_equality_resolution,[status(thm)],[f329])).
% 111.06/14.50 fof(f1073,plain,(
% 111.06/14.50 ![X0]: (~in(X0,empty_set))),
% 111.06/14.50 inference(destructive_equality_resolution,[status(thm)],[f341])).
% 111.06/14.50 fof(f1088,plain,(
% 111.06/14.50 ![X0,X1]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|apply(X0,X1)=empty_set)),
% 111.06/14.50 inference(destructive_equality_resolution,[status(thm)],[f419])).
% 111.06/14.50 fof(f1130,plain,(
% 111.06/14.50 ![X0]: (~function(sK79_skl)|in(X0,relation_dom(sK79_skl))|apply(sK79_skl,X0)=empty_set)),
% 111.06/14.50 inference(resolution,[status(thm)],[f1088,f972])).
% 111.06/14.50 fof(f1131,definition,(
% 111.06/14.50 sQ0_spl <=> (function(sK79_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1133,plain,(
% 111.06/14.50 ~function(sK79_skl)|sQ0_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1131])).
% 111.06/14.50 fof(f1134,definition,(
% 111.06/14.50 ![X0]: (sQ1_spl <=> (in(X0,relation_dom(sK79_skl))|apply(sK79_skl,X0)=empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1135,plain,(
% 111.06/14.50 ![X0]: (in(X0,relation_dom(sK79_skl))|apply(sK79_skl,X0)=empty_set|~sQ1_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1134])).
% 111.06/14.50 fof(f1137,plain,(
% 111.06/14.50 ~sQ0_spl|sQ1_spl),
% 111.06/14.50 inference(split_clause,[status(thm)],[f1130,f1131,f1134])).
% 111.06/14.50 fof(f1138,plain,(
% 111.06/14.50 $false|sQ0_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f1133,f973])).
% 111.06/14.50 fof(f1139,plain,(
% 111.06/14.50 sQ0_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f1138])).
% 111.06/14.50 fof(f1165,definition,(
% 111.06/14.50 sQ7_spl <=> (function(empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1167,plain,(
% 111.06/14.50 ~function(empty_set)|sQ7_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1165])).
% 111.06/14.50 fof(f1181,definition,(
% 111.06/14.50 sQ11_spl <=> (function(sK56_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1183,plain,(
% 111.06/14.50 ~function(sK56_skl)|sQ11_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1181])).
% 111.06/14.50 fof(f1232,definition,(
% 111.06/14.50 sQ22_spl <=> (relation(sK79_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1234,plain,(
% 111.06/14.50 ~relation(sK79_skl)|sQ22_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1232])).
% 111.06/14.50 fof(f1239,plain,(
% 111.06/14.50 $false|sQ22_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f1234,f972])).
% 111.06/14.50 fof(f1240,plain,(
% 111.06/14.50 sQ22_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f1239])).
% 111.06/14.50 fof(f1302,definition,(
% 111.06/14.50 sQ38_spl <=> (function(relation_dom(sK59_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1304,plain,(
% 111.06/14.50 ~function(relation_dom(sK59_skl))|sQ38_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1302])).
% 111.06/14.50 fof(f1358,plain,(
% 111.06/14.50 ![X0,X1]: (~relation(sK79_skl)|in(X0,relation_dom(relation_dom_restriction(sK79_skl,X1)))|~in(X0,X1)|apply(sK79_skl,X0)=empty_set|~sQ1_spl)),
% 111.06/14.50 inference(resolution,[status(thm)],[f995,f1135])).
% 111.06/14.50 fof(f1371,definition,(
% 111.06/14.50 ![X0,X1]: (sQ54_spl <=> (in(X0,relation_dom(relation_dom_restriction(sK79_skl,X1)))|~in(X0,X1)|apply(sK79_skl,X0)=empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1372,plain,(
% 111.06/14.50 ![X0,X1]: (in(X0,relation_dom(relation_dom_restriction(sK79_skl,X1)))|~in(X0,X1)|apply(sK79_skl,X0)=empty_set|~sQ54_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1371])).
% 111.06/14.50 fof(f1374,plain,(
% 111.06/14.50 ~sQ22_spl|sQ54_spl|~sQ1_spl),
% 111.06/14.50 inference(split_clause,[status(thm)],[f1358,f1232,f1371,f1134])).
% 111.06/14.50 fof(f1430,plain,(
% 111.06/14.50 in(sK81_skl,relation_dom(relation_dom_restriction(sK79_skl,sK80_skl)))|apply(sK79_skl,sK81_skl)=empty_set|~sQ54_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f1372,f974])).
% 111.06/14.50 fof(f1435,definition,(
% 111.06/14.50 sQ58_spl <=> (in(sK81_skl,relation_dom(relation_dom_restriction(sK79_skl,sK80_skl))))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1436,plain,(
% 111.06/14.50 in(sK81_skl,relation_dom(relation_dom_restriction(sK79_skl,sK80_skl)))|~sQ58_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1435])).
% 111.06/14.50 fof(f1437,plain,(
% 111.06/14.50 ~in(sK81_skl,relation_dom(relation_dom_restriction(sK79_skl,sK80_skl)))|sQ58_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1435])).
% 111.06/14.50 fof(f1438,definition,(
% 111.06/14.50 sQ59_spl <=> (apply(sK79_skl,sK81_skl)=empty_set)),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1439,plain,(
% 111.06/14.50 apply(sK79_skl,sK81_skl)=empty_set|~sQ59_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1438])).
% 111.06/14.50 fof(f1441,plain,(
% 111.06/14.50 sQ58_spl|sQ59_spl|~sQ54_spl),
% 111.06/14.50 inference(split_clause,[status(thm)],[f1430,f1435,f1438,f1371])).
% 111.06/14.50 fof(f1467,plain,(
% 111.06/14.50 ~relation(sK79_skl)|~function(sK79_skl)|apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=apply(sK79_skl,sK81_skl)|~sQ58_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f1436,f965])).
% 111.06/14.50 fof(f1475,definition,(
% 111.06/14.50 sQ64_spl <=> (apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=apply(sK79_skl,sK81_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1476,plain,(
% 111.06/14.50 apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=apply(sK79_skl,sK81_skl)|~sQ64_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1475])).
% 111.06/14.50 fof(f1478,plain,(
% 111.06/14.50 ~sQ22_spl|~sQ0_spl|sQ64_spl|~sQ58_spl),
% 111.06/14.50 inference(split_clause,[status(thm)],[f1467,f1232,f1131,f1475,f1435])).
% 111.06/14.50 fof(f1483,definition,(
% 111.06/14.50 sQ66_spl <=> (in(sK81_skl,sK80_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1485,plain,(
% 111.06/14.50 ~in(sK81_skl,sK80_skl)|sQ66_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1483])).
% 111.06/14.50 fof(f1487,definition,(
% 111.06/14.50 sQ67_spl <=> (relation(relation_dom_restriction(sK79_skl,sK80_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1489,plain,(
% 111.06/14.50 ~relation(relation_dom_restriction(sK79_skl,sK80_skl))|sQ67_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1487])).
% 111.06/14.50 fof(f1494,definition,(
% 111.06/14.50 sQ69_spl <=> (function(relation_dom_restriction(sK79_skl,sK80_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f1496,plain,(
% 111.06/14.50 ~function(relation_dom_restriction(sK79_skl,sK80_skl))|sQ69_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f1494])).
% 111.06/14.50 fof(f1505,plain,(
% 111.06/14.50 $false|~sQ64_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f1476,f975])).
% 111.06/14.50 fof(f1506,plain,(
% 111.06/14.50 ~sQ64_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f1505])).
% 111.06/14.50 fof(f1507,plain,(
% 111.06/14.50 ~apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=empty_set|~sQ59_spl),
% 111.06/14.50 inference(backward_demodulation,[status(thm)],[f1439,f975])).
% 111.06/14.50 fof(f2160,plain,(
% 111.06/14.50 function(empty_set)),
% 111.06/14.50 inference(resolution,[status(thm)],[f539,f247])).
% 111.06/14.50 fof(f2161,plain,(
% 111.06/14.50 $false|sQ7_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f2160,f1167])).
% 111.06/14.50 fof(f2162,plain,(
% 111.06/14.50 sQ7_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f2161])).
% 111.06/14.50 fof(f2170,definition,(
% 111.06/14.50 sQ160_spl <=> (relation(empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f2172,plain,(
% 111.06/14.50 ~relation(empty_set)|sQ160_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f2170])).
% 111.06/14.50 fof(f2201,plain,(
% 111.06/14.50 $false|sQ160_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f2172,f540])).
% 111.06/14.50 fof(f2202,plain,(
% 111.06/14.50 sQ160_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f2201])).
% 111.06/14.50 fof(f2204,plain,(
% 111.06/14.50 function(sK56_skl)),
% 111.06/14.50 inference(resolution,[status(thm)],[f649,f247])).
% 111.06/14.50 fof(f2205,plain,(
% 111.06/14.50 $false|sQ11_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f2204,f1183])).
% 111.06/14.50 fof(f2206,plain,(
% 111.06/14.50 sQ11_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f2205])).
% 111.06/14.50 fof(f2214,definition,(
% 111.06/14.50 sQ168_spl <=> (relation(sK56_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f2216,plain,(
% 111.06/14.50 ~relation(sK56_skl)|sQ168_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f2214])).
% 111.06/14.50 fof(f2245,plain,(
% 111.06/14.50 $false|sQ168_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f2216,f650])).
% 111.06/14.50 fof(f2246,plain,(
% 111.06/14.50 sQ168_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f2245])).
% 111.06/14.50 fof(f2319,plain,(
% 111.06/14.50 relation(sK58_skl)),
% 111.06/14.50 inference(resolution,[status(thm)],[f656,f249])).
% 111.06/14.50 fof(f2320,plain,(
% 111.06/14.50 function(sK58_skl)),
% 111.06/14.50 inference(resolution,[status(thm)],[f656,f247])).
% 111.06/14.50 fof(f2326,definition,(
% 111.06/14.50 sQ192_spl <=> (function(sK58_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f2328,plain,(
% 111.06/14.50 ~function(sK58_skl)|sQ192_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f2326])).
% 111.06/14.50 fof(f2401,definition,(
% 111.06/14.50 sQ194_spl <=> (relation(sK58_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f2403,plain,(
% 111.06/14.50 ~relation(sK58_skl)|sQ194_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f2401])).
% 111.06/14.50 fof(f2427,plain,(
% 111.06/14.50 $false|sQ194_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f2403,f2319])).
% 111.06/14.50 fof(f2428,plain,(
% 111.06/14.50 sQ194_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f2427])).
% 111.06/14.50 fof(f2661,plain,(
% 111.06/14.50 $false|sQ192_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f2320,f2328])).
% 111.06/14.50 fof(f2662,plain,(
% 111.06/14.50 sQ192_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f2661])).
% 111.06/14.50 fof(f3122,definition,(
% 111.06/14.50 sQ296_spl <=> (subset(sK58_skl,sK79_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f3124,plain,(
% 111.06/14.50 ~subset(sK58_skl,sK79_skl)|sQ296_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f3122])).
% 111.06/14.50 fof(f3549,definition,(
% 111.06/14.50 sQ317_spl <=> (relation(sK64_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f3551,plain,(
% 111.06/14.50 ~relation(sK64_skl)|sQ317_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f3549])).
% 111.06/14.50 fof(f3627,plain,(
% 111.06/14.50 $false|sQ317_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f3551,f674])).
% 111.06/14.50 fof(f3628,plain,(
% 111.06/14.50 sQ317_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f3627])).
% 111.06/14.50 fof(f7105,plain,(
% 111.06/14.50 sK59_skl=empty_set),
% 111.06/14.50 inference(resolution,[status(thm)],[f960,f659])).
% 111.06/14.50 fof(f7106,plain,(
% 111.06/14.50 sK58_skl=empty_set),
% 111.06/14.50 inference(resolution,[status(thm)],[f960,f656])).
% 111.06/14.50 fof(f7136,plain,(
% 111.06/14.50 ~function(relation_dom(empty_set))|sQ38_spl),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f7105,f1304])).
% 111.06/14.50 fof(f7137,plain,(
% 111.06/14.50 ~function(empty_set)|sQ38_spl),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f930,f7136])).
% 111.06/14.50 fof(f7138,plain,(
% 111.06/14.50 $false|sQ38_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f7137,f2160])).
% 111.06/14.50 fof(f7139,plain,(
% 111.06/14.50 sQ38_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f7138])).
% 111.06/14.50 fof(f7157,plain,(
% 111.06/14.50 ~subset(empty_set,sK79_skl)|sQ296_spl),
% 111.06/14.50 inference(backward_demodulation,[status(thm)],[f7106,f3124])).
% 111.06/14.50 fof(f7167,plain,(
% 111.06/14.50 $false|sQ296_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f7157,f809])).
% 111.06/14.50 fof(f7168,plain,(
% 111.06/14.50 sQ296_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f7167])).
% 111.06/14.50 fof(f8089,definition,(
% 111.06/14.50 ![X0]: (sQ431_spl <=> (~subset(empty_set,X0)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f8090,plain,(
% 111.06/14.50 ![X0]: (~subset(empty_set,X0)|~sQ431_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f8089])).
% 111.06/14.50 fof(f8103,definition,(
% 111.06/14.50 ![X0]: (sQ434_spl <=> (~relation(X0)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f8104,plain,(
% 111.06/14.50 ![X0]: (~relation(X0)|~sQ434_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f8103])).
% 111.06/14.50 fof(f8267,definition,(
% 111.06/14.50 ![X0]: (sQ441_spl <=> (~subset(X0,empty_set)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f8268,plain,(
% 111.06/14.50 ![X0]: (~subset(X0,empty_set)|~sQ441_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f8267])).
% 111.06/14.50 fof(f8381,plain,(
% 111.06/14.50 ~relation(sK79_skl)|sQ67_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f1489,f525])).
% 111.06/14.50 fof(f8382,plain,(
% 111.06/14.50 ~sQ22_spl|sQ67_spl),
% 111.06/14.50 inference(split_clause,[status(thm)],[f8381,f1232,f1487])).
% 111.06/14.50 fof(f8415,plain,(
% 111.06/14.50 $false|~sQ441_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f8268,f809])).
% 111.06/14.50 fof(f8424,plain,(
% 111.06/14.50 ~sQ441_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f8415])).
% 111.06/14.50 fof(f8750,plain,(
% 111.06/14.50 ~relation(sK79_skl)|~function(sK79_skl)|sQ69_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f1496,f573])).
% 111.06/14.50 fof(f8751,plain,(
% 111.06/14.50 ~sQ22_spl|~sQ0_spl|sQ69_spl),
% 111.06/14.50 inference(split_clause,[status(thm)],[f8750,f1232,f1131,f1494])).
% 111.06/14.50 fof(f9278,plain,(
% 111.06/14.50 ![X0]: (element(X0,powerset(X0)))),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f429,f509])).
% 111.06/14.50 fof(f9279,plain,(
% 111.06/14.50 relation(relation_inverse(sK79_skl))),
% 111.06/14.50 inference(resolution,[status(thm)],[f513,f972])).
% 111.06/14.50 fof(f9280,plain,(
% 111.06/14.50 ![X0]: (relation(relation_inverse(identity_relation(X0))))),
% 111.06/14.50 inference(resolution,[status(thm)],[f513,f518])).
% 111.06/14.50 fof(f9286,plain,(
% 111.06/14.50 relation(relation_inverse(sK64_skl))),
% 111.06/14.50 inference(resolution,[status(thm)],[f513,f674])).
% 111.06/14.50 fof(f9287,plain,(
% 111.06/14.50 relation(relation_inverse(sK63_skl))),
% 111.06/14.50 inference(resolution,[status(thm)],[f513,f670])).
% 111.06/14.50 fof(f9288,plain,(
% 111.06/14.50 relation(relation_inverse(sK60_skl))),
% 111.06/14.50 inference(resolution,[status(thm)],[f513,f663])).
% 111.06/14.50 fof(f9289,plain,(
% 111.06/14.50 relation(relation_inverse(sK55_skl))),
% 111.06/14.50 inference(resolution,[status(thm)],[f513,f646])).
% 111.06/14.50 fof(f9571,definition,(
% 111.06/14.50 ![X0]: (sQ473_spl <=> (in(X0,set_meet(empty_set))))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ473_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f9572,plain,(
% 111.06/14.50 ![X0]: (in(X0,set_meet(empty_set))|~sQ473_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f9571])).
% 111.06/14.50 fof(f9575,definition,(
% 111.06/14.50 ![X0]: (sQ474_spl <=> (in(X0,set_meet(empty_set))|in(sK15_skl(X0,empty_set,empty_set),empty_set)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f9576,plain,(
% 111.06/14.50 ![X0]: (in(X0,set_meet(empty_set))|in(sK15_skl(X0,empty_set,empty_set),empty_set)|~sQ474_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f9575])).
% 111.06/14.50 fof(f9579,plain,(
% 111.06/14.50 ![X0]: (in(X0,empty_set)|in(sK15_skl(X0,empty_set,empty_set),empty_set)|~sQ474_spl)),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f1069,f9576])).
% 111.06/14.50 fof(f9580,plain,(
% 111.06/14.50 ![X0]: (in(sK15_skl(X0,empty_set,empty_set),empty_set)|~sQ474_spl)),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f9579,f1073])).
% 111.06/14.50 fof(f9581,plain,(
% 111.06/14.50 ![X0]: (in(X0,empty_set)|~sQ473_spl)),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f1069,f9572])).
% 111.06/14.50 fof(f9582,plain,(
% 111.06/14.50 $false|~sQ473_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f9581,f1073])).
% 111.06/14.50 fof(f9583,plain,(
% 111.06/14.50 ~sQ473_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f9582])).
% 111.06/14.50 fof(f12060,definition,(
% 111.06/14.50 sQ486_spl <=> (function(relation_inverse(empty_set)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f12062,plain,(
% 111.06/14.50 ~function(relation_inverse(empty_set))|sQ486_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f12060])).
% 111.06/14.50 fof(f12344,plain,(
% 111.06/14.50 empty(relation_inverse(empty_set))),
% 111.06/14.50 inference(resolution,[status(thm)],[f537,f539])).
% 111.06/14.50 fof(f12349,plain,(
% 111.06/14.50 function(relation_inverse(empty_set))),
% 111.06/14.50 inference(resolution,[status(thm)],[f12344,f247])).
% 111.06/14.50 fof(f12350,plain,(
% 111.06/14.50 $false|sQ486_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f12349,f12062])).
% 111.06/14.50 fof(f12351,plain,(
% 111.06/14.50 sQ486_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f12350])).
% 111.06/14.50 fof(f12811,definition,(
% 111.06/14.50 sQ519_spl <=> (in(sK14_skl(relation_rng(empty_set)),relation_rng(empty_set)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f12812,plain,(
% 111.06/14.50 in(sK14_skl(relation_rng(empty_set)),relation_rng(empty_set))|~sQ519_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f12811])).
% 111.06/14.50 fof(f12832,plain,(
% 111.06/14.50 in(sK14_skl(empty_set),relation_rng(empty_set))|~sQ519_spl),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f931,f12812])).
% 111.06/14.50 fof(f12833,plain,(
% 111.06/14.50 in(sK14_skl(empty_set),empty_set)|~sQ519_spl),
% 111.06/14.50 inference(forward_demodulation,[status(thm)],[f931,f12832])).
% 111.06/14.50 fof(f12834,plain,(
% 111.06/14.50 $false|~sQ519_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f12833,f1073])).
% 111.06/14.50 fof(f12835,plain,(
% 111.06/14.50 ~sQ519_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f12834])).
% 111.06/14.50 fof(f13748,plain,(
% 111.06/14.50 $false|~sQ434_spl),
% 111.06/14.50 inference(backward_subsumption_resolution,[status(thm)],[f9280,f8104])).
% 111.06/14.50 fof(f13765,plain,(
% 111.06/14.50 ~sQ434_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f13748])).
% 111.06/14.50 fof(f14175,plain,(
% 111.06/14.50 ![X0]: (empty(powerset(X0))|in(X0,powerset(X0)))),
% 111.06/14.50 inference(resolution,[status(thm)],[f361,f9278])).
% 111.06/14.50 fof(f14178,plain,(
% 111.06/14.50 ![X0]: (in(X0,powerset(X0)))),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f14175,f551])).
% 111.06/14.50 fof(f14230,definition,(
% 111.06/14.50 sQ545_spl <=> (relation(relation_inverse(sK79_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ545_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f14232,plain,(
% 111.06/14.50 ~relation(relation_inverse(sK79_skl))|sQ545_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f14230])).
% 111.06/14.50 fof(f14252,plain,(
% 111.06/14.50 $false|sQ545_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f14232,f9279])).
% 111.06/14.50 fof(f14253,plain,(
% 111.06/14.50 sQ545_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f14252])).
% 111.06/14.50 fof(f19082,plain,(
% 111.06/14.50 $false|sQ66_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f1485,f974])).
% 111.06/14.50 fof(f19083,plain,(
% 111.06/14.50 sQ66_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f19082])).
% 111.06/14.50 fof(f19558,definition,(
% 111.06/14.50 ![X0]: (sQ618_spl <=> (in(empty_set,X0)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f19559,plain,(
% 111.06/14.50 ![X0]: (in(empty_set,X0)|~sQ618_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f19558])).
% 111.06/14.50 fof(f19586,plain,(
% 111.06/14.50 $false|~sQ618_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f19559,f1073])).
% 111.06/14.50 fof(f19613,plain,(
% 111.06/14.50 ~sQ618_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f19586])).
% 111.06/14.50 fof(f23239,definition,(
% 111.06/14.50 sQ654_spl <=> (subset(empty_set,relation_dom(sK79_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f23241,plain,(
% 111.06/14.50 ~subset(empty_set,relation_dom(sK79_skl))|sQ654_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f23239])).
% 111.06/14.50 fof(f24600,definition,(
% 111.06/14.50 sQ689_spl <=> (in(ordered_pair(sK21_skl(sK79_skl,empty_set),sK22_skl(sK79_skl,empty_set)),empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ689_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f24601,plain,(
% 111.06/14.50 in(ordered_pair(sK21_skl(sK79_skl,empty_set),sK22_skl(sK79_skl,empty_set)),empty_set)|~sQ689_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f24600])).
% 111.06/14.50 fof(f24654,plain,(
% 111.06/14.50 $false|~sQ689_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f24601,f1073])).
% 111.06/14.50 fof(f24655,plain,(
% 111.06/14.50 ~sQ689_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f24654])).
% 111.06/14.50 fof(f24999,plain,(
% 111.06/14.50 $false|~sQ474_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f9580,f1073])).
% 111.06/14.50 fof(f25000,plain,(
% 111.06/14.50 ~sQ474_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f24999])).
% 111.06/14.50 fof(f25003,plain,(
% 111.06/14.50 $false|~sQ431_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f8090,f809])).
% 111.06/14.50 fof(f25004,plain,(
% 111.06/14.50 ~sQ431_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f25003])).
% 111.06/14.50 fof(f25221,definition,(
% 111.06/14.50 sQ714_spl <=> (relation(sK60_skl))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f25223,plain,(
% 111.06/14.50 ~relation(sK60_skl)|sQ714_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f25221])).
% 111.06/14.50 fof(f25249,plain,(
% 111.06/14.50 $false|sQ714_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f25223,f663])).
% 111.06/14.50 fof(f25250,plain,(
% 111.06/14.50 sQ714_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f25249])).
% 111.06/14.50 fof(f29329,definition,(
% 111.06/14.50 sQ822_spl <=> (in(ordered_pair(sK30_skl(sK79_skl,empty_set),sK31_skl(sK79_skl,empty_set)),empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ822_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f29330,plain,(
% 111.06/14.50 in(ordered_pair(sK30_skl(sK79_skl,empty_set),sK31_skl(sK79_skl,empty_set)),empty_set)|~sQ822_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f29329])).
% 111.06/14.50 fof(f29351,plain,(
% 111.06/14.50 $false|~sQ822_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f29330,f1073])).
% 111.06/14.50 fof(f29352,plain,(
% 111.06/14.50 ~sQ822_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f29351])).
% 111.06/14.50 fof(f30679,plain,(
% 111.06/14.50 $false|sQ654_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f23241,f809])).
% 111.06/14.50 fof(f30680,plain,(
% 111.06/14.50 sQ654_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f30679])).
% 111.06/14.50 fof(f33883,definition,(
% 111.06/14.50 sQ959_spl <=> (relation(relation_inverse(sK55_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ959_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f33885,plain,(
% 111.06/14.50 ~relation(relation_inverse(sK55_skl))|sQ959_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f33883])).
% 111.06/14.50 fof(f33922,plain,(
% 111.06/14.50 $false|sQ959_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f33885,f9289])).
% 111.06/14.50 fof(f33923,plain,(
% 111.06/14.50 sQ959_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f33922])).
% 111.06/14.50 fof(f33939,definition,(
% 111.06/14.50 sQ970_spl <=> (relation(relation_inverse(sK60_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ970_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f33941,plain,(
% 111.06/14.50 ~relation(relation_inverse(sK60_skl))|sQ970_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f33939])).
% 111.06/14.50 fof(f33996,definition,(
% 111.06/14.50 sQ981_spl <=> (relation(relation_inverse(sK63_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ981_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f33998,plain,(
% 111.06/14.50 ~relation(relation_inverse(sK63_skl))|sQ981_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f33996])).
% 111.06/14.50 fof(f34079,plain,(
% 111.06/14.50 $false|sQ970_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f9288,f33941])).
% 111.06/14.50 fof(f34080,plain,(
% 111.06/14.50 sQ970_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f34079])).
% 111.06/14.50 fof(f34081,plain,(
% 111.06/14.50 $false|sQ981_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f9287,f33998])).
% 111.06/14.50 fof(f34082,plain,(
% 111.06/14.50 sQ981_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f34081])).
% 111.06/14.50 fof(f34700,definition,(
% 111.06/14.50 sQ1000_spl <=> (relation(relation_inverse(sK64_skl)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ1000_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f34702,plain,(
% 111.06/14.50 ~relation(relation_inverse(sK64_skl))|sQ1000_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f34700])).
% 111.06/14.50 fof(f35053,plain,(
% 111.06/14.50 $false|sQ1000_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f9286,f34702])).
% 111.06/14.50 fof(f35054,plain,(
% 111.06/14.50 sQ1000_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f35053])).
% 111.06/14.50 fof(f35903,definition,(
% 111.06/14.50 ![X0]: (sQ1057_spl <=> (~in(sK19_skl(empty_set),X0)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ1057_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f35904,plain,(
% 111.06/14.50 ![X0]: (~in(sK19_skl(empty_set),X0)|~sQ1057_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f35903])).
% 111.06/14.50 fof(f35906,definition,(
% 111.06/14.50 ![X1]: (sQ1058_spl <=> (in(sK19_skl(empty_set),X1)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ1058_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f35907,plain,(
% 111.06/14.50 ![X0]: (in(sK19_skl(empty_set),X0)|~sQ1058_spl)),
% 111.06/14.50 inference(component_clause,[status(thm)],[f35906])).
% 111.06/14.50 fof(f35920,plain,(
% 111.06/14.50 $false|~sQ1057_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f35904,f14178])).
% 111.06/14.50 fof(f35943,plain,(
% 111.06/14.50 ~sQ1057_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f35920])).
% 111.06/14.50 fof(f35958,plain,(
% 111.06/14.50 $false|~sQ1058_spl),
% 111.06/14.50 inference(resolution,[status(thm)],[f35907,f1073])).
% 111.06/14.50 fof(f36030,plain,(
% 111.06/14.50 ~sQ1058_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f35958])).
% 111.06/14.50 fof(f39821,definition,(
% 111.06/14.50 sQ1080_spl <=> (empty(empty_set))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ1080_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f39823,plain,(
% 111.06/14.50 ~empty(empty_set)|sQ1080_spl),
% 111.06/14.50 inference(component_clause,[status(thm)],[f39821])).
% 111.06/14.50 fof(f39825,plain,(
% 111.06/14.50 $false|sQ1080_spl),
% 111.06/14.50 inference(forward_subsumption_resolution,[status(thm)],[f39823,f539])).
% 111.06/14.50 fof(f39826,plain,(
% 111.06/14.50 sQ1080_spl),
% 111.06/14.50 inference(contradiction_clause,[status(thm)],[f39825])).
% 111.06/14.50 fof(f45222,definition,(
% 111.06/14.50 ![X0]: (sQ1136_spl <=> (empty_set=singleton(X0)))),
% 111.06/14.50 introduced(definition,[new_symbols(definition,[sQ1136_spl])],[split_symbol_definition])).
% 111.06/14.50 fof(f45223,plain,(
% 111.06/14.50 ![X0]: (empty_set=singleton(X0)|~sQ1136_spl)),
% 111.06/14.57 inference(component_clause,[status(thm)],[f45222])).
% 111.06/14.57 fof(f45226,plain,(
% 111.06/14.57 $false|~sQ1136_spl),
% 111.06/14.57 inference(forward_subsumption_resolution,[status(thm)],[f45223,f603])).
% 111.06/14.57 fof(f45227,plain,(
% 111.06/14.57 ~sQ1136_spl),
% 111.06/14.57 inference(contradiction_clause,[status(thm)],[f45226])).
% 111.06/14.57 fof(f46188,definition,(
% 111.06/14.57 ![X0,X1]: (sQ1147_spl <=> (~in(X0,X1)))),
% 111.06/14.57 introduced(definition,[new_symbols(definition,[sQ1147_spl])],[split_symbol_definition])).
% 111.06/14.57 fof(f46189,plain,(
% 111.06/14.57 ![X0,X1]: (~in(X0,X1)|~sQ1147_spl)),
% 111.06/14.57 inference(component_clause,[status(thm)],[f46188])).
% 111.06/14.57 fof(f47162,plain,(
% 111.06/14.57 $false|~sQ1147_spl),
% 111.06/14.57 inference(backward_subsumption_resolution,[status(thm)],[f974,f46189])).
% 111.06/14.57 fof(f47200,plain,(
% 111.06/14.57 ~sQ1147_spl),
% 111.06/14.57 inference(contradiction_clause,[status(thm)],[f47162])).
% 111.06/14.57 fof(f47305,plain,(
% 111.06/14.57 ~relation(relation_dom_restriction(sK79_skl,sK80_skl))|~function(relation_dom_restriction(sK79_skl,sK80_skl))|apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=empty_set|sQ58_spl),
% 111.06/14.57 inference(resolution,[status(thm)],[f1088,f1437])).
% 111.06/14.57 fof(f47314,definition,(
% 111.06/14.57 sQ1168_spl <=> (apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=empty_set)),
% 111.06/14.57 introduced(definition,[new_symbols(definition,[sQ1168_spl])],[split_symbol_definition])).
% 111.06/14.57 fof(f47315,plain,(
% 111.06/14.57 apply(relation_dom_restriction(sK79_skl,sK80_skl),sK81_skl)=empty_set|~sQ1168_spl),
% 111.06/14.57 inference(component_clause,[status(thm)],[f47314])).
% 111.06/14.57 fof(f47317,plain,(
% 111.06/14.57 ~sQ67_spl|~sQ69_spl|sQ1168_spl|sQ58_spl),
% 111.06/14.57 inference(split_clause,[status(thm)],[f47305,f1487,f1494,f47314,f1435])).
% 111.06/14.57 fof(f47320,plain,(
% 111.06/14.57 $false|~sQ59_spl|~sQ1168_spl),
% 111.06/14.57 inference(forward_subsumption_resolution,[status(thm)],[f47315,f1507])).
% 111.06/14.57 fof(f47321,plain,(
% 111.06/14.57 ~sQ59_spl|~sQ1168_spl),
% 111.06/14.57 inference(contradiction_clause,[status(thm)],[f47320])).
% 111.06/14.57 fof(f47322,plain,(
% 111.06/14.57 $false),
% 111.06/14.57 inference(sat_refutation,[status(thm)],[f1137,f1139,f1240,f1374,f1441,f1478,f1506,f2162,f2202,f2206,f2246,f2428,f2662,f3628,f7139,f7168,f8382,f8424,f8751,f9583,f12351,f12835,f13765,f14253,f19083,f19613,f24655,f25000,f25004,f25250,f29352,f30680,f33923,f34080,f34082,f35054,f35943,f36030,f39826,f45227,f47200,f47317,f47321])).
% 111.06/14.57 % SZS output end CNFRefutation for theBenchmark.p
% 7.17/14.66 % Elapsed time: 14.286834 seconds
% 7.17/14.66 % CPU time: 112.481080 seconds
% 7.17/14.66 % Total memory used: 744.747 MB
% 7.17/14.66 % Net memory used: 667.987 MB
%------------------------------------------------------------------------------