%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC379+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:42:19 PM UTC 2026
% Result : Theorem 0.15s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC379+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.53 % Computer : n018.cluster.edu
% 0.10/0.53 % Model : x86_64 x86_64
% 0.10/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.53 % Memory : 8046.5625MB
% 0.10/0.53 % OS : Linux 6.8.0-71-generic
% 0.10/0.53 % CPULimit : 300
% 0.10/0.53 % WCLimit : 300
% 0.10/0.53 % DateTime : Mon Sep 21 08:21:29 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.15/0.55 % Drodi V4.1.1
% 0.15/0.62 % Refutation found
% 0.15/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.62 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.62 fof(f2,axiom,(
% 0.15/0.62 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f3,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ( memberP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(W,cons(V,X)) = U ) )) )) ) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f5,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f6,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f17,axiom,(
% 0.15/0.62 ssList(nil) ),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f28,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f29,axiom,(
% 0.15/0.62 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( ( leq(U,V)& leq(V,U) )=> U = V ) ) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f30,axiom,(
% 0.15/0.62 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> ( ( leq(U,V)& leq(V,W) )=> leq(U,W) ) ) )) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f31,axiom,(
% 0.15/0.62 (! [U] :( ssItem(U)=> leq(U,U) ) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f36,axiom,(
% 0.15/0.62 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f45,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f51,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f84,axiom,(
% 0.15/0.62 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f96,conjecture,(
% 0.15/0.62 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& ( ( ~ memberP(W,Y)& (! [Z] :( ssItem(Z)=> ( ~ memberP(X,Z)| ~ leq(Z,Y)| Y = Z ) ))& memberP(X,Y) )| ( memberP(W,Y)& ( ~ memberP(X,Y)| (? [Z] :( ssItem(Z)& Y != Z& memberP(X,Z)& leq(Z,Y) ) )) ) ) ))| (! [X1] :( ssItem(X1)=> ( ( ~ memberP(U,X1)& ( ~ memberP(V,X1)| (? [X2] :( ssItem(X2)& X1 != X2& memberP(V,X2)& leq(X2,X1) ) )) )| ( (! [X2] :( ssItem(X2)=> ( ~ memberP(V,X2)| ~ leq(X2,X1)| X1 = X2 ) ))& memberP(V,X1)& memberP(U,X1) ) ) ) )) ) )) )) )) )),
% 0.15/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.62 fof(f97,negated_conjecture,(
% 0.15/0.62 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& ( ( ~ memberP(W,Y)& (! [Z] :( ssItem(Z)=> ( ~ memberP(X,Z)| ~ leq(Z,Y)| Y = Z ) ))& memberP(X,Y) )| ( memberP(W,Y)& ( ~ memberP(X,Y)| (? [Z] :( ssItem(Z)& Y != Z& memberP(X,Z)& leq(Z,Y) ) )) ) ) ))| (! [X1] :( ssItem(X1)=> ( ( ~ memberP(U,X1)& ( ~ memberP(V,X1)| (? [X2] :( ssItem(X2)& X1 != X2& memberP(V,X2)& leq(X2,X1) ) )) )| ( (! [X2] :( ssItem(X2)=> ( ~ memberP(V,X2)| ~ leq(X2,X1)| X1 = X2 ) ))& memberP(V,X1)& memberP(U,X1) ) ) ) )) ) )) )) )) ))),
% 0.15/0.62 inference(negated_conjecture,[status(cth)],[f96])).
% 0.15/0.62 fof(f102,plain,(
% 0.15/0.62 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.15/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.15/0.62 fof(f103,plain,(
% 0.15/0.62 ssItem(sK0_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/0.62 fof(f104,plain,(
% 0.15/0.62 ssItem(sK1_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/0.62 fof(f106,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|(memberP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U))))))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.15/0.62 fof(f107,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|((~memberP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U)))))&(memberP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(W,cons(V,X))=U)))))))))),
% 0.15/0.62 inference(NNF_transformation,[status(thm)],[f106])).
% 0.15/0.62 fof(f108,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|((~memberP(U,V)|(ssList(sK2_skl(V,U))&(ssList(sK3_skl(V,U))&app(sK2_skl(V,U),cons(V,sK3_skl(V,U)))=U)))&(memberP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(W,cons(V,X))=U)))))))))),
% 0.15/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W,sK2_skl(V,U)),skolemize(X,sK3_skl(V,U))],[f107])).
% 0.15/0.62 fof(f111,plain,(
% 0.15/0.62 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~memberP(X0,X1)|app(sK2_skl(X1,X0),cons(X1,sK3_skl(X1,X0)))=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f108])).
% 0.15/0.62 fof(f119,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/0.62 fof(f120,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(?[W]: (ssList(W)&app(V,W)=U)))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 0.15/0.62 inference(NNF_transformation,[status(thm)],[f119])).
% 0.15/0.62 fof(f121,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(ssList(sK5_skl(V,U))&app(V,sK5_skl(V,U))=U))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 0.15/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.15/0.62 fof(f123,plain,(
% 0.15/0.62 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/0.62 fof(f124,plain,(
% 0.15/0.62 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/0.62 fof(f125,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.15/0.62 fof(f126,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(?[W]: (ssList(W)&app(W,V)=U)))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.15/0.62 inference(NNF_transformation,[status(thm)],[f125])).
% 0.15/0.62 fof(f127,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(ssList(sK6_skl(V,U))&app(sK6_skl(V,U),V)=U))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.15/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.15/0.62 fof(f129,plain,(
% 0.15/0.62 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/0.62 fof(f130,plain,(
% 0.15/0.62 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/0.62 fof(f223,plain,(
% 0.15/0.62 ssList(nil)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f17])).
% 0.15/0.62 fof(f248,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.15/0.62 fof(f249,plain,(
% 0.15/0.62 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f248])).
% 0.15/0.62 fof(f250,plain,(
% 0.15/0.62 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~leq(U,V)|~leq(V,U))|U=V))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.15/0.62 fof(f251,plain,(
% 0.15/0.62 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f250])).
% 0.15/0.62 fof(f252,plain,(
% 0.15/0.62 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|((~leq(U,V)|~leq(V,W))|leq(U,W)))))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.15/0.62 fof(f253,plain,(
% 0.15/0.62 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssItem(X2)|~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f252])).
% 0.15/0.62 fof(f254,plain,(
% 0.15/0.62 ![U]: (~ssItem(U)|leq(U,U))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.15/0.62 fof(f255,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f254])).
% 0.15/0.62 fof(f268,plain,(
% 0.15/0.62 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.15/0.62 fof(f269,plain,(
% 0.15/0.62 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~memberP(app(V,W),U)|(memberP(V,U)|memberP(W,U)))&(memberP(app(V,W),U)|(~memberP(V,U)&~memberP(W,U)))))))))),
% 0.15/0.62 inference(NNF_transformation,[status(thm)],[f268])).
% 0.15/0.62 fof(f270,plain,(
% 0.15/0.62 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~memberP(app(X1,X2),X0)|memberP(X1,X0)|memberP(X2,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/0.62 fof(f271,plain,(
% 0.15/0.62 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/0.62 fof(f272,plain,(
% 0.15/0.62 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X2,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/0.62 fof(f294,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.15/0.62 fof(f295,plain,(
% 0.15/0.62 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f294])).
% 0.15/0.62 fof(f308,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.15/0.62 fof(f309,plain,(
% 0.15/0.62 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f308])).
% 0.15/0.62 fof(f388,plain,(
% 0.15/0.62 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.15/0.62 fof(f389,plain,(
% 0.15/0.62 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f388])).
% 0.15/0.62 fof(f415,plain,(
% 0.15/0.62 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(![Y]: (~ssItem(Y)|(((memberP(W,Y)|(?[Z]: (ssItem(Z)&((memberP(X,Z)&leq(Z,Y))&~Y=Z))))|~memberP(X,Y))&(~memberP(W,Y)|(memberP(X,Y)&(![Z]: (((~ssItem(Z)|Y=Z)|~memberP(X,Z))|~leq(Z,Y)))))))))&(?[X1]: (ssItem(X1)&((memberP(U,X1)|(memberP(V,X1)&(![X2]: (((~ssItem(X2)|X1=X2)|~memberP(V,X2))|~leq(X2,X1)))))&(((?[X2]: (ssItem(X2)&((memberP(V,X2)&leq(X2,X1))&~X1=X2)))|~memberP(V,X1))|~memberP(U,X1))))))))))))))),
% 0.15/0.62 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.15/0.62 fof(f416,plain,(
% 0.15/0.62 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(![Y]: (~ssItem(Y)|(((memberP(sK49_skl,Y)|(ssItem(sK51_skl(Y))&((memberP(sK50_skl,sK51_skl(Y))&leq(sK51_skl(Y),Y))&~Y=sK51_skl(Y))))|~memberP(sK50_skl,Y))&(~memberP(sK49_skl,Y)|(memberP(sK50_skl,Y)&(![Z]: (((~ssItem(Z)|Y=Z)|~memberP(sK50_skl,Z))|~leq(Z,Y)))))))))&(ssItem(sK52_skl)&((memberP(sK47_skl,sK52_skl)|(memberP(sK48_skl,sK52_skl)&(![X2]: (((~ssItem(X2)|sK52_skl=X2)|~memberP(sK48_skl,X2))|~leq(X2,sK52_skl)))))&(((ssItem(sK53_skl)&((memberP(sK48_skl,sK53_skl)&leq(sK53_skl,sK52_skl))&~sK52_skl=sK53_skl))|~memberP(sK48_skl,sK52_skl))|~memberP(sK47_skl,sK52_skl)))))))))),
% 0.15/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Z,sK51_skl(Y)),skolemize(X1,sK52_skl),skolemize(X2,sK53_skl)],[f415])).
% 0.15/0.62 fof(f417,plain,(
% 0.15/0.62 ssList(sK47_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f418,plain,(
% 0.15/0.62 ssList(sK48_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f421,plain,(
% 0.15/0.62 sK48_skl=sK50_skl),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f422,plain,(
% 0.15/0.62 sK47_skl=sK49_skl),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f423,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK49_skl,X0)|ssItem(sK51_skl(X0))|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f424,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK49_skl,X0)|memberP(sK50_skl,sK51_skl(X0))|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f425,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK49_skl,X0)|leq(sK51_skl(X0),X0)|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f426,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK49_skl,X0)|~X0=sK51_skl(X0)|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f427,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~memberP(sK49_skl,X0)|memberP(sK50_skl,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f428,plain,(
% 0.15/0.62 ![X0,X1]: (~ssItem(X0)|~memberP(sK49_skl,X0)|~ssItem(X1)|X0=X1|~memberP(sK50_skl,X1)|~leq(X1,X0))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f429,plain,(
% 0.15/0.62 ssItem(sK52_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f430,plain,(
% 0.15/0.62 memberP(sK47_skl,sK52_skl)|memberP(sK48_skl,sK52_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f431,plain,(
% 0.15/0.62 ![X0]: (memberP(sK47_skl,sK52_skl)|~ssItem(X0)|sK52_skl=X0|~memberP(sK48_skl,X0)|~leq(X0,sK52_skl))),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f432,plain,(
% 0.15/0.62 ssItem(sK53_skl)|~memberP(sK48_skl,sK52_skl)|~memberP(sK47_skl,sK52_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f433,plain,(
% 0.15/0.62 memberP(sK48_skl,sK53_skl)|~memberP(sK48_skl,sK52_skl)|~memberP(sK47_skl,sK52_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f434,plain,(
% 0.15/0.62 leq(sK53_skl,sK52_skl)|~memberP(sK48_skl,sK52_skl)|~memberP(sK47_skl,sK52_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f435,plain,(
% 0.15/0.62 ~sK52_skl=sK53_skl|~memberP(sK48_skl,sK52_skl)|~memberP(sK47_skl,sK52_skl)),
% 0.15/0.62 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/0.62 fof(f436,definition,(
% 0.15/0.62 sQ0_spl <=> (memberP(sK47_skl,sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f437,plain,(
% 0.15/0.62 memberP(sK47_skl,sK52_skl)|~sQ0_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f436])).
% 0.15/0.62 fof(f439,definition,(
% 0.15/0.62 sQ1_spl <=> (memberP(sK48_skl,sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f440,plain,(
% 0.15/0.62 memberP(sK48_skl,sK52_skl)|~sQ1_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f439])).
% 0.15/0.62 fof(f441,plain,(
% 0.15/0.62 ~memberP(sK48_skl,sK52_skl)|sQ1_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f439])).
% 0.15/0.62 fof(f442,plain,(
% 0.15/0.62 sQ0_spl|sQ1_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f430,f436,f439])).
% 0.15/0.62 fof(f443,definition,(
% 0.15/0.62 ![X0]: (sQ2_spl <=> (~ssItem(X0)|sK52_skl=X0|~memberP(sK48_skl,X0)|~leq(X0,sK52_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f444,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|sK52_skl=X0|~memberP(sK48_skl,X0)|~leq(X0,sK52_skl)|~sQ2_spl)),
% 0.15/0.62 inference(component_clause,[status(thm)],[f443])).
% 0.15/0.62 fof(f446,plain,(
% 0.15/0.62 sQ0_spl|sQ2_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f431,f436,f443])).
% 0.15/0.62 fof(f447,definition,(
% 0.15/0.62 sQ3_spl <=> (ssItem(sK53_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f450,plain,(
% 0.15/0.62 sQ3_spl|~sQ1_spl|~sQ0_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f432,f447,f439,f436])).
% 0.15/0.62 fof(f451,definition,(
% 0.15/0.62 sQ4_spl <=> (memberP(sK48_skl,sK53_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f452,plain,(
% 0.15/0.62 memberP(sK48_skl,sK53_skl)|~sQ4_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f451])).
% 0.15/0.62 fof(f454,plain,(
% 0.15/0.62 sQ4_spl|~sQ1_spl|~sQ0_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f433,f451,f439,f436])).
% 0.15/0.62 fof(f455,definition,(
% 0.15/0.62 sQ5_spl <=> (leq(sK53_skl,sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f458,plain,(
% 0.15/0.62 sQ5_spl|~sQ1_spl|~sQ0_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f434,f455,f439,f436])).
% 0.15/0.62 fof(f459,definition,(
% 0.15/0.62 sQ6_spl <=> (sK52_skl=sK53_skl)),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f462,plain,(
% 0.15/0.62 ~sQ6_spl|~sQ1_spl|~sQ0_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f435,f459,f439,f436])).
% 0.15/0.62 fof(f467,plain,(
% 0.15/0.62 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.15/0.62 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.15/0.62 fof(f468,plain,(
% 0.15/0.62 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 0.15/0.62 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.15/0.62 fof(f495,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~leq(X0,sK52_skl)|~leq(sK52_skl,X0)|X0=sK52_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f251,f429])).
% 0.15/0.62 fof(f496,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~leq(X0,sK0_skl)|~leq(sK0_skl,X0)|X0=sK0_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f103,f251])).
% 0.15/0.62 fof(f497,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~leq(X0,sK1_skl)|~leq(sK1_skl,X0)|X0=sK1_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f104,f251])).
% 0.15/0.62 fof(f499,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(sK50_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f422,f427])).
% 0.15/0.62 fof(f500,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(sK48_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f421,f499])).
% 0.15/0.62 fof(f501,plain,(
% 0.15/0.62 ~ssItem(sK52_skl)|~memberP(sK47_skl,sK52_skl)|sQ1_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f500,f441])).
% 0.15/0.62 fof(f502,definition,(
% 0.15/0.62 sQ7_spl <=> (ssItem(sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f504,plain,(
% 0.15/0.62 ~ssItem(sK52_skl)|sQ7_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f502])).
% 0.15/0.62 fof(f505,plain,(
% 0.15/0.62 ~sQ7_spl|~sQ0_spl|sQ1_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f501,f502,f436,f439])).
% 0.15/0.62 fof(f506,plain,(
% 0.15/0.62 $false|sQ7_spl),
% 0.15/0.62 inference(forward_subsumption_resolution,[status(thm)],[f504,f429])).
% 0.15/0.62 fof(f507,plain,(
% 0.15/0.62 sQ7_spl),
% 0.15/0.62 inference(contradiction_clause,[status(thm)],[f506])).
% 0.15/0.62 fof(f508,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|ssItem(sK51_skl(X0))|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f422,f423])).
% 0.15/0.62 fof(f509,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|ssItem(sK51_skl(X0))|~memberP(sK48_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f421,f508])).
% 0.15/0.62 fof(f511,plain,(
% 0.15/0.62 ~ssItem(sK52_skl)|~leq(sK52_skl,sK52_skl)|sK52_skl=sK52_skl|~ssItem(sK52_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f495,f255])).
% 0.15/0.62 fof(f512,definition,(
% 0.15/0.62 sQ8_spl <=> (leq(sK52_skl,sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f513,plain,(
% 0.15/0.62 leq(sK52_skl,sK52_skl)|~sQ8_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f512])).
% 0.15/0.62 fof(f514,plain,(
% 0.15/0.62 ~leq(sK52_skl,sK52_skl)|sQ8_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f512])).
% 0.15/0.62 fof(f515,definition,(
% 0.15/0.62 sQ9_spl <=> (sK52_skl=sK52_skl)),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f518,plain,(
% 0.15/0.62 ~sQ7_spl|~sQ8_spl|sQ9_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f511,f502,f512,f515])).
% 0.15/0.62 fof(f519,plain,(
% 0.15/0.62 ~ssItem(sK52_skl)|sQ8_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f514,f255])).
% 0.15/0.62 fof(f520,plain,(
% 0.15/0.62 ~sQ7_spl|sQ8_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f519,f502,f512])).
% 0.15/0.62 fof(f523,plain,(
% 0.15/0.62 ~ssItem(sK0_skl)|~leq(sK0_skl,sK0_skl)|sK0_skl=sK0_skl|~ssItem(sK0_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f496,f255])).
% 0.15/0.62 fof(f524,definition,(
% 0.15/0.62 sQ10_spl <=> (ssItem(sK0_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f526,plain,(
% 0.15/0.62 ~ssItem(sK0_skl)|sQ10_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f524])).
% 0.15/0.62 fof(f527,definition,(
% 0.15/0.62 sQ11_spl <=> (leq(sK0_skl,sK0_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f528,plain,(
% 0.15/0.62 leq(sK0_skl,sK0_skl)|~sQ11_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f527])).
% 0.15/0.62 fof(f529,plain,(
% 0.15/0.62 ~leq(sK0_skl,sK0_skl)|sQ11_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f527])).
% 0.15/0.62 fof(f530,definition,(
% 0.15/0.62 sQ12_spl <=> (sK0_skl=sK0_skl)),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f533,plain,(
% 0.15/0.62 ~sQ10_spl|~sQ11_spl|sQ12_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f523,f524,f527,f530])).
% 0.15/0.62 fof(f534,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~ssItem(sK52_skl)|~ssItem(sK52_skl)|~leq(X0,sK52_skl)|leq(X0,sK52_skl)|~sQ8_spl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f253,f513])).
% 0.15/0.62 fof(f537,plain,(
% 0.15/0.62 ![X0,X1]: (~ssItem(sK0_skl)|~ssItem(X0)|~ssItem(X1)|~leq(sK0_skl,X0)|~leq(X0,X1)|~ssItem(X1)|~leq(X1,sK0_skl)|X1=sK0_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f253,f496])).
% 0.15/0.62 fof(f538,plain,(
% 0.15/0.62 ![X0,X1]: (~ssItem(sK52_skl)|~ssItem(X0)|~ssItem(X1)|~leq(sK52_skl,X0)|~leq(X0,X1)|~ssItem(X1)|~leq(X1,sK52_skl)|X1=sK52_skl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f253,f495])).
% 0.15/0.62 fof(f540,definition,(
% 0.15/0.62 ![X0]: (sQ13_spl <=> (~ssItem(X0)|~leq(X0,sK52_skl)|leq(X0,sK52_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f543,plain,(
% 0.15/0.62 sQ13_spl|~sQ7_spl|~sQ8_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f534,f540,f502,f512])).
% 0.15/0.62 fof(f545,definition,(
% 0.15/0.62 ![X0,X1]: (sQ14_spl <=> (~ssItem(X0)|~ssItem(X1)|~leq(sK0_skl,X0)|~leq(X0,X1)|~ssItem(X1)|~leq(X1,sK0_skl)|X1=sK0_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f548,plain,(
% 0.15/0.62 ~sQ10_spl|sQ14_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f537,f524,f545])).
% 0.15/0.62 fof(f549,definition,(
% 0.15/0.62 ![X0,X1]: (sQ15_spl <=> (~ssItem(X0)|~ssItem(X1)|~leq(sK52_skl,X0)|~leq(X0,X1)|~ssItem(X1)|~leq(X1,sK52_skl)|X1=sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f552,plain,(
% 0.15/0.62 ~sQ7_spl|sQ15_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f538,f502,f549])).
% 0.15/0.62 fof(f554,plain,(
% 0.15/0.62 $false|sQ10_spl),
% 0.15/0.62 inference(forward_subsumption_resolution,[status(thm)],[f526,f103])).
% 0.15/0.62 fof(f555,plain,(
% 0.15/0.62 sQ10_spl),
% 0.15/0.62 inference(contradiction_clause,[status(thm)],[f554])).
% 0.15/0.62 fof(f559,plain,(
% 0.15/0.62 ~ssItem(sK0_skl)|sQ11_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f529,f255])).
% 0.15/0.62 fof(f564,plain,(
% 0.15/0.62 ~sQ10_spl|sQ11_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f559,f524,f527])).
% 0.15/0.62 fof(f566,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|~ssItem(sK0_skl)|~ssItem(sK0_skl)|~leq(X0,sK0_skl)|leq(X0,sK0_skl)|~sQ11_spl)),
% 0.15/0.62 inference(resolution,[status(thm)],[f528,f253])).
% 0.15/0.62 fof(f568,definition,(
% 0.15/0.62 ![X0]: (sQ17_spl <=> (~ssItem(X0)|~leq(X0,sK0_skl)|leq(X0,sK0_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f571,plain,(
% 0.15/0.62 sQ17_spl|~sQ10_spl|~sQ11_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f566,f568,f524,f527])).
% 0.15/0.62 fof(f574,plain,(
% 0.15/0.62 ~ssList(sK48_skl)|~ssItem(sK52_skl)|app(sK2_skl(sK52_skl,sK48_skl),cons(sK52_skl,sK3_skl(sK52_skl,sK48_skl)))=sK48_skl|~sQ1_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f111,f440])).
% 0.15/0.62 fof(f575,plain,(
% 0.15/0.62 ![X0]: (~ssList(sK48_skl)|~ssItem(X0)|app(sK2_skl(X0,sK48_skl),cons(X0,sK3_skl(X0,sK48_skl)))=sK48_skl|~ssItem(X0)|~memberP(sK47_skl,X0))),
% 0.15/0.62 inference(resolution,[status(thm)],[f111,f500])).
% 0.15/0.62 fof(f577,definition,(
% 0.15/0.62 sQ18_spl <=> (ssList(sK48_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f579,plain,(
% 0.15/0.62 ~ssList(sK48_skl)|sQ18_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f577])).
% 0.15/0.62 fof(f580,definition,(
% 0.15/0.62 sQ19_spl <=> (app(sK2_skl(sK52_skl,sK48_skl),cons(sK52_skl,sK3_skl(sK52_skl,sK48_skl)))=sK48_skl)),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f583,plain,(
% 0.15/0.62 ~sQ18_spl|~sQ7_spl|sQ19_spl|~sQ1_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f574,f577,f502,f580,f439])).
% 0.15/0.62 fof(f584,definition,(
% 0.15/0.62 ![X0]: (sQ20_spl <=> (~ssItem(X0)|app(sK2_skl(X0,sK48_skl),cons(X0,sK3_skl(X0,sK48_skl)))=sK48_skl|~ssItem(X0)|~memberP(sK47_skl,X0)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f587,plain,(
% 0.15/0.62 ~sQ18_spl|sQ20_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f575,f577,f584])).
% 0.15/0.62 fof(f588,plain,(
% 0.15/0.62 $false|sQ18_spl),
% 0.15/0.62 inference(forward_subsumption_resolution,[status(thm)],[f579,f418])).
% 0.15/0.62 fof(f589,plain,(
% 0.15/0.62 sQ18_spl),
% 0.15/0.62 inference(contradiction_clause,[status(thm)],[f588])).
% 0.15/0.62 fof(f595,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|~X0=sK51_skl(X0)|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f422,f426])).
% 0.15/0.62 fof(f596,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|~X0=sK51_skl(X0)|~memberP(sK48_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f421,f595])).
% 0.15/0.62 fof(f597,plain,(
% 0.15/0.62 ~ssItem(sK52_skl)|memberP(sK47_skl,sK52_skl)|~sK52_skl=sK51_skl(sK52_skl)|~sQ1_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f596,f440])).
% 0.15/0.62 fof(f599,definition,(
% 0.15/0.62 sQ21_spl <=> (sK52_skl=sK51_skl(sK52_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f602,plain,(
% 0.15/0.62 ~sQ7_spl|sQ0_spl|~sQ21_spl|~sQ1_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f597,f502,f436,f599,f439])).
% 0.15/0.62 fof(f603,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|memberP(sK50_skl,sK51_skl(X0))|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f422,f424])).
% 0.15/0.62 fof(f604,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|memberP(sK48_skl,sK51_skl(X0))|~memberP(sK50_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f421,f603])).
% 0.15/0.62 fof(f605,plain,(
% 0.15/0.62 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|memberP(sK48_skl,sK51_skl(X0))|~memberP(sK48_skl,X0))),
% 0.15/0.62 inference(forward_demodulation,[status(thm)],[f421,f604])).
% 0.15/0.62 fof(f606,plain,(
% 0.15/0.62 ~ssItem(sK52_skl)|memberP(sK47_skl,sK52_skl)|memberP(sK48_skl,sK51_skl(sK52_skl))|~sQ1_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f605,f440])).
% 0.15/0.62 fof(f608,definition,(
% 0.15/0.62 sQ22_spl <=> (memberP(sK48_skl,sK51_skl(sK52_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f609,plain,(
% 0.15/0.62 memberP(sK48_skl,sK51_skl(sK52_skl))|~sQ22_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f608])).
% 0.15/0.62 fof(f611,plain,(
% 0.15/0.62 ~sQ7_spl|sQ0_spl|sQ22_spl|~sQ1_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f606,f502,f436,f608,f439])).
% 0.15/0.62 fof(f613,plain,(
% 0.15/0.62 ~ssItem(sK53_skl)|memberP(sK47_skl,sK53_skl)|memberP(sK48_skl,sK51_skl(sK53_skl))|~sQ4_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f452,f605])).
% 0.15/0.62 fof(f614,plain,(
% 0.15/0.62 ~ssItem(sK53_skl)|memberP(sK47_skl,sK53_skl)|~sK53_skl=sK51_skl(sK53_skl)|~sQ4_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f452,f596])).
% 0.15/0.62 fof(f615,plain,(
% 0.15/0.62 ~ssList(sK48_skl)|~ssItem(sK53_skl)|app(sK2_skl(sK53_skl,sK48_skl),cons(sK53_skl,sK3_skl(sK53_skl,sK48_skl)))=sK48_skl|~sQ4_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f452,f111])).
% 0.15/0.62 fof(f616,definition,(
% 0.15/0.62 sQ23_spl <=> (memberP(sK47_skl,sK53_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f617,plain,(
% 0.15/0.62 memberP(sK47_skl,sK53_skl)|~sQ23_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f616])).
% 0.15/0.62 fof(f619,definition,(
% 0.15/0.62 sQ24_spl <=> (memberP(sK48_skl,sK51_skl(sK53_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f620,plain,(
% 0.15/0.62 memberP(sK48_skl,sK51_skl(sK53_skl))|~sQ24_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f619])).
% 0.15/0.62 fof(f622,plain,(
% 0.15/0.62 ~sQ3_spl|sQ23_spl|sQ24_spl|~sQ4_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f613,f447,f616,f619,f451])).
% 0.15/0.62 fof(f623,definition,(
% 0.15/0.62 sQ25_spl <=> (sK53_skl=sK51_skl(sK53_skl))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f626,plain,(
% 0.15/0.62 ~sQ3_spl|sQ23_spl|~sQ25_spl|~sQ4_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f614,f447,f616,f623,f451])).
% 0.15/0.62 fof(f627,definition,(
% 0.15/0.62 sQ26_spl <=> (app(sK2_skl(sK53_skl,sK48_skl),cons(sK53_skl,sK3_skl(sK53_skl,sK48_skl)))=sK48_skl)),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f630,plain,(
% 0.15/0.62 ~sQ18_spl|~sQ3_spl|sQ26_spl|~sQ4_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f615,f577,f447,f627,f451])).
% 0.15/0.62 fof(f650,plain,(
% 0.15/0.62 ~ssItem(sK51_skl(sK53_skl))|memberP(sK47_skl,sK51_skl(sK53_skl))|memberP(sK48_skl,sK51_skl(sK51_skl(sK53_skl)))|~sQ24_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f620,f605])).
% 0.15/0.62 fof(f651,plain,(
% 0.15/0.62 ~ssItem(sK51_skl(sK53_skl))|memberP(sK47_skl,sK51_skl(sK53_skl))|~sK51_skl(sK53_skl)=sK51_skl(sK51_skl(sK53_skl))|~sQ24_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f620,f596])).
% 0.15/0.62 fof(f652,plain,(
% 0.15/0.62 ~ssList(sK48_skl)|~ssItem(sK51_skl(sK53_skl))|app(sK2_skl(sK51_skl(sK53_skl),sK48_skl),cons(sK51_skl(sK53_skl),sK3_skl(sK51_skl(sK53_skl),sK48_skl)))=sK48_skl|~sQ24_spl),
% 0.15/0.62 inference(resolution,[status(thm)],[f620,f111])).
% 0.15/0.62 fof(f653,definition,(
% 0.15/0.62 sQ28_spl <=> (ssItem(sK51_skl(sK53_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f655,plain,(
% 0.15/0.62 ~ssItem(sK51_skl(sK53_skl))|sQ28_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f653])).
% 0.15/0.62 fof(f656,definition,(
% 0.15/0.62 sQ29_spl <=> (memberP(sK47_skl,sK51_skl(sK53_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f657,plain,(
% 0.15/0.62 memberP(sK47_skl,sK51_skl(sK53_skl))|~sQ29_spl),
% 0.15/0.62 inference(component_clause,[status(thm)],[f656])).
% 0.15/0.62 fof(f659,definition,(
% 0.15/0.62 sQ30_spl <=> (memberP(sK48_skl,sK51_skl(sK51_skl(sK53_skl))))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f662,plain,(
% 0.15/0.62 ~sQ28_spl|sQ29_spl|sQ30_spl|~sQ24_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f650,f653,f656,f659,f619])).
% 0.15/0.62 fof(f663,definition,(
% 0.15/0.62 sQ31_spl <=> (sK51_skl(sK53_skl)=sK51_skl(sK51_skl(sK53_skl)))),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f666,plain,(
% 0.15/0.62 ~sQ28_spl|sQ29_spl|~sQ31_spl|~sQ24_spl),
% 0.15/0.62 inference(split_clause,[status(thm)],[f651,f653,f656,f663,f619])).
% 0.15/0.62 fof(f667,definition,(
% 0.15/0.62 sQ32_spl <=> (app(sK2_skl(sK51_skl(sK53_skl),sK48_skl),cons(sK51_skl(sK53_skl),sK3_skl(sK51_skl(sK53_skl),sK48_skl)))=sK48_skl)),
% 0.15/0.62 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/0.62 fof(f670,plain,(
% 0.15/0.62 ~sQ18_spl|~sQ28_spl|sQ32_spl|~sQ24_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f652,f577,f653,f667,f619])).
% 0.15/0.63 fof(f671,plain,(
% 0.15/0.63 ~ssItem(sK53_skl)|memberP(sK47_skl,sK53_skl)|~memberP(sK48_skl,sK53_skl)|sQ28_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f655,f509])).
% 0.15/0.63 fof(f672,plain,(
% 0.15/0.63 ~sQ3_spl|sQ23_spl|~sQ4_spl|sQ28_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f671,f447,f616,f451,f653])).
% 0.15/0.63 fof(f675,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|leq(sK51_skl(X0),X0)|~memberP(sK50_skl,X0))),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f422,f425])).
% 0.15/0.63 fof(f676,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|memberP(sK47_skl,X0)|leq(sK51_skl(X0),X0)|~memberP(sK48_skl,X0))),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f421,f675])).
% 0.15/0.63 fof(f683,definition,(
% 0.15/0.63 sQ33_spl <=> (ssItem(sK51_skl(sK52_skl)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f685,plain,(
% 0.15/0.63 ~ssItem(sK51_skl(sK52_skl))|sQ33_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f683])).
% 0.15/0.63 fof(f701,plain,(
% 0.15/0.63 ~ssItem(sK52_skl)|memberP(sK47_skl,sK52_skl)|~memberP(sK48_skl,sK52_skl)|sQ33_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f685,f509])).
% 0.15/0.63 fof(f702,plain,(
% 0.15/0.63 ~sQ7_spl|sQ0_spl|~sQ1_spl|sQ33_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f701,f502,f436,f439,f683])).
% 0.15/0.63 fof(f704,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssItem(sK51_skl(sK53_skl))|app(sK2_skl(sK51_skl(sK53_skl),sK47_skl),cons(sK51_skl(sK53_skl),sK3_skl(sK51_skl(sK53_skl),sK47_skl)))=sK47_skl|~sQ29_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f657,f111])).
% 0.15/0.63 fof(f705,definition,(
% 0.15/0.63 sQ38_spl <=> (ssList(sK47_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f707,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|sQ38_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f705])).
% 0.15/0.63 fof(f708,definition,(
% 0.15/0.63 sQ39_spl <=> (app(sK2_skl(sK51_skl(sK53_skl),sK47_skl),cons(sK51_skl(sK53_skl),sK3_skl(sK51_skl(sK53_skl),sK47_skl)))=sK47_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f711,plain,(
% 0.15/0.63 ~sQ38_spl|~sQ28_spl|sQ39_spl|~sQ29_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f704,f705,f653,f708,f656])).
% 0.15/0.63 fof(f712,plain,(
% 0.15/0.63 $false|sQ38_spl),
% 0.15/0.63 inference(forward_subsumption_resolution,[status(thm)],[f707,f417])).
% 0.15/0.63 fof(f713,plain,(
% 0.15/0.63 sQ38_spl),
% 0.15/0.63 inference(contradiction_clause,[status(thm)],[f712])).
% 0.15/0.63 fof(f726,plain,(
% 0.15/0.63 app(nil,nil)=nil),
% 0.15/0.63 inference(resolution,[status(thm)],[f249,f223])).
% 0.15/0.63 fof(f727,plain,(
% 0.15/0.63 app(nil,sK48_skl)=sK48_skl),
% 0.15/0.63 inference(resolution,[status(thm)],[f249,f418])).
% 0.15/0.63 fof(f728,plain,(
% 0.15/0.63 app(nil,sK47_skl)=sK47_skl),
% 0.15/0.63 inference(resolution,[status(thm)],[f249,f417])).
% 0.15/0.63 fof(f729,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|memberP(nil,X0)|~memberP(nil,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f726,f272])).
% 0.15/0.63 fof(f731,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f726,f270])).
% 0.15/0.63 fof(f732,definition,(
% 0.15/0.63 ![X0]: (sQ41_spl <=> (~ssItem(X0)|memberP(nil,X0)|~memberP(nil,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f735,definition,(
% 0.15/0.63 sQ42_spl <=> (ssList(nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f737,plain,(
% 0.15/0.63 ~ssList(nil)|sQ42_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f735])).
% 0.15/0.63 fof(f738,plain,(
% 0.15/0.63 sQ41_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f729,f732,f735])).
% 0.15/0.63 fof(f740,definition,(
% 0.15/0.63 ![X0]: (sQ43_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f743,plain,(
% 0.15/0.63 sQ43_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f731,f740,f735])).
% 0.15/0.63 fof(f744,plain,(
% 0.15/0.63 $false|sQ42_spl),
% 0.15/0.63 inference(forward_subsumption_resolution,[status(thm)],[f737,f223])).
% 0.15/0.63 fof(f745,plain,(
% 0.15/0.63 sQ42_spl),
% 0.15/0.63 inference(contradiction_clause,[status(thm)],[f744])).
% 0.15/0.63 fof(f746,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK48_skl)|memberP(sK48_skl,X0)|~memberP(sK48_skl,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f727,f272])).
% 0.15/0.63 fof(f747,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK48_skl)|memberP(sK48_skl,X0)|~memberP(nil,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f727,f271])).
% 0.15/0.63 fof(f748,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK48_skl)|~memberP(sK48_skl,X0)|memberP(nil,X0)|memberP(sK48_skl,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f727,f270])).
% 0.15/0.63 fof(f749,definition,(
% 0.15/0.63 ![X0]: (sQ44_spl <=> (~ssItem(X0)|memberP(sK48_skl,X0)|~memberP(sK48_skl,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f752,plain,(
% 0.15/0.63 sQ44_spl|~sQ42_spl|~sQ18_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f746,f749,f735,f577])).
% 0.15/0.63 fof(f753,definition,(
% 0.15/0.63 ![X0]: (sQ45_spl <=> (~ssItem(X0)|memberP(sK48_skl,X0)|~memberP(nil,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f756,plain,(
% 0.15/0.63 sQ45_spl|~sQ42_spl|~sQ18_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f747,f753,f735,f577])).
% 0.15/0.63 fof(f757,definition,(
% 0.15/0.63 ![X0]: (sQ46_spl <=> (~ssItem(X0)|~memberP(sK48_skl,X0)|memberP(nil,X0)|memberP(sK48_skl,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f760,plain,(
% 0.15/0.63 sQ46_spl|~sQ42_spl|~sQ18_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f748,f757,f735,f577])).
% 0.15/0.63 fof(f761,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK47_skl)|memberP(sK47_skl,X0)|~memberP(sK47_skl,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f728,f272])).
% 0.15/0.63 fof(f762,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK47_skl)|memberP(sK47_skl,X0)|~memberP(nil,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f728,f271])).
% 0.15/0.63 fof(f763,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK47_skl)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK47_skl,X0))),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f728,f270])).
% 0.15/0.63 fof(f764,definition,(
% 0.15/0.63 ![X0]: (sQ47_spl <=> (~ssItem(X0)|memberP(sK47_skl,X0)|~memberP(sK47_skl,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f767,plain,(
% 0.15/0.63 sQ47_spl|~sQ42_spl|~sQ38_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f761,f764,f735,f705])).
% 0.15/0.63 fof(f768,definition,(
% 0.15/0.63 ![X0]: (sQ48_spl <=> (~ssItem(X0)|memberP(sK47_skl,X0)|~memberP(nil,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f771,plain,(
% 0.15/0.63 sQ48_spl|~sQ42_spl|~sQ38_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f762,f768,f735,f705])).
% 0.15/0.63 fof(f772,definition,(
% 0.15/0.63 ![X0]: (sQ49_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK47_skl,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f775,plain,(
% 0.15/0.63 sQ49_spl|~sQ42_spl|~sQ38_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f763,f772,f735,f705])).
% 0.15/0.63 fof(f780,plain,(
% 0.15/0.63 app(sK48_skl,nil)=sK48_skl),
% 0.15/0.63 inference(resolution,[status(thm)],[f389,f418])).
% 0.15/0.63 fof(f781,plain,(
% 0.15/0.63 app(sK47_skl,nil)=sK47_skl),
% 0.15/0.63 inference(resolution,[status(thm)],[f389,f417])).
% 0.15/0.63 fof(f788,plain,(
% 0.15/0.63 ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 0.15/0.63 inference(resolution,[status(thm)],[f123,f295])).
% 0.15/0.63 fof(f790,definition,(
% 0.15/0.63 ![X0]: (sQ50_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f793,plain,(
% 0.15/0.63 sQ50_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f788,f790,f735])).
% 0.15/0.63 fof(f796,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(sK48_skl)|frontsegP(app(sK48_skl,nil),sK48_skl)|~ssList(nil)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f780,f467])).
% 0.15/0.63 fof(f797,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f728,f467])).
% 0.15/0.63 fof(f798,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(nil)|frontsegP(app(nil,sK48_skl),nil)|~ssList(sK48_skl)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f727,f467])).
% 0.15/0.63 fof(f799,plain,(
% 0.15/0.63 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f726,f467])).
% 0.15/0.63 fof(f800,definition,(
% 0.15/0.63 sQ51_spl <=> (frontsegP(app(sK48_skl,nil),sK48_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f801,plain,(
% 0.15/0.63 frontsegP(app(sK48_skl,nil),sK48_skl)|~sQ51_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f800])).
% 0.15/0.63 fof(f803,plain,(
% 0.15/0.63 ~sQ18_spl|sQ51_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f796,f577,f800,f735])).
% 0.15/0.63 fof(f804,definition,(
% 0.15/0.63 sQ52_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f805,plain,(
% 0.15/0.63 frontsegP(app(nil,sK47_skl),nil)|~sQ52_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f804])).
% 0.15/0.63 fof(f807,plain,(
% 0.15/0.63 ~sQ38_spl|~sQ42_spl|sQ52_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f797,f705,f735,f804])).
% 0.15/0.63 fof(f808,definition,(
% 0.15/0.63 sQ53_spl <=> (frontsegP(app(nil,sK48_skl),nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f809,plain,(
% 0.15/0.63 frontsegP(app(nil,sK48_skl),nil)|~sQ53_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f808])).
% 0.15/0.63 fof(f811,plain,(
% 0.15/0.63 ~sQ18_spl|~sQ42_spl|sQ53_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f798,f577,f735,f808])).
% 0.15/0.63 fof(f812,definition,(
% 0.15/0.63 sQ54_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f813,plain,(
% 0.15/0.63 frontsegP(app(nil,nil),nil)|~sQ54_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f812])).
% 0.15/0.63 fof(f815,plain,(
% 0.15/0.63 ~sQ42_spl|sQ54_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f799,f735,f812])).
% 0.15/0.63 fof(f816,plain,(
% 0.15/0.63 frontsegP(sK48_skl,sK48_skl)|~sQ51_spl),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f780,f801])).
% 0.15/0.63 fof(f817,plain,(
% 0.15/0.63 frontsegP(sK48_skl,nil)|~sQ53_spl),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f727,f809])).
% 0.15/0.63 fof(f818,plain,(
% 0.15/0.63 frontsegP(sK47_skl,nil)|~sQ52_spl),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f728,f805])).
% 0.15/0.63 fof(f819,plain,(
% 0.15/0.63 frontsegP(nil,nil)|~sQ54_spl),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f726,f813])).
% 0.15/0.63 fof(f822,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl|~sQ51_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f816,f123])).
% 0.15/0.63 fof(f823,definition,(
% 0.15/0.63 sQ55_spl <=> (app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f826,plain,(
% 0.15/0.63 ~sQ18_spl|sQ55_spl|~sQ51_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f822,f577,f823,f800])).
% 0.15/0.63 fof(f827,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK48_skl))=sK48_skl|~sQ53_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f817,f123])).
% 0.15/0.63 fof(f828,definition,(
% 0.15/0.63 sQ56_spl <=> (app(nil,sK5_skl(nil,sK48_skl))=sK48_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f831,plain,(
% 0.15/0.63 ~sQ18_spl|~sQ42_spl|sQ56_spl|~sQ53_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f827,f577,f735,f828,f808])).
% 0.15/0.63 fof(f832,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ52_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f818,f123])).
% 0.15/0.63 fof(f833,definition,(
% 0.15/0.63 sQ57_spl <=> (app(nil,sK5_skl(nil,sK47_skl))=sK47_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f836,plain,(
% 0.15/0.63 ~sQ38_spl|~sQ42_spl|sQ57_spl|~sQ52_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f832,f705,f735,f833,f804])).
% 0.15/0.63 fof(f837,plain,(
% 0.15/0.63 ![X0,X1]: (~ssItem(X0)|~memberP(sK47_skl,X0)|~ssItem(X1)|X0=X1|~memberP(sK50_skl,X1)|~leq(X1,X0))),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f422,f428])).
% 0.15/0.63 fof(f838,plain,(
% 0.15/0.63 ![X0,X1]: (~ssItem(X0)|~memberP(sK47_skl,X0)|~ssItem(X1)|X0=X1|~memberP(sK48_skl,X1)|~leq(X1,X0))),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f421,f837])).
% 0.15/0.63 fof(f844,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f781,f467])).
% 0.15/0.63 fof(f848,definition,(
% 0.15/0.63 sQ59_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f849,plain,(
% 0.15/0.63 frontsegP(app(sK47_skl,nil),sK47_skl)|~sQ59_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f848])).
% 0.15/0.63 fof(f851,plain,(
% 0.15/0.63 ~sQ38_spl|sQ59_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f844,f705,f848,f735])).
% 0.15/0.63 fof(f855,plain,(
% 0.15/0.63 frontsegP(sK47_skl,sK47_skl)|~sQ59_spl),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f781,f849])).
% 0.15/0.63 fof(f856,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ59_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f855,f123])).
% 0.15/0.63 fof(f857,definition,(
% 0.15/0.63 sQ60_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f860,plain,(
% 0.15/0.63 ~sQ38_spl|sQ60_spl|~sQ59_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f856,f705,f857,f848])).
% 0.15/0.63 fof(f889,plain,(
% 0.15/0.63 ~ssItem(sK51_skl(sK52_skl))|sK52_skl=sK51_skl(sK52_skl)|~leq(sK51_skl(sK52_skl),sK52_skl)|~sQ2_spl|~sQ22_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f444,f609])).
% 0.15/0.63 fof(f899,definition,(
% 0.15/0.63 sQ68_spl <=> (leq(sK51_skl(sK52_skl),sK52_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f901,plain,(
% 0.15/0.63 ~leq(sK51_skl(sK52_skl),sK52_skl)|sQ68_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f899])).
% 0.15/0.63 fof(f902,plain,(
% 0.15/0.63 ~sQ33_spl|sQ21_spl|~sQ68_spl|~sQ2_spl|~sQ22_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f889,f683,f599,f899,f443,f608])).
% 0.15/0.63 fof(f905,plain,(
% 0.15/0.63 ![X0,X1]: (~ssItem(X0)|~leq(X0,sK1_skl)|X0=sK1_skl|~ssItem(sK1_skl)|~ssItem(X1)|~ssItem(X0)|~leq(sK1_skl,X1)|~leq(X1,X0))),
% 0.15/0.63 inference(resolution,[status(thm)],[f497,f253])).
% 0.15/0.63 fof(f906,plain,(
% 0.15/0.63 ~ssItem(sK1_skl)|~leq(sK1_skl,sK1_skl)|sK1_skl=sK1_skl|~ssItem(sK1_skl)),
% 0.15/0.63 inference(resolution,[status(thm)],[f497,f255])).
% 0.15/0.63 fof(f907,definition,(
% 0.15/0.63 ![X0,X1]: (sQ69_spl <=> (~ssItem(X0)|~leq(X0,sK1_skl)|X0=sK1_skl|~ssItem(X1)|~ssItem(X0)|~leq(sK1_skl,X1)|~leq(X1,X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f910,definition,(
% 0.15/0.63 sQ70_spl <=> (ssItem(sK1_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f912,plain,(
% 0.15/0.63 ~ssItem(sK1_skl)|sQ70_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f910])).
% 0.15/0.63 fof(f913,plain,(
% 0.15/0.63 sQ69_spl|~sQ70_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f905,f907,f910])).
% 0.15/0.63 fof(f914,definition,(
% 0.15/0.63 sQ71_spl <=> (leq(sK1_skl,sK1_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f915,plain,(
% 0.15/0.63 leq(sK1_skl,sK1_skl)|~sQ71_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f914])).
% 0.15/0.63 fof(f916,plain,(
% 0.15/0.63 ~leq(sK1_skl,sK1_skl)|sQ71_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f914])).
% 0.15/0.63 fof(f917,definition,(
% 0.15/0.63 sQ72_spl <=> (sK1_skl=sK1_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f920,plain,(
% 0.15/0.63 ~sQ70_spl|~sQ71_spl|sQ72_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f906,f910,f914,f917])).
% 0.15/0.63 fof(f921,plain,(
% 0.15/0.63 $false|sQ70_spl),
% 0.15/0.63 inference(forward_subsumption_resolution,[status(thm)],[f912,f104])).
% 0.15/0.63 fof(f922,plain,(
% 0.15/0.63 sQ70_spl),
% 0.15/0.63 inference(contradiction_clause,[status(thm)],[f921])).
% 0.15/0.63 fof(f924,plain,(
% 0.15/0.63 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ54_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f819,f123])).
% 0.15/0.63 fof(f925,definition,(
% 0.15/0.63 sQ73_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f928,plain,(
% 0.15/0.63 ~sQ42_spl|sQ73_spl|~sQ54_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f924,f735,f925,f812])).
% 0.15/0.63 fof(f930,plain,(
% 0.15/0.63 ~ssItem(sK1_skl)|sQ71_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f916,f255])).
% 0.15/0.63 fof(f935,plain,(
% 0.15/0.63 ~sQ70_spl|sQ71_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f930,f910,f914])).
% 0.15/0.63 fof(f937,plain,(
% 0.15/0.63 ![X0]: (~ssItem(X0)|~ssItem(sK1_skl)|~ssItem(sK1_skl)|~leq(X0,sK1_skl)|leq(X0,sK1_skl)|~sQ71_spl)),
% 0.15/0.63 inference(resolution,[status(thm)],[f915,f253])).
% 0.15/0.63 fof(f939,definition,(
% 0.15/0.63 ![X0]: (sQ75_spl <=> (~ssItem(X0)|~leq(X0,sK1_skl)|leq(X0,sK1_skl)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f942,plain,(
% 0.15/0.63 sQ75_spl|~sQ70_spl|~sQ71_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f937,f939,f910,f914])).
% 0.15/0.63 fof(f943,plain,(
% 0.15/0.63 ~ssItem(sK52_skl)|memberP(sK47_skl,sK52_skl)|~memberP(sK48_skl,sK52_skl)|sQ68_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f901,f676])).
% 0.15/0.63 fof(f945,plain,(
% 0.15/0.63 ~sQ7_spl|sQ0_spl|~sQ1_spl|sQ68_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f943,f502,f436,f439,f899])).
% 0.15/0.63 fof(f958,plain,(
% 0.15/0.63 ![X0]: (~ssItem(sK53_skl)|~ssItem(X0)|sK53_skl=X0|~memberP(sK48_skl,X0)|~leq(X0,sK53_skl)|~sQ23_spl)),
% 0.15/0.63 inference(resolution,[status(thm)],[f617,f838])).
% 0.15/0.63 fof(f959,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssItem(sK53_skl)|app(sK2_skl(sK53_skl,sK47_skl),cons(sK53_skl,sK3_skl(sK53_skl,sK47_skl)))=sK47_skl|~sQ23_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f617,f111])).
% 0.15/0.63 fof(f960,definition,(
% 0.15/0.63 ![X0]: (sQ77_spl <=> (~ssItem(X0)|sK53_skl=X0|~memberP(sK48_skl,X0)|~leq(X0,sK53_skl)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f963,plain,(
% 0.15/0.63 ~sQ3_spl|sQ77_spl|~sQ23_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f958,f447,f960,f616])).
% 0.15/0.63 fof(f964,definition,(
% 0.15/0.63 sQ78_spl <=> (app(sK2_skl(sK53_skl,sK47_skl),cons(sK53_skl,sK3_skl(sK53_skl,sK47_skl)))=sK47_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f967,plain,(
% 0.15/0.63 ~sQ38_spl|~sQ3_spl|sQ78_spl|~sQ23_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f959,f705,f447,f964,f616])).
% 0.15/0.63 fof(f968,plain,(
% 0.15/0.63 ![X0]: (~ssItem(sK52_skl)|~ssItem(X0)|sK52_skl=X0|~memberP(sK48_skl,X0)|~leq(X0,sK52_skl)|~sQ0_spl)),
% 0.15/0.63 inference(resolution,[status(thm)],[f437,f838])).
% 0.15/0.63 fof(f970,plain,(
% 0.15/0.63 ~sQ7_spl|sQ2_spl|~sQ0_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f968,f502,f443,f436])).
% 0.15/0.63 fof(f975,plain,(
% 0.15/0.63 ![X0]: (~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0))),
% 0.15/0.63 inference(resolution,[status(thm)],[f129,f309])).
% 0.15/0.63 fof(f977,definition,(
% 0.15/0.63 ![X0]: (sQ80_spl <=> (~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0)))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f980,plain,(
% 0.15/0.63 sQ80_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f975,f977,f735])).
% 0.15/0.63 fof(f983,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssList(nil)|rearsegP(app(sK47_skl,nil),nil)|~ssList(sK47_skl)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f781,f468])).
% 0.15/0.63 fof(f984,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(nil)|rearsegP(app(sK48_skl,nil),nil)|~ssList(sK48_skl)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f780,f468])).
% 0.15/0.63 fof(f985,plain,(
% 0.15/0.63 ~ssList(sK47_skl)|~ssList(sK47_skl)|rearsegP(app(nil,sK47_skl),sK47_skl)|~ssList(nil)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f728,f468])).
% 0.15/0.63 fof(f986,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(sK48_skl)|rearsegP(app(nil,sK48_skl),sK48_skl)|~ssList(nil)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f727,f468])).
% 0.15/0.63 fof(f987,plain,(
% 0.15/0.63 ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.15/0.63 inference(paramodulation,[status(thm)],[f726,f468])).
% 0.15/0.63 fof(f988,definition,(
% 0.15/0.63 sQ81_spl <=> (rearsegP(app(sK47_skl,nil),nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f991,plain,(
% 0.15/0.63 ~sQ38_spl|~sQ42_spl|sQ81_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f983,f705,f735,f988])).
% 0.15/0.63 fof(f992,definition,(
% 0.15/0.63 sQ82_spl <=> (rearsegP(app(sK48_skl,nil),nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f993,plain,(
% 0.15/0.63 rearsegP(app(sK48_skl,nil),nil)|~sQ82_spl),
% 0.15/0.63 inference(component_clause,[status(thm)],[f992])).
% 0.15/0.63 fof(f995,plain,(
% 0.15/0.63 ~sQ18_spl|~sQ42_spl|sQ82_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f984,f577,f735,f992])).
% 0.15/0.63 fof(f996,definition,(
% 0.15/0.63 sQ83_spl <=> (rearsegP(app(nil,sK47_skl),sK47_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f999,plain,(
% 0.15/0.63 ~sQ38_spl|sQ83_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f985,f705,f996,f735])).
% 0.15/0.63 fof(f1000,definition,(
% 0.15/0.63 sQ84_spl <=> (rearsegP(app(nil,sK48_skl),sK48_skl))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f1003,plain,(
% 0.15/0.63 ~sQ18_spl|sQ84_spl|~sQ42_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f986,f577,f1000,f735])).
% 0.15/0.63 fof(f1004,definition,(
% 0.15/0.63 sQ85_spl <=> (rearsegP(app(nil,nil),nil))),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f1007,plain,(
% 0.15/0.63 ~sQ42_spl|sQ85_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f987,f735,f1004])).
% 0.15/0.63 fof(f1008,plain,(
% 0.15/0.63 rearsegP(sK48_skl,nil)|~sQ82_spl),
% 0.15/0.63 inference(forward_demodulation,[status(thm)],[f780,f993])).
% 0.15/0.63 fof(f1019,plain,(
% 0.15/0.63 ~ssList(sK48_skl)|~ssList(nil)|app(sK6_skl(nil,sK48_skl),nil)=sK48_skl|~sQ82_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f1008,f129])).
% 0.15/0.63 fof(f1020,definition,(
% 0.15/0.63 sQ86_spl <=> (app(sK6_skl(nil,sK48_skl),nil)=sK48_skl)),
% 0.15/0.63 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.15/0.63 fof(f1023,plain,(
% 0.15/0.63 ~sQ18_spl|~sQ42_spl|sQ86_spl|~sQ82_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f1019,f577,f735,f1020,f992])).
% 0.15/0.63 fof(f1024,plain,(
% 0.15/0.63 ~ssItem(sK53_skl)|sK52_skl=sK53_skl|~leq(sK53_skl,sK52_skl)|~sQ2_spl|~sQ4_spl),
% 0.15/0.63 inference(resolution,[status(thm)],[f444,f452])).
% 0.15/0.63 fof(f1027,plain,(
% 0.15/0.63 ~sQ3_spl|sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl),
% 0.15/0.63 inference(split_clause,[status(thm)],[f1024,f447,f459,f455,f443,f451])).
% 0.15/0.63 fof(f1030,plain,(
% 0.15/0.63 $false),
% 0.15/0.63 inference(sat_refutation,[status(thm)],[f442,f446,f450,f454,f458,f462,f505,f507,f518,f520,f533,f543,f548,f552,f555,f564,f571,f583,f587,f589,f602,f611,f622,f626,f630,f662,f666,f670,f672,f702,f711,f713,f738,f743,f745,f752,f756,f760,f767,f771,f775,f793,f803,f807,f811,f815,f826,f831,f836,f851,f860,f902,f913,f920,f922,f928,f935,f942,f945,f963,f967,f970,f980,f991,f995,f999,f1003,f1007,f1023,f1027])).
% 0.15/0.63 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.64 % Elapsed time: 0.097748 seconds
% 0.15/0.64 % CPU time: 0.430186 seconds
% 0.15/0.64 % Total memory used: 115.499 MB
% 0.15/0.64 % Net memory used: 115.036 MB
%------------------------------------------------------------------------------