%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC322+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 : n011.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:09 PM UTC 2026
% Result : Theorem 10.19s 1.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC322+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.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 08:15:10 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 10.19/1.78 % Refutation found
% 10.19/1.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.19/1.78 % SZS output start CNFRefutation for theBenchmark
% 10.19/1.78 fof(f2,axiom,(
% 10.19/1.78 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f3,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ( memberP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(W,cons(V,X)) = U ) )) )) ) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f4,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f7,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f8,axiom,(
% 10.19/1.78 (! [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) ) ) ) )) )) )) )) )) ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f9,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> ( totalorderP(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) ) ) ) )) )) )) )) )) ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f10,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> ( strictorderP(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=> ( lt(V,W)| lt(W,V) ) ) ) )) )) )) )) )) ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f11,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> ( totalorderedP(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) ) ) )) )) )) )) )) ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f16,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f17,axiom,(
% 10.19/1.78 ssList(nil) ),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f19,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssItem(X)=> ( cons(W,U) = cons(X,V)=> ( W = X& V = U ) ) ) )) )) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f28,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f79,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(W,V) = app(U,V)=> W = U ) ) )) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f80,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(V,W) = app(V,U)=> W = U ) ) )) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f81,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> cons(V,U) = app(cons(V,nil),U) ) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f82,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> app(app(U,V),W) = app(U,app(V,W)) ) )) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f83,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( nil = app(U,V)<=> ( nil = V& nil = U ) ) ) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f84,axiom,(
% 10.19/1.78 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f96,conjecture,(
% 10.19/1.78 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& app(cons(Y,nil),Z) != W& app(Z,cons(Y,nil)) = X ) )))| ( nil != W& nil = X )| ( (! [X1] :( ssItem(X1)=> (! [X2] :( ssList(X2)=> ( app(X2,cons(X1,nil)) != V| app(cons(X1,nil),X2) = U ) ) )))& ( nil != V| nil = U ) ) ) ) )) )) )) )),
% 10.19/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.19/1.78 fof(f97,negated_conjecture,(
% 10.19/1.78 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& app(cons(Y,nil),Z) != W& app(Z,cons(Y,nil)) = X ) )))| ( nil != W& nil = X )| ( (! [X1] :( ssItem(X1)=> (! [X2] :( ssList(X2)=> ( app(X2,cons(X1,nil)) != V| app(cons(X1,nil),X2) = U ) ) )))& ( nil != V| nil = U ) ) ) ) )) )) )) ))),
% 10.19/1.78 inference(negated_conjecture,[status(cth)],[f96])).
% 10.19/1.78 fof(f102,plain,(
% 10.19/1.78 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 10.19/1.78 fof(f103,plain,(
% 10.19/1.78 ssItem(sK0_skl)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f102])).
% 10.19/1.78 fof(f104,plain,(
% 10.19/1.78 ssItem(sK1_skl)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f102])).
% 10.19/1.78 fof(f106,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|(memberP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 10.19/1.78 fof(f107,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|((~memberP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U)))))&(memberP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(W,cons(V,X))=U)))))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f106])).
% 10.19/1.78 fof(f108,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|((~memberP(U,V)|(ssList(sK2_skl(V,U))&(ssList(sK3_skl(V,U))&app(sK2_skl(V,U),cons(V,sK3_skl(V,U)))=U)))&(memberP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(W,cons(V,X))=U)))))))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W,sK2_skl(V,U)),skolemize(X,sK3_skl(V,U))],[f107])).
% 10.19/1.78 fof(f112,plain,(
% 10.19/1.78 ![X0,X1,X2,X3]: (~ssList(X0)|~ssItem(X1)|memberP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(X2,cons(X1,X3))=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f108])).
% 10.19/1.78 fof(f113,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 10.19/1.78 fof(f114,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f113])).
% 10.19/1.78 fof(f115,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~singletonP(U)|(ssItem(sK4_skl(U))&cons(sK4_skl(U),nil)=U))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 10.19/1.78 fof(f116,plain,(
% 10.19/1.78 ![X0]: (~ssList(X0)|~singletonP(X0)|ssItem(sK4_skl(X0)))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f115])).
% 10.19/1.78 fof(f117,plain,(
% 10.19/1.78 ![X0]: (~ssList(X0)|~singletonP(X0)|cons(sK4_skl(X0),nil)=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f115])).
% 10.19/1.78 fof(f118,plain,(
% 10.19/1.78 ![X0,X1]: (~ssList(X0)|singletonP(X0)|~ssItem(X1)|~cons(X1,nil)=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f115])).
% 10.19/1.78 fof(f131,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 10.19/1.78 fof(f132,plain,(
% 10.19/1.78 ![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)))))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f131])).
% 10.19/1.78 fof(f133,plain,(
% 10.19/1.78 ![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)))))))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 10.19/1.78 fof(f137,plain,(
% 10.19/1.78 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f133])).
% 10.19/1.78 fof(f138,plain,(
% 10.19/1.78 ![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)))))))))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 10.19/1.78 fof(f139,plain,(
% 10.19/1.78 ![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))))))))))))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f138])).
% 10.19/1.78 fof(f140,plain,(
% 10.19/1.78 ![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))))))))))))),
% 10.19/1.78 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])).
% 10.19/1.78 fof(f141,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4,X5]: (~ssList(X0)|~cyclefreeP(X0)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~app(app(X3,cons(X1,X4)),cons(X2,X5))=X0|~leq(X1,X2)|~leq(X2,X1))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f140])).
% 10.19/1.78 fof(f150,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(totalorderP(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)))))))))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 10.19/1.78 fof(f151,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~totalorderP(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))))))))))))))&(totalorderP(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))))))))))))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f150])).
% 10.19/1.78 fof(f152,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~totalorderP(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))))))))))))))&(totalorderP(U)|(ssItem(sK14_skl(U))&(ssItem(sK15_skl(U))&(ssList(sK16_skl(U))&(ssList(sK17_skl(U))&(ssList(sK18_skl(U))&(app(app(sK16_skl(U),cons(sK14_skl(U),sK17_skl(U))),cons(sK15_skl(U),sK18_skl(U)))=U&(~leq(sK14_skl(U),sK15_skl(U))&~leq(sK15_skl(U),sK14_skl(U))))))))))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(V,sK14_skl(U)),skolemize(W,sK15_skl(U)),skolemize(X,sK16_skl(U)),skolemize(Y,sK17_skl(U)),skolemize(Z,sK18_skl(U))],[f151])).
% 10.19/1.78 fof(f153,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4,X5]: (~ssList(X0)|~totalorderP(X0)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~app(app(X3,cons(X1,X4)),cons(X2,X5))=X0|leq(X1,X2)|leq(X2,X1))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f152])).
% 10.19/1.78 fof(f162,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(strictorderP(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|(lt(V,W)|lt(W,V)))))))))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 10.19/1.78 fof(f163,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~strictorderP(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|(lt(V,W)|lt(W,V))))))))))))))&(strictorderP(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&(~lt(V,W)&~lt(W,V))))))))))))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f162])).
% 10.19/1.78 fof(f164,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~strictorderP(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|(lt(V,W)|lt(W,V))))))))))))))&(strictorderP(U)|(ssItem(sK19_skl(U))&(ssItem(sK20_skl(U))&(ssList(sK21_skl(U))&(ssList(sK22_skl(U))&(ssList(sK23_skl(U))&(app(app(sK21_skl(U),cons(sK19_skl(U),sK22_skl(U))),cons(sK20_skl(U),sK23_skl(U)))=U&(~lt(sK19_skl(U),sK20_skl(U))&~lt(sK20_skl(U),sK19_skl(U))))))))))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl]),skolemize(V,sK19_skl(U)),skolemize(W,sK20_skl(U)),skolemize(X,sK21_skl(U)),skolemize(Y,sK22_skl(U)),skolemize(Z,sK23_skl(U))],[f163])).
% 10.19/1.78 fof(f165,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4,X5]: (~ssList(X0)|~strictorderP(X0)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~app(app(X3,cons(X1,X4)),cons(X2,X5))=X0|lt(X1,X2)|lt(X2,X1))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f164])).
% 10.19/1.78 fof(f174,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(totalorderedP(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))))))))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 10.19/1.78 fof(f175,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~totalorderedP(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)))))))))))))&(totalorderedP(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)))))))))))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f174])).
% 10.19/1.78 fof(f176,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|((~totalorderedP(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)))))))))))))&(totalorderedP(U)|(ssItem(sK24_skl(U))&(ssItem(sK25_skl(U))&(ssList(sK26_skl(U))&(ssList(sK27_skl(U))&(ssList(sK28_skl(U))&(app(app(sK26_skl(U),cons(sK24_skl(U),sK27_skl(U))),cons(sK25_skl(U),sK28_skl(U)))=U&~leq(sK24_skl(U),sK25_skl(U)))))))))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(V,sK24_skl(U)),skolemize(W,sK25_skl(U)),skolemize(X,sK26_skl(U)),skolemize(Y,sK27_skl(U)),skolemize(Z,sK28_skl(U))],[f175])).
% 10.19/1.78 fof(f177,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4,X5]: (~ssList(X0)|~totalorderedP(X0)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~app(app(X3,cons(X1,X4)),cons(X2,X5))=X0|leq(X1,X2))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f176])).
% 10.19/1.78 fof(f221,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 10.19/1.78 fof(f222,plain,(
% 10.19/1.78 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f221])).
% 10.19/1.78 fof(f223,plain,(
% 10.19/1.78 ssList(nil)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f17])).
% 10.19/1.78 fof(f226,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssItem(W)|(![X]: (~ssItem(X)|(~cons(W,U)=cons(X,V)|(W=X&V=U)))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 10.19/1.78 fof(f227,plain,(
% 10.19/1.78 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X2=X3)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f226])).
% 10.19/1.78 fof(f228,plain,(
% 10.19/1.78 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X1=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f226])).
% 10.19/1.78 fof(f248,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|app(nil,U)=U)),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 10.19/1.78 fof(f249,plain,(
% 10.19/1.78 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f248])).
% 10.19/1.78 fof(f375,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(W,V)=app(U,V)|W=U))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 10.19/1.78 fof(f376,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X2,X1)=app(X0,X1)|X2=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f375])).
% 10.19/1.78 fof(f377,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(V,W)=app(V,U)|W=U))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 10.19/1.78 fof(f378,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X1,X2)=app(X1,X0)|X2=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f377])).
% 10.19/1.78 fof(f379,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|cons(V,U)=app(cons(V,nil),U))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 10.19/1.78 fof(f380,plain,(
% 10.19/1.78 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|cons(X1,X0)=app(cons(X1,nil),X0))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f379])).
% 10.19/1.78 fof(f381,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|app(app(U,V),W)=app(U,app(V,W)))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 10.19/1.78 fof(f382,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|app(app(X0,X1),X2)=app(X0,app(X1,X2)))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f381])).
% 10.19/1.78 fof(f383,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(nil=app(U,V)<=>(nil=V&nil=U)))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 10.19/1.78 fof(f384,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~nil=app(U,V)|(nil=V&nil=U))&(nil=app(U,V)|(~nil=V|~nil=U))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f383])).
% 10.19/1.78 fof(f385,plain,(
% 10.19/1.78 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~nil=app(X0,X1)|nil=X1)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f384])).
% 10.19/1.78 fof(f388,plain,(
% 10.19/1.78 ![U]: (~ssList(U)|app(U,nil)=U)),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 10.19/1.78 fof(f389,plain,(
% 10.19/1.78 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f388])).
% 10.19/1.78 fof(f415,plain,(
% 10.19/1.78 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(![Y]: (~ssItem(Y)|(![Z]: ((~ssList(Z)|app(cons(Y,nil),Z)=W)|~app(Z,cons(Y,nil))=X)))))&(nil=W|~nil=X))&((?[X1]: (ssItem(X1)&(?[X2]: (ssList(X2)&(app(X2,cons(X1,nil))=V&~app(cons(X1,nil),X2)=U)))))|(nil=V&~nil=U)))))))))))),
% 10.19/1.78 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 10.19/1.78 fof(f416,definition,(
% 10.19/1.78 ![U,V,X1]: (sP0_prd(X1,V,U)<=>(ssItem(X1)&(?[X2]: (ssList(X2)&(app(X2,cons(X1,nil))=V&~app(cons(X1,nil),X2)=U)))))),
% 10.19/1.78 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 10.19/1.78 fof(f417,plain,(
% 10.19/1.78 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(![Y]: (~ssItem(Y)|(![Z]: ((~ssList(Z)|app(cons(Y,nil),Z)=W)|~app(Z,cons(Y,nil))=X)))))&(nil=W|~nil=X))&((?[X1]: sP0_prd(X1,V,U))|(nil=V&~nil=U))))))))))),
% 10.19/1.78 inference(formula_renaming,[status(thm)],[f415,f416])).
% 10.19/1.78 fof(f418,plain,(
% 10.19/1.78 (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)|app(cons(Y,nil),Z)=sK49_skl)|~app(Z,cons(Y,nil))=sK50_skl)))))&(nil=sK49_skl|~nil=sK50_skl))&(sP0_prd(sK51_skl,sK48_skl,sK47_skl)|(nil=sK48_skl&~nil=sK47_skl)))))))),
% 10.19/1.78 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(X1,sK51_skl)],[f417])).
% 10.19/1.78 fof(f419,plain,(
% 10.19/1.78 ssList(sK47_skl)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f420,plain,(
% 10.19/1.78 ssList(sK48_skl)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f421,plain,(
% 10.19/1.78 ssList(sK49_skl)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f423,plain,(
% 10.19/1.78 sK48_skl=sK50_skl),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f424,plain,(
% 10.19/1.78 sK47_skl=sK49_skl),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f425,plain,(
% 10.19/1.78 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=sK49_skl|~app(X1,cons(X0,nil))=sK50_skl)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f426,plain,(
% 10.19/1.78 nil=sK49_skl|~nil=sK50_skl),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f427,plain,(
% 10.19/1.78 sP0_prd(sK51_skl,sK48_skl,sK47_skl)|nil=sK48_skl),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f428,plain,(
% 10.19/1.78 sP0_prd(sK51_skl,sK48_skl,sK47_skl)|~nil=sK47_skl),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f418])).
% 10.19/1.78 fof(f429,plain,(
% 10.19/1.78 ![U,V,X1]: ((~sP0_prd(X1,V,U)|(ssItem(X1)&(?[X2]: (ssList(X2)&(app(X2,cons(X1,nil))=V&~app(cons(X1,nil),X2)=U)))))&(sP0_prd(X1,V,U)|(~ssItem(X1)|(![X2]: (~ssList(X2)|(~app(X2,cons(X1,nil))=V|app(cons(X1,nil),X2)=U))))))),
% 10.19/1.78 inference(NNF_transformation,[status(thm)],[f416])).
% 10.19/1.78 fof(f430,plain,(
% 10.19/1.78 (![U,V,X1]: (~sP0_prd(X1,V,U)|(ssItem(X1)&(?[X2]: (ssList(X2)&(app(X2,cons(X1,nil))=V&~app(cons(X1,nil),X2)=U))))))&(![U,V,X1]: (sP0_prd(X1,V,U)|(~ssItem(X1)|(![X2]: (~ssList(X2)|(~app(X2,cons(X1,nil))=V|app(cons(X1,nil),X2)=U))))))),
% 10.19/1.78 inference(miniscoping,[status(thm)],[f429])).
% 10.19/1.78 fof(f431,plain,(
% 10.19/1.78 (![U,V,X1]: (~sP0_prd(X1,V,U)|(ssItem(X1)&(ssList(sK52_skl(X1,V,U))&(app(sK52_skl(X1,V,U),cons(X1,nil))=V&~app(cons(X1,nil),sK52_skl(X1,V,U))=U)))))&(![U,V,X1]: (sP0_prd(X1,V,U)|(~ssItem(X1)|(![X2]: (~ssList(X2)|(~app(X2,cons(X1,nil))=V|app(cons(X1,nil),X2)=U))))))),
% 10.19/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl]),skolemize(X2,sK52_skl(X1,V,U))],[f430])).
% 10.19/1.78 fof(f432,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssItem(X0))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f431])).
% 10.19/1.78 fof(f433,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssList(sK52_skl(X0,X1,X2)))),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f431])).
% 10.19/1.78 fof(f434,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|app(sK52_skl(X0,X1,X2),cons(X0,nil))=X1)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f431])).
% 10.19/1.78 fof(f435,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~app(cons(X0,nil),sK52_skl(X0,X1,X2))=X2)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f431])).
% 10.19/1.78 fof(f436,plain,(
% 10.19/1.78 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2)|~ssItem(X0)|~ssList(X3)|~app(X3,cons(X0,nil))=X1|app(cons(X0,nil),X3)=X2)),
% 10.19/1.78 inference(cnf_transformation,[status(thm)],[f431])).
% 10.19/1.78 fof(f437,definition,(
% 10.19/1.78 sQ0_spl <=> (nil=sK49_skl)),
% 10.19/1.78 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 10.19/1.78 fof(f438,plain,(
% 10.19/1.78 nil=sK49_skl|~sQ0_spl),
% 10.19/1.78 inference(component_clause,[status(thm)],[f437])).
% 10.19/1.78 fof(f440,definition,(
% 10.19/1.78 sQ1_spl <=> (nil=sK50_skl)),
% 10.19/1.78 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 10.19/1.78 fof(f442,plain,(
% 10.19/1.78 ~nil=sK50_skl|sQ1_spl),
% 10.19/1.78 inference(component_clause,[status(thm)],[f440])).
% 10.19/1.78 fof(f443,plain,(
% 10.19/1.78 sQ0_spl|~sQ1_spl),
% 10.19/1.78 inference(split_clause,[status(thm)],[f426,f437,f440])).
% 10.19/1.78 fof(f444,definition,(
% 10.19/1.78 sQ2_spl <=> (sP0_prd(sK51_skl,sK48_skl,sK47_skl))),
% 10.19/1.78 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 10.19/1.78 fof(f445,plain,(
% 10.19/1.78 sP0_prd(sK51_skl,sK48_skl,sK47_skl)|~sQ2_spl),
% 10.19/1.78 inference(component_clause,[status(thm)],[f444])).
% 10.19/1.78 fof(f447,definition,(
% 10.19/1.78 sQ3_spl <=> (nil=sK48_skl)),
% 10.19/1.78 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 10.19/1.78 fof(f448,plain,(
% 10.19/1.78 nil=sK48_skl|~sQ3_spl),
% 10.19/1.78 inference(component_clause,[status(thm)],[f447])).
% 10.19/1.78 fof(f450,plain,(
% 10.19/1.78 sQ2_spl|sQ3_spl),
% 10.19/1.78 inference(split_clause,[status(thm)],[f427,f444,f447])).
% 10.19/1.78 fof(f451,definition,(
% 10.19/1.78 sQ4_spl <=> (nil=sK47_skl)),
% 10.19/1.78 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 10.19/1.78 fof(f453,plain,(
% 10.19/1.78 ~nil=sK47_skl|sQ4_spl),
% 10.19/1.78 inference(component_clause,[status(thm)],[f451])).
% 10.19/1.78 fof(f454,plain,(
% 10.19/1.78 sQ2_spl|~sQ4_spl),
% 10.19/1.78 inference(split_clause,[status(thm)],[f428,f444,f451])).
% 10.19/1.78 fof(f457,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~ssList(app(X0,cons(X1,X2)))|~ssItem(X1)|memberP(app(X0,cons(X1,X2)),X1)|~ssList(X0)|~ssList(X2))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f112])).
% 10.19/1.78 fof(f458,plain,(
% 10.19/1.78 ![X0]: (~ssList(cons(X0,nil))|singletonP(cons(X0,nil))|~ssItem(X0))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 10.19/1.78 fof(f461,plain,(
% 10.19/1.78 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 10.19/1.78 fof(f462,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4]: (~ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~cyclefreeP(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~ssItem(X1)|~ssItem(X3)|~ssList(X0)|~ssList(X2)|~ssList(X4)|~leq(X1,X3)|~leq(X3,X1))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 10.19/1.78 fof(f463,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4]: (~ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~totalorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~ssItem(X1)|~ssItem(X3)|~ssList(X0)|~ssList(X2)|~ssList(X4)|leq(X1,X3)|leq(X3,X1))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f153])).
% 10.19/1.78 fof(f464,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4]: (~ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~strictorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~ssItem(X1)|~ssItem(X3)|~ssList(X0)|~ssList(X2)|~ssList(X4)|lt(X1,X3)|lt(X3,X1))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f165])).
% 10.19/1.78 fof(f465,plain,(
% 10.19/1.78 ![X0,X1,X2,X3,X4]: (~ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~totalorderedP(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~ssItem(X1)|~ssItem(X3)|~ssList(X0)|~ssList(X2)|~ssList(X4)|leq(X1,X3))),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f177])).
% 10.19/1.78 fof(f485,plain,(
% 10.19/1.78 ![X0,X1,X2]: (sP0_prd(X0,app(X1,cons(X0,nil)),X2)|~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=X2)),
% 10.19/1.78 inference(destructive_equality_resolution,[status(thm)],[f436])).
% 10.19/1.79 fof(f494,plain,(
% 10.19/1.79 app(nil,sK48_skl)=sK48_skl),
% 10.19/1.79 inference(resolution,[status(thm)],[f249,f420])).
% 10.19/1.79 fof(f495,plain,(
% 10.19/1.79 app(nil,sK47_skl)=sK47_skl),
% 10.19/1.79 inference(resolution,[status(thm)],[f249,f419])).
% 10.19/1.79 fof(f496,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|cons(X0,sK49_skl)=app(cons(X0,nil),sK49_skl))),
% 10.19/1.79 inference(resolution,[status(thm)],[f380,f421])).
% 10.19/1.79 fof(f497,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|cons(X0,sK48_skl)=app(cons(X0,nil),sK48_skl))),
% 10.19/1.79 inference(resolution,[status(thm)],[f380,f420])).
% 10.19/1.79 fof(f498,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|cons(X0,sK47_skl)=app(cons(X0,nil),sK47_skl))),
% 10.19/1.79 inference(resolution,[status(thm)],[f380,f419])).
% 10.19/1.79 fof(f500,plain,(
% 10.19/1.79 app(sK48_skl,nil)=sK48_skl),
% 10.19/1.79 inference(resolution,[status(thm)],[f389,f420])).
% 10.19/1.79 fof(f501,plain,(
% 10.19/1.79 app(sK47_skl,nil)=sK47_skl),
% 10.19/1.79 inference(resolution,[status(thm)],[f389,f419])).
% 10.19/1.79 fof(f503,plain,(
% 10.19/1.79 app(nil,nil)=nil),
% 10.19/1.79 inference(resolution,[status(thm)],[f223,f389])).
% 10.19/1.79 fof(f504,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|cons(X0,nil)=app(cons(X0,nil),nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f223,f380])).
% 10.19/1.79 fof(f507,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|ssList(cons(X0,nil)))),
% 10.19/1.79 inference(resolution,[status(thm)],[f223,f222])).
% 10.19/1.79 fof(f508,plain,(
% 10.19/1.79 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X1=X1)),
% 10.19/1.79 inference(equality_resolution,[status(thm)],[f227])).
% 10.19/1.79 fof(f509,definition,(
% 10.19/1.79 ![X0]: (sQ5_spl <=> (~ssList(X0)|~ssList(X0)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f510,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ5_spl)),
% 10.19/1.79 inference(component_clause,[status(thm)],[f509])).
% 10.19/1.79 fof(f512,definition,(
% 10.19/1.79 ![X1]: (sQ6_spl <=> (~ssItem(X1)|~ssItem(X1)|X1=X1))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f515,plain,(
% 10.19/1.79 sQ5_spl|sQ6_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f508,f509,f512])).
% 10.19/1.79 fof(f516,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~sQ5_spl)),
% 10.19/1.79 inference(duplicate_literals_removal,[status(thm)],[f510])).
% 10.19/1.79 fof(f517,plain,(
% 10.19/1.79 app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),cons(sK51_skl,nil))=sK48_skl|~sQ2_spl),
% 10.19/1.79 inference(resolution,[status(thm)],[f445,f434])).
% 10.19/1.79 fof(f518,plain,(
% 10.19/1.79 ssItem(sK51_skl)|~sQ2_spl),
% 10.19/1.79 inference(resolution,[status(thm)],[f445,f432])).
% 10.19/1.79 fof(f526,plain,(
% 10.19/1.79 cons(sK1_skl,sK48_skl)=app(cons(sK1_skl,nil),sK48_skl)),
% 10.19/1.79 inference(resolution,[status(thm)],[f497,f104])).
% 10.19/1.79 fof(f527,plain,(
% 10.19/1.79 cons(sK0_skl,sK48_skl)=app(cons(sK0_skl,nil),sK48_skl)),
% 10.19/1.79 inference(resolution,[status(thm)],[f497,f103])).
% 10.19/1.79 fof(f528,plain,(
% 10.19/1.79 cons(sK1_skl,sK47_skl)=app(cons(sK1_skl,nil),sK47_skl)),
% 10.19/1.79 inference(resolution,[status(thm)],[f498,f104])).
% 10.19/1.79 fof(f529,plain,(
% 10.19/1.79 cons(sK0_skl,sK47_skl)=app(cons(sK0_skl,nil),sK47_skl)),
% 10.19/1.79 inference(resolution,[status(thm)],[f498,f103])).
% 10.19/1.79 fof(f538,definition,(
% 10.19/1.79 sQ7_spl <=> (ssItem(sK51_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f540,plain,(
% 10.19/1.79 ~ssItem(sK51_skl)|sQ7_spl),
% 10.19/1.79 inference(component_clause,[status(thm)],[f538])).
% 10.19/1.79 fof(f552,plain,(
% 10.19/1.79 ~nil=sK48_skl|sQ1_spl),
% 10.19/1.79 inference(forward_demodulation,[status(thm)],[f423,f442])).
% 10.19/1.79 fof(f553,plain,(
% 10.19/1.79 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=sK49_skl|~app(X1,cons(X0,nil))=sK48_skl)),
% 10.19/1.79 inference(forward_demodulation,[status(thm)],[f423,f425])).
% 10.19/1.79 fof(f554,plain,(
% 10.19/1.79 cons(sK1_skl,nil)=app(cons(sK1_skl,nil),nil)),
% 10.19/1.79 inference(resolution,[status(thm)],[f504,f104])).
% 10.19/1.79 fof(f555,plain,(
% 10.19/1.79 cons(sK0_skl,nil)=app(cons(sK0_skl,nil),nil)),
% 10.19/1.79 inference(resolution,[status(thm)],[f504,f103])).
% 10.19/1.79 fof(f556,plain,(
% 10.19/1.79 ssList(cons(sK1_skl,nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f507,f104])).
% 10.19/1.79 fof(f557,plain,(
% 10.19/1.79 ssList(cons(sK0_skl,nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f507,f103])).
% 10.19/1.79 fof(f559,plain,(
% 10.19/1.79 $false|~sQ5_spl),
% 10.19/1.79 inference(backward_subsumption_resolution,[status(thm)],[f223,f516])).
% 10.19/1.79 fof(f562,plain,(
% 10.19/1.79 ~sQ5_spl),
% 10.19/1.79 inference(contradiction_clause,[status(thm)],[f559])).
% 10.19/1.79 fof(f567,plain,(
% 10.19/1.79 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X0=X0)),
% 10.19/1.79 inference(equality_resolution,[status(thm)],[f228])).
% 10.19/1.79 fof(f568,definition,(
% 10.19/1.79 ![X0]: (sQ11_spl <=> (~ssList(X0)|~ssList(X0)|X0=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f571,definition,(
% 10.19/1.79 ![X1]: (sQ12_spl <=> (~ssItem(X1)|~ssItem(X1)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f572,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|~ssItem(X0)|~sQ12_spl)),
% 10.19/1.79 inference(component_clause,[status(thm)],[f571])).
% 10.19/1.79 fof(f574,plain,(
% 10.19/1.79 sQ11_spl|sQ12_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f567,f568,f571])).
% 10.19/1.79 fof(f575,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|~sQ12_spl)),
% 10.19/1.79 inference(duplicate_literals_removal,[status(thm)],[f572])).
% 10.19/1.79 fof(f578,plain,(
% 10.19/1.79 $false|sQ1_spl|~sQ3_spl),
% 10.19/1.79 inference(forward_subsumption_resolution,[status(thm)],[f448,f552])).
% 10.19/1.79 fof(f579,plain,(
% 10.19/1.79 sQ1_spl|~sQ3_spl),
% 10.19/1.79 inference(contradiction_clause,[status(thm)],[f578])).
% 10.19/1.79 fof(f580,plain,(
% 10.19/1.79 cons(sK1_skl,sK49_skl)=app(cons(sK1_skl,nil),sK49_skl)),
% 10.19/1.79 inference(resolution,[status(thm)],[f496,f104])).
% 10.19/1.79 fof(f581,plain,(
% 10.19/1.79 cons(sK0_skl,sK49_skl)=app(cons(sK0_skl,nil),sK49_skl)),
% 10.19/1.79 inference(resolution,[status(thm)],[f496,f103])).
% 10.19/1.79 fof(f602,plain,(
% 10.19/1.79 $false|~sQ12_spl),
% 10.19/1.79 inference(backward_subsumption_resolution,[status(thm)],[f104,f575])).
% 10.19/1.79 fof(f604,plain,(
% 10.19/1.79 ~sQ12_spl),
% 10.19/1.79 inference(contradiction_clause,[status(thm)],[f602])).
% 10.19/1.79 fof(f605,plain,(
% 10.19/1.79 sK47_skl=nil|~sQ0_spl),
% 10.19/1.79 inference(backward_demodulation,[status(thm)],[f438,f424])).
% 10.19/1.79 fof(f606,plain,(
% 10.19/1.79 $false|sQ4_spl|~sQ0_spl),
% 10.19/1.79 inference(forward_subsumption_resolution,[status(thm)],[f605,f453])).
% 10.19/1.79 fof(f607,plain,(
% 10.19/1.79 sQ4_spl|~sQ0_spl),
% 10.19/1.79 inference(contradiction_clause,[status(thm)],[f606])).
% 10.19/1.79 fof(f618,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(cons(sK0_skl,nil))|~cons(sK0_skl,nil)=app(X0,nil)|cons(sK0_skl,nil)=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f555,f376])).
% 10.19/1.79 fof(f619,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(cons(sK0_skl,nil))|~cons(sK0_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK0_skl,nil)=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f527,f376])).
% 10.19/1.79 fof(f620,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(cons(sK1_skl,nil))|~cons(sK1_skl,nil)=app(X0,nil)|cons(sK1_skl,nil)=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f554,f376])).
% 10.19/1.79 fof(f621,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(cons(sK1_skl,nil))|~cons(sK1_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK1_skl,nil)=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f526,f376])).
% 10.19/1.79 fof(f622,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK48_skl)|~sK48_skl=app(X0,nil)|sK48_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f500,f376])).
% 10.19/1.79 fof(f623,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~nil=app(X0,nil)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f503,f376])).
% 10.19/1.79 fof(f624,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~sK48_skl=app(X0,sK48_skl)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f494,f376])).
% 10.19/1.79 fof(f633,definition,(
% 10.19/1.79 ![X0]: (sQ13_spl <=> (~ssList(X0)|~cons(sK0_skl,nil)=app(X0,nil)|cons(sK0_skl,nil)=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f636,definition,(
% 10.19/1.79 sQ14_spl <=> (ssList(nil))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f639,definition,(
% 10.19/1.79 sQ15_spl <=> (ssList(cons(sK0_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f642,plain,(
% 10.19/1.79 sQ13_spl|~sQ14_spl|~sQ15_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f618,f633,f636,f639])).
% 10.19/1.79 fof(f643,definition,(
% 10.19/1.79 ![X0]: (sQ16_spl <=> (~ssList(X0)|~cons(sK0_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK0_skl,nil)=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f646,definition,(
% 10.19/1.79 sQ17_spl <=> (ssList(sK48_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f648,plain,(
% 10.19/1.79 ~ssList(sK48_skl)|sQ17_spl),
% 10.19/1.79 inference(component_clause,[status(thm)],[f646])).
% 10.19/1.79 fof(f649,plain,(
% 10.19/1.79 sQ16_spl|~sQ17_spl|~sQ15_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f619,f643,f646,f639])).
% 10.19/1.79 fof(f650,definition,(
% 10.19/1.79 ![X0]: (sQ18_spl <=> (~ssList(X0)|~cons(sK1_skl,nil)=app(X0,nil)|cons(sK1_skl,nil)=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f653,definition,(
% 10.19/1.79 sQ19_spl <=> (ssList(cons(sK1_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f656,plain,(
% 10.19/1.79 sQ18_spl|~sQ14_spl|~sQ19_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f620,f650,f636,f653])).
% 10.19/1.79 fof(f657,definition,(
% 10.19/1.79 ![X0]: (sQ20_spl <=> (~ssList(X0)|~cons(sK1_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK1_skl,nil)=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f660,plain,(
% 10.19/1.79 sQ20_spl|~sQ17_spl|~sQ19_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f621,f657,f646,f653])).
% 10.19/1.79 fof(f661,definition,(
% 10.19/1.79 ![X0]: (sQ21_spl <=> (~ssList(X0)|~sK48_skl=app(X0,nil)|sK48_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f664,plain,(
% 10.19/1.79 sQ21_spl|~sQ14_spl|~sQ17_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f622,f661,f636,f646])).
% 10.19/1.79 fof(f665,definition,(
% 10.19/1.79 ![X0]: (sQ22_spl <=> (~ssList(X0)|~nil=app(X0,nil)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f668,plain,(
% 10.19/1.79 sQ22_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f623,f665,f636])).
% 10.19/1.79 fof(f669,definition,(
% 10.19/1.79 ![X0]: (sQ23_spl <=> (~ssList(X0)|~sK48_skl=app(X0,sK48_skl)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f672,plain,(
% 10.19/1.79 sQ23_spl|~sQ17_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f624,f669,f646,f636])).
% 10.19/1.79 fof(f684,plain,(
% 10.19/1.79 $false|sQ17_spl),
% 10.19/1.79 inference(forward_subsumption_resolution,[status(thm)],[f648,f420])).
% 10.19/1.79 fof(f685,plain,(
% 10.19/1.79 sQ17_spl),
% 10.19/1.79 inference(contradiction_clause,[status(thm)],[f684])).
% 10.19/1.79 fof(f686,plain,(
% 10.19/1.79 ssList(sK52_skl(sK51_skl,sK48_skl,sK47_skl))|~sQ2_spl),
% 10.19/1.79 inference(resolution,[status(thm)],[f445,f433])).
% 10.19/1.79 fof(f707,definition,(
% 10.19/1.79 sQ28_spl <=> (ssList(sK47_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f709,plain,(
% 10.19/1.79 ~ssList(sK47_skl)|sQ28_spl),
% 10.19/1.79 inference(component_clause,[status(thm)],[f707])).
% 10.19/1.79 fof(f722,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(sK49_skl)|~ssList(X0)|~app(X0,sK49_skl)=cons(sK1_skl,sK49_skl)|X0=cons(sK1_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f580,f376])).
% 10.19/1.79 fof(f724,definition,(
% 10.19/1.79 sQ31_spl <=> (ssList(sK49_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f727,definition,(
% 10.19/1.79 ![X0]: (sQ32_spl <=> (~ssList(X0)|~app(X0,sK49_skl)=cons(sK1_skl,sK49_skl)|X0=cons(sK1_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f730,plain,(
% 10.19/1.79 ~sQ19_spl|~sQ31_spl|sQ32_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f722,f653,f724,f727])).
% 10.19/1.79 fof(f732,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(sK49_skl)|~ssList(X0)|~app(X0,sK49_skl)=cons(sK0_skl,sK49_skl)|X0=cons(sK0_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f581,f376])).
% 10.19/1.79 fof(f734,definition,(
% 10.19/1.79 ![X0]: (sQ33_spl <=> (~ssList(X0)|~app(X0,sK49_skl)=cons(sK0_skl,sK49_skl)|X0=cons(sK0_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f737,plain,(
% 10.19/1.79 ~sQ15_spl|~sQ31_spl|sQ33_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f732,f639,f724,f734])).
% 10.19/1.79 fof(f759,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(sK47_skl)|~ssList(X0)|~app(X0,sK47_skl)=cons(sK0_skl,sK47_skl)|X0=cons(sK0_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f529,f376])).
% 10.19/1.79 fof(f761,definition,(
% 10.19/1.79 ![X0]: (sQ35_spl <=> (~ssList(X0)|~app(X0,sK47_skl)=cons(sK0_skl,sK47_skl)|X0=cons(sK0_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f764,plain,(
% 10.19/1.79 ~sQ15_spl|~sQ28_spl|sQ35_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f759,f639,f707,f761])).
% 10.19/1.79 fof(f766,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(sK47_skl)|~ssList(X0)|~app(X0,sK47_skl)=cons(sK1_skl,sK47_skl)|X0=cons(sK1_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f528,f376])).
% 10.19/1.79 fof(f768,definition,(
% 10.19/1.79 ![X0]: (sQ36_spl <=> (~ssList(X0)|~app(X0,sK47_skl)=cons(sK1_skl,sK47_skl)|X0=cons(sK1_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f771,plain,(
% 10.19/1.79 ~sQ19_spl|~sQ28_spl|sQ36_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f766,f653,f707,f768])).
% 10.19/1.79 fof(f773,plain,(
% 10.19/1.79 ![X0]: (~ssList(sK47_skl)|~ssList(nil)|~ssList(X0)|~app(X0,nil)=sK47_skl|X0=sK47_skl)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f501,f376])).
% 10.19/1.79 fof(f775,definition,(
% 10.19/1.79 ![X0]: (sQ37_spl <=> (~ssList(X0)|~app(X0,nil)=sK47_skl|X0=sK47_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f778,plain,(
% 10.19/1.79 ~sQ28_spl|~sQ14_spl|sQ37_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f773,f707,f636,f775])).
% 10.19/1.79 fof(f780,plain,(
% 10.19/1.79 ![X0]: (~ssList(nil)|~ssList(sK47_skl)|~ssList(X0)|~app(X0,sK47_skl)=sK47_skl|X0=nil)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f495,f376])).
% 10.19/1.79 fof(f782,definition,(
% 10.19/1.79 ![X0]: (sQ38_spl <=> (~ssList(X0)|~app(X0,sK47_skl)=sK47_skl|X0=nil))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f785,plain,(
% 10.19/1.79 ~sQ14_spl|~sQ28_spl|sQ38_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f780,f636,f707,f782])).
% 10.19/1.79 fof(f792,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~sK47_skl=app(sK47_skl,X0)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f501,f378])).
% 10.19/1.79 fof(f797,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(cons(sK0_skl,nil))|~ssList(sK47_skl)|~cons(sK0_skl,sK47_skl)=app(cons(sK0_skl,nil),X0)|sK47_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f529,f378])).
% 10.19/1.79 fof(f798,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~cons(sK0_skl,nil)=app(cons(sK0_skl,nil),X0)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f555,f378])).
% 10.19/1.79 fof(f799,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(cons(sK0_skl,nil))|~ssList(sK48_skl)|~cons(sK0_skl,sK48_skl)=app(cons(sK0_skl,nil),X0)|sK48_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f527,f378])).
% 10.19/1.79 fof(f800,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(cons(sK1_skl,nil))|~ssList(sK47_skl)|~cons(sK1_skl,sK47_skl)=app(cons(sK1_skl,nil),X0)|sK47_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f528,f378])).
% 10.19/1.79 fof(f801,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~cons(sK1_skl,nil)=app(cons(sK1_skl,nil),X0)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f554,f378])).
% 10.19/1.79 fof(f802,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(cons(sK1_skl,nil))|~ssList(sK48_skl)|~cons(sK1_skl,sK48_skl)=app(cons(sK1_skl,nil),X0)|sK48_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f526,f378])).
% 10.19/1.79 fof(f803,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~sK48_skl=app(sK48_skl,X0)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f500,f378])).
% 10.19/1.79 fof(f804,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK47_skl)|~sK47_skl=app(nil,X0)|sK47_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f495,f378])).
% 10.19/1.79 fof(f805,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~nil=app(nil,X0)|nil=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f503,f378])).
% 10.19/1.79 fof(f806,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK48_skl)|~sK48_skl=app(nil,X0)|sK48_skl=X0)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f494,f378])).
% 10.19/1.79 fof(f823,definition,(
% 10.19/1.79 ![X0]: (sQ39_spl <=> (~ssList(X0)|~sK47_skl=app(sK47_skl,X0)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f826,plain,(
% 10.19/1.79 sQ39_spl|~sQ28_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f792,f823,f707,f636])).
% 10.19/1.79 fof(f843,definition,(
% 10.19/1.79 ![X0]: (sQ44_spl <=> (~ssList(X0)|~cons(sK0_skl,sK47_skl)=app(cons(sK0_skl,nil),X0)|sK47_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f846,plain,(
% 10.19/1.79 sQ44_spl|~sQ15_spl|~sQ28_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f797,f843,f639,f707])).
% 10.19/1.79 fof(f847,definition,(
% 10.19/1.79 ![X0]: (sQ45_spl <=> (~ssList(X0)|~cons(sK0_skl,nil)=app(cons(sK0_skl,nil),X0)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f850,plain,(
% 10.19/1.79 sQ45_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f798,f847,f639,f636])).
% 10.19/1.79 fof(f851,definition,(
% 10.19/1.79 ![X0]: (sQ46_spl <=> (~ssList(X0)|~cons(sK0_skl,sK48_skl)=app(cons(sK0_skl,nil),X0)|sK48_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f854,plain,(
% 10.19/1.79 sQ46_spl|~sQ15_spl|~sQ17_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f799,f851,f639,f646])).
% 10.19/1.79 fof(f855,definition,(
% 10.19/1.79 ![X0]: (sQ47_spl <=> (~ssList(X0)|~cons(sK1_skl,sK47_skl)=app(cons(sK1_skl,nil),X0)|sK47_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f858,plain,(
% 10.19/1.79 sQ47_spl|~sQ19_spl|~sQ28_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f800,f855,f653,f707])).
% 10.19/1.79 fof(f859,definition,(
% 10.19/1.79 ![X0]: (sQ48_spl <=> (~ssList(X0)|~cons(sK1_skl,nil)=app(cons(sK1_skl,nil),X0)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f862,plain,(
% 10.19/1.79 sQ48_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f801,f859,f653,f636])).
% 10.19/1.79 fof(f863,definition,(
% 10.19/1.79 ![X0]: (sQ49_spl <=> (~ssList(X0)|~cons(sK1_skl,sK48_skl)=app(cons(sK1_skl,nil),X0)|sK48_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f866,plain,(
% 10.19/1.79 sQ49_spl|~sQ19_spl|~sQ17_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f802,f863,f653,f646])).
% 10.19/1.79 fof(f867,definition,(
% 10.19/1.79 ![X0]: (sQ50_spl <=> (~ssList(X0)|~sK48_skl=app(sK48_skl,X0)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f870,plain,(
% 10.19/1.79 sQ50_spl|~sQ17_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f803,f867,f646,f636])).
% 10.19/1.79 fof(f871,definition,(
% 10.19/1.79 ![X0]: (sQ51_spl <=> (~ssList(X0)|~sK47_skl=app(nil,X0)|sK47_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f874,plain,(
% 10.19/1.79 sQ51_spl|~sQ14_spl|~sQ28_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f804,f871,f636,f707])).
% 10.19/1.79 fof(f875,definition,(
% 10.19/1.79 ![X0]: (sQ52_spl <=> (~ssList(X0)|~nil=app(nil,X0)|nil=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f878,plain,(
% 10.19/1.79 sQ52_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f805,f875,f636])).
% 10.19/1.79 fof(f879,definition,(
% 10.19/1.79 ![X0]: (sQ53_spl <=> (~ssList(X0)|~sK48_skl=app(nil,X0)|sK48_skl=X0))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f882,plain,(
% 10.19/1.79 sQ53_spl|~sQ14_spl|~sQ17_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f806,f879,f636,f646])).
% 10.19/1.79 fof(f899,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|app(app(X0,sK47_skl),sK47_skl)=app(X0,app(sK47_skl,sK47_skl)))),
% 10.19/1.79 inference(resolution,[status(thm)],[f382,f419])).
% 10.19/1.79 fof(f901,plain,(
% 10.19/1.79 ![X0]: (~ssList(X0)|app(app(X0,sK48_skl),sK48_skl)=app(X0,app(sK48_skl,sK48_skl)))),
% 10.19/1.79 inference(resolution,[status(thm)],[f382,f420])).
% 10.19/1.79 fof(f925,plain,(
% 10.19/1.79 ![X0]: (singletonP(cons(X0,nil))|~ssItem(X0))),
% 10.19/1.79 inference(forward_subsumption_resolution,[status(thm)],[f458,f507])).
% 10.19/1.79 fof(f926,plain,(
% 10.19/1.79 singletonP(cons(sK0_skl,nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f925,f103])).
% 10.19/1.79 fof(f927,plain,(
% 10.19/1.79 singletonP(cons(sK1_skl,nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f925,f104])).
% 10.19/1.79 fof(f942,plain,(
% 10.19/1.79 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=sK47_skl|~app(X1,cons(X0,nil))=sK48_skl)),
% 10.19/1.79 inference(forward_demodulation,[status(thm)],[f424,f553])).
% 10.19/1.79 fof(f950,plain,(
% 10.19/1.79 $false|sQ28_spl),
% 10.19/1.79 inference(forward_subsumption_resolution,[status(thm)],[f709,f419])).
% 10.19/1.79 fof(f951,plain,(
% 10.19/1.79 sQ28_spl),
% 10.19/1.79 inference(contradiction_clause,[status(thm)],[f950])).
% 10.19/1.79 fof(f952,plain,(
% 10.19/1.79 ~ssList(nil)|~ssList(nil)|nil=nil),
% 10.19/1.79 inference(resolution,[status(thm)],[f385,f503])).
% 10.19/1.79 fof(f958,plain,(
% 10.19/1.79 ~ssList(cons(sK0_skl,nil))|~ssList(sK47_skl)|~nil=cons(sK0_skl,sK47_skl)|nil=sK47_skl),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f529,f385])).
% 10.19/1.79 fof(f961,plain,(
% 10.19/1.79 ~ssList(cons(sK1_skl,nil))|~ssList(sK47_skl)|~nil=cons(sK1_skl,sK47_skl)|nil=sK47_skl),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f528,f385])).
% 10.19/1.79 fof(f968,definition,(
% 10.19/1.79 sQ55_spl <=> (nil=nil)),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f971,plain,(
% 10.19/1.79 ~sQ14_spl|sQ55_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f952,f636,f968])).
% 10.19/1.79 fof(f986,definition,(
% 10.19/1.79 sQ59_spl <=> (nil=cons(sK0_skl,sK47_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f989,plain,(
% 10.19/1.79 ~sQ15_spl|~sQ28_spl|~sQ59_spl|sQ4_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f958,f639,f707,f986,f451])).
% 10.19/1.79 fof(f998,definition,(
% 10.19/1.79 sQ62_spl <=> (nil=cons(sK1_skl,sK47_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1001,plain,(
% 10.19/1.79 ~sQ19_spl|~sQ28_spl|~sQ62_spl|sQ4_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f961,f653,f707,f998,f451])).
% 10.19/1.79 fof(f1064,plain,(
% 10.19/1.79 ![X0]: (~ssItem(X0)|cons(X0,cons(sK1_skl,nil))=app(cons(X0,nil),cons(sK1_skl,nil)))),
% 10.19/1.79 inference(resolution,[status(thm)],[f556,f380])).
% 10.19/1.79 fof(f1067,plain,(
% 10.19/1.79 app(nil,cons(sK1_skl,nil))=cons(sK1_skl,nil)),
% 10.19/1.79 inference(resolution,[status(thm)],[f556,f249])).
% 10.19/1.79 fof(f1070,plain,(
% 10.19/1.79 cons(sK0_skl,cons(sK1_skl,nil))=app(cons(sK0_skl,nil),cons(sK1_skl,nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f1064,f103])).
% 10.19/1.79 fof(f1071,plain,(
% 10.19/1.79 cons(sK1_skl,cons(sK1_skl,nil))=app(cons(sK1_skl,nil),cons(sK1_skl,nil))),
% 10.19/1.79 inference(resolution,[status(thm)],[f1064,f104])).
% 10.19/1.79 fof(f1095,plain,(
% 10.19/1.79 ~ssItem(sK1_skl)|~ssList(nil)|app(cons(sK1_skl,nil),nil)=sK47_skl|~cons(sK1_skl,nil)=sK48_skl),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1067,f942])).
% 10.19/1.79 fof(f1096,plain,(
% 10.19/1.79 ~ssList(cons(sK1_skl,nil))|~ssItem(sK1_skl)|memberP(app(nil,cons(sK1_skl,nil)),sK1_skl)|~ssList(nil)|~ssList(nil)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1067,f457])).
% 10.19/1.79 fof(f1099,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X0)|~app(nil,X0)=cons(sK1_skl,nil)|X0=cons(sK1_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1067,f378])).
% 10.19/1.79 fof(f1101,plain,(
% 10.19/1.79 ![X0]: (~ssList(nil)|~ssList(cons(sK1_skl,nil))|~ssList(X0)|~app(X0,cons(sK1_skl,nil))=cons(sK1_skl,nil)|X0=nil)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1067,f376])).
% 10.19/1.79 fof(f1103,definition,(
% 10.19/1.79 sQ66_spl <=> (ssItem(sK1_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1105,plain,(
% 10.19/1.79 ~ssItem(sK1_skl)|sQ66_spl),
% 10.19/1.79 inference(component_clause,[status(thm)],[f1103])).
% 10.19/1.79 fof(f1106,definition,(
% 10.19/1.79 sQ67_spl <=> (app(cons(sK1_skl,nil),nil)=sK47_skl)),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1109,definition,(
% 10.19/1.79 sQ68_spl <=> (cons(sK1_skl,nil)=sK48_skl)),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1112,plain,(
% 10.19/1.79 ~sQ66_spl|~sQ14_spl|sQ67_spl|~sQ68_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1095,f1103,f636,f1106,f1109])).
% 10.19/1.79 fof(f1113,definition,(
% 10.19/1.79 sQ69_spl <=> (memberP(app(nil,cons(sK1_skl,nil)),sK1_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1116,plain,(
% 10.19/1.79 ~sQ19_spl|~sQ66_spl|sQ69_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1096,f653,f1103,f1113,f636])).
% 10.19/1.79 fof(f1119,definition,(
% 10.19/1.79 ![X0]: (sQ70_spl <=> (~ssList(X0)|~app(nil,X0)=cons(sK1_skl,nil)|X0=cons(sK1_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1122,plain,(
% 10.19/1.79 ~sQ19_spl|~sQ14_spl|sQ70_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1099,f653,f636,f1119])).
% 10.19/1.79 fof(f1124,definition,(
% 10.19/1.79 ![X0]: (sQ71_spl <=> (~ssList(X0)|~app(X0,cons(sK1_skl,nil))=cons(sK1_skl,nil)|X0=nil))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1127,plain,(
% 10.19/1.79 ~sQ14_spl|~sQ19_spl|sQ71_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1101,f636,f653,f1124])).
% 10.19/1.79 fof(f1130,plain,(
% 10.19/1.79 ~ssList(cons(sK0_skl,cons(sK1_skl,nil)))|~ssItem(sK1_skl)|memberP(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),sK1_skl)|~ssList(cons(sK0_skl,nil))|~ssList(nil)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1070,f457])).
% 10.19/1.79 fof(f1133,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(cons(sK0_skl,nil))|~ssList(X0)|~app(cons(sK0_skl,nil),X0)=cons(sK0_skl,cons(sK1_skl,nil))|X0=cons(sK1_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1070,f378])).
% 10.19/1.79 fof(f1135,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(cons(sK1_skl,nil))|~ssList(X0)|~app(X0,cons(sK1_skl,nil))=cons(sK0_skl,cons(sK1_skl,nil))|X0=cons(sK0_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1070,f376])).
% 10.19/1.79 fof(f1144,definition,(
% 10.19/1.79 sQ74_spl <=> (ssList(cons(sK0_skl,cons(sK1_skl,nil))))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1147,definition,(
% 10.19/1.79 sQ75_spl <=> (memberP(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),sK1_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1150,plain,(
% 10.19/1.79 ~sQ74_spl|~sQ66_spl|sQ75_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1130,f1144,f1103,f1147,f639,f636])).
% 10.19/1.79 fof(f1156,definition,(
% 10.19/1.79 ![X0]: (sQ77_spl <=> (~ssList(X0)|~app(cons(sK0_skl,nil),X0)=cons(sK0_skl,cons(sK1_skl,nil))|X0=cons(sK1_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1159,plain,(
% 10.19/1.79 ~sQ19_spl|~sQ15_spl|sQ77_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1133,f653,f639,f1156])).
% 10.19/1.79 fof(f1161,definition,(
% 10.19/1.79 ![X0]: (sQ78_spl <=> (~ssList(X0)|~app(X0,cons(sK1_skl,nil))=cons(sK0_skl,cons(sK1_skl,nil))|X0=cons(sK0_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1164,plain,(
% 10.19/1.79 ~sQ15_spl|~sQ19_spl|sQ78_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1135,f639,f653,f1161])).
% 10.19/1.79 fof(f1167,plain,(
% 10.19/1.79 ~ssList(cons(sK1_skl,cons(sK1_skl,nil)))|~ssItem(sK1_skl)|memberP(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),sK1_skl)|~ssList(cons(sK1_skl,nil))|~ssList(nil)),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1071,f457])).
% 10.19/1.79 fof(f1170,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(cons(sK1_skl,nil))|~ssList(X0)|~app(cons(sK1_skl,nil),X0)=cons(sK1_skl,cons(sK1_skl,nil))|X0=cons(sK1_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1071,f378])).
% 10.19/1.79 fof(f1172,plain,(
% 10.19/1.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(cons(sK1_skl,nil))|~ssList(X0)|~app(X0,cons(sK1_skl,nil))=cons(sK1_skl,cons(sK1_skl,nil))|X0=cons(sK1_skl,nil))),
% 10.19/1.79 inference(paramodulation,[status(thm)],[f1071,f376])).
% 10.19/1.79 fof(f1181,definition,(
% 10.19/1.79 sQ81_spl <=> (ssList(cons(sK1_skl,cons(sK1_skl,nil))))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1184,definition,(
% 10.19/1.79 sQ82_spl <=> (memberP(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),sK1_skl))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 10.19/1.79 fof(f1187,plain,(
% 10.19/1.79 ~sQ81_spl|~sQ66_spl|sQ82_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.79 inference(split_clause,[status(thm)],[f1167,f1181,f1103,f1184,f653,f636])).
% 10.19/1.79 fof(f1193,definition,(
% 10.19/1.79 ![X0]: (sQ84_spl <=> (~ssList(X0)|~app(cons(sK1_skl,nil),X0)=cons(sK1_skl,cons(sK1_skl,nil))|X0=cons(sK1_skl,nil)))),
% 10.19/1.79 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1196,plain,(
% 10.19/1.80 ~sQ19_spl|sQ84_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1170,f653,f1193])).
% 10.19/1.80 fof(f1198,definition,(
% 10.19/1.80 ![X0]: (sQ85_spl <=> (~ssList(X0)|~app(X0,cons(sK1_skl,nil))=cons(sK1_skl,cons(sK1_skl,nil))|X0=cons(sK1_skl,nil)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1201,plain,(
% 10.19/1.80 ~sQ19_spl|sQ85_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1172,f653,f1198])).
% 10.19/1.80 fof(f1240,plain,(
% 10.19/1.80 $false|sQ66_spl),
% 10.19/1.80 inference(forward_subsumption_resolution,[status(thm)],[f1105,f104])).
% 10.19/1.80 fof(f1241,plain,(
% 10.19/1.80 sQ66_spl),
% 10.19/1.80 inference(contradiction_clause,[status(thm)],[f1240])).
% 10.19/1.80 fof(f1259,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f501,f461])).
% 10.19/1.80 fof(f1265,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK0_skl,cons(sK1_skl,nil)),X0))|~ssList(cons(sK1_skl,nil))|segmentP(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),X0),cons(sK1_skl,nil))|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1070,f461])).
% 10.19/1.80 fof(f1266,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK0_skl,sK47_skl),X0))|~ssList(sK47_skl)|segmentP(app(app(cons(sK0_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f529,f461])).
% 10.19/1.80 fof(f1267,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK0_skl,nil),X0))|~ssList(nil)|segmentP(app(app(cons(sK0_skl,nil),nil),X0),nil)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f555,f461])).
% 10.19/1.80 fof(f1268,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK0_skl,sK48_skl),X0))|~ssList(sK48_skl)|segmentP(app(app(cons(sK0_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f527,f461])).
% 10.19/1.80 fof(f1269,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK1_skl,cons(sK1_skl,nil)),X0))|~ssList(cons(sK1_skl,nil))|segmentP(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),X0),cons(sK1_skl,nil))|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1071,f461])).
% 10.19/1.80 fof(f1270,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK1_skl,sK47_skl),X0))|~ssList(sK47_skl)|segmentP(app(app(cons(sK1_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f528,f461])).
% 10.19/1.80 fof(f1271,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK1_skl,nil),X0))|~ssList(nil)|segmentP(app(app(cons(sK1_skl,nil),nil),X0),nil)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f554,f461])).
% 10.19/1.80 fof(f1272,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK1_skl,sK48_skl),X0))|~ssList(sK48_skl)|segmentP(app(app(cons(sK1_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f526,f461])).
% 10.19/1.80 fof(f1273,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f500,f461])).
% 10.19/1.80 fof(f1274,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK1_skl,nil),X0))|~ssList(cons(sK1_skl,nil))|segmentP(app(app(nil,cons(sK1_skl,nil)),X0),cons(sK1_skl,nil))|~ssList(nil)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1067,f461])).
% 10.19/1.80 fof(f1275,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f495,f461])).
% 10.19/1.80 fof(f1276,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f503,f461])).
% 10.19/1.80 fof(f1277,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f494,f461])).
% 10.19/1.80 fof(f1278,definition,(
% 10.19/1.80 ![X0]: (sQ93_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1281,plain,(
% 10.19/1.80 sQ93_spl|~sQ14_spl|~sQ28_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1259,f1278,f636,f707])).
% 10.19/1.80 fof(f1302,definition,(
% 10.19/1.80 ![X0]: (sQ99_spl <=> (~ssList(app(cons(sK0_skl,cons(sK1_skl,nil)),X0))|segmentP(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),X0),cons(sK1_skl,nil))|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1305,plain,(
% 10.19/1.80 sQ99_spl|~sQ19_spl|~sQ15_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1265,f1302,f653,f639])).
% 10.19/1.80 fof(f1306,definition,(
% 10.19/1.80 ![X0]: (sQ100_spl <=> (~ssList(app(cons(sK0_skl,sK47_skl),X0))|segmentP(app(app(cons(sK0_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1309,plain,(
% 10.19/1.80 sQ100_spl|~sQ28_spl|~sQ15_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1266,f1306,f707,f639])).
% 10.19/1.80 fof(f1310,definition,(
% 10.19/1.80 ![X0]: (sQ101_spl <=> (~ssList(app(cons(sK0_skl,nil),X0))|segmentP(app(app(cons(sK0_skl,nil),nil),X0),nil)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1313,plain,(
% 10.19/1.80 sQ101_spl|~sQ14_spl|~sQ15_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1267,f1310,f636,f639])).
% 10.19/1.80 fof(f1314,definition,(
% 10.19/1.80 ![X0]: (sQ102_spl <=> (~ssList(app(cons(sK0_skl,sK48_skl),X0))|segmentP(app(app(cons(sK0_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1317,plain,(
% 10.19/1.80 sQ102_spl|~sQ17_spl|~sQ15_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1268,f1314,f646,f639])).
% 10.19/1.80 fof(f1318,definition,(
% 10.19/1.80 ![X0]: (sQ103_spl <=> (~ssList(app(cons(sK1_skl,cons(sK1_skl,nil)),X0))|segmentP(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),X0),cons(sK1_skl,nil))|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1321,plain,(
% 10.19/1.80 sQ103_spl|~sQ19_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1269,f1318,f653])).
% 10.19/1.80 fof(f1322,definition,(
% 10.19/1.80 ![X0]: (sQ104_spl <=> (~ssList(app(cons(sK1_skl,sK47_skl),X0))|segmentP(app(app(cons(sK1_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1325,plain,(
% 10.19/1.80 sQ104_spl|~sQ28_spl|~sQ19_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1270,f1322,f707,f653])).
% 10.19/1.80 fof(f1326,definition,(
% 10.19/1.80 ![X0]: (sQ105_spl <=> (~ssList(app(cons(sK1_skl,nil),X0))|segmentP(app(app(cons(sK1_skl,nil),nil),X0),nil)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1329,plain,(
% 10.19/1.80 sQ105_spl|~sQ14_spl|~sQ19_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1271,f1326,f636,f653])).
% 10.19/1.80 fof(f1330,definition,(
% 10.19/1.80 ![X0]: (sQ106_spl <=> (~ssList(app(cons(sK1_skl,sK48_skl),X0))|segmentP(app(app(cons(sK1_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1333,plain,(
% 10.19/1.80 sQ106_spl|~sQ17_spl|~sQ19_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1272,f1330,f646,f653])).
% 10.19/1.80 fof(f1334,definition,(
% 10.19/1.80 ![X0]: (sQ107_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1337,plain,(
% 10.19/1.80 sQ107_spl|~sQ14_spl|~sQ17_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1273,f1334,f636,f646])).
% 10.19/1.80 fof(f1338,definition,(
% 10.19/1.80 ![X0]: (sQ108_spl <=> (~ssList(app(cons(sK1_skl,nil),X0))|segmentP(app(app(nil,cons(sK1_skl,nil)),X0),cons(sK1_skl,nil))|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1341,plain,(
% 10.19/1.80 sQ108_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1274,f1338,f653,f636])).
% 10.19/1.80 fof(f1342,definition,(
% 10.19/1.80 ![X0]: (sQ109_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1345,plain,(
% 10.19/1.80 sQ109_spl|~sQ28_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1275,f1342,f707,f636])).
% 10.19/1.80 fof(f1346,definition,(
% 10.19/1.80 ![X0]: (sQ110_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1349,plain,(
% 10.19/1.80 sQ110_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1276,f1346,f636])).
% 10.19/1.80 fof(f1350,definition,(
% 10.19/1.80 ![X0]: (sQ111_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1353,plain,(
% 10.19/1.80 sQ111_spl|~sQ17_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1277,f1350,f646,f636])).
% 10.19/1.80 fof(f1356,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|~leq(sK1_skl,X0)|~leq(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1070,f462])).
% 10.19/1.80 fof(f1357,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|~leq(sK1_skl,X0)|~leq(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1071,f462])).
% 10.19/1.80 fof(f1358,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|~leq(sK1_skl,X0)|~leq(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1067,f462])).
% 10.19/1.80 fof(f1367,definition,(
% 10.19/1.80 ![X0,X1]: (sQ114_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|~leq(sK1_skl,X0)|~leq(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1370,plain,(
% 10.19/1.80 sQ114_spl|~sQ66_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1356,f1367,f1103,f639,f636])).
% 10.19/1.80 fof(f1371,definition,(
% 10.19/1.80 ![X0,X1]: (sQ115_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|~leq(sK1_skl,X0)|~leq(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1374,plain,(
% 10.19/1.80 sQ115_spl|~sQ66_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1357,f1371,f1103,f653,f636])).
% 10.19/1.80 fof(f1375,definition,(
% 10.19/1.80 ![X0,X1]: (sQ116_spl <=> (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|~leq(sK1_skl,X0)|~leq(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1378,plain,(
% 10.19/1.80 sQ116_spl|~sQ66_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1358,f1375,f1103,f636])).
% 10.19/1.80 fof(f1415,plain,(
% 10.19/1.80 ![X0]: (~ssItem(X0)|cons(X0,cons(sK0_skl,nil))=app(cons(X0,nil),cons(sK0_skl,nil)))),
% 10.19/1.80 inference(resolution,[status(thm)],[f557,f380])).
% 10.19/1.80 fof(f1418,plain,(
% 10.19/1.80 app(nil,cons(sK0_skl,nil))=cons(sK0_skl,nil)),
% 10.19/1.80 inference(resolution,[status(thm)],[f557,f249])).
% 10.19/1.80 fof(f1422,plain,(
% 10.19/1.80 cons(sK0_skl,cons(sK0_skl,nil))=app(cons(sK0_skl,nil),cons(sK0_skl,nil))),
% 10.19/1.80 inference(resolution,[status(thm)],[f1415,f103])).
% 10.19/1.80 fof(f1423,plain,(
% 10.19/1.80 cons(sK1_skl,cons(sK0_skl,nil))=app(cons(sK1_skl,nil),cons(sK0_skl,nil))),
% 10.19/1.80 inference(resolution,[status(thm)],[f1415,f104])).
% 10.19/1.80 fof(f1425,plain,(
% 10.19/1.80 ~ssItem(sK0_skl)|~ssList(nil)|app(cons(sK0_skl,nil),nil)=sK47_skl|~cons(sK0_skl,nil)=sK48_skl),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f942])).
% 10.19/1.80 fof(f1426,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|~leq(sK0_skl,X0)|~leq(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f462])).
% 10.19/1.80 fof(f1427,plain,(
% 10.19/1.80 ~ssList(cons(sK0_skl,nil))|~ssItem(sK0_skl)|memberP(app(nil,cons(sK0_skl,nil)),sK0_skl)|~ssList(nil)|~ssList(nil)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f457])).
% 10.19/1.80 fof(f1428,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK0_skl,nil),X0))|~ssList(cons(sK0_skl,nil))|segmentP(app(app(nil,cons(sK0_skl,nil)),X0),cons(sK0_skl,nil))|~ssList(nil)|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f461])).
% 10.19/1.80 fof(f1431,plain,(
% 10.19/1.80 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X0)|~app(nil,X0)=cons(sK0_skl,nil)|X0=cons(sK0_skl,nil))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f378])).
% 10.19/1.80 fof(f1433,plain,(
% 10.19/1.80 ![X0]: (~ssList(nil)|~ssList(cons(sK0_skl,nil))|~ssList(X0)|~app(X0,cons(sK0_skl,nil))=cons(sK0_skl,nil)|X0=nil)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f376])).
% 10.19/1.80 fof(f1435,definition,(
% 10.19/1.80 sQ123_spl <=> (ssItem(sK0_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1437,plain,(
% 10.19/1.80 ~ssItem(sK0_skl)|sQ123_spl),
% 10.19/1.80 inference(component_clause,[status(thm)],[f1435])).
% 10.19/1.80 fof(f1438,definition,(
% 10.19/1.80 sQ124_spl <=> (app(cons(sK0_skl,nil),nil)=sK47_skl)),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1441,definition,(
% 10.19/1.80 sQ125_spl <=> (cons(sK0_skl,nil)=sK48_skl)),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1444,plain,(
% 10.19/1.80 ~sQ123_spl|~sQ14_spl|sQ124_spl|~sQ125_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1425,f1435,f636,f1438,f1441])).
% 10.19/1.80 fof(f1445,definition,(
% 10.19/1.80 ![X0,X1]: (sQ126_spl <=> (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|~leq(sK0_skl,X0)|~leq(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1448,plain,(
% 10.19/1.80 sQ126_spl|~sQ123_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1426,f1445,f1435,f636])).
% 10.19/1.80 fof(f1449,definition,(
% 10.19/1.80 sQ127_spl <=> (memberP(app(nil,cons(sK0_skl,nil)),sK0_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1452,plain,(
% 10.19/1.80 ~sQ15_spl|~sQ123_spl|sQ127_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1427,f639,f1435,f1449,f636])).
% 10.19/1.80 fof(f1453,definition,(
% 10.19/1.80 ![X0]: (sQ128_spl <=> (~ssList(app(cons(sK0_skl,nil),X0))|segmentP(app(app(nil,cons(sK0_skl,nil)),X0),cons(sK0_skl,nil))|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1456,plain,(
% 10.19/1.80 sQ128_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1428,f1453,f639,f636])).
% 10.19/1.80 fof(f1459,definition,(
% 10.19/1.80 ![X0]: (sQ129_spl <=> (~ssList(X0)|~app(nil,X0)=cons(sK0_skl,nil)|X0=cons(sK0_skl,nil)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1462,plain,(
% 10.19/1.80 ~sQ15_spl|~sQ14_spl|sQ129_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1431,f639,f636,f1459])).
% 10.19/1.80 fof(f1464,definition,(
% 10.19/1.80 ![X0]: (sQ130_spl <=> (~ssList(X0)|~app(X0,cons(sK0_skl,nil))=cons(sK0_skl,nil)|X0=nil))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1467,plain,(
% 10.19/1.80 ~sQ14_spl|~sQ15_spl|sQ130_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1433,f636,f639,f1464])).
% 10.19/1.80 fof(f1470,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|~leq(sK0_skl,X0)|~leq(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f462])).
% 10.19/1.80 fof(f1471,plain,(
% 10.19/1.80 ~ssList(cons(sK0_skl,cons(sK0_skl,nil)))|~ssItem(sK0_skl)|memberP(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),sK0_skl)|~ssList(cons(sK0_skl,nil))|~ssList(nil)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f457])).
% 10.19/1.80 fof(f1472,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK0_skl,cons(sK0_skl,nil)),X0))|~ssList(cons(sK0_skl,nil))|segmentP(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),X0),cons(sK0_skl,nil))|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f461])).
% 10.19/1.80 fof(f1475,plain,(
% 10.19/1.80 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(cons(sK0_skl,nil))|~ssList(X0)|~app(cons(sK0_skl,nil),X0)=cons(sK0_skl,cons(sK0_skl,nil))|X0=cons(sK0_skl,nil))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f378])).
% 10.19/1.80 fof(f1477,plain,(
% 10.19/1.80 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(cons(sK0_skl,nil))|~ssList(X0)|~app(X0,cons(sK0_skl,nil))=cons(sK0_skl,cons(sK0_skl,nil))|X0=cons(sK0_skl,nil))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f376])).
% 10.19/1.80 fof(f1486,definition,(
% 10.19/1.80 ![X0,X1]: (sQ133_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|~leq(sK0_skl,X0)|~leq(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1489,plain,(
% 10.19/1.80 sQ133_spl|~sQ123_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1470,f1486,f1435,f639,f636])).
% 10.19/1.80 fof(f1490,definition,(
% 10.19/1.80 sQ134_spl <=> (ssList(cons(sK0_skl,cons(sK0_skl,nil))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1493,definition,(
% 10.19/1.80 sQ135_spl <=> (memberP(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),sK0_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1496,plain,(
% 10.19/1.80 ~sQ134_spl|~sQ123_spl|sQ135_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1471,f1490,f1435,f1493,f639,f636])).
% 10.19/1.80 fof(f1497,definition,(
% 10.19/1.80 ![X0]: (sQ136_spl <=> (~ssList(app(cons(sK0_skl,cons(sK0_skl,nil)),X0))|segmentP(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),X0),cons(sK0_skl,nil))|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1500,plain,(
% 10.19/1.80 sQ136_spl|~sQ15_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1472,f1497,f639])).
% 10.19/1.80 fof(f1506,definition,(
% 10.19/1.80 ![X0]: (sQ138_spl <=> (~ssList(X0)|~app(cons(sK0_skl,nil),X0)=cons(sK0_skl,cons(sK0_skl,nil))|X0=cons(sK0_skl,nil)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1509,plain,(
% 10.19/1.80 ~sQ15_spl|sQ138_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1475,f639,f1506])).
% 10.19/1.80 fof(f1511,definition,(
% 10.19/1.80 ![X0]: (sQ139_spl <=> (~ssList(X0)|~app(X0,cons(sK0_skl,nil))=cons(sK0_skl,cons(sK0_skl,nil))|X0=cons(sK0_skl,nil)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1514,plain,(
% 10.19/1.80 ~sQ15_spl|sQ139_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1477,f639,f1511])).
% 10.19/1.80 fof(f1517,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|~leq(sK0_skl,X0)|~leq(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f462])).
% 10.19/1.80 fof(f1518,plain,(
% 10.19/1.80 ~ssList(cons(sK1_skl,cons(sK0_skl,nil)))|~ssItem(sK0_skl)|memberP(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),sK0_skl)|~ssList(cons(sK1_skl,nil))|~ssList(nil)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f457])).
% 10.19/1.80 fof(f1519,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(cons(sK1_skl,cons(sK0_skl,nil)),X0))|~ssList(cons(sK0_skl,nil))|segmentP(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),X0),cons(sK0_skl,nil))|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f461])).
% 10.19/1.80 fof(f1522,plain,(
% 10.19/1.80 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(cons(sK1_skl,nil))|~ssList(X0)|~app(cons(sK1_skl,nil),X0)=cons(sK1_skl,cons(sK0_skl,nil))|X0=cons(sK0_skl,nil))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f378])).
% 10.19/1.80 fof(f1524,plain,(
% 10.19/1.80 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(cons(sK0_skl,nil))|~ssList(X0)|~app(X0,cons(sK0_skl,nil))=cons(sK1_skl,cons(sK0_skl,nil))|X0=cons(sK1_skl,nil))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f376])).
% 10.19/1.80 fof(f1533,definition,(
% 10.19/1.80 ![X0,X1]: (sQ142_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~cyclefreeP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|~leq(sK0_skl,X0)|~leq(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1536,plain,(
% 10.19/1.80 sQ142_spl|~sQ123_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1517,f1533,f1435,f653,f636])).
% 10.19/1.80 fof(f1537,definition,(
% 10.19/1.80 sQ143_spl <=> (ssList(cons(sK1_skl,cons(sK0_skl,nil))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1540,definition,(
% 10.19/1.80 sQ144_spl <=> (memberP(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),sK0_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1543,plain,(
% 10.19/1.80 ~sQ143_spl|~sQ123_spl|sQ144_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1518,f1537,f1435,f1540,f653,f636])).
% 10.19/1.80 fof(f1544,definition,(
% 10.19/1.80 ![X0]: (sQ145_spl <=> (~ssList(app(cons(sK1_skl,cons(sK0_skl,nil)),X0))|segmentP(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),X0),cons(sK0_skl,nil))|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1547,plain,(
% 10.19/1.80 sQ145_spl|~sQ15_spl|~sQ19_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1519,f1544,f639,f653])).
% 10.19/1.80 fof(f1553,definition,(
% 10.19/1.80 ![X0]: (sQ147_spl <=> (~ssList(X0)|~app(cons(sK1_skl,nil),X0)=cons(sK1_skl,cons(sK0_skl,nil))|X0=cons(sK0_skl,nil)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1556,plain,(
% 10.19/1.80 ~sQ15_spl|~sQ19_spl|sQ147_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1522,f639,f653,f1553])).
% 10.19/1.80 fof(f1558,definition,(
% 10.19/1.80 ![X0]: (sQ148_spl <=> (~ssList(X0)|~app(X0,cons(sK0_skl,nil))=cons(sK1_skl,cons(sK0_skl,nil))|X0=cons(sK1_skl,nil)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1561,plain,(
% 10.19/1.80 ~sQ19_spl|~sQ15_spl|sQ148_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1524,f653,f639,f1558])).
% 10.19/1.80 fof(f1563,plain,(
% 10.19/1.80 $false|sQ123_spl),
% 10.19/1.80 inference(forward_subsumption_resolution,[status(thm)],[f1437,f103])).
% 10.19/1.80 fof(f1564,plain,(
% 10.19/1.80 sQ123_spl),
% 10.19/1.80 inference(contradiction_clause,[status(thm)],[f1563])).
% 10.19/1.80 fof(f1832,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK0_skl,X0)|leq(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f463])).
% 10.19/1.80 fof(f1833,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK1_skl,X0)|leq(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1070,f463])).
% 10.19/1.80 fof(f1834,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK0_skl,X0)|leq(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f463])).
% 10.19/1.80 fof(f1835,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK1_skl,X0)|leq(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1071,f463])).
% 10.19/1.80 fof(f1836,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|leq(sK0_skl,X0)|leq(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f463])).
% 10.19/1.80 fof(f1837,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|leq(sK1_skl,X0)|leq(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1067,f463])).
% 10.19/1.80 fof(f1850,definition,(
% 10.19/1.80 ![X0,X1]: (sQ206_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK0_skl,X0)|leq(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1853,plain,(
% 10.19/1.80 sQ206_spl|~sQ123_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1832,f1850,f1435,f639,f636])).
% 10.19/1.80 fof(f1854,definition,(
% 10.19/1.80 ![X0,X1]: (sQ207_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK1_skl,X0)|leq(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1857,plain,(
% 10.19/1.80 sQ207_spl|~sQ66_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1833,f1854,f1103,f639,f636])).
% 10.19/1.80 fof(f1858,definition,(
% 10.19/1.80 ![X0,X1]: (sQ208_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK0_skl,X0)|leq(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1861,plain,(
% 10.19/1.80 sQ208_spl|~sQ123_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1834,f1858,f1435,f653,f636])).
% 10.19/1.80 fof(f1862,definition,(
% 10.19/1.80 ![X0,X1]: (sQ209_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK1_skl,X0)|leq(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1865,plain,(
% 10.19/1.80 sQ209_spl|~sQ66_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1835,f1862,f1103,f653,f636])).
% 10.19/1.80 fof(f1866,definition,(
% 10.19/1.80 ![X0,X1]: (sQ210_spl <=> (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK0_skl,X0)|leq(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1869,plain,(
% 10.19/1.80 sQ210_spl|~sQ123_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1836,f1866,f1435,f636])).
% 10.19/1.80 fof(f1870,definition,(
% 10.19/1.80 ![X0,X1]: (sQ211_spl <=> (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK1_skl,X0)|leq(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f1873,plain,(
% 10.19/1.80 sQ211_spl|~sQ66_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f1837,f1870,f1103,f636])).
% 10.19/1.80 fof(f2071,plain,(
% 10.19/1.80 ![X0,X1]: (sP0_prd(X0,app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),cons(X0,nil)),X1)|~ssItem(X0)|app(cons(X0,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X1|~sQ2_spl)),
% 10.19/1.80 inference(resolution,[status(thm)],[f686,f485])).
% 10.19/1.80 fof(f2072,plain,(
% 10.19/1.80 ![X0]: (~ssItem(X0)|cons(X0,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=app(cons(X0,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))|~sQ2_spl)),
% 10.19/1.80 inference(resolution,[status(thm)],[f686,f380])).
% 10.19/1.80 fof(f2204,plain,(
% 10.19/1.80 ![X0]: (sP0_prd(sK51_skl,app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),cons(sK51_skl,nil)),X0)|app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|~sQ2_spl)),
% 10.19/1.80 inference(resolution,[status(thm)],[f2071,f518])).
% 10.19/1.80 fof(f2205,plain,(
% 10.19/1.80 ![X0]: (sP0_prd(sK51_skl,sK48_skl,X0)|app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|~sQ2_spl)),
% 10.19/1.80 inference(forward_demodulation,[status(thm)],[f517,f2204])).
% 10.19/1.80 fof(f2208,plain,(
% 10.19/1.80 cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))|~sQ2_spl),
% 10.19/1.80 inference(resolution,[status(thm)],[f2072,f518])).
% 10.19/1.80 fof(f2625,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|lt(sK0_skl,X0)|lt(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f464])).
% 10.19/1.80 fof(f2626,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|lt(sK1_skl,X0)|lt(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1070,f464])).
% 10.19/1.80 fof(f2627,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|lt(sK0_skl,X0)|lt(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f464])).
% 10.19/1.80 fof(f2628,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|lt(sK1_skl,X0)|lt(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1071,f464])).
% 10.19/1.80 fof(f2629,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|lt(sK0_skl,X0)|lt(X0,sK0_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f464])).
% 10.19/1.80 fof(f2630,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|lt(sK1_skl,X0)|lt(X0,sK1_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1067,f464])).
% 10.19/1.80 fof(f2643,definition,(
% 10.19/1.80 ![X0,X1]: (sQ339_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|lt(sK0_skl,X0)|lt(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2646,plain,(
% 10.19/1.80 sQ339_spl|~sQ123_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2625,f2643,f1435,f639,f636])).
% 10.19/1.80 fof(f2647,definition,(
% 10.19/1.80 ![X0,X1]: (sQ340_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|lt(sK1_skl,X0)|lt(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2650,plain,(
% 10.19/1.80 sQ340_spl|~sQ66_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2626,f2647,f1103,f639,f636])).
% 10.19/1.80 fof(f2651,definition,(
% 10.19/1.80 ![X0,X1]: (sQ341_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|lt(sK0_skl,X0)|lt(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2654,plain,(
% 10.19/1.80 sQ341_spl|~sQ123_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2627,f2651,f1435,f653,f636])).
% 10.19/1.80 fof(f2655,definition,(
% 10.19/1.80 ![X0,X1]: (sQ342_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|lt(sK1_skl,X0)|lt(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2658,plain,(
% 10.19/1.80 sQ342_spl|~sQ66_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2628,f2655,f1103,f653,f636])).
% 10.19/1.80 fof(f2659,definition,(
% 10.19/1.80 ![X0,X1]: (sQ343_spl <=> (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|lt(sK0_skl,X0)|lt(X0,sK0_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2662,plain,(
% 10.19/1.80 sQ343_spl|~sQ123_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2629,f2659,f1435,f636])).
% 10.19/1.80 fof(f2663,definition,(
% 10.19/1.80 ![X0,X1]: (sQ344_spl <=> (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~strictorderP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|lt(sK1_skl,X0)|lt(X0,sK1_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2666,plain,(
% 10.19/1.80 sQ344_spl|~sQ66_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2630,f2663,f1103,f636])).
% 10.19/1.80 fof(f2811,plain,(
% 10.19/1.80 ![X0]: (app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|ssList(sK52_skl(sK51_skl,sK48_skl,X0))|~sQ2_spl)),
% 10.19/1.80 inference(resolution,[status(thm)],[f2205,f433])).
% 10.19/1.80 fof(f2812,plain,(
% 10.19/1.80 ![X0]: (app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|app(sK52_skl(sK51_skl,sK48_skl,X0),cons(sK51_skl,nil))=sK48_skl|~sQ2_spl)),
% 10.19/1.80 inference(resolution,[status(thm)],[f2205,f434])).
% 10.19/1.80 fof(f2878,plain,(
% 10.19/1.80 ~sP0_prd(sK51_skl,sK48_skl,sK47_skl)|~cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=sK47_skl|~sQ2_spl),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f2208,f435])).
% 10.19/1.80 fof(f2886,definition,(
% 10.19/1.80 sQ374_spl <=> (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=sK47_skl)),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f2889,plain,(
% 10.19/1.80 ~sQ2_spl|~sQ374_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f2878,f444,f2886])).
% 10.19/1.80 fof(f2914,plain,(
% 10.19/1.80 app(app(sK48_skl,sK47_skl),sK47_skl)=app(sK48_skl,app(sK47_skl,sK47_skl))),
% 10.19/1.80 inference(resolution,[status(thm)],[f899,f420])).
% 10.19/1.80 fof(f3370,definition,(
% 10.19/1.80 sQ458_spl <=> (ssList(app(sK47_skl,sK48_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ458_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f3410,definition,(
% 10.19/1.80 sQ466_spl <=> (ssList(app(sK48_skl,sK48_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f3555,plain,(
% 10.19/1.80 app(app(sK47_skl,sK48_skl),sK48_skl)=app(sK47_skl,app(sK48_skl,sK48_skl))),
% 10.19/1.80 inference(resolution,[status(thm)],[f901,f419])).
% 10.19/1.80 fof(f3556,plain,(
% 10.19/1.80 app(app(sK48_skl,sK48_skl),sK48_skl)=app(sK48_skl,app(sK48_skl,sK48_skl))),
% 10.19/1.80 inference(resolution,[status(thm)],[f901,f420])).
% 10.19/1.80 fof(f3679,plain,(
% 10.19/1.80 ![X0]: (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|ssList(sK52_skl(sK51_skl,sK48_skl,X0))|~sQ2_spl)),
% 10.19/1.80 inference(forward_demodulation,[status(thm)],[f2208,f2811])).
% 10.19/1.80 fof(f3726,plain,(
% 10.19/1.80 ![X0]: (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|app(sK52_skl(sK51_skl,sK48_skl,X0),cons(sK51_skl,nil))=sK48_skl|~sQ2_spl)),
% 10.19/1.80 inference(forward_demodulation,[status(thm)],[f2208,f2812])).
% 10.19/1.80 fof(f3727,plain,(
% 10.19/1.80 ![X0]: (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|~ssItem(sK51_skl)|~ssList(sK52_skl(sK51_skl,sK48_skl,X0))|app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,X0))=sK47_skl|~sQ2_spl)),
% 10.19/1.80 inference(resolution,[status(thm)],[f3726,f942])).
% 10.19/1.80 fof(f3742,definition,(
% 10.19/1.80 ![X0]: (sQ499_spl <=> (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|~ssList(sK52_skl(sK51_skl,sK48_skl,X0))|app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,X0))=sK47_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ499_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f3743,plain,(
% 10.19/1.80 ![X0]: (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|~ssList(sK52_skl(sK51_skl,sK48_skl,X0))|app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,X0))=sK47_skl|~sQ499_spl)),
% 10.19/1.80 inference(component_clause,[status(thm)],[f3742])).
% 10.19/1.80 fof(f3745,plain,(
% 10.19/1.80 sQ499_spl|~sQ7_spl|~sQ2_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f3727,f3742,f538,f444])).
% 10.19/1.80 fof(f3787,plain,(
% 10.19/1.80 ![X0]: (cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=X0|app(cons(sK51_skl,nil),sK52_skl(sK51_skl,sK48_skl,X0))=sK47_skl|~sQ2_spl|~sQ499_spl)),
% 10.19/1.80 inference(forward_subsumption_resolution,[status(thm)],[f3743,f3679])).
% 10.19/1.80 fof(f4003,plain,(
% 10.19/1.80 ~ssList(app(sK48_skl,app(sK47_skl,sK47_skl)))|~ssList(sK47_skl)|segmentP(app(app(sK48_skl,sK47_skl),sK47_skl),sK47_skl)|~ssList(sK48_skl)|~ssList(sK47_skl)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f2914,f461])).
% 10.19/1.80 fof(f4011,definition,(
% 10.19/1.80 sQ540_spl <=> (ssList(app(sK48_skl,app(sK47_skl,sK47_skl))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ540_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4014,definition,(
% 10.19/1.80 sQ541_spl <=> (segmentP(app(app(sK48_skl,sK47_skl),sK47_skl),sK47_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4017,plain,(
% 10.19/1.80 ~sQ540_spl|~sQ28_spl|sQ541_spl|~sQ17_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4003,f4011,f707,f4014,f646])).
% 10.19/1.80 fof(f4520,plain,(
% 10.19/1.80 ~ssList(app(sK47_skl,app(sK48_skl,sK48_skl)))|~ssList(sK48_skl)|segmentP(app(app(sK47_skl,sK48_skl),sK48_skl),sK48_skl)|~ssList(sK47_skl)|~ssList(sK48_skl)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3555,f461])).
% 10.19/1.80 fof(f4521,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(app(sK47_skl,app(sK48_skl,sK48_skl)),X0))|~ssList(sK48_skl)|segmentP(app(app(app(sK47_skl,sK48_skl),sK48_skl),X0),sK48_skl)|~ssList(app(sK47_skl,sK48_skl))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3555,f461])).
% 10.19/1.80 fof(f4523,plain,(
% 10.19/1.80 ~ssList(app(sK47_skl,sK48_skl))|~ssList(sK48_skl)|~nil=app(sK47_skl,app(sK48_skl,sK48_skl))|nil=sK48_skl),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3555,f385])).
% 10.19/1.80 fof(f4524,plain,(
% 10.19/1.80 ![X0]: (~ssList(sK48_skl)|~ssList(app(sK47_skl,sK48_skl))|~ssList(X0)|~app(app(sK47_skl,sK48_skl),X0)=app(sK47_skl,app(sK48_skl,sK48_skl))|X0=sK48_skl)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3555,f378])).
% 10.19/1.80 fof(f4526,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(sK47_skl,sK48_skl))|~ssList(sK48_skl)|~ssList(X0)|~app(X0,sK48_skl)=app(sK47_skl,app(sK48_skl,sK48_skl))|X0=app(sK47_skl,sK48_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3555,f376])).
% 10.19/1.80 fof(f4528,definition,(
% 10.19/1.80 sQ627_spl <=> (ssList(app(sK47_skl,app(sK48_skl,sK48_skl))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4531,definition,(
% 10.19/1.80 sQ628_spl <=> (segmentP(app(app(sK47_skl,sK48_skl),sK48_skl),sK48_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4534,plain,(
% 10.19/1.80 ~sQ627_spl|~sQ17_spl|sQ628_spl|~sQ28_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4520,f4528,f646,f4531,f707])).
% 10.19/1.80 fof(f4535,definition,(
% 10.19/1.80 ![X0]: (sQ629_spl <=> (~ssList(app(app(sK47_skl,app(sK48_skl,sK48_skl)),X0))|segmentP(app(app(app(sK47_skl,sK48_skl),sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4538,plain,(
% 10.19/1.80 sQ629_spl|~sQ17_spl|~sQ458_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4521,f4535,f646,f3370])).
% 10.19/1.80 fof(f4539,definition,(
% 10.19/1.80 sQ630_spl <=> (nil=app(sK47_skl,app(sK48_skl,sK48_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ630_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4543,plain,(
% 10.19/1.80 ~sQ458_spl|~sQ17_spl|~sQ630_spl|sQ3_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4523,f3370,f646,f4539,f447])).
% 10.19/1.80 fof(f4544,definition,(
% 10.19/1.80 ![X0]: (sQ631_spl <=> (~ssList(X0)|~app(app(sK47_skl,sK48_skl),X0)=app(sK47_skl,app(sK48_skl,sK48_skl))|X0=sK48_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4547,plain,(
% 10.19/1.80 ~sQ17_spl|~sQ458_spl|sQ631_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4524,f646,f3370,f4544])).
% 10.19/1.80 fof(f4549,definition,(
% 10.19/1.80 ![X0]: (sQ632_spl <=> (~ssList(X0)|~app(X0,sK48_skl)=app(sK47_skl,app(sK48_skl,sK48_skl))|X0=app(sK47_skl,sK48_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4552,plain,(
% 10.19/1.80 ~sQ458_spl|~sQ17_spl|sQ632_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4526,f3370,f646,f4549])).
% 10.19/1.80 fof(f4554,plain,(
% 10.19/1.80 ~ssList(app(sK48_skl,app(sK48_skl,sK48_skl)))|~ssList(sK48_skl)|segmentP(app(app(sK48_skl,sK48_skl),sK48_skl),sK48_skl)|~ssList(sK48_skl)|~ssList(sK48_skl)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3556,f461])).
% 10.19/1.80 fof(f4555,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(app(sK48_skl,app(sK48_skl,sK48_skl)),X0))|~ssList(sK48_skl)|segmentP(app(app(app(sK48_skl,sK48_skl),sK48_skl),X0),sK48_skl)|~ssList(app(sK48_skl,sK48_skl))|~ssList(X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3556,f461])).
% 10.19/1.80 fof(f4557,plain,(
% 10.19/1.80 ~ssList(app(sK48_skl,sK48_skl))|~ssList(sK48_skl)|~nil=app(sK48_skl,app(sK48_skl,sK48_skl))|nil=sK48_skl),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3556,f385])).
% 10.19/1.80 fof(f4558,plain,(
% 10.19/1.80 ![X0]: (~ssList(sK48_skl)|~ssList(app(sK48_skl,sK48_skl))|~ssList(X0)|~app(app(sK48_skl,sK48_skl),X0)=app(sK48_skl,app(sK48_skl,sK48_skl))|X0=sK48_skl)),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3556,f378])).
% 10.19/1.80 fof(f4560,plain,(
% 10.19/1.80 ![X0]: (~ssList(app(sK48_skl,sK48_skl))|~ssList(sK48_skl)|~ssList(X0)|~app(X0,sK48_skl)=app(sK48_skl,app(sK48_skl,sK48_skl))|X0=app(sK48_skl,sK48_skl))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f3556,f376])).
% 10.19/1.80 fof(f4562,definition,(
% 10.19/1.80 sQ633_spl <=> (ssList(app(sK48_skl,app(sK48_skl,sK48_skl))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4565,definition,(
% 10.19/1.80 sQ634_spl <=> (segmentP(app(app(sK48_skl,sK48_skl),sK48_skl),sK48_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ634_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4568,plain,(
% 10.19/1.80 ~sQ633_spl|~sQ17_spl|sQ634_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4554,f4562,f646,f4565])).
% 10.19/1.80 fof(f4569,definition,(
% 10.19/1.80 ![X0]: (sQ635_spl <=> (~ssList(app(app(sK48_skl,app(sK48_skl,sK48_skl)),X0))|segmentP(app(app(app(sK48_skl,sK48_skl),sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ635_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4572,plain,(
% 10.19/1.80 sQ635_spl|~sQ17_spl|~sQ466_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4555,f4569,f646,f3410])).
% 10.19/1.80 fof(f4573,definition,(
% 10.19/1.80 sQ636_spl <=> (nil=app(sK48_skl,app(sK48_skl,sK48_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4577,plain,(
% 10.19/1.80 ~sQ466_spl|~sQ17_spl|~sQ636_spl|sQ3_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4557,f3410,f646,f4573,f447])).
% 10.19/1.80 fof(f4578,definition,(
% 10.19/1.80 ![X0]: (sQ637_spl <=> (~ssList(X0)|~app(app(sK48_skl,sK48_skl),X0)=app(sK48_skl,app(sK48_skl,sK48_skl))|X0=sK48_skl))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4581,plain,(
% 10.19/1.80 ~sQ17_spl|~sQ466_spl|sQ637_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4558,f646,f3410,f4578])).
% 10.19/1.80 fof(f4583,definition,(
% 10.19/1.80 ![X0]: (sQ638_spl <=> (~ssList(X0)|~app(X0,sK48_skl)=app(sK48_skl,app(sK48_skl,sK48_skl))|X0=app(sK48_skl,sK48_skl)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4586,plain,(
% 10.19/1.80 ~sQ466_spl|~sQ17_spl|sQ638_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4560,f3410,f646,f4583])).
% 10.19/1.80 fof(f4690,plain,(
% 10.19/1.80 ~ssList(cons(sK0_skl,nil))|cons(sK4_skl(cons(sK0_skl,nil)),nil)=cons(sK0_skl,nil)),
% 10.19/1.80 inference(resolution,[status(thm)],[f926,f117])).
% 10.19/1.80 fof(f4691,plain,(
% 10.19/1.80 ~ssList(cons(sK0_skl,nil))|ssItem(sK4_skl(cons(sK0_skl,nil)))),
% 10.19/1.80 inference(resolution,[status(thm)],[f926,f116])).
% 10.19/1.80 fof(f4692,definition,(
% 10.19/1.80 sQ657_spl <=> (cons(sK4_skl(cons(sK0_skl,nil)),nil)=cons(sK0_skl,nil))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4695,plain,(
% 10.19/1.80 ~sQ15_spl|sQ657_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4690,f639,f4692])).
% 10.19/1.80 fof(f4696,definition,(
% 10.19/1.80 sQ658_spl <=> (ssItem(sK4_skl(cons(sK0_skl,nil))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4699,plain,(
% 10.19/1.80 ~sQ15_spl|sQ658_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4691,f639,f4696])).
% 10.19/1.80 fof(f4700,plain,(
% 10.19/1.80 ~ssList(cons(sK1_skl,nil))|cons(sK4_skl(cons(sK1_skl,nil)),nil)=cons(sK1_skl,nil)),
% 10.19/1.80 inference(resolution,[status(thm)],[f927,f117])).
% 10.19/1.80 fof(f4701,plain,(
% 10.19/1.80 ~ssList(cons(sK1_skl,nil))|ssItem(sK4_skl(cons(sK1_skl,nil)))),
% 10.19/1.80 inference(resolution,[status(thm)],[f927,f116])).
% 10.19/1.80 fof(f4702,definition,(
% 10.19/1.80 sQ659_spl <=> (cons(sK4_skl(cons(sK1_skl,nil)),nil)=cons(sK1_skl,nil))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4705,plain,(
% 10.19/1.80 ~sQ19_spl|sQ659_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4700,f653,f4702])).
% 10.19/1.80 fof(f4706,definition,(
% 10.19/1.80 sQ660_spl <=> (ssItem(sK4_skl(cons(sK1_skl,nil))))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ660_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f4709,plain,(
% 10.19/1.80 ~sQ19_spl|sQ660_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f4701,f653,f4706])).
% 10.19/1.80 fof(f5128,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK0_skl,X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1422,f465])).
% 10.19/1.80 fof(f5129,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK1_skl,X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1070,f465])).
% 10.19/1.80 fof(f5130,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK0_skl,X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1423,f465])).
% 10.19/1.80 fof(f5131,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~ssList(X1)|leq(sK1_skl,X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1071,f465])).
% 10.19/1.80 fof(f5132,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(sK0_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|leq(sK0_skl,X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1418,f465])).
% 10.19/1.80 fof(f5133,plain,(
% 10.19/1.80 ![X0,X1]: (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(sK1_skl)|~ssItem(X0)|~ssList(nil)|~ssList(nil)|~ssList(X1)|leq(sK1_skl,X0))),
% 10.19/1.80 inference(paramodulation,[status(thm)],[f1067,f465])).
% 10.19/1.80 fof(f5158,definition,(
% 10.19/1.80 ![X0,X1]: (sQ733_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK0_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK0_skl,X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ733_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f5161,plain,(
% 10.19/1.80 sQ733_spl|~sQ123_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5128,f5158,f1435,f639,f636])).
% 10.19/1.80 fof(f5162,definition,(
% 10.19/1.80 ![X0,X1]: (sQ734_spl <=> (~ssList(app(app(cons(sK0_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK0_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK1_skl,X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f5165,plain,(
% 10.19/1.80 sQ734_spl|~sQ66_spl|~sQ15_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5129,f5162,f1103,f639,f636])).
% 10.19/1.80 fof(f5166,definition,(
% 10.19/1.80 ![X0,X1]: (sQ735_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK1_skl,cons(sK0_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK0_skl,X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ735_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f5169,plain,(
% 10.19/1.80 sQ735_spl|~sQ123_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5130,f5166,f1435,f653,f636])).
% 10.19/1.80 fof(f5170,definition,(
% 10.19/1.80 ![X0,X1]: (sQ736_spl <=> (~ssList(app(app(cons(sK1_skl,nil),cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK1_skl,cons(sK1_skl,nil)),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK1_skl,X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ736_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f5173,plain,(
% 10.19/1.80 sQ736_spl|~sQ66_spl|~sQ19_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5131,f5170,f1103,f653,f636])).
% 10.19/1.80 fof(f5174,definition,(
% 10.19/1.80 ![X0,X1]: (sQ737_spl <=> (~ssList(app(app(nil,cons(sK0_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK0_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK0_skl,X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ737_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f5177,plain,(
% 10.19/1.80 sQ737_spl|~sQ123_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5132,f5174,f1435,f636])).
% 10.19/1.80 fof(f5178,definition,(
% 10.19/1.80 ![X0,X1]: (sQ738_spl <=> (~ssList(app(app(nil,cons(sK1_skl,nil)),cons(X0,X1)))|~totalorderedP(app(cons(sK1_skl,nil),cons(X0,X1)))|~ssItem(X0)|~ssList(X1)|leq(sK1_skl,X0)))),
% 10.19/1.80 introduced(definition,[new_symbols(definition,[sQ738_spl])],[split_symbol_definition])).
% 10.19/1.80 fof(f5181,plain,(
% 10.19/1.80 sQ738_spl|~sQ66_spl|~sQ14_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5133,f5178,f1103,f636])).
% 10.19/1.80 fof(f5411,plain,(
% 10.19/1.80 cons(sK51_skl,sK52_skl(sK51_skl,sK48_skl,sK47_skl))=sK47_skl|~sP0_prd(sK51_skl,sK48_skl,sK47_skl)|~sQ2_spl|~sQ499_spl),
% 10.19/1.80 inference(resolution,[status(thm)],[f3787,f435])).
% 10.19/1.80 fof(f5422,plain,(
% 10.19/1.80 sQ374_spl|~sQ2_spl|~sQ499_spl),
% 10.19/1.80 inference(split_clause,[status(thm)],[f5411,f2886,f444,f3742])).
% 10.19/1.80 fof(f5443,plain,(
% 10.19/1.80 $false|~sQ2_spl|sQ7_spl),
% 10.19/1.80 inference(forward_subsumption_resolution,[status(thm)],[f540,f518])).
% 10.19/1.80 fof(f5444,plain,(
% 10.19/1.80 ~sQ2_spl|sQ7_spl),
% 10.19/1.80 inference(contradiction_clause,[status(thm)],[f5443])).
% 10.19/1.80 fof(f5445,plain,(
% 10.19/1.80 $false),
% 10.19/1.80 inference(sat_refutation,[status(thm)],[f443,f450,f454,f515,f562,f574,f579,f604,f607,f642,f649,f656,f660,f664,f668,f672,f685,f730,f737,f764,f771,f778,f785,f826,f846,f850,f854,f858,f862,f866,f870,f874,f878,f882,f951,f971,f989,f1001,f1112,f1116,f1122,f1127,f1150,f1159,f1164,f1187,f1196,f1201,f1241,f1281,f1305,f1309,f1313,f1317,f1321,f1325,f1329,f1333,f1337,f1341,f1345,f1349,f1353,f1370,f1374,f1378,f1444,f1448,f1452,f1456,f1462,f1467,f1489,f1496,f1500,f1509,f1514,f1536,f1543,f1547,f1556,f1561,f1564,f1853,f1857,f1861,f1865,f1869,f1873,f2646,f2650,f2654,f2658,f2662,f2666,f2889,f3745,f4017,f4534,f4538,f4543,f4547,f4552,f4568,f4572,f4577,f4581,f4586,f4695,f4699,f4705,f4709,f5161,f5165,f5169,f5173,f5177,f5181,f5422,f5444])).
% 10.19/1.80 % SZS output end CNFRefutation for theBenchmark.p
% 10.19/1.82 % Elapsed time: 1.430303 seconds
% 10.19/1.82 % CPU time: 10.749433 seconds
% 10.19/1.82 % Total memory used: 197.505 MB
% 10.19/1.82 % Net memory used: 190.624 MB
%------------------------------------------------------------------------------