%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC279+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 : n026.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:03 PM UTC 2026
% Result : Theorem 0.22s 6.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC279+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.44 % Computer : n026.cluster.edu
% 0.18/5.44 % Model : x86_64 x86_64
% 0.18/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.44 % Memory : 8046.5625MB
% 0.18/5.44 % OS : Linux 6.8.0-71-generic
% 0.18/5.44 % CPULimit : 300
% 0.18/5.44 % WCLimit : 300
% 0.18/5.44 % DateTime : Mon Sep 21 08:14:28 UTC 2026
% 0.18/5.44 % CPUTime :
% 0.18/5.45 % Drodi V4.1.1
% 0.22/6.00 % Refutation found
% 0.22/6.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/6.00 % SZS output start CNFRefutation for theBenchmark
% 0.22/6.00 fof(f2,axiom,(
% 0.22/6.00 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f5,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f7,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f17,axiom,(
% 0.22/6.00 ssList(nil) ),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f19,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssItem(X)=> ( cons(W,U) = cons(X,V)=> ( W = X& V = U ) ) ) )) )) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f28,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f29,axiom,(
% 0.22/6.00 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( ( leq(U,V)& leq(V,U) )=> U = V ) ) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f30,axiom,(
% 0.22/6.00 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> ( ( leq(U,V)& leq(V,W) )=> leq(U,W) ) ) )) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f31,axiom,(
% 0.22/6.00 (! [U] :( ssItem(U)=> leq(U,U) ) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f36,axiom,(
% 0.22/6.00 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f79,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(W,V) = app(U,V)=> W = U ) ) )) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f80,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(V,W) = app(V,U)=> W = U ) ) )) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f83,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( nil = app(U,V)<=> ( nil = V& nil = U ) ) ) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f84,axiom,(
% 0.22/6.00 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f96,conjecture,(
% 0.22/6.00 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Z,cons(Y,nil)),X1) = W& (? [X2] :( ssItem(X2)& ( ( ~ leq(Y,X2)& memberP(X1,X2) )| ( ~ leq(X2,Y)& memberP(Z,X2) ) ) ) )) )) )))| (! [X3] :( ssItem(X3)=> (! [X4] :( ssList(X4)=> (! [X5] :( ssList(X5)=> ( app(app(X4,cons(X3,nil)),X5) != U| (! [X6] :( ssItem(X6)=> ( ( ~ memberP(X4,X6)| leq(X6,X3) )& ( ~ memberP(X5,X6)| leq(X3,X6) ) ) ) )) ) )) )) )) ) )) )) )) )),
% 0.22/6.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/6.00 fof(f97,negated_conjecture,(
% 0.22/6.00 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Z,cons(Y,nil)),X1) = W& (? [X2] :( ssItem(X2)& ( ( ~ leq(Y,X2)& memberP(X1,X2) )| ( ~ leq(X2,Y)& memberP(Z,X2) ) ) ) )) )) )))| (! [X3] :( ssItem(X3)=> (! [X4] :( ssList(X4)=> (! [X5] :( ssList(X5)=> ( app(app(X4,cons(X3,nil)),X5) != U| (! [X6] :( ssItem(X6)=> ( ( ~ memberP(X4,X6)| leq(X6,X3) )& ( ~ memberP(X5,X6)| leq(X3,X6) ) ) ) )) ) )) )) )) ) )) )) )) ))),
% 0.22/6.00 inference(negated_conjecture,[status(cth)],[f96])).
% 0.22/6.00 fof(f102,plain,(
% 0.22/6.00 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.22/6.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.22/6.00 fof(f103,plain,(
% 0.22/6.00 ssItem(sK0_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f102])).
% 0.22/6.00 fof(f104,plain,(
% 0.22/6.00 ssItem(sK1_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f102])).
% 0.22/6.00 fof(f119,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.22/6.00 fof(f120,plain,(
% 0.22/6.00 ![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.22/6.00 inference(NNF_transformation,[status(thm)],[f119])).
% 0.22/6.00 fof(f121,plain,(
% 0.22/6.00 ![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.22/6.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.22/6.00 fof(f124,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f121])).
% 0.22/6.00 fof(f131,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.22/6.00 fof(f132,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U)))))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 0.22/6.00 inference(NNF_transformation,[status(thm)],[f131])).
% 0.22/6.00 fof(f133,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(ssList(sK7_skl(V,U))&(ssList(sK8_skl(V,U))&app(app(sK7_skl(V,U),V),sK8_skl(V,U))=U)))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 0.22/6.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 0.22/6.00 fof(f137,plain,(
% 0.22/6.00 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f133])).
% 0.22/6.00 fof(f223,plain,(
% 0.22/6.00 ssList(nil)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f17])).
% 0.22/6.00 fof(f226,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssItem(W)|(![X]: (~ssItem(X)|(~cons(W,U)=cons(X,V)|(W=X&V=U)))))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.22/6.00 fof(f227,plain,(
% 0.22/6.00 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X2=X3)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f226])).
% 0.22/6.00 fof(f248,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.22/6.00 fof(f249,plain,(
% 0.22/6.00 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f248])).
% 0.22/6.00 fof(f250,plain,(
% 0.22/6.00 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~leq(U,V)|~leq(V,U))|U=V))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.22/6.00 fof(f251,plain,(
% 0.22/6.00 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f250])).
% 0.22/6.00 fof(f252,plain,(
% 0.22/6.00 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|((~leq(U,V)|~leq(V,W))|leq(U,W)))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.22/6.00 fof(f253,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssItem(X2)|~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f252])).
% 0.22/6.00 fof(f254,plain,(
% 0.22/6.00 ![U]: (~ssItem(U)|leq(U,U))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.22/6.00 fof(f255,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f254])).
% 0.22/6.00 fof(f268,plain,(
% 0.22/6.00 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.22/6.00 fof(f269,plain,(
% 0.22/6.00 ![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.22/6.00 inference(NNF_transformation,[status(thm)],[f268])).
% 0.22/6.00 fof(f270,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~memberP(app(X1,X2),X0)|memberP(X1,X0)|memberP(X2,X0))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f269])).
% 0.22/6.00 fof(f271,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f269])).
% 0.22/6.00 fof(f375,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(W,V)=app(U,V)|W=U))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 0.22/6.00 fof(f376,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X2,X1)=app(X0,X1)|X2=X0)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f375])).
% 0.22/6.00 fof(f377,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(V,W)=app(V,U)|W=U))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 0.22/6.00 fof(f378,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X1,X2)=app(X1,X0)|X2=X0)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f377])).
% 0.22/6.00 fof(f383,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(nil=app(U,V)<=>(nil=V&nil=U)))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 0.22/6.00 fof(f384,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~nil=app(U,V)|(nil=V&nil=U))&(nil=app(U,V)|(~nil=V|~nil=U))))))),
% 0.22/6.00 inference(NNF_transformation,[status(thm)],[f383])).
% 0.22/6.00 fof(f385,plain,(
% 0.22/6.00 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~nil=app(X0,X1)|nil=X1)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f384])).
% 0.22/6.00 fof(f388,plain,(
% 0.22/6.00 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.22/6.00 fof(f389,plain,(
% 0.22/6.00 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f388])).
% 0.22/6.00 fof(f415,plain,(
% 0.22/6.00 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=W)|(![X2]: (~ssItem(X2)|((leq(Y,X2)|~memberP(X1,X2))&(leq(X2,Y)|~memberP(Z,X2))))))))))))&(?[X3]: (ssItem(X3)&(?[X4]: (ssList(X4)&(?[X5]: (ssList(X5)&(app(app(X4,cons(X3,nil)),X5)=U&(?[X6]: (ssItem(X6)&((memberP(X4,X6)&~leq(X6,X3))|(memberP(X5,X6)&~leq(X3,X6)))))))))))))))))))))),
% 0.22/6.00 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.22/6.00 fof(f416,definition,(
% 0.22/6.00 ![X3,X4,X6]: (sP0_prd(X6,X4,X3)<=>(memberP(X4,X6)&~leq(X6,X3)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.22/6.00 fof(f417,plain,(
% 0.22/6.00 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=W)|(![X2]: (~ssItem(X2)|((leq(Y,X2)|~memberP(X1,X2))&(leq(X2,Y)|~memberP(Z,X2))))))))))))&(?[X3]: (ssItem(X3)&(?[X4]: (ssList(X4)&(?[X5]: (ssList(X5)&(app(app(X4,cons(X3,nil)),X5)=U&(?[X6]: (ssItem(X6)&(sP0_prd(X6,X4,X3)|(memberP(X5,X6)&~leq(X3,X6))))))))))))))))))))),
% 0.22/6.00 inference(formula_renaming,[status(thm)],[f415,f416])).
% 0.22/6.00 fof(f418,plain,(
% 0.22/6.00 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=sK49_skl)|(![X2]: (~ssItem(X2)|((leq(Y,X2)|~memberP(X1,X2))&(leq(X2,Y)|~memberP(Z,X2))))))))))))&(ssItem(sK51_skl)&(ssList(sK52_skl)&(ssList(sK53_skl)&(app(app(sK52_skl,cons(sK51_skl,nil)),sK53_skl)=sK47_skl&(ssItem(sK54_skl)&(sP0_prd(sK54_skl,sK52_skl,sK51_skl)|(memberP(sK53_skl,sK54_skl)&~leq(sK51_skl,sK54_skl)))))))))))))),
% 0.22/6.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(X3,sK51_skl),skolemize(X4,sK52_skl),skolemize(X5,sK53_skl),skolemize(X6,sK54_skl)],[f417])).
% 0.22/6.00 fof(f419,plain,(
% 0.22/6.00 ssList(sK47_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f420,plain,(
% 0.22/6.00 ssList(sK48_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f421,plain,(
% 0.22/6.00 ssList(sK49_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f424,plain,(
% 0.22/6.00 sK47_skl=sK49_skl),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f425,plain,(
% 0.22/6.00 ![X0,X1,X2,X3]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK49_skl|~ssItem(X3)|leq(X0,X3)|~memberP(X2,X3))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f426,plain,(
% 0.22/6.00 ![X0,X1,X2,X3]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK49_skl|~ssItem(X3)|leq(X3,X0)|~memberP(X1,X3))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f427,plain,(
% 0.22/6.00 ssItem(sK51_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f428,plain,(
% 0.22/6.00 ssList(sK52_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f429,plain,(
% 0.22/6.00 ssList(sK53_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f430,plain,(
% 0.22/6.00 app(app(sK52_skl,cons(sK51_skl,nil)),sK53_skl)=sK47_skl),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f431,plain,(
% 0.22/6.00 ssItem(sK54_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f432,plain,(
% 0.22/6.00 sP0_prd(sK54_skl,sK52_skl,sK51_skl)|memberP(sK53_skl,sK54_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f433,plain,(
% 0.22/6.00 sP0_prd(sK54_skl,sK52_skl,sK51_skl)|~leq(sK51_skl,sK54_skl)),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f418])).
% 0.22/6.00 fof(f434,plain,(
% 0.22/6.00 ![X3,X4,X6]: ((~sP0_prd(X6,X4,X3)|(memberP(X4,X6)&~leq(X6,X3)))&(sP0_prd(X6,X4,X3)|(~memberP(X4,X6)|leq(X6,X3))))),
% 0.22/6.00 inference(NNF_transformation,[status(thm)],[f416])).
% 0.22/6.00 fof(f435,plain,(
% 0.22/6.00 (![X3,X4,X6]: (~sP0_prd(X6,X4,X3)|(memberP(X4,X6)&~leq(X6,X3))))&(![X3,X4,X6]: (sP0_prd(X6,X4,X3)|(~memberP(X4,X6)|leq(X6,X3))))),
% 0.22/6.00 inference(miniscoping,[status(thm)],[f434])).
% 0.22/6.00 fof(f436,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|memberP(X1,X0))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f435])).
% 0.22/6.00 fof(f437,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~leq(X0,X2))),
% 0.22/6.00 inference(cnf_transformation,[status(thm)],[f435])).
% 0.22/6.00 fof(f439,definition,(
% 0.22/6.00 sQ0_spl <=> (sP0_prd(sK54_skl,sK52_skl,sK51_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f440,plain,(
% 0.22/6.00 sP0_prd(sK54_skl,sK52_skl,sK51_skl)|~sQ0_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f439])).
% 0.22/6.00 fof(f442,definition,(
% 0.22/6.00 sQ1_spl <=> (memberP(sK53_skl,sK54_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f443,plain,(
% 0.22/6.00 memberP(sK53_skl,sK54_skl)|~sQ1_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f442])).
% 0.22/6.00 fof(f445,plain,(
% 0.22/6.00 sQ0_spl|sQ1_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f432,f439,f442])).
% 0.22/6.00 fof(f446,definition,(
% 0.22/6.00 sQ2_spl <=> (leq(sK51_skl,sK54_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f449,plain,(
% 0.22/6.00 sQ0_spl|~sQ2_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f433,f439,f446])).
% 0.22/6.00 fof(f454,plain,(
% 0.22/6.00 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.22/6.00 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.22/6.00 fof(f456,plain,(
% 0.22/6.00 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 0.22/6.00 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 0.22/6.00 fof(f487,plain,(
% 0.22/6.00 app(nil,sK49_skl)=sK49_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f249,f421])).
% 0.22/6.00 fof(f488,plain,(
% 0.22/6.00 app(nil,sK48_skl)=sK48_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f249,f420])).
% 0.22/6.00 fof(f493,plain,(
% 0.22/6.00 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(X1,nil),X0)|~memberP(X1,X0))),
% 0.22/6.00 inference(resolution,[status(thm)],[f223,f271])).
% 0.22/6.00 fof(f494,plain,(
% 0.22/6.00 app(nil,nil)=nil),
% 0.22/6.00 inference(resolution,[status(thm)],[f223,f249])).
% 0.22/6.00 fof(f497,plain,(
% 0.22/6.00 leq(sK0_skl,sK0_skl)),
% 0.22/6.00 inference(resolution,[status(thm)],[f103,f255])).
% 0.22/6.00 fof(f498,plain,(
% 0.22/6.00 leq(sK1_skl,sK1_skl)),
% 0.22/6.00 inference(resolution,[status(thm)],[f104,f255])).
% 0.22/6.00 fof(f512,plain,(
% 0.22/6.00 app(sK49_skl,nil)=sK49_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f389,f421])).
% 0.22/6.00 fof(f513,plain,(
% 0.22/6.00 app(sK48_skl,nil)=sK48_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f389,f420])).
% 0.22/6.00 fof(f518,plain,(
% 0.22/6.00 leq(sK51_skl,sK51_skl)),
% 0.22/6.00 inference(resolution,[status(thm)],[f427,f255])).
% 0.22/6.00 fof(f519,plain,(
% 0.22/6.00 app(sK52_skl,nil)=sK52_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f428,f389])).
% 0.22/6.00 fof(f523,plain,(
% 0.22/6.00 app(nil,sK52_skl)=sK52_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f428,f249])).
% 0.22/6.00 fof(f526,plain,(
% 0.22/6.00 app(sK53_skl,nil)=sK53_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f429,f389])).
% 0.22/6.00 fof(f530,plain,(
% 0.22/6.00 app(nil,sK53_skl)=sK53_skl),
% 0.22/6.00 inference(resolution,[status(thm)],[f429,f249])).
% 0.22/6.00 fof(f540,definition,(
% 0.22/6.00 sQ5_spl <=> (ssList(sK53_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f542,plain,(
% 0.22/6.00 ~ssList(sK53_skl)|sQ5_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f540])).
% 0.22/6.00 fof(f544,plain,(
% 0.22/6.00 $false|sQ5_spl),
% 0.22/6.00 inference(forward_subsumption_resolution,[status(thm)],[f542,f429])).
% 0.22/6.00 fof(f545,plain,(
% 0.22/6.00 sQ5_spl),
% 0.22/6.00 inference(contradiction_clause,[status(thm)],[f544])).
% 0.22/6.00 fof(f552,plain,(
% 0.22/6.00 leq(sK54_skl,sK54_skl)),
% 0.22/6.00 inference(resolution,[status(thm)],[f431,f255])).
% 0.22/6.00 fof(f553,plain,(
% 0.22/6.00 ![X0,X1,X2,X3]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|~ssItem(X3)|leq(X0,X3)|~memberP(X2,X3))),
% 0.22/6.00 inference(forward_demodulation,[status(thm)],[f424,f425])).
% 0.22/6.00 fof(f554,plain,(
% 0.22/6.00 ![X0]: (~ssItem(sK51_skl)|~ssList(sK52_skl)|~ssList(sK53_skl)|~ssItem(X0)|leq(sK51_skl,X0)|~memberP(sK53_skl,X0))),
% 0.22/6.00 inference(resolution,[status(thm)],[f553,f430])).
% 0.22/6.00 fof(f556,definition,(
% 0.22/6.00 sQ6_spl <=> (ssItem(sK51_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f558,plain,(
% 0.22/6.00 ~ssItem(sK51_skl)|sQ6_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f556])).
% 0.22/6.00 fof(f559,definition,(
% 0.22/6.00 sQ7_spl <=> (ssList(sK52_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f561,plain,(
% 0.22/6.00 ~ssList(sK52_skl)|sQ7_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f559])).
% 0.22/6.00 fof(f562,definition,(
% 0.22/6.00 ![X0]: (sQ8_spl <=> (~ssItem(X0)|leq(sK51_skl,X0)|~memberP(sK53_skl,X0)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f563,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|leq(sK51_skl,X0)|~memberP(sK53_skl,X0)|~sQ8_spl)),
% 0.22/6.00 inference(component_clause,[status(thm)],[f562])).
% 0.22/6.00 fof(f565,plain,(
% 0.22/6.00 ~sQ6_spl|~sQ7_spl|~sQ5_spl|sQ8_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f554,f556,f559,f540,f562])).
% 0.22/6.00 fof(f571,plain,(
% 0.22/6.00 memberP(sK52_skl,sK54_skl)|~sQ0_spl),
% 0.22/6.00 inference(resolution,[status(thm)],[f440,f436])).
% 0.22/6.00 fof(f572,plain,(
% 0.22/6.00 app(nil,sK47_skl)=sK49_skl),
% 0.22/6.00 inference(forward_demodulation,[status(thm)],[f424,f487])).
% 0.22/6.00 fof(f573,plain,(
% 0.22/6.00 app(nil,sK47_skl)=sK47_skl),
% 0.22/6.00 inference(forward_demodulation,[status(thm)],[f424,f572])).
% 0.22/6.00 fof(f574,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK47_skl)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK47_skl,X0))),
% 0.22/6.00 inference(paramodulation,[status(thm)],[f573,f270])).
% 0.22/6.00 fof(f575,definition,(
% 0.22/6.00 ![X0]: (sQ10_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK47_skl,X0)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f578,definition,(
% 0.22/6.00 sQ11_spl <=> (ssList(nil))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f580,plain,(
% 0.22/6.00 ~ssList(nil)|sQ11_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f578])).
% 0.22/6.00 fof(f581,definition,(
% 0.22/6.00 sQ12_spl <=> (ssList(sK47_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f583,plain,(
% 0.22/6.00 ~ssList(sK47_skl)|sQ12_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f581])).
% 0.22/6.00 fof(f584,plain,(
% 0.22/6.00 sQ10_spl|~sQ11_spl|~sQ12_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f574,f575,f578,f581])).
% 0.22/6.00 fof(f585,plain,(
% 0.22/6.00 $false|sQ12_spl),
% 0.22/6.00 inference(forward_subsumption_resolution,[status(thm)],[f583,f419])).
% 0.22/6.00 fof(f586,plain,(
% 0.22/6.00 sQ12_spl),
% 0.22/6.00 inference(contradiction_clause,[status(thm)],[f585])).
% 0.22/6.00 fof(f587,plain,(
% 0.22/6.00 $false|sQ11_spl),
% 0.22/6.00 inference(forward_subsumption_resolution,[status(thm)],[f580,f223])).
% 0.22/6.00 fof(f588,plain,(
% 0.22/6.00 sQ11_spl),
% 0.22/6.00 inference(contradiction_clause,[status(thm)],[f587])).
% 0.22/6.00 fof(f589,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK48_skl)|~memberP(sK48_skl,X0)|memberP(nil,X0)|memberP(sK48_skl,X0))),
% 0.22/6.00 inference(paramodulation,[status(thm)],[f488,f270])).
% 0.22/6.00 fof(f590,definition,(
% 0.22/6.00 ![X0]: (sQ13_spl <=> (~ssItem(X0)|~memberP(sK48_skl,X0)|memberP(nil,X0)|memberP(sK48_skl,X0)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f593,definition,(
% 0.22/6.00 sQ14_spl <=> (ssList(sK48_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f595,plain,(
% 0.22/6.00 ~ssList(sK48_skl)|sQ14_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f593])).
% 0.22/6.00 fof(f596,plain,(
% 0.22/6.00 sQ13_spl|~sQ11_spl|~sQ14_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f589,f590,f578,f593])).
% 0.22/6.00 fof(f597,plain,(
% 0.22/6.00 $false|sQ14_spl),
% 0.22/6.00 inference(forward_subsumption_resolution,[status(thm)],[f595,f420])).
% 0.22/6.00 fof(f598,plain,(
% 0.22/6.00 sQ14_spl),
% 0.22/6.00 inference(contradiction_clause,[status(thm)],[f597])).
% 0.22/6.00 fof(f599,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.22/6.00 inference(paramodulation,[status(thm)],[f494,f270])).
% 0.22/6.00 fof(f600,definition,(
% 0.22/6.00 ![X0]: (sQ15_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f603,plain,(
% 0.22/6.00 sQ15_spl|~sQ11_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f599,f600,f578])).
% 0.22/6.00 fof(f608,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|~ssItem(sK0_skl)|~ssItem(sK0_skl)|~leq(X0,sK0_skl)|leq(X0,sK0_skl))),
% 0.22/6.00 inference(resolution,[status(thm)],[f497,f253])).
% 0.22/6.00 fof(f609,definition,(
% 0.22/6.00 ![X0]: (sQ16_spl <=> (~ssItem(X0)|~leq(X0,sK0_skl)|leq(X0,sK0_skl)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f612,definition,(
% 0.22/6.00 sQ17_spl <=> (ssItem(sK0_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f614,plain,(
% 0.22/6.00 ~ssItem(sK0_skl)|sQ17_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f612])).
% 0.22/6.00 fof(f615,plain,(
% 0.22/6.00 sQ16_spl|~sQ17_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f608,f609,f612])).
% 0.22/6.00 fof(f616,plain,(
% 0.22/6.00 $false|sQ17_spl),
% 0.22/6.00 inference(forward_subsumption_resolution,[status(thm)],[f614,f103])).
% 0.22/6.00 fof(f617,plain,(
% 0.22/6.00 sQ17_spl),
% 0.22/6.00 inference(contradiction_clause,[status(thm)],[f616])).
% 0.22/6.00 fof(f618,plain,(
% 0.22/6.00 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X1=X1)),
% 0.22/6.00 inference(equality_resolution,[status(thm)],[f227])).
% 0.22/6.00 fof(f619,definition,(
% 0.22/6.00 ![X0]: (sQ18_spl <=> (~ssList(X0)|~ssList(X0)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f620,plain,(
% 0.22/6.00 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ18_spl)),
% 0.22/6.00 inference(component_clause,[status(thm)],[f619])).
% 0.22/6.00 fof(f622,definition,(
% 0.22/6.00 ![X1]: (sQ19_spl <=> (~ssItem(X1)|~ssItem(X1)|X1=X1))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f625,plain,(
% 0.22/6.00 sQ18_spl|sQ19_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f618,f619,f622])).
% 0.22/6.00 fof(f626,plain,(
% 0.22/6.00 ![X0]: (~ssList(X0)|~sQ18_spl)),
% 0.22/6.00 inference(duplicate_literals_removal,[status(thm)],[f620])).
% 0.22/6.00 fof(f636,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|~ssItem(sK1_skl)|~ssItem(sK1_skl)|~leq(X0,sK1_skl)|leq(X0,sK1_skl))),
% 0.22/6.00 inference(resolution,[status(thm)],[f498,f253])).
% 0.22/6.00 fof(f637,definition,(
% 0.22/6.00 ![X0]: (sQ22_spl <=> (~ssItem(X0)|~leq(X0,sK1_skl)|leq(X0,sK1_skl)))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f640,definition,(
% 0.22/6.00 sQ23_spl <=> (ssItem(sK1_skl))),
% 0.22/6.00 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.22/6.00 fof(f642,plain,(
% 0.22/6.00 ~ssItem(sK1_skl)|sQ23_spl),
% 0.22/6.00 inference(component_clause,[status(thm)],[f640])).
% 0.22/6.00 fof(f643,plain,(
% 0.22/6.00 sQ22_spl|~sQ23_spl),
% 0.22/6.00 inference(split_clause,[status(thm)],[f636,f637,f640])).
% 0.22/6.00 fof(f644,plain,(
% 0.22/6.00 $false|sQ23_spl),
% 0.22/6.00 inference(forward_subsumption_resolution,[status(thm)],[f642,f104])).
% 0.22/6.00 fof(f645,plain,(
% 0.22/6.00 sQ23_spl),
% 0.22/6.00 inference(contradiction_clause,[status(thm)],[f644])).
% 0.22/6.00 fof(f670,plain,(
% 0.22/6.00 app(sK47_skl,nil)=sK49_skl),
% 0.22/6.00 inference(forward_demodulation,[status(thm)],[f424,f512])).
% 0.22/6.00 fof(f671,plain,(
% 0.22/6.00 app(sK47_skl,nil)=sK47_skl),
% 0.22/6.00 inference(forward_demodulation,[status(thm)],[f424,f670])).
% 0.22/6.00 fof(f681,plain,(
% 0.22/6.00 ![X0]: (~ssItem(X0)|~ssItem(sK51_skl)|~ssItem(sK51_skl)|~leq(X0,sK51_skl)|leq(X0,sK51_skl))),
% 0.22/6.00 inference(resolution,[status(thm)],[f518,f253])).
% 0.22/6.00 fof(f682,definition,(
% 0.22/6.00 ![X0]: (sQ24_spl <=> (~ssItem(X0)|~leq(X0,sK51_skl)|leq(X0,sK51_skl)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f685,plain,(
% 0.22/6.02 sQ24_spl|~sQ6_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f681,f682,f556])).
% 0.22/6.02 fof(f686,plain,(
% 0.22/6.02 $false|sQ6_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f558,f427])).
% 0.22/6.02 fof(f687,plain,(
% 0.22/6.02 sQ6_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f686])).
% 0.22/6.02 fof(f688,plain,(
% 0.22/6.02 $false|sQ7_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f561,f428])).
% 0.22/6.02 fof(f689,plain,(
% 0.22/6.02 sQ7_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f688])).
% 0.22/6.02 fof(f690,plain,(
% 0.22/6.02 ![X0]: (~ssItem(X0)|~ssList(sK52_skl)|~ssList(nil)|~memberP(sK52_skl,X0)|memberP(sK52_skl,X0)|memberP(nil,X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f519,f270])).
% 0.22/6.02 fof(f691,definition,(
% 0.22/6.02 ![X0]: (sQ25_spl <=> (~ssItem(X0)|~memberP(sK52_skl,X0)|memberP(sK52_skl,X0)|memberP(nil,X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f694,plain,(
% 0.22/6.02 sQ25_spl|~sQ7_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f690,f691,f559,f578])).
% 0.22/6.02 fof(f701,plain,(
% 0.22/6.02 ![X0,X1,X2,X3]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|~ssItem(X3)|leq(X3,X0)|~memberP(X1,X3))),
% 0.22/6.02 inference(forward_demodulation,[status(thm)],[f424,f426])).
% 0.22/6.02 fof(f702,plain,(
% 0.22/6.02 ![X0]: (~ssItem(sK51_skl)|~ssList(sK52_skl)|~ssList(sK53_skl)|~ssItem(X0)|leq(X0,sK51_skl)|~memberP(sK52_skl,X0))),
% 0.22/6.02 inference(resolution,[status(thm)],[f701,f430])).
% 0.22/6.02 fof(f704,definition,(
% 0.22/6.02 ![X0]: (sQ26_spl <=> (~ssItem(X0)|leq(X0,sK51_skl)|~memberP(sK52_skl,X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f705,plain,(
% 0.22/6.02 ![X0]: (~ssItem(X0)|leq(X0,sK51_skl)|~memberP(sK52_skl,X0)|~sQ26_spl)),
% 0.22/6.02 inference(component_clause,[status(thm)],[f704])).
% 0.22/6.02 fof(f707,plain,(
% 0.22/6.02 ~sQ6_spl|~sQ7_spl|~sQ5_spl|sQ26_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f702,f556,f559,f540,f704])).
% 0.22/6.02 fof(f709,plain,(
% 0.22/6.02 ![X0]: (~ssItem(X0)|~ssList(sK53_skl)|~ssList(nil)|~memberP(sK53_skl,X0)|memberP(sK53_skl,X0)|memberP(nil,X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f526,f270])).
% 0.22/6.02 fof(f710,definition,(
% 0.22/6.02 ![X0]: (sQ27_spl <=> (~ssItem(X0)|~memberP(sK53_skl,X0)|memberP(sK53_skl,X0)|memberP(nil,X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f713,plain,(
% 0.22/6.02 sQ27_spl|~sQ5_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f709,f710,f540,f578])).
% 0.22/6.02 fof(f725,plain,(
% 0.22/6.02 ![X0]: (~ssItem(X0)|~ssItem(sK54_skl)|~ssItem(sK54_skl)|~leq(X0,sK54_skl)|leq(X0,sK54_skl))),
% 0.22/6.02 inference(resolution,[status(thm)],[f552,f253])).
% 0.22/6.02 fof(f726,definition,(
% 0.22/6.02 ![X0]: (sQ28_spl <=> (~ssItem(X0)|~leq(X0,sK54_skl)|leq(X0,sK54_skl)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f729,definition,(
% 0.22/6.02 sQ29_spl <=> (ssItem(sK54_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f731,plain,(
% 0.22/6.02 ~ssItem(sK54_skl)|sQ29_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f729])).
% 0.22/6.02 fof(f732,plain,(
% 0.22/6.02 sQ28_spl|~sQ29_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f725,f726,f729])).
% 0.22/6.02 fof(f736,plain,(
% 0.22/6.02 ~ssItem(sK54_skl)|~ssList(sK52_skl)|memberP(app(sK52_skl,nil),sK54_skl)|~sQ0_spl),
% 0.22/6.02 inference(resolution,[status(thm)],[f571,f493])).
% 0.22/6.02 fof(f750,definition,(
% 0.22/6.02 sQ33_spl <=> (memberP(app(sK52_skl,nil),sK54_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f751,plain,(
% 0.22/6.02 memberP(app(sK52_skl,nil),sK54_skl)|~sQ33_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f750])).
% 0.22/6.02 fof(f753,plain,(
% 0.22/6.02 ~sQ29_spl|~sQ7_spl|sQ33_spl|~sQ0_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f736,f729,f559,f750,f439])).
% 0.22/6.02 fof(f754,plain,(
% 0.22/6.02 $false|sQ29_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f731,f431])).
% 0.22/6.02 fof(f755,plain,(
% 0.22/6.02 sQ29_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f754])).
% 0.22/6.02 fof(f757,plain,(
% 0.22/6.02 $false|~sQ18_spl),
% 0.22/6.02 inference(backward_subsumption_resolution,[status(thm)],[f429,f626])).
% 0.22/6.02 fof(f762,plain,(
% 0.22/6.02 ~sQ18_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f757])).
% 0.22/6.02 fof(f777,plain,(
% 0.22/6.02 ~ssItem(sK54_skl)|~ssItem(sK54_skl)|~leq(sK54_skl,sK54_skl)|sK54_skl=sK54_skl),
% 0.22/6.02 inference(resolution,[status(thm)],[f251,f552])).
% 0.22/6.02 fof(f778,plain,(
% 0.22/6.02 ~ssItem(sK51_skl)|~ssItem(sK51_skl)|~leq(sK51_skl,sK51_skl)|sK51_skl=sK51_skl),
% 0.22/6.02 inference(resolution,[status(thm)],[f251,f518])).
% 0.22/6.02 fof(f779,plain,(
% 0.22/6.02 ~ssItem(sK1_skl)|~ssItem(sK1_skl)|~leq(sK1_skl,sK1_skl)|sK1_skl=sK1_skl),
% 0.22/6.02 inference(resolution,[status(thm)],[f251,f498])).
% 0.22/6.02 fof(f780,plain,(
% 0.22/6.02 ~ssItem(sK0_skl)|~ssItem(sK0_skl)|~leq(sK0_skl,sK0_skl)|sK0_skl=sK0_skl),
% 0.22/6.02 inference(resolution,[status(thm)],[f251,f497])).
% 0.22/6.02 fof(f781,definition,(
% 0.22/6.02 sQ34_spl <=> (leq(sK54_skl,sK54_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f783,plain,(
% 0.22/6.02 ~leq(sK54_skl,sK54_skl)|sQ34_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f781])).
% 0.22/6.02 fof(f784,definition,(
% 0.22/6.02 sQ35_spl <=> (sK54_skl=sK54_skl)),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f787,plain,(
% 0.22/6.02 ~sQ29_spl|~sQ34_spl|sQ35_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f777,f729,f781,f784])).
% 0.22/6.02 fof(f788,definition,(
% 0.22/6.02 sQ36_spl <=> (leq(sK51_skl,sK51_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f790,plain,(
% 0.22/6.02 ~leq(sK51_skl,sK51_skl)|sQ36_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f788])).
% 0.22/6.02 fof(f791,definition,(
% 0.22/6.02 sQ37_spl <=> (sK51_skl=sK51_skl)),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f794,plain,(
% 0.22/6.02 ~sQ6_spl|~sQ36_spl|sQ37_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f778,f556,f788,f791])).
% 0.22/6.02 fof(f795,definition,(
% 0.22/6.02 sQ38_spl <=> (leq(sK1_skl,sK1_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f797,plain,(
% 0.22/6.02 ~leq(sK1_skl,sK1_skl)|sQ38_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f795])).
% 0.22/6.02 fof(f798,definition,(
% 0.22/6.02 sQ39_spl <=> (sK1_skl=sK1_skl)),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f801,plain,(
% 0.22/6.02 ~sQ23_spl|~sQ38_spl|sQ39_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f779,f640,f795,f798])).
% 0.22/6.02 fof(f802,definition,(
% 0.22/6.02 sQ40_spl <=> (leq(sK0_skl,sK0_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f804,plain,(
% 0.22/6.02 ~leq(sK0_skl,sK0_skl)|sQ40_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f802])).
% 0.22/6.02 fof(f805,definition,(
% 0.22/6.02 sQ41_spl <=> (sK0_skl=sK0_skl)),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f808,plain,(
% 0.22/6.02 ~sQ17_spl|~sQ40_spl|sQ41_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f780,f612,f802,f805])).
% 0.22/6.02 fof(f809,plain,(
% 0.22/6.02 $false|sQ40_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f804,f497])).
% 0.22/6.02 fof(f810,plain,(
% 0.22/6.02 sQ40_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f809])).
% 0.22/6.02 fof(f811,plain,(
% 0.22/6.02 $false|sQ38_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f797,f498])).
% 0.22/6.02 fof(f812,plain,(
% 0.22/6.02 sQ38_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f811])).
% 0.22/6.02 fof(f813,plain,(
% 0.22/6.02 $false|sQ36_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f790,f518])).
% 0.22/6.02 fof(f814,plain,(
% 0.22/6.02 sQ36_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f813])).
% 0.22/6.02 fof(f815,plain,(
% 0.22/6.02 $false|sQ34_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f783,f552])).
% 0.22/6.02 fof(f816,plain,(
% 0.22/6.02 sQ34_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f815])).
% 0.22/6.02 fof(f894,plain,(
% 0.22/6.02 ~ssItem(sK54_skl)|leq(sK51_skl,sK54_skl)|~sQ8_spl|~sQ1_spl),
% 0.22/6.02 inference(resolution,[status(thm)],[f563,f443])).
% 0.22/6.02 fof(f895,plain,(
% 0.22/6.02 ~sQ29_spl|sQ2_spl|~sQ8_spl|~sQ1_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f894,f729,f446,f562,f442])).
% 0.22/6.02 fof(f896,plain,(
% 0.22/6.02 memberP(sK52_skl,sK54_skl)|~sQ33_spl),
% 0.22/6.02 inference(forward_demodulation,[status(thm)],[f519,f751])).
% 0.22/6.02 fof(f917,plain,(
% 0.22/6.02 ~ssList(sK53_skl)|~ssList(sK53_skl)|frontsegP(app(sK53_skl,nil),sK53_skl)|~ssList(nil)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f526,f454])).
% 0.22/6.02 fof(f918,plain,(
% 0.22/6.02 ~ssList(sK52_skl)|~ssList(sK52_skl)|frontsegP(app(sK52_skl,nil),sK52_skl)|~ssList(nil)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f519,f454])).
% 0.22/6.02 fof(f919,plain,(
% 0.22/6.02 ~ssList(sK48_skl)|~ssList(sK48_skl)|frontsegP(app(sK48_skl,nil),sK48_skl)|~ssList(nil)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f513,f454])).
% 0.22/6.02 fof(f920,plain,(
% 0.22/6.02 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f671,f454])).
% 0.22/6.02 fof(f921,plain,(
% 0.22/6.02 ~ssList(sK53_skl)|~ssList(nil)|frontsegP(app(nil,sK53_skl),nil)|~ssList(sK53_skl)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f530,f454])).
% 0.22/6.02 fof(f922,plain,(
% 0.22/6.02 ~ssList(sK52_skl)|~ssList(nil)|frontsegP(app(nil,sK52_skl),nil)|~ssList(sK52_skl)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f523,f454])).
% 0.22/6.02 fof(f923,plain,(
% 0.22/6.02 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f494,f454])).
% 0.22/6.02 fof(f924,plain,(
% 0.22/6.02 ~ssList(sK48_skl)|~ssList(nil)|frontsegP(app(nil,sK48_skl),nil)|~ssList(sK48_skl)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f488,f454])).
% 0.22/6.02 fof(f925,plain,(
% 0.22/6.02 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f573,f454])).
% 0.22/6.02 fof(f1067,definition,(
% 0.22/6.02 sQ97_spl <=> (frontsegP(app(sK53_skl,nil),sK53_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1070,plain,(
% 0.22/6.02 ~sQ5_spl|sQ97_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f917,f540,f1067,f578])).
% 0.22/6.02 fof(f1071,definition,(
% 0.22/6.02 sQ98_spl <=> (frontsegP(app(sK52_skl,nil),sK52_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1074,plain,(
% 0.22/6.02 ~sQ7_spl|sQ98_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f918,f559,f1071,f578])).
% 0.22/6.02 fof(f1075,definition,(
% 0.22/6.02 sQ99_spl <=> (frontsegP(app(sK48_skl,nil),sK48_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1078,plain,(
% 0.22/6.02 ~sQ14_spl|sQ99_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f919,f593,f1075,f578])).
% 0.22/6.02 fof(f1079,definition,(
% 0.22/6.02 sQ100_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1082,plain,(
% 0.22/6.02 ~sQ12_spl|sQ100_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f920,f581,f1079,f578])).
% 0.22/6.02 fof(f1083,definition,(
% 0.22/6.02 sQ101_spl <=> (frontsegP(app(nil,sK53_skl),nil))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1086,plain,(
% 0.22/6.02 ~sQ5_spl|~sQ11_spl|sQ101_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f921,f540,f578,f1083])).
% 0.22/6.02 fof(f1087,definition,(
% 0.22/6.02 sQ102_spl <=> (frontsegP(app(nil,sK52_skl),nil))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1090,plain,(
% 0.22/6.02 ~sQ7_spl|~sQ11_spl|sQ102_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f922,f559,f578,f1087])).
% 0.22/6.02 fof(f1091,definition,(
% 0.22/6.02 sQ103_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1094,plain,(
% 0.22/6.02 ~sQ11_spl|sQ103_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f923,f578,f1091])).
% 0.22/6.02 fof(f1095,definition,(
% 0.22/6.02 sQ104_spl <=> (frontsegP(app(nil,sK48_skl),nil))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1098,plain,(
% 0.22/6.02 ~sQ14_spl|~sQ11_spl|sQ104_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f924,f593,f578,f1095])).
% 0.22/6.02 fof(f1099,definition,(
% 0.22/6.02 sQ105_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1102,plain,(
% 0.22/6.02 ~sQ12_spl|~sQ11_spl|sQ105_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f925,f581,f578,f1099])).
% 0.22/6.02 fof(f1396,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK53_skl)|~sK53_skl=app(X0,nil)|sK53_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f526,f376])).
% 0.22/6.02 fof(f1397,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK52_skl)|~sK52_skl=app(X0,nil)|sK52_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f519,f376])).
% 0.22/6.02 fof(f1398,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK48_skl)|~sK48_skl=app(X0,nil)|sK48_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f513,f376])).
% 0.22/6.02 fof(f1399,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK47_skl)|~sK47_skl=app(X0,nil)|sK47_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f671,f376])).
% 0.22/6.02 fof(f1400,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK53_skl)|~ssList(nil)|~sK53_skl=app(X0,sK53_skl)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f530,f376])).
% 0.22/6.02 fof(f1401,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK52_skl)|~ssList(nil)|~sK52_skl=app(X0,sK52_skl)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f523,f376])).
% 0.22/6.02 fof(f1402,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~nil=app(X0,nil)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f494,f376])).
% 0.22/6.02 fof(f1403,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~sK48_skl=app(X0,sK48_skl)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f488,f376])).
% 0.22/6.02 fof(f1404,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~sK47_skl=app(X0,sK47_skl)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f573,f376])).
% 0.22/6.02 fof(f1517,definition,(
% 0.22/6.02 ![X0]: (sQ171_spl <=> (~ssList(X0)|~sK53_skl=app(X0,nil)|sK53_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1520,plain,(
% 0.22/6.02 sQ171_spl|~sQ11_spl|~sQ5_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1396,f1517,f578,f540])).
% 0.22/6.02 fof(f1521,definition,(
% 0.22/6.02 ![X0]: (sQ172_spl <=> (~ssList(X0)|~sK52_skl=app(X0,nil)|sK52_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1524,plain,(
% 0.22/6.02 sQ172_spl|~sQ11_spl|~sQ7_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1397,f1521,f578,f559])).
% 0.22/6.02 fof(f1525,definition,(
% 0.22/6.02 ![X0]: (sQ173_spl <=> (~ssList(X0)|~sK48_skl=app(X0,nil)|sK48_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1528,plain,(
% 0.22/6.02 sQ173_spl|~sQ11_spl|~sQ14_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1398,f1525,f578,f593])).
% 0.22/6.02 fof(f1529,definition,(
% 0.22/6.02 ![X0]: (sQ174_spl <=> (~ssList(X0)|~sK47_skl=app(X0,nil)|sK47_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1532,plain,(
% 0.22/6.02 sQ174_spl|~sQ11_spl|~sQ12_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1399,f1529,f578,f581])).
% 0.22/6.02 fof(f1533,definition,(
% 0.22/6.02 ![X0]: (sQ175_spl <=> (~ssList(X0)|~sK53_skl=app(X0,sK53_skl)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1536,plain,(
% 0.22/6.02 sQ175_spl|~sQ5_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1400,f1533,f540,f578])).
% 0.22/6.02 fof(f1537,definition,(
% 0.22/6.02 ![X0]: (sQ176_spl <=> (~ssList(X0)|~sK52_skl=app(X0,sK52_skl)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1540,plain,(
% 0.22/6.02 sQ176_spl|~sQ7_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1401,f1537,f559,f578])).
% 0.22/6.02 fof(f1541,definition,(
% 0.22/6.02 ![X0]: (sQ177_spl <=> (~ssList(X0)|~nil=app(X0,nil)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1544,plain,(
% 0.22/6.02 sQ177_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1402,f1541,f578])).
% 0.22/6.02 fof(f1545,definition,(
% 0.22/6.02 ![X0]: (sQ178_spl <=> (~ssList(X0)|~sK48_skl=app(X0,sK48_skl)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1548,plain,(
% 0.22/6.02 sQ178_spl|~sQ14_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1403,f1545,f593,f578])).
% 0.22/6.02 fof(f1549,definition,(
% 0.22/6.02 ![X0]: (sQ179_spl <=> (~ssList(X0)|~sK47_skl=app(X0,sK47_skl)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1552,plain,(
% 0.22/6.02 sQ179_spl|~sQ12_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1404,f1549,f581,f578])).
% 0.22/6.02 fof(f1739,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK53_skl)|~ssList(nil)|~sK53_skl=app(sK53_skl,X0)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f526,f378])).
% 0.22/6.02 fof(f1740,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK52_skl)|~ssList(nil)|~sK52_skl=app(sK52_skl,X0)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f519,f378])).
% 0.22/6.02 fof(f1741,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~sK48_skl=app(sK48_skl,X0)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f513,f378])).
% 0.22/6.02 fof(f1742,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~sK47_skl=app(sK47_skl,X0)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f671,f378])).
% 0.22/6.02 fof(f1743,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK53_skl)|~sK53_skl=app(nil,X0)|sK53_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f530,f378])).
% 0.22/6.02 fof(f1744,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK52_skl)|~sK52_skl=app(nil,X0)|sK52_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f523,f378])).
% 0.22/6.02 fof(f1745,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~nil=app(nil,X0)|nil=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f494,f378])).
% 0.22/6.02 fof(f1746,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK48_skl)|~sK48_skl=app(nil,X0)|sK48_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f488,f378])).
% 0.22/6.02 fof(f1747,plain,(
% 0.22/6.02 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK47_skl)|~sK47_skl=app(nil,X0)|sK47_skl=X0)),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f573,f378])).
% 0.22/6.02 fof(f1860,definition,(
% 0.22/6.02 ![X0]: (sQ214_spl <=> (~ssList(X0)|~sK53_skl=app(sK53_skl,X0)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1863,plain,(
% 0.22/6.02 sQ214_spl|~sQ5_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1739,f1860,f540,f578])).
% 0.22/6.02 fof(f1864,definition,(
% 0.22/6.02 ![X0]: (sQ215_spl <=> (~ssList(X0)|~sK52_skl=app(sK52_skl,X0)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1867,plain,(
% 0.22/6.02 sQ215_spl|~sQ7_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1740,f1864,f559,f578])).
% 0.22/6.02 fof(f1868,definition,(
% 0.22/6.02 ![X0]: (sQ216_spl <=> (~ssList(X0)|~sK48_skl=app(sK48_skl,X0)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1871,plain,(
% 0.22/6.02 sQ216_spl|~sQ14_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1741,f1868,f593,f578])).
% 0.22/6.02 fof(f1872,definition,(
% 0.22/6.02 ![X0]: (sQ217_spl <=> (~ssList(X0)|~sK47_skl=app(sK47_skl,X0)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1875,plain,(
% 0.22/6.02 sQ217_spl|~sQ12_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1742,f1872,f581,f578])).
% 0.22/6.02 fof(f1876,definition,(
% 0.22/6.02 ![X0]: (sQ218_spl <=> (~ssList(X0)|~sK53_skl=app(nil,X0)|sK53_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1879,plain,(
% 0.22/6.02 sQ218_spl|~sQ11_spl|~sQ5_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1743,f1876,f578,f540])).
% 0.22/6.02 fof(f1880,definition,(
% 0.22/6.02 ![X0]: (sQ219_spl <=> (~ssList(X0)|~sK52_skl=app(nil,X0)|sK52_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1883,plain,(
% 0.22/6.02 sQ219_spl|~sQ11_spl|~sQ7_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1744,f1880,f578,f559])).
% 0.22/6.02 fof(f1884,definition,(
% 0.22/6.02 ![X0]: (sQ220_spl <=> (~ssList(X0)|~nil=app(nil,X0)|nil=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1887,plain,(
% 0.22/6.02 sQ220_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1745,f1884,f578])).
% 0.22/6.02 fof(f1888,definition,(
% 0.22/6.02 ![X0]: (sQ221_spl <=> (~ssList(X0)|~sK48_skl=app(nil,X0)|sK48_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1891,plain,(
% 0.22/6.02 sQ221_spl|~sQ11_spl|~sQ14_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1746,f1888,f578,f593])).
% 0.22/6.02 fof(f1892,definition,(
% 0.22/6.02 ![X0]: (sQ222_spl <=> (~ssList(X0)|~sK47_skl=app(nil,X0)|sK47_skl=X0))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f1895,plain,(
% 0.22/6.02 sQ222_spl|~sQ11_spl|~sQ12_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1747,f1892,f578,f581])).
% 0.22/6.02 fof(f1998,plain,(
% 0.22/6.02 ~ssItem(sK54_skl)|leq(sK54_skl,sK51_skl)|~sQ33_spl|~sQ26_spl),
% 0.22/6.02 inference(resolution,[status(thm)],[f896,f705])).
% 0.22/6.02 fof(f2001,definition,(
% 0.22/6.02 sQ234_spl <=> (leq(sK54_skl,sK51_skl))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2002,plain,(
% 0.22/6.02 leq(sK54_skl,sK51_skl)|~sQ234_spl),
% 0.22/6.02 inference(component_clause,[status(thm)],[f2001])).
% 0.22/6.02 fof(f2004,plain,(
% 0.22/6.02 ~sQ29_spl|sQ234_spl|~sQ33_spl|~sQ26_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f1998,f729,f2001,f750,f704])).
% 0.22/6.02 fof(f2084,plain,(
% 0.22/6.02 ~ssList(nil)|~ssList(nil)|nil=nil),
% 0.22/6.02 inference(resolution,[status(thm)],[f385,f494])).
% 0.22/6.02 fof(f2116,definition,(
% 0.22/6.02 sQ249_spl <=> (nil=nil)),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2119,plain,(
% 0.22/6.02 ~sQ11_spl|sQ249_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2084,f578,f2116])).
% 0.22/6.02 fof(f2362,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK53_skl,X0))|~ssList(nil)|segmentP(app(app(sK53_skl,nil),X0),nil)|~ssList(sK53_skl)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f526,f456])).
% 0.22/6.02 fof(f2363,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK52_skl,X0))|~ssList(nil)|segmentP(app(app(sK52_skl,nil),X0),nil)|~ssList(sK52_skl)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f519,f456])).
% 0.22/6.02 fof(f2364,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f513,f456])).
% 0.22/6.02 fof(f2365,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f671,f456])).
% 0.22/6.02 fof(f2366,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK53_skl,X0))|~ssList(sK53_skl)|segmentP(app(app(nil,sK53_skl),X0),sK53_skl)|~ssList(nil)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f530,f456])).
% 0.22/6.02 fof(f2367,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK52_skl,X0))|~ssList(sK52_skl)|segmentP(app(app(nil,sK52_skl),X0),sK52_skl)|~ssList(nil)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f523,f456])).
% 0.22/6.02 fof(f2368,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f494,f456])).
% 0.22/6.02 fof(f2369,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f488,f456])).
% 0.22/6.02 fof(f2370,plain,(
% 0.22/6.02 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 0.22/6.02 inference(paramodulation,[status(thm)],[f573,f456])).
% 0.22/6.02 fof(f2460,definition,(
% 0.22/6.02 ![X0]: (sQ301_spl <=> (~ssList(app(sK53_skl,X0))|segmentP(app(app(sK53_skl,nil),X0),nil)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2463,plain,(
% 0.22/6.02 sQ301_spl|~sQ11_spl|~sQ5_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2362,f2460,f578,f540])).
% 0.22/6.02 fof(f2464,definition,(
% 0.22/6.02 ![X0]: (sQ302_spl <=> (~ssList(app(sK52_skl,X0))|segmentP(app(app(sK52_skl,nil),X0),nil)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2467,plain,(
% 0.22/6.02 sQ302_spl|~sQ11_spl|~sQ7_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2363,f2464,f578,f559])).
% 0.22/6.02 fof(f2468,definition,(
% 0.22/6.02 ![X0]: (sQ303_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2471,plain,(
% 0.22/6.02 sQ303_spl|~sQ11_spl|~sQ14_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2364,f2468,f578,f593])).
% 0.22/6.02 fof(f2472,definition,(
% 0.22/6.02 ![X0]: (sQ304_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2475,plain,(
% 0.22/6.02 sQ304_spl|~sQ11_spl|~sQ12_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2365,f2472,f578,f581])).
% 0.22/6.02 fof(f2476,definition,(
% 0.22/6.02 ![X0]: (sQ305_spl <=> (~ssList(app(sK53_skl,X0))|segmentP(app(app(nil,sK53_skl),X0),sK53_skl)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2479,plain,(
% 0.22/6.02 sQ305_spl|~sQ5_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2366,f2476,f540,f578])).
% 0.22/6.02 fof(f2480,definition,(
% 0.22/6.02 ![X0]: (sQ306_spl <=> (~ssList(app(sK52_skl,X0))|segmentP(app(app(nil,sK52_skl),X0),sK52_skl)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2483,plain,(
% 0.22/6.02 sQ306_spl|~sQ7_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2367,f2480,f559,f578])).
% 0.22/6.02 fof(f2484,definition,(
% 0.22/6.02 ![X0]: (sQ307_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2487,plain,(
% 0.22/6.02 sQ307_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2368,f2484,f578])).
% 0.22/6.02 fof(f2488,definition,(
% 0.22/6.02 ![X0]: (sQ308_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2491,plain,(
% 0.22/6.02 sQ308_spl|~sQ14_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2369,f2488,f593,f578])).
% 0.22/6.02 fof(f2492,definition,(
% 0.22/6.02 ![X0]: (sQ309_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 0.22/6.02 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 0.22/6.02 fof(f2495,plain,(
% 0.22/6.02 sQ309_spl|~sQ12_spl|~sQ11_spl),
% 0.22/6.02 inference(split_clause,[status(thm)],[f2370,f2492,f581,f578])).
% 0.22/6.02 fof(f4680,plain,(
% 0.22/6.02 ~leq(sK54_skl,sK51_skl)|~sQ0_spl),
% 0.22/6.02 inference(resolution,[status(thm)],[f440,f437])).
% 0.22/6.02 fof(f4682,plain,(
% 0.22/6.02 $false|~sQ234_spl|~sQ0_spl),
% 0.22/6.02 inference(forward_subsumption_resolution,[status(thm)],[f4680,f2002])).
% 0.22/6.02 fof(f4683,plain,(
% 0.22/6.02 ~sQ234_spl|~sQ0_spl),
% 0.22/6.02 inference(contradiction_clause,[status(thm)],[f4682])).
% 0.22/6.02 fof(f4684,plain,(
% 0.22/6.02 $false),
% 0.22/6.02 inference(sat_refutation,[status(thm)],[f445,f449,f545,f565,f584,f586,f588,f596,f598,f603,f615,f617,f625,f643,f645,f685,f687,f689,f694,f707,f713,f732,f753,f755,f762,f787,f794,f801,f808,f810,f812,f814,f816,f895,f1070,f1074,f1078,f1082,f1086,f1090,f1094,f1098,f1102,f1520,f1524,f1528,f1532,f1536,f1540,f1544,f1548,f1552,f1863,f1867,f1871,f1875,f1879,f1883,f1887,f1891,f1895,f2004,f2119,f2463,f2467,f2471,f2475,f2479,f2483,f2487,f2491,f2495,f4683])).
% 0.22/6.02 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/6.03 % Elapsed time: 0.574707 seconds
% 0.22/6.03 % CPU time: 4.314483 seconds
% 0.22/6.03 % Total memory used: 150.784 MB
% 0.22/6.03 % Net memory used: 147.976 MB
%------------------------------------------------------------------------------