%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC386+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 : n015.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:20 PM UTC 2026
% Result : Theorem 0.13s 5.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC386+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.09/5.36 % Computer : n015.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 08:23:28 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.13/5.42 % Refutation found
% 0.13/5.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.42 fof(f2,axiom,(
% 0.13/5.42 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f5,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f6,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f7,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f8,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> ( cyclefreeP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ~ ( leq(V,W)& leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f15,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f17,axiom,(
% 0.13/5.42 ssList(nil) ),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f19,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssItem(X)=> ( cons(W,U) = cons(X,V)=> ( W = X& V = U ) ) ) )) )) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f28,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f36,axiom,(
% 0.13/5.42 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f38,axiom,(
% 0.13/5.42 (! [U] :( ssItem(U)=> ~ memberP(nil,U) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f42,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> frontsegP(U,U) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f45,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f49,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> rearsegP(U,U) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f51,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f55,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> segmentP(U,U) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f57,axiom,(
% 0.13/5.42 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f96,conjecture,(
% 0.13/5.42 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| ( (! [Y] :( ssItem(Y)=> ( cons(Y,nil) != W| ~ memberP(X,Y) ) ))& ( nil != X| nil != W ) )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| (? [Z] :( ssItem(Z)& cons(Z,nil) = U& memberP(V,Z) ) )) ) ) ) )) )) )) )),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f97,negated_conjecture,(
% 0.13/5.42 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| ( (! [Y] :( ssItem(Y)=> ( cons(Y,nil) != W| ~ memberP(X,Y) ) ))& ( nil != X| nil != W ) )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| (? [Z] :( ssItem(Z)& cons(Z,nil) = U& memberP(V,Z) ) )) ) ) ) )) )) )) ))),
% 0.13/5.42 inference(negated_conjecture,[status(cth)],[f96])).
% 0.13/5.42 fof(f102,plain,(
% 0.13/5.42 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.13/5.42 fof(f105,plain,(
% 0.13/5.42 ~sK0_skl=sK1_skl),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f102])).
% 0.13/5.42 fof(f119,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/5.42 fof(f120,plain,(
% 0.13/5.42 ![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.13/5.42 inference(NNF_transformation,[status(thm)],[f119])).
% 0.13/5.42 fof(f121,plain,(
% 0.13/5.42 ![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.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.13/5.42 fof(f122,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.13/5.42 fof(f123,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.13/5.42 fof(f124,plain,(
% 0.13/5.42 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.13/5.42 fof(f125,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.13/5.42 fof(f126,plain,(
% 0.13/5.42 ![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.13/5.42 inference(NNF_transformation,[status(thm)],[f125])).
% 0.13/5.42 fof(f127,plain,(
% 0.13/5.42 ![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.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.13/5.42 fof(f128,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/5.42 fof(f129,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/5.42 fof(f130,plain,(
% 0.13/5.42 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/5.42 fof(f131,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/5.42 fof(f132,plain,(
% 0.13/5.42 ![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.13/5.42 inference(NNF_transformation,[status(thm)],[f131])).
% 0.13/5.42 fof(f133,plain,(
% 0.13/5.42 ![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.13/5.42 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.13/5.42 fof(f134,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f133])).
% 0.13/5.42 fof(f135,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f133])).
% 0.13/5.42 fof(f136,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f133])).
% 0.13/5.42 fof(f138,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(cyclefreeP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V)))))))))))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.13/5.42 fof(f139,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(leq(V,W)&leq(W,V))))))))))))))))),
% 0.13/5.42 inference(NNF_transformation,[status(thm)],[f138])).
% 0.13/5.42 fof(f140,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(ssItem(sK9_skl(U))&(ssItem(sK10_skl(U))&(ssList(sK11_skl(U))&(ssList(sK12_skl(U))&(ssList(sK13_skl(U))&(app(app(sK11_skl(U),cons(sK9_skl(U),sK12_skl(U))),cons(sK10_skl(U),sK13_skl(U)))=U&(leq(sK9_skl(U),sK10_skl(U))&leq(sK10_skl(U),sK9_skl(U))))))))))))),
% 0.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(V,sK9_skl(U)),skolemize(W,sK10_skl(U)),skolemize(X,sK11_skl(U)),skolemize(Y,sK12_skl(U)),skolemize(Z,sK13_skl(U))],[f139])).
% 0.13/5.42 fof(f142,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|cyclefreeP(X0)|ssItem(sK9_skl(X0)))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f140])).
% 0.13/5.42 fof(f217,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.13/5.42 fof(f218,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 0.13/5.42 inference(NNF_transformation,[status(thm)],[f217])).
% 0.13/5.42 fof(f219,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f218])).
% 0.13/5.42 fof(f223,plain,(
% 0.13/5.42 ssList(nil)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/5.42 fof(f226,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssItem(W)|(![X]: (~ssItem(X)|(~cons(W,U)=cons(X,V)|(W=X&V=U)))))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.13/5.42 fof(f227,plain,(
% 0.13/5.42 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X2=X3)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f226])).
% 0.13/5.42 fof(f248,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.13/5.42 fof(f249,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f248])).
% 0.13/5.42 fof(f268,plain,(
% 0.13/5.42 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.13/5.42 fof(f269,plain,(
% 0.13/5.42 ![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.13/5.42 inference(NNF_transformation,[status(thm)],[f268])).
% 0.13/5.42 fof(f270,plain,(
% 0.13/5.42 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~memberP(app(X1,X2),X0)|memberP(X1,X0)|memberP(X2,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f269])).
% 0.13/5.42 fof(f278,plain,(
% 0.13/5.42 ![U]: (~ssItem(U)|~memberP(nil,U))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.13/5.42 fof(f279,plain,(
% 0.13/5.42 ![X0]: (~ssItem(X0)|~memberP(nil,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f278])).
% 0.13/5.42 fof(f285,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|frontsegP(U,U))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.13/5.42 fof(f286,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f285])).
% 0.13/5.42 fof(f294,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.13/5.42 fof(f295,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f294])).
% 0.13/5.42 fof(f304,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|rearsegP(U,U))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.13/5.42 fof(f305,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f304])).
% 0.13/5.42 fof(f308,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.13/5.42 fof(f309,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f308])).
% 0.13/5.42 fof(f318,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|segmentP(U,U))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.13/5.42 fof(f319,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f318])).
% 0.13/5.42 fof(f322,plain,(
% 0.13/5.42 ![U]: (~ssList(U)|segmentP(U,nil))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.13/5.42 fof(f323,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f322])).
% 0.13/5.42 fof(f415,plain,(
% 0.13/5.42 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&((?[Y]: (ssItem(Y)&(cons(Y,nil)=W&memberP(X,Y))))|(nil=X&nil=W)))&((nil=V&~nil=U)|(neq(V,nil)&(![Z]: ((~ssItem(Z)|~cons(Z,nil)=U)|~memberP(V,Z))))))))))))))),
% 0.13/5.42 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.13/5.42 fof(f416,definition,(
% 0.13/5.42 ![W,X,Y]: (sP0_prd(Y,X,W)<=>(ssItem(Y)&(cons(Y,nil)=W&memberP(X,Y))))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/5.42 fof(f417,definition,(
% 0.13/5.42 ![U,V]: (sP1_prd(V,U)<=>(nil=V&~nil=U))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/5.42 fof(f418,plain,(
% 0.13/5.42 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&((?[Y]: sP0_prd(Y,X,W))|(nil=X&nil=W)))&(sP1_prd(V,U)|(neq(V,nil)&(![Z]: ((~ssItem(Z)|~cons(Z,nil)=U)|~memberP(V,Z)))))))))))))),
% 0.13/5.42 inference(formula_renaming,[status(thm)],[f415,f417,f416])).
% 0.13/5.42 fof(f419,plain,(
% 0.13/5.42 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(sP0_prd(sK51_skl,sK50_skl,sK49_skl)|(nil=sK50_skl&nil=sK49_skl)))&(sP1_prd(sK48_skl,sK47_skl)|(neq(sK48_skl,nil)&(![Z]: ((~ssItem(Z)|~cons(Z,nil)=sK47_skl)|~memberP(sK48_skl,Z))))))))))),
% 0.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl)],[f418])).
% 0.13/5.42 fof(f422,plain,(
% 0.13/5.42 ssList(sK49_skl)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f423,plain,(
% 0.13/5.42 ssList(sK50_skl)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f424,plain,(
% 0.13/5.42 sK48_skl=sK50_skl),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f425,plain,(
% 0.13/5.42 sK47_skl=sK49_skl),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f426,plain,(
% 0.13/5.42 sP0_prd(sK51_skl,sK50_skl,sK49_skl)|nil=sK50_skl),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f427,plain,(
% 0.13/5.42 sP0_prd(sK51_skl,sK50_skl,sK49_skl)|nil=sK49_skl),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f428,plain,(
% 0.13/5.42 sP1_prd(sK48_skl,sK47_skl)|neq(sK48_skl,nil)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f429,plain,(
% 0.13/5.42 ![X0]: (sP1_prd(sK48_skl,sK47_skl)|~ssItem(X0)|~cons(X0,nil)=sK47_skl|~memberP(sK48_skl,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f419])).
% 0.13/5.42 fof(f430,plain,(
% 0.13/5.42 ![W,X,Y]: ((~sP0_prd(Y,X,W)|(ssItem(Y)&(cons(Y,nil)=W&memberP(X,Y))))&(sP0_prd(Y,X,W)|(~ssItem(Y)|(~cons(Y,nil)=W|~memberP(X,Y)))))),
% 0.13/5.42 inference(NNF_transformation,[status(thm)],[f416])).
% 0.13/5.42 fof(f431,plain,(
% 0.13/5.42 (![W,X,Y]: (~sP0_prd(Y,X,W)|(ssItem(Y)&(cons(Y,nil)=W&memberP(X,Y)))))&(![W,X,Y]: (sP0_prd(Y,X,W)|(~ssItem(Y)|(~cons(Y,nil)=W|~memberP(X,Y)))))),
% 0.13/5.42 inference(miniscoping,[status(thm)],[f430])).
% 0.13/5.42 fof(f432,plain,(
% 0.13/5.42 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssItem(X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.13/5.42 fof(f433,plain,(
% 0.13/5.42 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|cons(X0,nil)=X2)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.13/5.42 fof(f434,plain,(
% 0.13/5.42 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|memberP(X1,X0))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.13/5.42 fof(f436,plain,(
% 0.13/5.42 ![U,V]: ((~sP1_prd(V,U)|(nil=V&~nil=U))&(sP1_prd(V,U)|(~nil=V|nil=U)))),
% 0.13/5.42 inference(NNF_transformation,[status(thm)],[f417])).
% 0.13/5.42 fof(f437,plain,(
% 0.13/5.42 (![U,V]: (~sP1_prd(V,U)|(nil=V&~nil=U)))&(![U,V]: (sP1_prd(V,U)|(~nil=V|nil=U)))),
% 0.13/5.42 inference(miniscoping,[status(thm)],[f436])).
% 0.13/5.42 fof(f438,plain,(
% 0.13/5.42 ![X0,X1]: (~sP1_prd(X0,X1)|nil=X0)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f437])).
% 0.13/5.42 fof(f439,plain,(
% 0.13/5.42 ![X0,X1]: (~sP1_prd(X0,X1)|~nil=X1)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f437])).
% 0.13/5.42 fof(f440,plain,(
% 0.13/5.42 ![X0,X1]: (sP1_prd(X0,X1)|~nil=X0|nil=X1)),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f437])).
% 0.13/5.42 fof(f441,definition,(
% 0.13/5.42 sQ0_spl <=> (sP0_prd(sK51_skl,sK50_skl,sK49_skl))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f442,plain,(
% 0.13/5.42 sP0_prd(sK51_skl,sK50_skl,sK49_skl)|~sQ0_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f441])).
% 0.13/5.42 fof(f444,definition,(
% 0.13/5.42 sQ1_spl <=> (nil=sK50_skl)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f445,plain,(
% 0.13/5.42 nil=sK50_skl|~sQ1_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f444])).
% 0.13/5.42 fof(f447,plain,(
% 0.13/5.42 sQ0_spl|sQ1_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f426,f441,f444])).
% 0.13/5.42 fof(f448,definition,(
% 0.13/5.42 sQ2_spl <=> (nil=sK49_skl)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f449,plain,(
% 0.13/5.42 nil=sK49_skl|~sQ2_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f448])).
% 0.13/5.42 fof(f451,plain,(
% 0.13/5.42 sQ0_spl|sQ2_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f427,f441,f448])).
% 0.13/5.42 fof(f452,definition,(
% 0.13/5.42 sQ3_spl <=> (sP1_prd(sK48_skl,sK47_skl))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f453,plain,(
% 0.13/5.42 sP1_prd(sK48_skl,sK47_skl)|~sQ3_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f452])).
% 0.13/5.42 fof(f455,definition,(
% 0.13/5.42 sQ4_spl <=> (neq(sK48_skl,nil))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f456,plain,(
% 0.13/5.42 neq(sK48_skl,nil)|~sQ4_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f455])).
% 0.13/5.42 fof(f458,plain,(
% 0.13/5.42 sQ3_spl|sQ4_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f428,f452,f455])).
% 0.13/5.42 fof(f459,definition,(
% 0.13/5.42 ![X0]: (sQ5_spl <=> (~ssItem(X0)|~cons(X0,nil)=sK47_skl|~memberP(sK48_skl,X0)))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f460,plain,(
% 0.13/5.42 ![X0]: (~ssItem(X0)|~cons(X0,nil)=sK47_skl|~memberP(sK48_skl,X0)|~sQ5_spl)),
% 0.13/5.42 inference(component_clause,[status(thm)],[f459])).
% 0.13/5.42 fof(f462,plain,(
% 0.13/5.42 sQ3_spl|sQ5_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f429,f452,f459])).
% 0.13/5.42 fof(f467,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.13/5.42 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.13/5.42 fof(f468,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 0.13/5.42 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.13/5.42 fof(f478,plain,(
% 0.13/5.42 ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 0.13/5.42 inference(destructive_equality_resolution,[status(thm)],[f219])).
% 0.13/5.42 fof(f479,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 0.13/5.42 inference(duplicate_literals_removal,[status(thm)],[f478])).
% 0.13/5.42 fof(f494,plain,(
% 0.13/5.42 ![X0]: (~sP1_prd(X0,nil))),
% 0.13/5.42 inference(destructive_equality_resolution,[status(thm)],[f439])).
% 0.13/5.42 fof(f495,plain,(
% 0.13/5.42 ![X0]: (sP1_prd(nil,X0)|nil=X0)),
% 0.13/5.42 inference(destructive_equality_resolution,[status(thm)],[f440])).
% 0.13/5.42 fof(f498,plain,(
% 0.13/5.42 sP1_prd(sK50_skl,sK47_skl)|~sQ3_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f424,f453])).
% 0.13/5.42 fof(f499,plain,(
% 0.13/5.42 sP1_prd(sK50_skl,sK49_skl)|~sQ3_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f425,f498])).
% 0.13/5.42 fof(f500,plain,(
% 0.13/5.42 nil=sK50_skl|~sQ3_spl),
% 0.13/5.42 inference(resolution,[status(thm)],[f438,f499])).
% 0.13/5.42 fof(f501,plain,(
% 0.13/5.42 ![X0,X1]: (~sP1_prd(X0,X1)|sK50_skl=X0|~sQ3_spl)),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f500,f438])).
% 0.13/5.42 fof(f505,plain,(
% 0.13/5.42 ![X0]: (~ssItem(X0)|~memberP(sK50_skl,X0)|~sQ3_spl)),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f500,f279])).
% 0.13/5.42 fof(f518,plain,(
% 0.13/5.42 frontsegP(sK50_skl,sK50_skl)),
% 0.13/5.42 inference(resolution,[status(thm)],[f286,f423])).
% 0.13/5.42 fof(f519,plain,(
% 0.13/5.42 frontsegP(sK49_skl,sK49_skl)),
% 0.13/5.42 inference(resolution,[status(thm)],[f286,f422])).
% 0.13/5.42 fof(f520,plain,(
% 0.13/5.42 ![X0]: (sP1_prd(sK50_skl,X0)|nil=X0|~sQ3_spl)),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f500,f495])).
% 0.13/5.42 fof(f521,plain,(
% 0.13/5.42 ![X0]: (sP1_prd(sK50_skl,X0)|sK50_skl=X0|~sQ3_spl)),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f500,f520])).
% 0.13/5.42 fof(f523,plain,(
% 0.13/5.42 ![X0]: (sK50_skl=X0|sK50_skl=sK50_skl|~sQ3_spl)),
% 0.13/5.42 inference(resolution,[status(thm)],[f521,f501])).
% 0.13/5.42 fof(f524,definition,(
% 0.13/5.42 ![X0]: (sQ6_spl <=> (sK50_skl=X0))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f525,plain,(
% 0.13/5.42 ![X0]: (sK50_skl=X0|~sQ6_spl)),
% 0.13/5.42 inference(component_clause,[status(thm)],[f524])).
% 0.13/5.42 fof(f527,definition,(
% 0.13/5.42 sQ7_spl <=> (sK50_skl=sK50_skl)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f530,plain,(
% 0.13/5.42 sQ6_spl|sQ7_spl|~sQ3_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f523,f524,f527,f452])).
% 0.13/5.42 fof(f531,plain,(
% 0.13/5.42 ![X0,X1]: (X0=X1|~sQ6_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f525,f525])).
% 0.13/5.42 fof(f546,plain,(
% 0.13/5.42 $false|~sQ6_spl),
% 0.13/5.42 inference(backward_subsumption_resolution,[status(thm)],[f105,f531])).
% 0.13/5.42 fof(f547,plain,(
% 0.13/5.42 ~sQ6_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f546])).
% 0.13/5.42 fof(f549,plain,(
% 0.13/5.42 ssItem(sK51_skl)|~sQ0_spl),
% 0.13/5.42 inference(resolution,[status(thm)],[f442,f432])).
% 0.13/5.42 fof(f554,plain,(
% 0.13/5.42 memberP(sK50_skl,sK51_skl)|~sQ0_spl),
% 0.13/5.42 inference(resolution,[status(thm)],[f434,f442])).
% 0.13/5.42 fof(f559,plain,(
% 0.13/5.42 ~ssItem(sK51_skl)|~sQ0_spl|~sQ3_spl),
% 0.13/5.42 inference(resolution,[status(thm)],[f554,f505])).
% 0.13/5.42 fof(f562,plain,(
% 0.13/5.42 $false|~sQ0_spl|~sQ3_spl),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f559,f549])).
% 0.13/5.42 fof(f563,plain,(
% 0.13/5.42 ~sQ0_spl|~sQ3_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f562])).
% 0.13/5.42 fof(f564,plain,(
% 0.13/5.42 neq(sK50_skl,nil)|~sQ4_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f424,f456])).
% 0.13/5.42 fof(f565,plain,(
% 0.13/5.42 ![X0]: (~ssItem(X0)|~cons(X0,nil)=sK49_skl|~memberP(sK48_skl,X0)|~sQ5_spl)),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f425,f460])).
% 0.13/5.42 fof(f566,plain,(
% 0.13/5.42 ![X0]: (~ssItem(X0)|~cons(X0,nil)=sK49_skl|~memberP(sK50_skl,X0)|~sQ5_spl)),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f424,f565])).
% 0.13/5.42 fof(f570,plain,(
% 0.13/5.42 sK50_skl=sK49_skl|~sQ1_spl|~sQ2_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f445,f449])).
% 0.13/5.42 fof(f581,plain,(
% 0.13/5.42 ![X0]: (~sP1_prd(X0,sK50_skl)|~sQ1_spl)),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f445,f494])).
% 0.13/5.42 fof(f590,definition,(
% 0.13/5.42 sQ10_spl <=> (ssList(sK50_skl))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f592,plain,(
% 0.13/5.42 ~ssList(sK50_skl)|sQ10_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f590])).
% 0.13/5.42 fof(f593,definition,(
% 0.13/5.42 sQ11_spl <=> (ssItem(sK51_skl))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f595,plain,(
% 0.13/5.42 ~ssItem(sK51_skl)|sQ11_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f593])).
% 0.13/5.42 fof(f627,plain,(
% 0.13/5.42 $false|~sQ0_spl|sQ11_spl),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f595,f549])).
% 0.13/5.42 fof(f628,plain,(
% 0.13/5.42 ~sQ0_spl|sQ11_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f627])).
% 0.13/5.42 fof(f633,plain,(
% 0.13/5.42 frontsegP(nil,nil)),
% 0.13/5.42 inference(resolution,[status(thm)],[f223,f286])).
% 0.13/5.42 fof(f645,plain,(
% 0.13/5.42 $false|sQ10_spl),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f592,f423])).
% 0.13/5.42 fof(f646,plain,(
% 0.13/5.42 sQ10_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f645])).
% 0.13/5.42 fof(f649,plain,(
% 0.13/5.42 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X1=X1)),
% 0.13/5.42 inference(equality_resolution,[status(thm)],[f227])).
% 0.13/5.42 fof(f650,definition,(
% 0.13/5.42 ![X0]: (sQ21_spl <=> (~ssList(X0)|~ssList(X0)))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f651,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ21_spl)),
% 0.13/5.42 inference(component_clause,[status(thm)],[f650])).
% 0.13/5.42 fof(f653,definition,(
% 0.13/5.42 ![X1]: (sQ22_spl <=> (~ssItem(X1)|~ssItem(X1)|X1=X1))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f656,plain,(
% 0.13/5.42 sQ21_spl|sQ22_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f649,f650,f653])).
% 0.13/5.42 fof(f657,plain,(
% 0.13/5.42 ![X0]: (~ssList(X0)|~sQ21_spl)),
% 0.13/5.42 inference(duplicate_literals_removal,[status(thm)],[f651])).
% 0.13/5.42 fof(f658,plain,(
% 0.13/5.42 $false|~sQ21_spl),
% 0.13/5.42 inference(backward_subsumption_resolution,[status(thm)],[f223,f657])).
% 0.13/5.42 fof(f661,plain,(
% 0.13/5.42 ~sQ21_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f658])).
% 0.13/5.42 fof(f667,plain,(
% 0.13/5.42 ~ssList(nil)|~ssList(nil)|ssList(sK5_skl(nil,nil))),
% 0.13/5.42 inference(resolution,[status(thm)],[f122,f633])).
% 0.13/5.42 fof(f668,plain,(
% 0.13/5.42 ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK5_skl(sK49_skl,sK49_skl))),
% 0.13/5.42 inference(resolution,[status(thm)],[f122,f519])).
% 0.13/5.42 fof(f669,plain,(
% 0.13/5.42 ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK5_skl(sK50_skl,sK50_skl))),
% 0.13/5.42 inference(resolution,[status(thm)],[f122,f518])).
% 0.13/5.42 fof(f670,definition,(
% 0.13/5.42 sQ24_spl <=> (ssList(nil))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f672,plain,(
% 0.13/5.42 ~ssList(nil)|sQ24_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f670])).
% 0.13/5.42 fof(f673,definition,(
% 0.13/5.42 sQ25_spl <=> (ssList(sK5_skl(nil,nil)))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f676,plain,(
% 0.13/5.42 ~sQ24_spl|sQ25_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f667,f670,f673])).
% 0.13/5.42 fof(f677,definition,(
% 0.13/5.42 sQ26_spl <=> (ssList(sK49_skl))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f679,plain,(
% 0.13/5.42 ~ssList(sK49_skl)|sQ26_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f677])).
% 0.13/5.42 fof(f680,definition,(
% 0.13/5.42 sQ27_spl <=> (ssList(sK5_skl(sK49_skl,sK49_skl)))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f683,plain,(
% 0.13/5.42 ~sQ26_spl|sQ27_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f668,f677,f680])).
% 0.13/5.42 fof(f684,definition,(
% 0.13/5.42 sQ28_spl <=> (ssList(sK5_skl(sK50_skl,sK50_skl)))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f685,plain,(
% 0.13/5.42 ssList(sK5_skl(sK50_skl,sK50_skl))|~sQ28_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f684])).
% 0.13/5.42 fof(f687,plain,(
% 0.13/5.42 ~sQ10_spl|sQ28_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f669,f590,f684])).
% 0.13/5.42 fof(f688,plain,(
% 0.13/5.42 $false|sQ26_spl),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f679,f422])).
% 0.13/5.42 fof(f689,plain,(
% 0.13/5.42 sQ26_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f688])).
% 0.13/5.42 fof(f690,plain,(
% 0.13/5.42 $false|sQ24_spl),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f672,f223])).
% 0.13/5.42 fof(f691,plain,(
% 0.13/5.42 sQ24_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f690])).
% 0.13/5.42 fof(f692,plain,(
% 0.13/5.42 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil),
% 0.13/5.42 inference(resolution,[status(thm)],[f123,f633])).
% 0.13/5.42 fof(f693,plain,(
% 0.13/5.42 ~ssList(sK49_skl)|~ssList(sK49_skl)|app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl),
% 0.13/5.42 inference(resolution,[status(thm)],[f123,f519])).
% 0.13/5.42 fof(f694,plain,(
% 0.13/5.42 ~ssList(sK50_skl)|~ssList(sK50_skl)|app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))=sK50_skl),
% 0.13/5.42 inference(resolution,[status(thm)],[f123,f518])).
% 0.13/5.42 fof(f695,definition,(
% 0.13/5.42 sQ29_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f698,plain,(
% 0.13/5.42 ~sQ24_spl|sQ29_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f692,f670,f695])).
% 0.13/5.42 fof(f699,definition,(
% 0.13/5.42 sQ30_spl <=> (app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f702,plain,(
% 0.13/5.42 ~sQ26_spl|sQ30_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f693,f677,f699])).
% 0.13/5.42 fof(f703,definition,(
% 0.13/5.42 sQ31_spl <=> (app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))=sK50_skl)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f706,plain,(
% 0.13/5.42 ~sQ10_spl|sQ31_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f694,f590,f703])).
% 0.13/5.43 fof(f708,plain,(
% 0.13/5.43 ![X0]: (nil=X0|nil=nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f495,f438])).
% 0.13/5.43 fof(f709,definition,(
% 0.13/5.43 ![X0]: (sQ32_spl <=> (nil=X0))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f710,plain,(
% 0.13/5.43 ![X0]: (nil=X0|~sQ32_spl)),
% 0.13/5.43 inference(component_clause,[status(thm)],[f709])).
% 0.13/5.43 fof(f712,definition,(
% 0.13/5.43 sQ33_spl <=> (nil=nil)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f715,plain,(
% 0.13/5.43 sQ32_spl|sQ33_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f708,f709,f712])).
% 0.13/5.43 fof(f716,plain,(
% 0.13/5.43 ![X0,X1]: (X0=X1|~sQ32_spl)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f710,f710])).
% 0.13/5.43 fof(f730,plain,(
% 0.13/5.43 $false|~sQ32_spl),
% 0.13/5.43 inference(backward_subsumption_resolution,[status(thm)],[f105,f716])).
% 0.13/5.43 fof(f731,plain,(
% 0.13/5.43 ~sQ32_spl),
% 0.13/5.43 inference(contradiction_clause,[status(thm)],[f730])).
% 0.13/5.43 fof(f745,plain,(
% 0.13/5.43 rearsegP(sK50_skl,sK50_skl)),
% 0.13/5.43 inference(resolution,[status(thm)],[f305,f423])).
% 0.13/5.43 fof(f746,plain,(
% 0.13/5.43 rearsegP(sK49_skl,sK49_skl)),
% 0.13/5.43 inference(resolution,[status(thm)],[f305,f422])).
% 0.13/5.43 fof(f747,plain,(
% 0.13/5.43 rearsegP(nil,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f305,f223])).
% 0.13/5.43 fof(f751,plain,(
% 0.13/5.43 segmentP(sK50_skl,sK50_skl)),
% 0.13/5.43 inference(resolution,[status(thm)],[f319,f423])).
% 0.13/5.43 fof(f752,plain,(
% 0.13/5.43 segmentP(sK49_skl,sK49_skl)),
% 0.13/5.43 inference(resolution,[status(thm)],[f319,f422])).
% 0.13/5.43 fof(f753,plain,(
% 0.13/5.43 segmentP(nil,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f319,f223])).
% 0.13/5.43 fof(f757,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|ssList(sK6_skl(nil,nil))),
% 0.13/5.43 inference(resolution,[status(thm)],[f128,f747])).
% 0.13/5.43 fof(f758,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK6_skl(sK49_skl,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f128,f746])).
% 0.13/5.43 fof(f759,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK6_skl(sK50_skl,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f128,f745])).
% 0.13/5.43 fof(f760,definition,(
% 0.13/5.43 sQ36_spl <=> (ssList(sK6_skl(nil,nil)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f763,plain,(
% 0.13/5.43 ~sQ24_spl|sQ36_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f757,f670,f760])).
% 0.13/5.43 fof(f764,definition,(
% 0.13/5.43 sQ37_spl <=> (ssList(sK6_skl(sK49_skl,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f767,plain,(
% 0.13/5.43 ~sQ26_spl|sQ37_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f758,f677,f764])).
% 0.13/5.43 fof(f768,definition,(
% 0.13/5.43 sQ38_spl <=> (ssList(sK6_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f769,plain,(
% 0.13/5.43 ssList(sK6_skl(sK50_skl,sK50_skl))|~sQ38_spl),
% 0.13/5.43 inference(component_clause,[status(thm)],[f768])).
% 0.13/5.43 fof(f771,plain,(
% 0.13/5.43 ~sQ10_spl|sQ38_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f759,f590,f768])).
% 0.13/5.43 fof(f772,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil),
% 0.13/5.43 inference(resolution,[status(thm)],[f129,f747])).
% 0.13/5.43 fof(f773,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(sK49_skl)|app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)=sK49_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f129,f746])).
% 0.13/5.43 fof(f774,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(sK50_skl)|app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)=sK50_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f129,f745])).
% 0.13/5.43 fof(f775,definition,(
% 0.13/5.43 sQ39_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f778,plain,(
% 0.13/5.43 ~sQ24_spl|sQ39_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f772,f670,f775])).
% 0.13/5.43 fof(f779,definition,(
% 0.13/5.43 sQ40_spl <=> (app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)=sK49_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f782,plain,(
% 0.13/5.43 ~sQ26_spl|sQ40_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f773,f677,f779])).
% 0.13/5.43 fof(f783,definition,(
% 0.13/5.43 sQ41_spl <=> (app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)=sK50_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f786,plain,(
% 0.13/5.43 ~sQ10_spl|sQ41_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f774,f590,f783])).
% 0.13/5.43 fof(f866,plain,(
% 0.13/5.43 frontsegP(sK50_skl,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f295,f423])).
% 0.13/5.43 fof(f867,plain,(
% 0.13/5.43 frontsegP(sK49_skl,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f295,f422])).
% 0.13/5.43 fof(f869,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|ssList(sK5_skl(nil,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f866,f122])).
% 0.13/5.43 fof(f870,definition,(
% 0.13/5.43 sQ42_spl <=> (ssList(sK5_skl(nil,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f873,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ42_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f869,f590,f670,f870])).
% 0.13/5.43 fof(f874,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|ssList(sK5_skl(nil,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f867,f122])).
% 0.13/5.43 fof(f875,definition,(
% 0.13/5.43 sQ43_spl <=> (ssList(sK5_skl(nil,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f878,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ43_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f874,f677,f670,f875])).
% 0.13/5.43 fof(f893,plain,(
% 0.13/5.43 rearsegP(sK50_skl,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f309,f423])).
% 0.13/5.43 fof(f894,plain,(
% 0.13/5.43 rearsegP(sK49_skl,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f309,f422])).
% 0.13/5.43 fof(f896,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|app(sK6_skl(nil,sK50_skl),nil)=sK50_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f893,f129])).
% 0.13/5.43 fof(f897,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f893,f128])).
% 0.13/5.43 fof(f898,definition,(
% 0.13/5.43 sQ44_spl <=> (app(sK6_skl(nil,sK50_skl),nil)=sK50_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f901,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ44_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f896,f590,f670,f898])).
% 0.13/5.43 fof(f902,definition,(
% 0.13/5.43 sQ45_spl <=> (ssList(sK6_skl(nil,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f905,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ45_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f897,f590,f670,f902])).
% 0.13/5.43 fof(f906,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|app(sK6_skl(nil,sK49_skl),nil)=sK49_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f894,f129])).
% 0.13/5.43 fof(f907,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f894,f128])).
% 0.13/5.43 fof(f908,definition,(
% 0.13/5.43 sQ46_spl <=> (app(sK6_skl(nil,sK49_skl),nil)=sK49_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f911,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ46_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f906,f677,f670,f908])).
% 0.13/5.43 fof(f912,definition,(
% 0.13/5.43 sQ47_spl <=> (ssList(sK6_skl(nil,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f915,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ47_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f907,f677,f670,f912])).
% 0.13/5.43 fof(f930,plain,(
% 0.13/5.43 segmentP(sK50_skl,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f323,f423])).
% 0.13/5.43 fof(f931,plain,(
% 0.13/5.43 segmentP(sK49_skl,nil)),
% 0.13/5.43 inference(resolution,[status(thm)],[f323,f422])).
% 0.13/5.43 fof(f979,plain,(
% 0.13/5.43 app(nil,sK50_skl)=sK50_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f249,f423])).
% 0.13/5.43 fof(f980,plain,(
% 0.13/5.43 app(nil,sK49_skl)=sK49_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f249,f422])).
% 0.13/5.43 fof(f981,plain,(
% 0.13/5.43 app(nil,nil)=nil),
% 0.13/5.43 inference(resolution,[status(thm)],[f249,f223])).
% 0.13/5.43 fof(f982,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|ssList(sK7_skl(nil,nil))),
% 0.13/5.43 inference(resolution,[status(thm)],[f134,f753])).
% 0.13/5.43 fof(f983,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|ssList(sK7_skl(nil,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f134,f931])).
% 0.13/5.43 fof(f984,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK7_skl(sK49_skl,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f134,f752])).
% 0.13/5.43 fof(f985,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|ssList(sK7_skl(nil,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f134,f930])).
% 0.13/5.43 fof(f986,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK7_skl(sK50_skl,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f134,f751])).
% 0.13/5.43 fof(f987,definition,(
% 0.13/5.43 sQ48_spl <=> (ssList(sK7_skl(nil,nil)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f990,plain,(
% 0.13/5.43 ~sQ24_spl|sQ48_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f982,f670,f987])).
% 0.13/5.43 fof(f991,definition,(
% 0.13/5.43 sQ49_spl <=> (ssList(sK7_skl(nil,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f994,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ49_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f983,f677,f670,f991])).
% 0.13/5.43 fof(f995,definition,(
% 0.13/5.43 sQ50_spl <=> (ssList(sK7_skl(sK49_skl,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f998,plain,(
% 0.13/5.43 ~sQ26_spl|sQ50_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f984,f677,f995])).
% 0.13/5.43 fof(f999,definition,(
% 0.13/5.43 sQ51_spl <=> (ssList(sK7_skl(nil,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1002,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ51_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f985,f590,f670,f999])).
% 0.13/5.43 fof(f1003,definition,(
% 0.13/5.43 sQ52_spl <=> (ssList(sK7_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1004,plain,(
% 0.13/5.43 ssList(sK7_skl(sK50_skl,sK50_skl))|~sQ52_spl),
% 0.13/5.43 inference(component_clause,[status(thm)],[f1003])).
% 0.13/5.43 fof(f1006,plain,(
% 0.13/5.43 ~sQ10_spl|sQ52_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f986,f590,f1003])).
% 0.13/5.43 fof(f1007,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|ssList(sK8_skl(nil,nil))),
% 0.13/5.43 inference(resolution,[status(thm)],[f135,f753])).
% 0.13/5.43 fof(f1008,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|ssList(sK8_skl(nil,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f135,f931])).
% 0.13/5.43 fof(f1009,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK8_skl(sK49_skl,sK49_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f135,f752])).
% 0.13/5.43 fof(f1010,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|ssList(sK8_skl(nil,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f135,f930])).
% 0.13/5.43 fof(f1011,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK8_skl(sK50_skl,sK50_skl))),
% 0.13/5.43 inference(resolution,[status(thm)],[f135,f751])).
% 0.13/5.43 fof(f1012,definition,(
% 0.13/5.43 sQ53_spl <=> (ssList(sK8_skl(nil,nil)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1015,plain,(
% 0.13/5.43 ~sQ24_spl|sQ53_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1007,f670,f1012])).
% 0.13/5.43 fof(f1016,definition,(
% 0.13/5.43 sQ54_spl <=> (ssList(sK8_skl(nil,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1019,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ54_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1008,f677,f670,f1016])).
% 0.13/5.43 fof(f1020,definition,(
% 0.13/5.43 sQ55_spl <=> (ssList(sK8_skl(sK49_skl,sK49_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1023,plain,(
% 0.13/5.43 ~sQ26_spl|sQ55_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1009,f677,f1020])).
% 0.13/5.43 fof(f1024,definition,(
% 0.13/5.43 sQ56_spl <=> (ssList(sK8_skl(nil,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1027,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ56_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1010,f590,f670,f1024])).
% 0.13/5.43 fof(f1028,definition,(
% 0.13/5.43 sQ57_spl <=> (ssList(sK8_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1029,plain,(
% 0.13/5.43 ssList(sK8_skl(sK50_skl,sK50_skl))|~sQ57_spl),
% 0.13/5.43 inference(component_clause,[status(thm)],[f1028])).
% 0.13/5.43 fof(f1031,plain,(
% 0.13/5.43 ~sQ10_spl|sQ57_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1011,f590,f1028])).
% 0.13/5.43 fof(f1032,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil))=nil),
% 0.13/5.43 inference(resolution,[status(thm)],[f136,f753])).
% 0.13/5.43 fof(f1033,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|app(app(sK7_skl(nil,sK49_skl),nil),sK8_skl(nil,sK49_skl))=sK49_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f136,f931])).
% 0.13/5.43 fof(f1034,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(sK49_skl)|app(app(sK7_skl(sK49_skl,sK49_skl),sK49_skl),sK8_skl(sK49_skl,sK49_skl))=sK49_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f136,f752])).
% 0.13/5.43 fof(f1035,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|app(app(sK7_skl(nil,sK50_skl),nil),sK8_skl(nil,sK50_skl))=sK50_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f136,f930])).
% 0.13/5.43 fof(f1036,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(sK50_skl)|app(app(sK7_skl(sK50_skl,sK50_skl),sK50_skl),sK8_skl(sK50_skl,sK50_skl))=sK50_skl),
% 0.13/5.43 inference(resolution,[status(thm)],[f136,f751])).
% 0.13/5.43 fof(f1037,definition,(
% 0.13/5.43 sQ58_spl <=> (app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil))=nil)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1040,plain,(
% 0.13/5.43 ~sQ24_spl|sQ58_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1032,f670,f1037])).
% 0.13/5.43 fof(f1041,definition,(
% 0.13/5.43 sQ59_spl <=> (app(app(sK7_skl(nil,sK49_skl),nil),sK8_skl(nil,sK49_skl))=sK49_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1044,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ59_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1033,f677,f670,f1041])).
% 0.13/5.43 fof(f1045,definition,(
% 0.13/5.43 sQ60_spl <=> (app(app(sK7_skl(sK49_skl,sK49_skl),sK49_skl),sK8_skl(sK49_skl,sK49_skl))=sK49_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1048,plain,(
% 0.13/5.43 ~sQ26_spl|sQ60_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1034,f677,f1045])).
% 0.13/5.43 fof(f1049,definition,(
% 0.13/5.43 sQ61_spl <=> (app(app(sK7_skl(nil,sK50_skl),nil),sK8_skl(nil,sK50_skl))=sK50_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1052,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ61_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1035,f590,f670,f1049])).
% 0.13/5.43 fof(f1053,definition,(
% 0.13/5.43 sQ62_spl <=> (app(app(sK7_skl(sK50_skl,sK50_skl),sK50_skl),sK8_skl(sK50_skl,sK50_skl))=sK50_skl)),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1056,plain,(
% 0.13/5.43 ~sQ10_spl|sQ62_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1036,f590,f1053])).
% 0.13/5.43 fof(f1057,plain,(
% 0.13/5.43 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK50_skl)|~memberP(sK50_skl,X0)|memberP(nil,X0)|memberP(sK50_skl,X0))),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f979,f270])).
% 0.13/5.43 fof(f1058,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(sK50_skl)|rearsegP(app(nil,sK50_skl),sK50_skl)|~ssList(nil)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f979,f468])).
% 0.13/5.43 fof(f1059,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~ssList(nil)|frontsegP(app(nil,sK50_skl),nil)|~ssList(sK50_skl)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f979,f467])).
% 0.13/5.43 fof(f1060,definition,(
% 0.13/5.43 ![X0]: (sQ63_spl <=> (~ssItem(X0)|~memberP(sK50_skl,X0)|memberP(nil,X0)|memberP(sK50_skl,X0)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1063,plain,(
% 0.13/5.43 sQ63_spl|~sQ24_spl|~sQ10_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1057,f1060,f670,f590])).
% 0.13/5.43 fof(f1064,definition,(
% 0.13/5.43 sQ64_spl <=> (rearsegP(app(nil,sK50_skl),sK50_skl))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1067,plain,(
% 0.13/5.43 ~sQ10_spl|sQ64_spl|~sQ24_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1058,f590,f1064,f670])).
% 0.13/5.43 fof(f1068,definition,(
% 0.13/5.43 sQ65_spl <=> (frontsegP(app(nil,sK50_skl),nil))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1071,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ24_spl|sQ65_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1059,f590,f670,f1068])).
% 0.13/5.43 fof(f1074,plain,(
% 0.13/5.43 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK49_skl)|~memberP(sK49_skl,X0)|memberP(nil,X0)|memberP(sK49_skl,X0))),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f980,f270])).
% 0.13/5.43 fof(f1075,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(sK49_skl)|rearsegP(app(nil,sK49_skl),sK49_skl)|~ssList(nil)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f980,f468])).
% 0.13/5.43 fof(f1076,plain,(
% 0.13/5.43 ~ssList(sK49_skl)|~ssList(nil)|frontsegP(app(nil,sK49_skl),nil)|~ssList(sK49_skl)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f980,f467])).
% 0.13/5.43 fof(f1077,definition,(
% 0.13/5.43 ![X0]: (sQ66_spl <=> (~ssItem(X0)|~memberP(sK49_skl,X0)|memberP(nil,X0)|memberP(sK49_skl,X0)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1080,plain,(
% 0.13/5.43 sQ66_spl|~sQ24_spl|~sQ26_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1074,f1077,f670,f677])).
% 0.13/5.43 fof(f1081,definition,(
% 0.13/5.43 sQ67_spl <=> (rearsegP(app(nil,sK49_skl),sK49_skl))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1084,plain,(
% 0.13/5.43 ~sQ26_spl|sQ67_spl|~sQ24_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1075,f677,f1081,f670])).
% 0.13/5.43 fof(f1085,definition,(
% 0.13/5.43 sQ68_spl <=> (frontsegP(app(nil,sK49_skl),nil))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1088,plain,(
% 0.13/5.43 ~sQ26_spl|~sQ24_spl|sQ68_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1076,f677,f670,f1085])).
% 0.13/5.43 fof(f1115,plain,(
% 0.13/5.43 cons(sK51_skl,nil)=sK49_skl|~sQ0_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f433,f442])).
% 0.13/5.43 fof(f1116,plain,(
% 0.13/5.43 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f981,f270])).
% 0.13/5.43 fof(f1117,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f981,f468])).
% 0.13/5.43 fof(f1118,plain,(
% 0.13/5.43 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.13/5.43 inference(paramodulation,[status(thm)],[f981,f467])).
% 0.13/5.43 fof(f1119,definition,(
% 0.13/5.43 ![X0]: (sQ69_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1122,plain,(
% 0.13/5.43 sQ69_spl|~sQ24_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1116,f1119,f670])).
% 0.13/5.43 fof(f1123,definition,(
% 0.13/5.43 sQ70_spl <=> (rearsegP(app(nil,nil),nil))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1126,plain,(
% 0.13/5.43 ~sQ24_spl|sQ70_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1117,f670,f1123])).
% 0.13/5.43 fof(f1127,definition,(
% 0.13/5.43 sQ71_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1130,plain,(
% 0.13/5.43 ~sQ24_spl|sQ71_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1118,f670,f1127])).
% 0.13/5.43 fof(f1189,plain,(
% 0.13/5.43 ~ssItem(sK51_skl)|~memberP(sK50_skl,sK51_skl)|~sQ0_spl|~sQ5_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f1115,f566])).
% 0.13/5.43 fof(f1194,definition,(
% 0.13/5.43 sQ72_spl <=> (memberP(sK50_skl,sK51_skl))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1196,plain,(
% 0.13/5.43 ~memberP(sK50_skl,sK51_skl)|sQ72_spl),
% 0.13/5.43 inference(component_clause,[status(thm)],[f1194])).
% 0.13/5.43 fof(f1197,plain,(
% 0.13/5.43 ~sQ11_spl|~sQ72_spl|~sQ0_spl|~sQ5_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1189,f593,f1194,f441,f459])).
% 0.13/5.43 fof(f1208,plain,(
% 0.13/5.43 $false|~sQ0_spl|sQ72_spl),
% 0.13/5.43 inference(forward_subsumption_resolution,[status(thm)],[f1196,f554])).
% 0.13/5.43 fof(f1209,plain,(
% 0.13/5.43 ~sQ0_spl|sQ72_spl),
% 0.13/5.43 inference(contradiction_clause,[status(thm)],[f1208])).
% 0.13/5.43 fof(f1251,plain,(
% 0.13/5.43 neq(sK50_skl,sK50_skl)|~sQ1_spl|~sQ4_spl),
% 0.13/5.43 inference(backward_demodulation,[status(thm)],[f445,f564])).
% 0.13/5.43 fof(f1300,plain,(
% 0.13/5.43 cyclefreeP(sK8_skl(sK50_skl,sK50_skl))|ssItem(sK9_skl(sK8_skl(sK50_skl,sK50_skl)))|~sQ57_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f142,f1029])).
% 0.13/5.43 fof(f1301,plain,(
% 0.13/5.43 cyclefreeP(sK7_skl(sK50_skl,sK50_skl))|ssItem(sK9_skl(sK7_skl(sK50_skl,sK50_skl)))|~sQ52_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f142,f1004])).
% 0.13/5.43 fof(f1304,plain,(
% 0.13/5.43 cyclefreeP(sK6_skl(sK50_skl,sK50_skl))|ssItem(sK9_skl(sK6_skl(sK50_skl,sK50_skl)))|~sQ38_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f142,f769])).
% 0.13/5.43 fof(f1305,plain,(
% 0.13/5.43 cyclefreeP(sK5_skl(sK50_skl,sK50_skl))|ssItem(sK9_skl(sK5_skl(sK50_skl,sK50_skl)))|~sQ28_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f142,f685])).
% 0.13/5.43 fof(f1307,definition,(
% 0.13/5.43 sQ75_spl <=> (cyclefreeP(sK8_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1310,definition,(
% 0.13/5.43 sQ76_spl <=> (ssItem(sK9_skl(sK8_skl(sK50_skl,sK50_skl))))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1313,plain,(
% 0.13/5.43 sQ75_spl|sQ76_spl|~sQ57_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1300,f1307,f1310,f1028])).
% 0.13/5.43 fof(f1314,definition,(
% 0.13/5.43 sQ77_spl <=> (cyclefreeP(sK7_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1317,definition,(
% 0.13/5.43 sQ78_spl <=> (ssItem(sK9_skl(sK7_skl(sK50_skl,sK50_skl))))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1320,plain,(
% 0.13/5.43 sQ77_spl|sQ78_spl|~sQ52_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1301,f1314,f1317,f1003])).
% 0.13/5.43 fof(f1335,definition,(
% 0.13/5.43 sQ83_spl <=> (cyclefreeP(sK6_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1338,definition,(
% 0.13/5.43 sQ84_spl <=> (ssItem(sK9_skl(sK6_skl(sK50_skl,sK50_skl))))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1341,plain,(
% 0.13/5.43 sQ83_spl|sQ84_spl|~sQ38_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1304,f1335,f1338,f768])).
% 0.13/5.43 fof(f1342,definition,(
% 0.13/5.43 sQ85_spl <=> (cyclefreeP(sK5_skl(sK50_skl,sK50_skl)))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1345,definition,(
% 0.13/5.43 sQ86_spl <=> (ssItem(sK9_skl(sK5_skl(sK50_skl,sK50_skl))))),
% 0.13/5.43 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.13/5.43 fof(f1348,plain,(
% 0.13/5.43 sQ85_spl|sQ86_spl|~sQ28_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1305,f1342,f1345,f684])).
% 0.13/5.43 fof(f1356,plain,(
% 0.13/5.43 sP1_prd(sK50_skl,sK50_skl)|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.13/5.43 inference(forward_demodulation,[status(thm)],[f570,f499])).
% 0.13/5.43 fof(f1357,plain,(
% 0.13/5.43 $false|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.13/5.43 inference(forward_subsumption_resolution,[status(thm)],[f1356,f581])).
% 0.13/5.43 fof(f1358,plain,(
% 0.13/5.43 ~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.13/5.43 inference(contradiction_clause,[status(thm)],[f1357])).
% 0.13/5.43 fof(f1369,plain,(
% 0.13/5.43 ~ssList(sK50_skl)|~sQ1_spl|~sQ4_spl),
% 0.13/5.43 inference(resolution,[status(thm)],[f1251,f479])).
% 0.13/5.43 fof(f1371,plain,(
% 0.13/5.43 ~sQ10_spl|~sQ1_spl|~sQ4_spl),
% 0.13/5.43 inference(split_clause,[status(thm)],[f1369,f590,f444,f455])).
% 0.13/5.43 fof(f1372,plain,(
% 0.13/5.43 $false),
% 0.13/5.43 inference(sat_refutation,[status(thm)],[f447,f451,f458,f462,f530,f547,f563,f628,f646,f656,f661,f676,f683,f687,f689,f691,f698,f702,f706,f715,f731,f763,f767,f771,f778,f782,f786,f873,f878,f901,f905,f911,f915,f990,f994,f998,f1002,f1006,f1015,f1019,f1023,f1027,f1031,f1040,f1044,f1048,f1052,f1056,f1063,f1067,f1071,f1080,f1084,f1088,f1122,f1126,f1130,f1197,f1209,f1313,f1320,f1341,f1348,f1358,f1371])).
% 0.13/5.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.44 % Elapsed time: 0.073208 seconds
% 0.13/5.44 % CPU time: 0.271492 seconds
% 0.13/5.44 % Total memory used: 112.418 MB
% 0.13/5.44 % Net memory used: 112.147 MB
%------------------------------------------------------------------------------