%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU298+1 : 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 : n003.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:15 PM UTC 2026
% Result : Theorem 0.16s 10.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/10.40 % Computer : n003.cluster.edu
% 0.12/10.40 % Model : x86_64 x86_64
% 0.12/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.40 % Memory : 8046.5625MB
% 0.12/10.40 % OS : Linux 6.8.0-71-generic
% 0.12/10.40 % CPULimit : 300
% 0.12/10.40 % WCLimit : 300
% 0.12/10.40 % DateTime : Mon Sep 21 06:10:41 UTC 2026
% 0.12/10.40 % CPUTime :
% 0.12/10.42 % Drodi V4.1.1
% 0.16/10.93 % Refutation found
% 0.16/10.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/10.93 % SZS output start CNFRefutation for theBenchmark
% 0.16/10.93 fof(f1,conjecture,(
% 0.16/10.93 (! [A,B] :( ( ordinal(A)& element(B,powerset(powerset(succ(A)))) )=> (? [C] :(! [D] :( in(D,C)<=> ( in(D,powerset(A))& (? [E] :( in(E,B)& D = set_difference(E,singleton(A)) ) )) ) ))) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f2,negated_conjecture,(
% 0.16/10.93 ~((! [A,B] :( ( ordinal(A)& element(B,powerset(powerset(succ(A)))) )=> (? [C] :(! [D] :( in(D,C)<=> ( in(D,powerset(A))& (? [E] :( in(E,B)& D = set_difference(E,singleton(A)) ) )) ) ))) ))),
% 0.16/10.93 inference(negated_conjecture,[status(cth)],[f1])).
% 0.16/10.93 fof(f5,axiom,(
% 0.16/10.93 (? [A] :( relation(A)& function(A)& one_to_one(A)& empty(A)& epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f7,axiom,(
% 0.16/10.93 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f8,axiom,(
% 0.16/10.93 (! [A] :( ( relation(A)& empty(A)& function(A) )=> ( relation(A)& function(A)& one_to_one(A) ) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f9,axiom,(
% 0.16/10.93 (? [A] :( empty(A)& relation(A) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f19,axiom,(
% 0.16/10.93 (! [A] :( empty(A)=> function(A) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f20,axiom,(
% 0.16/10.93 (! [A] :( empty(A)=> relation(A) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f28,axiom,(
% 0.16/10.93 (? [A] : empty(A) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f43,axiom,(
% 0.16/10.93 (! [A,B] :( ( ordinal(A)& element(B,powerset(powerset(succ(A)))) )=> ( (! [C,D,E] :( ( C = D& (? [F] :( in(F,B)& D = set_difference(F,singleton(A)) ))& C = E& (? [G] :( in(G,B)& E = set_difference(G,singleton(A)) ) ))=> D = E ))=> (? [C] :(! [D] :( in(D,C)<=> (? [E] :( in(E,powerset(A))& E = D& (? [H] :( in(H,B)& D = set_difference(H,singleton(A)) ) )) )) ))) ) )),
% 0.16/10.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/10.93 fof(f44,plain,(
% 0.16/10.93 (?[A,B]: ((ordinal(A)&element(B,powerset(powerset(succ(A)))))&(![C]: ?[D]: (in(D,C)<~>(in(D,powerset(A))&(?[E]: (in(E,B)&D=set_difference(E,singleton(A)))))))))),
% 0.16/10.93 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/10.93 fof(f45,plain,(
% 0.16/10.93 ?[A,B]: ((ordinal(A)&element(B,powerset(powerset(succ(A)))))&(![C]: ?[D]: ((in(D,C)|(in(D,powerset(A))&(?[E]: (in(E,B)&D=set_difference(E,singleton(A))))))&(~in(D,C)|(~in(D,powerset(A))|(![E]: (~in(E,B)|~D=set_difference(E,singleton(A)))))))))),
% 0.16/10.93 inference(NNF_transformation,[status(thm)],[f44])).
% 0.16/10.93 fof(f46,plain,(
% 0.16/10.93 ((ordinal(sK0_skl)&element(sK1_skl,powerset(powerset(succ(sK0_skl)))))&(![C]: ((in(sK2_skl(C),C)|(in(sK2_skl(C),powerset(sK0_skl))&(in(sK3_skl(C),sK1_skl)&sK2_skl(C)=set_difference(sK3_skl(C),singleton(sK0_skl)))))&(~in(sK2_skl(C),C)|(~in(sK2_skl(C),powerset(sK0_skl))|(![E]: (~in(E,sK1_skl)|~sK2_skl(C)=set_difference(E,singleton(sK0_skl)))))))))),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C)),skolemize(E,sK3_skl(C))],[f45])).
% 0.16/10.93 fof(f47,plain,(
% 0.16/10.93 ordinal(sK0_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/10.93 fof(f48,plain,(
% 0.16/10.93 element(sK1_skl,powerset(powerset(succ(sK0_skl))))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/10.93 fof(f49,plain,(
% 0.16/10.93 ![X0]: (in(sK2_skl(X0),X0)|in(sK2_skl(X0),powerset(sK0_skl)))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/10.93 fof(f50,plain,(
% 0.16/10.93 ![X0]: (in(sK2_skl(X0),X0)|in(sK3_skl(X0),sK1_skl))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/10.93 fof(f51,plain,(
% 0.16/10.93 ![X0]: (in(sK2_skl(X0),X0)|sK2_skl(X0)=set_difference(sK3_skl(X0),singleton(sK0_skl)))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/10.93 fof(f52,plain,(
% 0.16/10.93 ![X0,X1]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),powerset(sK0_skl))|~in(X1,sK1_skl)|~sK2_skl(X0)=set_difference(X1,singleton(sK0_skl)))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f46])).
% 0.16/10.93 fof(f68,plain,(
% 0.16/10.93 ((((((relation(sK6_skl)&function(sK6_skl))&one_to_one(sK6_skl))&empty(sK6_skl))&epsilon_transitive(sK6_skl))&epsilon_connected(sK6_skl))&ordinal(sK6_skl))),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f5])).
% 0.16/10.93 fof(f69,plain,(
% 0.16/10.93 relation(sK6_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f68])).
% 0.16/10.93 fof(f70,plain,(
% 0.16/10.93 function(sK6_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f68])).
% 0.16/10.93 fof(f72,plain,(
% 0.16/10.93 empty(sK6_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f68])).
% 0.16/10.93 fof(f79,plain,(
% 0.16/10.93 ((relation(sK8_skl)&empty(sK8_skl))&function(sK8_skl))),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f7])).
% 0.16/10.93 fof(f80,plain,(
% 0.16/10.93 relation(sK8_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f79])).
% 0.16/10.93 fof(f81,plain,(
% 0.16/10.93 empty(sK8_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f79])).
% 0.16/10.93 fof(f82,plain,(
% 0.16/10.93 function(sK8_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f79])).
% 0.16/10.93 fof(f83,plain,(
% 0.16/10.93 ![A]: (((~relation(A)|~empty(A))|~function(A))|((relation(A)&function(A))&one_to_one(A)))),
% 0.16/10.93 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.16/10.93 fof(f86,plain,(
% 0.16/10.93 ![X0]: (~relation(X0)|~empty(X0)|~function(X0)|one_to_one(X0))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f83])).
% 0.16/10.93 fof(f87,plain,(
% 0.16/10.93 (empty(sK9_skl)&relation(sK9_skl))),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f9])).
% 0.16/10.93 fof(f88,plain,(
% 0.16/10.93 empty(sK9_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f87])).
% 0.16/10.93 fof(f89,plain,(
% 0.16/10.93 relation(sK9_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f87])).
% 0.16/10.93 fof(f122,plain,(
% 0.16/10.93 ![A]: (~empty(A)|function(A))),
% 0.16/10.93 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.16/10.93 fof(f123,plain,(
% 0.16/10.93 ![X0]: (~empty(X0)|function(X0))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f122])).
% 0.16/10.93 fof(f124,plain,(
% 0.16/10.93 ![A]: (~empty(A)|relation(A))),
% 0.16/10.93 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.16/10.93 fof(f125,plain,(
% 0.16/10.93 ![X0]: (~empty(X0)|relation(X0))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f124])).
% 0.16/10.93 fof(f153,plain,(
% 0.16/10.93 empty(sK18_skl)),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f28])).
% 0.16/10.93 fof(f154,plain,(
% 0.16/10.93 empty(sK18_skl)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f153])).
% 0.16/10.93 fof(f177,plain,(
% 0.16/10.93 ![A,B]: ((~ordinal(A)|~element(B,powerset(powerset(succ(A)))))|((?[C,D,E]: ((((C=D&(?[F]: (in(F,B)&D=set_difference(F,singleton(A)))))&C=E)&(?[G]: (in(G,B)&E=set_difference(G,singleton(A)))))&~D=E))|(?[C]: ![D]: (in(D,C)<=>(?[E]: ((in(E,powerset(A))&E=D)&(?[H]: (in(H,B)&D=set_difference(H,singleton(A))))))))))),
% 0.16/10.93 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 0.16/10.93 fof(f178,definition,(
% 0.16/10.93 ![A,B,C,D,E]: (sP0_prd(E,D,C,B,A)<=>((((C=D&(?[F]: (in(F,B)&D=set_difference(F,singleton(A)))))&C=E)&(?[G]: (in(G,B)&E=set_difference(G,singleton(A)))))&~D=E))),
% 0.16/10.93 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.16/10.93 fof(f179,plain,(
% 0.16/10.93 ![A,B]: ((~ordinal(A)|~element(B,powerset(powerset(succ(A)))))|((?[C,D,E]: sP0_prd(E,D,C,B,A))|(?[C]: ![D]: (in(D,C)<=>(?[E]: ((in(E,powerset(A))&E=D)&(?[H]: (in(H,B)&D=set_difference(H,singleton(A))))))))))),
% 0.16/10.93 inference(formula_renaming,[status(thm)],[f177,f178])).
% 0.16/10.93 fof(f180,plain,(
% 0.16/10.93 ![A,B]: ((~ordinal(A)|~element(B,powerset(powerset(succ(A)))))|((?[C,D,E]: sP0_prd(E,D,C,B,A))|(?[C]: ![D]: ((~in(D,C)|(?[E]: ((in(E,powerset(A))&E=D)&(?[H]: (in(H,B)&D=set_difference(H,singleton(A)))))))&(in(D,C)|(![E]: ((~in(E,powerset(A))|~E=D)|(![H]: (~in(H,B)|~D=set_difference(H,singleton(A)))))))))))),
% 0.16/10.93 inference(NNF_transformation,[status(thm)],[f179])).
% 0.16/10.93 fof(f181,plain,(
% 0.16/10.93 ![A,B]: ((~ordinal(A)|~element(B,powerset(powerset(succ(A)))))|((?[C,D,E]: sP0_prd(E,D,C,B,A))|(?[C]: ((![D]: (~in(D,C)|((?[E]: (in(E,powerset(A))&E=D))&(?[H]: (in(H,B)&D=set_difference(H,singleton(A)))))))&(![D]: (in(D,C)|((![E]: (~in(E,powerset(A))|~E=D))|(![H]: (~in(H,B)|~D=set_difference(H,singleton(A)))))))))))),
% 0.16/10.93 inference(miniscoping,[status(thm)],[f180])).
% 0.16/10.93 fof(f182,plain,(
% 0.16/10.93 ![A,B]: ((~ordinal(A)|~element(B,powerset(powerset(succ(A)))))|(sP0_prd(sK22_skl(B,A),sK21_skl(B,A),sK20_skl(B,A),B,A)|((![D]: (~in(D,sK23_skl(B,A))|((in(sK24_skl(D,B,A),powerset(A))&sK24_skl(D,B,A)=D)&(in(sK25_skl(D,B,A),B)&D=set_difference(sK25_skl(D,B,A),singleton(A))))))&(![D]: (in(D,sK23_skl(B,A))|((![E]: (~in(E,powerset(A))|~E=D))|(![H]: (~in(H,B)|~D=set_difference(H,singleton(A))))))))))),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl]),skolemize(C,sK20_skl(B,A)),skolemize(D,sK21_skl(B,A)),skolemize(E,sK22_skl(B,A)),skolemize(C,sK23_skl(B,A)),skolemize(E,sK24_skl(D,B,A)),skolemize(H,sK25_skl(D,B,A))],[f181])).
% 0.16/10.93 fof(f183,plain,(
% 0.16/10.93 ![X0,X1,X2]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|~in(X2,sK23_skl(X1,X0))|in(sK24_skl(X2,X1,X0),powerset(X0)))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f182])).
% 0.16/10.93 fof(f184,plain,(
% 0.16/10.93 ![X0,X1,X2]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|~in(X2,sK23_skl(X1,X0))|sK24_skl(X2,X1,X0)=X2)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f182])).
% 0.16/10.93 fof(f185,plain,(
% 0.16/10.93 ![X0,X1,X2]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|~in(X2,sK23_skl(X1,X0))|in(sK25_skl(X2,X1,X0),X1))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f182])).
% 0.16/10.93 fof(f186,plain,(
% 0.16/10.93 ![X0,X1,X2]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|~in(X2,sK23_skl(X1,X0))|X2=set_difference(sK25_skl(X2,X1,X0),singleton(X0)))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f182])).
% 0.16/10.93 fof(f187,plain,(
% 0.16/10.93 ![X0,X1,X2,X3,X4]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|in(X2,sK23_skl(X1,X0))|~in(X3,powerset(X0))|~X3=X2|~in(X4,X1)|~X2=set_difference(X4,singleton(X0)))),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f182])).
% 0.16/10.93 fof(f188,plain,(
% 0.16/10.93 ![A,B,C,D,E]: ((~sP0_prd(E,D,C,B,A)|((((C=D&(?[F]: (in(F,B)&D=set_difference(F,singleton(A)))))&C=E)&(?[G]: (in(G,B)&E=set_difference(G,singleton(A)))))&~D=E))&(sP0_prd(E,D,C,B,A)|((((~C=D|(![F]: (~in(F,B)|~D=set_difference(F,singleton(A)))))|~C=E)|(![G]: (~in(G,B)|~E=set_difference(G,singleton(A)))))|D=E)))),
% 0.16/10.93 inference(NNF_transformation,[status(thm)],[f178])).
% 0.16/10.93 fof(f189,plain,(
% 0.16/10.93 (![A,B,C,D,E]: (~sP0_prd(E,D,C,B,A)|((((C=D&(?[F]: (in(F,B)&D=set_difference(F,singleton(A)))))&C=E)&(?[G]: (in(G,B)&E=set_difference(G,singleton(A)))))&~D=E)))&(![A,B,C,D,E]: (sP0_prd(E,D,C,B,A)|((((~C=D|(![F]: (~in(F,B)|~D=set_difference(F,singleton(A)))))|~C=E)|(![G]: (~in(G,B)|~E=set_difference(G,singleton(A)))))|D=E)))),
% 0.16/10.93 inference(miniscoping,[status(thm)],[f188])).
% 0.16/10.93 fof(f190,plain,(
% 0.16/10.93 (![A,B,C,D,E]: (~sP0_prd(E,D,C,B,A)|((((C=D&(in(sK26_skl(E,D,C,B,A),B)&D=set_difference(sK26_skl(E,D,C,B,A),singleton(A))))&C=E)&(in(sK27_skl(E,D,C,B,A),B)&E=set_difference(sK27_skl(E,D,C,B,A),singleton(A))))&~D=E)))&(![A,B,C,D,E]: (sP0_prd(E,D,C,B,A)|((((~C=D|(![F]: (~in(F,B)|~D=set_difference(F,singleton(A)))))|~C=E)|(![G]: (~in(G,B)|~E=set_difference(G,singleton(A)))))|D=E)))),
% 0.16/10.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl]),skolemize(F,sK26_skl(E,D,C,B,A)),skolemize(G,sK27_skl(E,D,C,B,A))],[f189])).
% 0.16/10.93 fof(f191,plain,(
% 0.16/10.93 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=X1)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f190])).
% 0.16/10.93 fof(f194,plain,(
% 0.16/10.93 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=X0)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f190])).
% 0.16/10.93 fof(f197,plain,(
% 0.16/10.93 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|~X1=X0)),
% 0.16/10.93 inference(cnf_transformation,[status(thm)],[f190])).
% 0.16/10.93 fof(f199,plain,(
% 0.16/10.93 ![X0,X1,X2]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|in(set_difference(X2,singleton(X0)),sK23_skl(X1,X0))|~in(set_difference(X2,singleton(X0)),powerset(X0))|~in(X2,X1))),
% 0.16/10.93 inference(destructive_equality_resolution,[status(thm)],[f187])).
% 0.16/10.93 fof(f200,plain,(
% 0.16/10.93 ![X0,X1,X2,X3]: (~sP0_prd(X0,X0,X1,X2,X3))),
% 0.16/10.93 inference(destructive_equality_resolution,[status(thm)],[f197])).
% 0.16/10.93 fof(f225,definition,(
% 0.16/10.93 sQ4_spl <=> (in(sK2_skl(powerset(sK0_skl)),powerset(sK0_skl)))),
% 0.16/10.93 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/10.93 fof(f226,plain,(
% 0.16/10.93 in(sK2_skl(powerset(sK0_skl)),powerset(sK0_skl))|~sQ4_spl),
% 0.16/10.93 inference(component_clause,[status(thm)],[f225])).
% 0.16/10.93 fof(f227,plain,(
% 0.16/10.93 ~in(sK2_skl(powerset(sK0_skl)),powerset(sK0_skl))|sQ4_spl),
% 0.16/10.93 inference(component_clause,[status(thm)],[f225])).
% 0.16/10.93 fof(f255,plain,(
% 0.16/10.93 $false|sQ4_spl),
% 0.16/10.93 inference(resolution,[status(thm)],[f227,f49])).
% 0.16/10.93 fof(f261,plain,(
% 0.16/10.93 sQ4_spl),
% 0.16/10.93 inference(contradiction_clause,[status(thm)],[f255])).
% 0.16/10.93 fof(f300,plain,(
% 0.16/10.93 ~relation(sK18_skl)|~function(sK18_skl)|one_to_one(sK18_skl)),
% 0.16/10.93 inference(resolution,[status(thm)],[f86,f154])).
% 0.16/10.93 fof(f302,plain,(
% 0.16/10.93 ~relation(sK9_skl)|~function(sK9_skl)|one_to_one(sK9_skl)),
% 0.16/10.93 inference(resolution,[status(thm)],[f86,f88])).
% 0.16/10.93 fof(f303,plain,(
% 0.16/10.93 ~relation(sK8_skl)|~function(sK8_skl)|one_to_one(sK8_skl)),
% 0.16/10.93 inference(resolution,[status(thm)],[f86,f81])).
% 0.16/10.93 fof(f304,plain,(
% 0.16/10.93 ~relation(sK6_skl)|~function(sK6_skl)|one_to_one(sK6_skl)),
% 0.16/10.93 inference(resolution,[status(thm)],[f86,f72])).
% 0.16/10.93 fof(f305,definition,(
% 0.16/10.93 sQ12_spl <=> (relation(sK18_skl))),
% 0.16/10.93 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.16/10.93 fof(f307,plain,(
% 0.16/10.93 ~relation(sK18_skl)|sQ12_spl),
% 0.16/10.93 inference(component_clause,[status(thm)],[f305])).
% 0.16/10.93 fof(f308,definition,(
% 0.16/10.93 sQ13_spl <=> (function(sK18_skl))),
% 0.16/10.93 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.16/10.93 fof(f310,plain,(
% 0.16/10.93 ~function(sK18_skl)|sQ13_spl),
% 0.16/10.93 inference(component_clause,[status(thm)],[f308])).
% 0.16/10.93 fof(f311,definition,(
% 0.16/10.93 sQ14_spl <=> (one_to_one(sK18_skl))),
% 0.16/10.93 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.16/10.93 fof(f314,plain,(
% 0.16/10.93 ~sQ12_spl|~sQ13_spl|sQ14_spl),
% 0.16/10.93 inference(split_clause,[status(thm)],[f300,f305,f308,f311])).
% 0.16/10.93 fof(f315,definition,(
% 0.16/10.93 sQ15_spl <=> (relation(sK9_skl))),
% 0.16/10.93 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f317,plain,(
% 0.16/10.94 ~relation(sK9_skl)|sQ15_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f315])).
% 0.16/10.94 fof(f318,definition,(
% 0.16/10.94 sQ16_spl <=> (function(sK9_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f320,plain,(
% 0.16/10.94 ~function(sK9_skl)|sQ16_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f318])).
% 0.16/10.94 fof(f321,definition,(
% 0.16/10.94 sQ17_spl <=> (one_to_one(sK9_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f324,plain,(
% 0.16/10.94 ~sQ15_spl|~sQ16_spl|sQ17_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f302,f315,f318,f321])).
% 0.16/10.94 fof(f325,definition,(
% 0.16/10.94 sQ18_spl <=> (relation(sK8_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f327,plain,(
% 0.16/10.94 ~relation(sK8_skl)|sQ18_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f325])).
% 0.16/10.94 fof(f328,definition,(
% 0.16/10.94 sQ19_spl <=> (function(sK8_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f330,plain,(
% 0.16/10.94 ~function(sK8_skl)|sQ19_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f328])).
% 0.16/10.94 fof(f331,definition,(
% 0.16/10.94 sQ20_spl <=> (one_to_one(sK8_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f334,plain,(
% 0.16/10.94 ~sQ18_spl|~sQ19_spl|sQ20_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f303,f325,f328,f331])).
% 0.16/10.94 fof(f335,definition,(
% 0.16/10.94 sQ21_spl <=> (relation(sK6_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f337,plain,(
% 0.16/10.94 ~relation(sK6_skl)|sQ21_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f335])).
% 0.16/10.94 fof(f338,definition,(
% 0.16/10.94 sQ22_spl <=> (function(sK6_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f340,plain,(
% 0.16/10.94 ~function(sK6_skl)|sQ22_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f338])).
% 0.16/10.94 fof(f341,definition,(
% 0.16/10.94 sQ23_spl <=> (one_to_one(sK6_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f344,plain,(
% 0.16/10.94 ~sQ21_spl|~sQ22_spl|sQ23_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f304,f335,f338,f341])).
% 0.16/10.94 fof(f345,plain,(
% 0.16/10.94 $false|sQ22_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f340,f70])).
% 0.16/10.94 fof(f346,plain,(
% 0.16/10.94 sQ22_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f345])).
% 0.16/10.94 fof(f347,plain,(
% 0.16/10.94 $false|sQ21_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f337,f69])).
% 0.16/10.94 fof(f348,plain,(
% 0.16/10.94 sQ21_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f347])).
% 0.16/10.94 fof(f349,plain,(
% 0.16/10.94 $false|sQ19_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f330,f82])).
% 0.16/10.94 fof(f350,plain,(
% 0.16/10.94 sQ19_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f349])).
% 0.16/10.94 fof(f351,plain,(
% 0.16/10.94 $false|sQ18_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f327,f80])).
% 0.16/10.94 fof(f352,plain,(
% 0.16/10.94 sQ18_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f351])).
% 0.16/10.94 fof(f353,plain,(
% 0.16/10.94 $false|sQ15_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f317,f89])).
% 0.16/10.94 fof(f354,plain,(
% 0.16/10.94 sQ15_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f353])).
% 0.16/10.94 fof(f415,plain,(
% 0.16/10.94 function(sK18_skl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f123,f154])).
% 0.16/10.94 fof(f417,plain,(
% 0.16/10.94 function(sK9_skl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f123,f88])).
% 0.16/10.94 fof(f420,plain,(
% 0.16/10.94 relation(sK18_skl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f125,f154])).
% 0.16/10.94 fof(f479,plain,(
% 0.16/10.94 $false|sQ16_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f320,f417])).
% 0.16/10.94 fof(f480,plain,(
% 0.16/10.94 sQ16_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f479])).
% 0.16/10.94 fof(f547,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|in(sK24_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),powerset(X0))|in(sK2_skl(sK23_skl(X1,X0)),powerset(sK0_skl)))),
% 0.16/10.94 inference(resolution,[status(thm)],[f183,f49])).
% 0.16/10.94 fof(f560,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|sK24_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0)=sK2_skl(sK23_skl(X1,X0))|in(sK2_skl(sK23_skl(X1,X0)),powerset(sK0_skl)))),
% 0.16/10.94 inference(resolution,[status(thm)],[f184,f49])).
% 0.16/10.94 fof(f562,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|in(sK25_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),X1)|sK2_skl(sK23_skl(X1,X0))=set_difference(sK3_skl(sK23_skl(X1,X0)),singleton(sK0_skl)))),
% 0.16/10.94 inference(resolution,[status(thm)],[f185,f51])).
% 0.16/10.94 fof(f563,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|in(sK25_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),X1)|in(sK2_skl(sK23_skl(X1,X0)),powerset(sK0_skl)))),
% 0.16/10.94 inference(resolution,[status(thm)],[f185,f49])).
% 0.16/10.94 fof(f564,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|in(sK25_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),X1)|in(sK3_skl(sK23_skl(X1,X0)),sK1_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f185,f50])).
% 0.16/10.94 fof(f565,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|sK2_skl(sK23_skl(X1,X0))=set_difference(sK25_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),singleton(X0))|sK2_skl(sK23_skl(X1,X0))=set_difference(sK3_skl(sK23_skl(X1,X0)),singleton(sK0_skl)))),
% 0.16/10.94 inference(resolution,[status(thm)],[f186,f51])).
% 0.16/10.94 fof(f566,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|sK2_skl(sK23_skl(X1,X0))=set_difference(sK25_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),singleton(X0))|in(sK2_skl(sK23_skl(X1,X0)),powerset(sK0_skl)))),
% 0.16/10.94 inference(resolution,[status(thm)],[f186,f49])).
% 0.16/10.94 fof(f567,plain,(
% 0.16/10.94 ![X0,X1]: (~ordinal(X0)|~element(X1,powerset(powerset(succ(X0))))|sP0_prd(sK22_skl(X1,X0),sK21_skl(X1,X0),sK20_skl(X1,X0),X1,X0)|sK2_skl(sK23_skl(X1,X0))=set_difference(sK25_skl(sK2_skl(sK23_skl(X1,X0)),X1,X0),singleton(X0))|in(sK3_skl(sK23_skl(X1,X0)),sK1_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f186,f50])).
% 0.16/10.94 fof(f572,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK1_skl)|in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f564,f48])).
% 0.16/10.94 fof(f575,definition,(
% 0.16/10.94 sQ37_spl <=> (ordinal(sK0_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f577,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sQ37_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f575])).
% 0.16/10.94 fof(f578,definition,(
% 0.16/10.94 sQ38_spl <=> (sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f579,plain,(
% 0.16/10.94 sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ38_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f578])).
% 0.16/10.94 fof(f581,definition,(
% 0.16/10.94 sQ39_spl <=> (in(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK1_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f582,plain,(
% 0.16/10.94 in(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK1_skl)|~sQ39_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f581])).
% 0.16/10.94 fof(f584,definition,(
% 0.16/10.94 sQ40_spl <=> (in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f585,plain,(
% 0.16/10.94 in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl)|~sQ40_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f584])).
% 0.16/10.94 fof(f587,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ39_spl|sQ40_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f572,f575,f578,f581,f584])).
% 0.16/10.94 fof(f588,plain,(
% 0.16/10.94 $false|sQ37_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f577,f47])).
% 0.16/10.94 fof(f589,plain,(
% 0.16/10.94 sQ37_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f588])).
% 0.16/10.94 fof(f594,plain,(
% 0.16/10.94 sK20_skl(sK1_skl,sK0_skl)=sK22_skl(sK1_skl,sK0_skl)|~sQ38_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f579,f194])).
% 0.16/10.94 fof(f606,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(sK0_skl))|in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f547,f48])).
% 0.16/10.94 fof(f609,definition,(
% 0.16/10.94 sQ42_spl <=> (in(sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f610,plain,(
% 0.16/10.94 in(sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(sK0_skl))|~sQ42_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f609])).
% 0.16/10.94 fof(f612,definition,(
% 0.16/10.94 sQ43_spl <=> (in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f613,plain,(
% 0.16/10.94 in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))|~sQ43_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f612])).
% 0.16/10.94 fof(f615,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ42_spl|sQ43_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f606,f575,f578,f609,f612])).
% 0.16/10.94 fof(f624,plain,(
% 0.16/10.94 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),powerset(sK0_skl))|~sK2_skl(X0)=set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl))|~sQ40_spl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f585,f52])).
% 0.16/10.94 fof(f626,plain,(
% 0.16/10.94 sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ38_spl),
% 0.16/10.94 inference(backward_demodulation,[status(thm)],[f594,f579])).
% 0.16/10.94 fof(f628,definition,(
% 0.16/10.94 sQ44_spl <=> (element(sK1_skl,powerset(powerset(succ(sK0_skl)))))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f630,plain,(
% 0.16/10.94 ~element(sK1_skl,powerset(powerset(succ(sK0_skl))))|sQ44_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f628])).
% 0.16/10.94 fof(f631,definition,(
% 0.16/10.94 sQ45_spl <=> (sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f632,plain,(
% 0.16/10.94 sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ45_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f631])).
% 0.16/10.94 fof(f634,definition,(
% 0.16/10.94 sQ46_spl <=> (sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f635,plain,(
% 0.16/10.94 sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl))|~sQ46_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f634])).
% 0.16/10.94 fof(f638,plain,(
% 0.16/10.94 $false|sQ44_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f630,f48])).
% 0.16/10.94 fof(f639,plain,(
% 0.16/10.94 sQ44_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f638])).
% 0.16/10.94 fof(f645,plain,(
% 0.16/10.94 sK20_skl(sK1_skl,sK0_skl)=sK21_skl(sK1_skl,sK0_skl)|~sQ45_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f632,f191])).
% 0.16/10.94 fof(f646,plain,(
% 0.16/10.94 sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ45_spl),
% 0.16/10.94 inference(backward_demodulation,[status(thm)],[f645,f632])).
% 0.16/10.94 fof(f648,plain,(
% 0.16/10.94 $false|~sQ45_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f646,f200])).
% 0.16/10.94 fof(f649,plain,(
% 0.16/10.94 ~sQ45_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f648])).
% 0.16/10.94 fof(f665,definition,(
% 0.16/10.94 sQ48_spl <=> (sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK23_skl(sK1_skl,sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f666,plain,(
% 0.16/10.94 sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ48_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f665])).
% 0.16/10.94 fof(f669,plain,(
% 0.16/10.94 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),powerset(sK0_skl))|~sK2_skl(X0)=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|~sQ39_spl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f582,f52])).
% 0.16/10.94 fof(f672,plain,(
% 0.16/10.94 ![X0]: (~ordinal(sK0_skl)|~element(X0,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(X0,sK0_skl),sK21_skl(X0,sK0_skl),sK20_skl(X0,sK0_skl),X0,sK0_skl)|in(set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl)),sK23_skl(X0,sK0_skl))|~in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))|~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),X0)|~sQ46_spl)),
% 0.16/10.94 inference(paramodulation,[status(thm)],[f635,f199])).
% 0.16/10.94 fof(f675,definition,(
% 0.16/10.94 ![X0]: (sQ49_spl <=> (~element(X0,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(X0,sK0_skl),sK21_skl(X0,sK0_skl),sK20_skl(X0,sK0_skl),X0,sK0_skl)|in(set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl)),sK23_skl(X0,sK0_skl))|~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),X0)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f676,plain,(
% 0.16/10.94 ![X0]: (~element(X0,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(X0,sK0_skl),sK21_skl(X0,sK0_skl),sK20_skl(X0,sK0_skl),X0,sK0_skl)|in(set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl)),sK23_skl(X0,sK0_skl))|~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),X0)|~sQ49_spl)),
% 0.16/10.94 inference(component_clause,[status(thm)],[f675])).
% 0.16/10.94 fof(f678,plain,(
% 0.16/10.94 ~sQ37_spl|sQ49_spl|~sQ43_spl|~sQ46_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f672,f575,f675,f612,f634])).
% 0.16/10.94 fof(f699,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|sK24_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f560,f48])).
% 0.16/10.94 fof(f702,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ48_spl|sQ43_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f699,f575,f578,f665,f612])).
% 0.16/10.94 fof(f716,plain,(
% 0.16/10.94 $false|sQ13_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f310,f415])).
% 0.16/10.94 fof(f717,plain,(
% 0.16/10.94 sQ13_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f716])).
% 0.16/10.94 fof(f718,plain,(
% 0.16/10.94 $false|sQ12_spl),
% 0.16/10.94 inference(forward_subsumption_resolution,[status(thm)],[f307,f420])).
% 0.16/10.94 fof(f719,plain,(
% 0.16/10.94 sQ12_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f718])).
% 0.16/10.94 fof(f720,plain,(
% 0.16/10.94 sQ45_spl|~sQ38_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f626,f631,f578])).
% 0.16/10.94 fof(f737,plain,(
% 0.16/10.94 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),powerset(sK0_skl))|~sK2_skl(X0)=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ46_spl|~sQ40_spl)),
% 0.16/10.94 inference(forward_demodulation,[status(thm)],[f635,f624])).
% 0.16/10.94 fof(f745,definition,(
% 0.16/10.94 sQ54_spl <=> (sK2_skl(powerset(sK0_skl))=sK2_skl(sK23_skl(sK1_skl,sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f792,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK1_skl)|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f562,f48])).
% 0.16/10.94 fof(f795,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ39_spl|sQ46_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f792,f575,f578,f581,f634])).
% 0.16/10.94 fof(f800,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK1_skl)|in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f563,f48])).
% 0.16/10.94 fof(f803,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ39_spl|sQ43_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f800,f575,f578,f581,f612])).
% 0.16/10.94 fof(f808,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f565,f48])).
% 0.16/10.94 fof(f811,definition,(
% 0.16/10.94 sQ57_spl <=> (sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f812,plain,(
% 0.16/10.94 sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|~sQ57_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f811])).
% 0.16/10.94 fof(f814,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ57_spl|sQ46_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f808,f575,f578,f811,f634])).
% 0.16/10.94 fof(f822,plain,(
% 0.16/10.94 ~in(sK2_skl(powerset(sK0_skl)),powerset(sK0_skl))|~sK2_skl(powerset(sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|~sQ39_spl|~sQ4_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f669,f226])).
% 0.16/10.94 fof(f825,plain,(
% 0.16/10.94 ![X0]: (~in(sK2_skl(X0),powerset(sK0_skl))|~sK2_skl(X0)=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|sK2_skl(X0)=set_difference(sK3_skl(X0),singleton(sK0_skl))|~sQ39_spl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f669,f51])).
% 0.16/10.94 fof(f828,plain,(
% 0.16/10.94 ![X0]: (~in(sK2_skl(X0),powerset(sK0_skl))|~sK2_skl(X0)=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|in(sK3_skl(X0),sK1_skl)|~sQ39_spl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f669,f50])).
% 0.16/10.94 fof(f829,definition,(
% 0.16/10.94 sQ58_spl <=> (sK2_skl(powerset(sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f832,plain,(
% 0.16/10.94 ~sQ4_spl|~sQ58_spl|~sQ39_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f822,f225,f829,f581])).
% 0.16/10.94 fof(f860,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))),
% 0.16/10.94 inference(resolution,[status(thm)],[f566,f48])).
% 0.16/10.94 fof(f863,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ57_spl|sQ43_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f860,f575,f578,f811,f612])).
% 0.16/10.94 fof(f868,plain,(
% 0.16/10.94 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),powerset(sK0_skl))|~sK2_skl(X0)=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ57_spl|~sQ39_spl)),
% 0.16/10.94 inference(backward_demodulation,[status(thm)],[f812,f669])).
% 0.16/10.94 fof(f885,plain,(
% 0.16/10.94 ~in(sK2_skl(powerset(sK0_skl)),powerset(sK0_skl))|~sK2_skl(powerset(sK0_skl))=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ57_spl|~sQ39_spl|~sQ4_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f868,f226])).
% 0.16/10.94 fof(f892,plain,(
% 0.16/10.94 ~sQ4_spl|~sQ54_spl|~sQ57_spl|~sQ39_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f885,f225,f745,f811,f581])).
% 0.16/10.94 fof(f900,plain,(
% 0.16/10.94 ~ordinal(sK0_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl)),
% 0.16/10.94 inference(resolution,[status(thm)],[f567,f48])).
% 0.16/10.94 fof(f903,plain,(
% 0.16/10.94 ~sQ37_spl|sQ38_spl|sQ57_spl|sQ40_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f900,f575,f578,f811,f584])).
% 0.16/10.94 fof(f938,definition,(
% 0.16/10.94 sQ64_spl <=> (sK2_skl(sK23_skl(sK1_skl,sK0_skl))=sK2_skl(sK23_skl(sK1_skl,sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f940,plain,(
% 0.16/10.94 ~sK2_skl(sK23_skl(sK1_skl,sK0_skl))=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|sQ64_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f938])).
% 0.16/10.94 fof(f1032,plain,(
% 0.16/10.94 in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))|~sQ48_spl|~sQ42_spl),
% 0.16/10.94 inference(backward_demodulation,[status(thm)],[f666,f610])).
% 0.16/10.94 fof(f1149,plain,(
% 0.16/10.94 ~sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl)|~sQ39_spl|~sQ43_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f828,f613])).
% 0.16/10.94 fof(f1158,plain,(
% 0.16/10.94 ~sQ57_spl|sQ40_spl|~sQ39_spl|~sQ43_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f1149,f811,f584,f581,f612])).
% 0.16/10.94 fof(f1166,plain,(
% 0.16/10.94 ~sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),singleton(sK0_skl))|~sQ39_spl|~sQ43_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f825,f613])).
% 0.16/10.94 fof(f1175,plain,(
% 0.16/10.94 ~sQ57_spl|sQ46_spl|~sQ39_spl|~sQ43_spl),
% 0.16/10.94 inference(split_clause,[status(thm)],[f1166,f811,f634,f581,f612])).
% 0.16/10.94 fof(f1209,plain,(
% 0.16/10.94 $false|sQ64_spl),
% 0.16/10.94 inference(trivial_equality_resolution,[status(thm)],[f940])).
% 0.16/10.94 fof(f1210,plain,(
% 0.16/10.94 sQ64_spl),
% 0.16/10.94 inference(contradiction_clause,[status(thm)],[f1209])).
% 0.16/10.94 fof(f1363,plain,(
% 0.16/10.94 ![X0]: (~element(X0,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(X0,sK0_skl),sK21_skl(X0,sK0_skl),sK20_skl(X0,sK0_skl),X0,sK0_skl)|in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(X0,sK0_skl))|~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),X0)|~sQ46_spl|~sQ49_spl)),
% 0.16/10.94 inference(forward_demodulation,[status(thm)],[f635,f676])).
% 0.16/10.94 fof(f1364,plain,(
% 0.16/10.94 ~element(sK1_skl,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl))|~sQ46_spl|~sQ49_spl|~sQ40_spl),
% 0.16/10.94 inference(resolution,[status(thm)],[f1363,f585])).
% 0.16/10.94 fof(f1365,definition,(
% 0.16/10.94 sQ80_spl <=> (in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)))),
% 0.16/10.94 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.16/10.94 fof(f1366,plain,(
% 0.16/10.94 in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl))|~sQ80_spl),
% 0.16/10.94 inference(component_clause,[status(thm)],[f1365])).
% 0.16/10.94 fof(f1368,plain,(
% 0.16/10.95 ~sQ44_spl|sQ38_spl|sQ80_spl|~sQ46_spl|~sQ49_spl|~sQ40_spl),
% 0.16/10.95 inference(split_clause,[status(thm)],[f1364,f628,f578,f1365,f634,f675,f584])).
% 0.16/10.95 fof(f1371,plain,(
% 0.16/10.95 ~in(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(sK0_skl))|~sK2_skl(sK23_skl(sK1_skl,sK0_skl))=sK2_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ80_spl|~sQ46_spl|~sQ40_spl),
% 0.16/10.95 inference(resolution,[status(thm)],[f1366,f737])).
% 0.16/10.95 fof(f1372,plain,(
% 0.16/10.95 ~ordinal(sK0_skl)|~element(sK1_skl,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|sK2_skl(sK23_skl(sK1_skl,sK0_skl))=set_difference(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK0_skl))|~sQ80_spl),
% 0.16/10.95 inference(resolution,[status(thm)],[f1366,f186])).
% 0.16/10.95 fof(f1373,plain,(
% 0.16/10.95 ~ordinal(sK0_skl)|~element(sK1_skl,powerset(powerset(succ(sK0_skl))))|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK25_skl(sK2_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK1_skl)|~sQ80_spl),
% 0.16/10.95 inference(resolution,[status(thm)],[f1366,f185])).
% 0.16/10.95 fof(f1379,plain,(
% 0.16/10.95 ~sQ43_spl|~sQ64_spl|~sQ80_spl|~sQ46_spl|~sQ40_spl),
% 0.16/10.95 inference(split_clause,[status(thm)],[f1371,f612,f938,f1365,f634,f584])).
% 0.16/10.95 fof(f1380,plain,(
% 0.16/10.95 ~sQ37_spl|~sQ44_spl|sQ38_spl|sQ57_spl|~sQ80_spl),
% 0.16/10.95 inference(split_clause,[status(thm)],[f1372,f575,f628,f578,f811,f1365])).
% 0.16/10.95 fof(f1381,plain,(
% 0.16/10.95 ~sQ37_spl|~sQ44_spl|sQ38_spl|sQ39_spl|~sQ80_spl),
% 0.16/10.95 inference(split_clause,[status(thm)],[f1373,f575,f628,f578,f581,f1365])).
% 0.16/10.95 fof(f1384,plain,(
% 0.16/10.95 sQ43_spl|~sQ48_spl|~sQ42_spl),
% 0.16/10.95 inference(split_clause,[status(thm)],[f1032,f612,f665,f609])).
% 0.16/10.95 fof(f1386,plain,(
% 0.16/10.95 $false),
% 0.16/10.95 inference(sat_refutation,[status(thm)],[f261,f314,f324,f334,f344,f346,f348,f350,f352,f354,f480,f587,f589,f615,f639,f649,f678,f702,f717,f719,f720,f795,f803,f814,f832,f863,f892,f903,f1158,f1175,f1210,f1368,f1379,f1380,f1381,f1384])).
% 0.16/10.95 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/10.96 % Elapsed time: 0.543026 seconds
% 0.16/10.96 % CPU time: 4.002077 seconds
% 0.16/10.96 % Total memory used: 160.935 MB
% 0.16/10.96 % Net memory used: 157.832 MB
%------------------------------------------------------------------------------