%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC389+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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:42:20 PM UTC 2026
% Result : Theorem 0.11s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC389+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n003.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:22:02 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 0.11/0.52 % Refutation found
% 0.11/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.52 fof(f4,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f5,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f6,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f7,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f8,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> ( cyclefreeP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ~ ( leq(V,W)& leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f9,axiom,(
% 0.11/0.52 (! [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) ) ) ) )) )) )) )) )) ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f10,axiom,(
% 0.11/0.52 (! [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) ) ) ) )) )) )) )) )) ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f15,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f16,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f17,axiom,(
% 0.11/0.52 ssList(nil) ),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f28,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f36,axiom,(
% 0.11/0.52 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f45,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f51,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f53,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( segmentP(U,V)& segmentP(V,W) )=> segmentP(U,W) ) ) )) )) )),
% 0.11/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.52 fof(f54,axiom,(
% 0.11/0.52 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( segmentP(U,V)& segmentP(V,U) )=> U = V ) ) )) )),
% 0.11/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.53 fof(f57,axiom,(
% 0.11/0.53 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 0.11/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.53 fof(f58,axiom,(
% 0.11/0.53 (! [U] :( ssList(U)=> ( segmentP(nil,U)<=> nil = U ) ) )),
% 0.11/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.53 fof(f84,axiom,(
% 0.11/0.53 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.11/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.53 fof(f96,conjecture,(
% 0.11/0.53 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ( (! [Y] :( ssItem(Y)=> (! [Z] :( ssList(Z)=> (! [X1] :( ~ ssList(X1)| cons(Y,nil) != W| app(app(Z,W),X1) != X| (? [X2] :( ssItem(X2)& memberP(Z,X2)& lt(Y,X2) ))| (? [X3] :( ssItem(X3)& memberP(X1,X3)& lt(X3,Y) ) )) )) )))& ( nil != X| nil != W ) )| ( segmentP(V,U)& ( ~ neq(V,nil)| singletonP(U) ) ) ) )) )) )) )),
% 0.11/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.53 fof(f97,negated_conjecture,(
% 0.11/0.53 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ( (! [Y] :( ssItem(Y)=> (! [Z] :( ssList(Z)=> (! [X1] :( ~ ssList(X1)| cons(Y,nil) != W| app(app(Z,W),X1) != X| (? [X2] :( ssItem(X2)& memberP(Z,X2)& lt(Y,X2) ))| (? [X3] :( ssItem(X3)& memberP(X1,X3)& lt(X3,Y) ) )) )) )))& ( nil != X| nil != W ) )| ( segmentP(V,U)& ( ~ neq(V,nil)| singletonP(U) ) ) ) )) )) )) ))),
% 0.11/0.53 inference(negated_conjecture,[status(cth)],[f96])).
% 0.11/0.53 fof(f113,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.11/0.53 fof(f114,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f113])).
% 0.11/0.53 fof(f115,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|((~singletonP(U)|(ssItem(sK4_skl(U))&cons(sK4_skl(U),nil)=U))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 0.11/0.53 fof(f116,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~singletonP(X0)|ssItem(sK4_skl(X0)))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f115])).
% 0.11/0.53 fof(f117,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~singletonP(X0)|cons(sK4_skl(X0),nil)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f115])).
% 0.11/0.53 fof(f118,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|singletonP(X0)|~ssItem(X1)|~cons(X1,nil)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f115])).
% 0.11/0.53 fof(f119,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.11/0.53 fof(f120,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(?[W]: (ssList(W)&app(V,W)=U)))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f119])).
% 0.11/0.53 fof(f121,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(ssList(sK5_skl(V,U))&app(V,sK5_skl(V,U))=U))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.11/0.53 fof(f122,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.53 fof(f123,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.53 fof(f124,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.53 fof(f125,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.11/0.53 fof(f126,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(?[W]: (ssList(W)&app(W,V)=U)))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f125])).
% 0.11/0.53 fof(f127,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(ssList(sK6_skl(V,U))&app(sK6_skl(V,U),V)=U))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.11/0.53 fof(f128,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f127])).
% 0.11/0.53 fof(f129,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f127])).
% 0.11/0.53 fof(f130,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f127])).
% 0.11/0.53 fof(f131,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.11/0.53 fof(f132,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U)))))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f131])).
% 0.11/0.53 fof(f133,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(ssList(sK7_skl(V,U))&(ssList(sK8_skl(V,U))&app(app(sK7_skl(V,U),V),sK8_skl(V,U))=U)))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 0.11/0.53 fof(f136,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f133])).
% 0.11/0.53 fof(f137,plain,(
% 0.11/0.53 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f133])).
% 0.11/0.53 fof(f138,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(cyclefreeP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V)))))))))))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.11/0.53 fof(f139,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(leq(V,W)&leq(W,V))))))))))))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f138])).
% 0.11/0.53 fof(f140,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(ssItem(sK9_skl(U))&(ssItem(sK10_skl(U))&(ssList(sK11_skl(U))&(ssList(sK12_skl(U))&(ssList(sK13_skl(U))&(app(app(sK11_skl(U),cons(sK9_skl(U),sK12_skl(U))),cons(sK10_skl(U),sK13_skl(U)))=U&(leq(sK9_skl(U),sK10_skl(U))&leq(sK10_skl(U),sK9_skl(U))))))))))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(V,sK9_skl(U)),skolemize(W,sK10_skl(U)),skolemize(X,sK11_skl(U)),skolemize(Y,sK12_skl(U)),skolemize(Z,sK13_skl(U))],[f139])).
% 0.11/0.53 fof(f147,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|cyclefreeP(X0)|app(app(sK11_skl(X0),cons(sK9_skl(X0),sK12_skl(X0))),cons(sK10_skl(X0),sK13_skl(X0)))=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f140])).
% 0.11/0.53 fof(f150,plain,(
% 0.11/0.53 ![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)))))))))))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.11/0.53 fof(f151,plain,(
% 0.11/0.53 ![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))))))))))))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f150])).
% 0.11/0.53 fof(f152,plain,(
% 0.11/0.53 ![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))))))))))))),
% 0.11/0.53 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])).
% 0.11/0.53 fof(f159,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|totalorderP(X0)|app(app(sK16_skl(X0),cons(sK14_skl(X0),sK17_skl(X0))),cons(sK15_skl(X0),sK18_skl(X0)))=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f152])).
% 0.11/0.53 fof(f162,plain,(
% 0.11/0.53 ![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)))))))))))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.11/0.53 fof(f163,plain,(
% 0.11/0.53 ![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))))))))))))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f162])).
% 0.11/0.53 fof(f164,plain,(
% 0.11/0.53 ![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))))))))))))),
% 0.11/0.53 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])).
% 0.11/0.53 fof(f171,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|strictorderP(X0)|app(app(sK21_skl(X0),cons(sK19_skl(X0),sK22_skl(X0))),cons(sK20_skl(X0),sK23_skl(X0)))=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f164])).
% 0.11/0.53 fof(f217,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.11/0.53 fof(f218,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f217])).
% 0.11/0.53 fof(f219,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f218])).
% 0.11/0.53 fof(f221,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.11/0.53 fof(f222,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f221])).
% 0.11/0.53 fof(f223,plain,(
% 0.11/0.53 ssList(nil)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f17])).
% 0.11/0.53 fof(f248,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.11/0.53 fof(f249,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f248])).
% 0.11/0.53 fof(f268,plain,(
% 0.11/0.53 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.11/0.53 fof(f269,plain,(
% 0.11/0.53 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~memberP(app(V,W),U)|(memberP(V,U)|memberP(W,U)))&(memberP(app(V,W),U)|(~memberP(V,U)&~memberP(W,U)))))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f268])).
% 0.11/0.53 fof(f270,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~memberP(app(X1,X2),X0)|memberP(X1,X0)|memberP(X2,X0))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f269])).
% 0.11/0.53 fof(f294,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.11/0.53 fof(f295,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f294])).
% 0.11/0.53 fof(f308,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.11/0.53 fof(f309,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f308])).
% 0.11/0.53 fof(f314,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~segmentP(U,V)|~segmentP(V,W))|segmentP(U,W)))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.11/0.53 fof(f315,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(X0,X1)|~segmentP(X1,X2)|segmentP(X0,X2))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f314])).
% 0.11/0.53 fof(f316,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|~segmentP(V,U))|U=V))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.11/0.53 fof(f317,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|~segmentP(X1,X0)|X0=X1)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f316])).
% 0.11/0.53 fof(f322,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|segmentP(U,nil))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.11/0.53 fof(f323,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f322])).
% 0.11/0.53 fof(f324,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|(segmentP(nil,U)<=>nil=U))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.11/0.53 fof(f325,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|((~segmentP(nil,U)|nil=U)&(segmentP(nil,U)|~nil=U)))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f324])).
% 0.11/0.53 fof(f326,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~segmentP(nil,X0)|nil=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f325])).
% 0.11/0.53 fof(f388,plain,(
% 0.11/0.53 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.11/0.53 fof(f389,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f388])).
% 0.11/0.53 fof(f415,plain,(
% 0.11/0.53 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((ssList(X)&V=X)&U=W)&((?[Y]: (ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: ((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2))))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))|(nil=X&nil=W)))&(~segmentP(V,U)|(neq(V,nil)&~singletonP(U)))))))))))),
% 0.11/0.53 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.11/0.53 fof(f416,definition,(
% 0.11/0.53 ![W,X,Y]: (sP0_prd(Y,X,W)<=>(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: ((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2))))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.11/0.53 fof(f417,plain,(
% 0.11/0.53 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((ssList(X)&V=X)&U=W)&((?[Y]: sP0_prd(Y,X,W))|(nil=X&nil=W)))&(~segmentP(V,U)|(neq(V,nil)&~singletonP(U))))))))))),
% 0.11/0.53 inference(formula_renaming,[status(thm)],[f415,f416])).
% 0.11/0.53 fof(f418,plain,(
% 0.11/0.53 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&((?[X]: (((ssList(X)&V=X)&U=W)&((?[Y]: sP0_prd(Y,X,W))|(nil=X&nil=W))))&(~segmentP(V,U)|(neq(V,nil)&~singletonP(U)))))))))),
% 0.11/0.53 inference(miniscoping,[status(thm)],[f417])).
% 0.11/0.53 fof(f419,plain,(
% 0.11/0.53 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&(sP0_prd(sK51_skl,sK50_skl,sK49_skl)|(nil=sK50_skl&nil=sK49_skl)))&(~segmentP(sK48_skl,sK47_skl)|(neq(sK48_skl,nil)&~singletonP(sK47_skl)))))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl)],[f418])).
% 0.11/0.53 fof(f420,plain,(
% 0.11/0.53 ssList(sK47_skl)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f421,plain,(
% 0.11/0.53 ssList(sK48_skl)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f424,plain,(
% 0.11/0.53 sK48_skl=sK50_skl),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f425,plain,(
% 0.11/0.53 sK47_skl=sK49_skl),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f426,plain,(
% 0.11/0.53 sP0_prd(sK51_skl,sK50_skl,sK49_skl)|nil=sK50_skl),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f427,plain,(
% 0.11/0.53 sP0_prd(sK51_skl,sK50_skl,sK49_skl)|nil=sK49_skl),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f428,plain,(
% 0.11/0.53 ~segmentP(sK48_skl,sK47_skl)|neq(sK48_skl,nil)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f429,plain,(
% 0.11/0.53 ~segmentP(sK48_skl,sK47_skl)|~singletonP(sK47_skl)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f419])).
% 0.11/0.53 fof(f430,definition,(
% 0.11/0.53 ![Y,Z,X2]: (sP1_prd(X2,Z,Y)<=>((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.11/0.53 fof(f431,plain,(
% 0.11/0.53 ![W,X,Y]: (sP0_prd(Y,X,W)<=>(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: sP1_prd(X2,Z,Y)))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))),
% 0.11/0.53 inference(formula_renaming,[status(thm)],[f416,f430])).
% 0.11/0.53 fof(f432,plain,(
% 0.11/0.53 ![W,X,Y]: ((~sP0_prd(Y,X,W)|(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: sP1_prd(X2,Z,Y)))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))&(sP0_prd(Y,X,W)|(~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~cons(Y,nil)=W)|~app(app(Z,W),X1)=X)|(?[X2]: ~sP1_prd(X2,Z,Y)))|(?[X3]: ((ssItem(X3)&memberP(X1,X3))<(X3,Y))))))))))),
% 0.11/0.53 inference(NNF_transformation,[status(thm)],[f431])).
% 0.11/0.53 fof(f433,plain,(
% 0.11/0.53 (![W,X,Y]: (~sP0_prd(Y,X,W)|(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: sP1_prd(X2,Z,Y)))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y))))))))))&(![W,X,Y]: (sP0_prd(Y,X,W)|(~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~cons(Y,nil)=W)|~app(app(Z,W),X1)=X)|(?[X2]: ~sP1_prd(X2,Z,Y)))|(?[X3]: ((ssItem(X3)&memberP(X1,X3))<(X3,Y))))))))))),
% 0.11/0.53 inference(miniscoping,[status(thm)],[f432])).
% 0.11/0.53 fof(f434,plain,(
% 0.11/0.53 (![W,X,Y]: (~sP0_prd(Y,X,W)|(ssItem(Y)&(ssList(sK52_skl(Y,X,W))&((((ssList(sK53_skl(Y,X,W))&cons(Y,nil)=W)&app(app(sK52_skl(Y,X,W),W),sK53_skl(Y,X,W))=X)&(![X2]: sP1_prd(X2,sK52_skl(Y,X,W),Y)))&(![X3]: ((~ssItem(X3)|~memberP(sK53_skl(Y,X,W),X3))|~lt(X3,Y))))))))&(![W,X,Y]: (sP0_prd(Y,X,W)|(~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~cons(Y,nil)=W)|~app(app(Z,W),X1)=X)|~sP1_prd(sK54_skl(X1,Z,Y,X,W),Z,Y))|((ssItem(sK55_skl(X1,Z,Y,X,W))&memberP(X1,sK55_skl(X1,Z,Y,X,W)))<(sK55_skl(X1,Z,Y,X,W),Y)))))))))),
% 0.11/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl,sK53_skl,sK54_skl,sK55_skl]),skolemize(Z,sK52_skl(Y,X,W)),skolemize(X1,sK53_skl(Y,X,W)),skolemize(X2,sK54_skl(X1,Z,Y,X,W)),skolemize(X3,sK55_skl(X1,Z,Y,X,W))],[f433])).
% 0.11/0.53 fof(f435,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssItem(X0))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f434])).
% 0.11/0.53 fof(f436,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssList(sK52_skl(X0,X1,X2)))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f434])).
% 0.11/0.53 fof(f437,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssList(sK53_skl(X0,X1,X2)))),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f434])).
% 0.11/0.53 fof(f438,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|cons(X0,nil)=X2)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f434])).
% 0.11/0.53 fof(f439,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|app(app(sK52_skl(X0,X1,X2),X2),sK53_skl(X0,X1,X2))=X1)),
% 0.11/0.53 inference(cnf_transformation,[status(thm)],[f434])).
% 0.11/0.53 fof(f451,definition,(
% 0.11/0.53 sQ0_spl <=> (sP0_prd(sK51_skl,sK50_skl,sK49_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f452,plain,(
% 0.11/0.53 sP0_prd(sK51_skl,sK50_skl,sK49_skl)|~sQ0_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f451])).
% 0.11/0.53 fof(f454,definition,(
% 0.11/0.53 sQ1_spl <=> (nil=sK50_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f455,plain,(
% 0.11/0.53 nil=sK50_skl|~sQ1_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f454])).
% 0.11/0.53 fof(f457,plain,(
% 0.11/0.53 sQ0_spl|sQ1_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f426,f451,f454])).
% 0.11/0.53 fof(f458,definition,(
% 0.11/0.53 sQ2_spl <=> (nil=sK49_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f459,plain,(
% 0.11/0.53 nil=sK49_skl|~sQ2_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f458])).
% 0.11/0.53 fof(f461,plain,(
% 0.11/0.53 sQ0_spl|sQ2_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f427,f451,f458])).
% 0.11/0.53 fof(f462,definition,(
% 0.11/0.53 sQ3_spl <=> (segmentP(sK48_skl,sK47_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f464,plain,(
% 0.11/0.53 ~segmentP(sK48_skl,sK47_skl)|sQ3_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f462])).
% 0.11/0.53 fof(f465,definition,(
% 0.11/0.53 sQ4_spl <=> (neq(sK48_skl,nil))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f466,plain,(
% 0.11/0.53 neq(sK48_skl,nil)|~sQ4_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f465])).
% 0.11/0.53 fof(f468,plain,(
% 0.11/0.53 ~sQ3_spl|sQ4_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f428,f462,f465])).
% 0.11/0.53 fof(f469,definition,(
% 0.11/0.53 sQ5_spl <=> (singletonP(sK47_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f472,plain,(
% 0.11/0.53 ~sQ3_spl|~sQ5_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f429,f462,f469])).
% 0.11/0.53 fof(f476,plain,(
% 0.11/0.53 ![X0]: (~ssList(cons(X0,nil))|singletonP(cons(X0,nil))|~ssItem(X0))),
% 0.11/0.53 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.11/0.53 fof(f477,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.11/0.53 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.11/0.53 fof(f478,plain,(
% 0.11/0.53 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 0.11/0.53 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.11/0.53 fof(f479,plain,(
% 0.11/0.53 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 0.11/0.53 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 0.11/0.53 fof(f488,plain,(
% 0.11/0.53 ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 0.11/0.53 inference(destructive_equality_resolution,[status(thm)],[f219])).
% 0.11/0.53 fof(f489,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 0.11/0.53 inference(duplicate_literals_removal,[status(thm)],[f488])).
% 0.11/0.53 fof(f512,plain,(
% 0.11/0.53 sP0_prd(sK51_skl,sK48_skl,sK49_skl)|~sQ0_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f424,f452])).
% 0.11/0.53 fof(f513,plain,(
% 0.11/0.53 sP0_prd(sK51_skl,sK48_skl,sK47_skl)|~sQ0_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f425,f512])).
% 0.11/0.53 fof(f514,plain,(
% 0.11/0.53 ssItem(sK51_skl)|~sQ0_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f513,f435])).
% 0.11/0.53 fof(f517,plain,(
% 0.11/0.53 cons(sK51_skl,nil)=sK47_skl|~sQ0_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f438,f513])).
% 0.11/0.53 fof(f518,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|singletonP(cons(sK51_skl,nil))|~ssItem(sK51_skl)|~sQ0_spl),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f517,f476])).
% 0.11/0.53 fof(f520,definition,(
% 0.11/0.53 sQ6_spl <=> (ssList(sK47_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f522,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|sQ6_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f520])).
% 0.11/0.53 fof(f523,definition,(
% 0.11/0.53 sQ7_spl <=> (singletonP(cons(sK51_skl,nil)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f524,plain,(
% 0.11/0.53 singletonP(cons(sK51_skl,nil))|~sQ7_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f523])).
% 0.11/0.53 fof(f526,definition,(
% 0.11/0.53 sQ8_spl <=> (ssItem(sK51_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f528,plain,(
% 0.11/0.53 ~ssItem(sK51_skl)|sQ8_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f526])).
% 0.11/0.53 fof(f529,plain,(
% 0.11/0.53 ~sQ6_spl|sQ7_spl|~sQ8_spl|~sQ0_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f518,f520,f523,f526,f451])).
% 0.11/0.53 fof(f533,definition,(
% 0.11/0.53 sQ10_spl <=> (ssList(nil))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f535,plain,(
% 0.11/0.53 ~ssList(nil)|sQ10_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f533])).
% 0.11/0.53 fof(f537,plain,(
% 0.11/0.53 sK48_skl=nil|~sQ1_spl),
% 0.11/0.53 inference(backward_demodulation,[status(thm)],[f455,f424])).
% 0.11/0.53 fof(f538,plain,(
% 0.11/0.53 sK47_skl=nil|~sQ2_spl),
% 0.11/0.53 inference(backward_demodulation,[status(thm)],[f459,f425])).
% 0.11/0.53 fof(f539,plain,(
% 0.11/0.53 ~segmentP(nil,sK47_skl)|~sQ1_spl|sQ3_spl),
% 0.11/0.53 inference(backward_demodulation,[status(thm)],[f537,f464])).
% 0.11/0.53 fof(f558,plain,(
% 0.11/0.53 ![X0]: (~ssList(nil)|~ssItem(X0)|singletonP(cons(X0,nil))|~ssItem(X0))),
% 0.11/0.53 inference(resolution,[status(thm)],[f222,f476])).
% 0.11/0.53 fof(f559,definition,(
% 0.11/0.53 ![X0]: (sQ15_spl <=> (~ssItem(X0)|singletonP(cons(X0,nil))|~ssItem(X0)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f560,plain,(
% 0.11/0.53 ![X0]: (~ssItem(X0)|singletonP(cons(X0,nil))|~ssItem(X0)|~sQ15_spl)),
% 0.11/0.53 inference(component_clause,[status(thm)],[f559])).
% 0.11/0.53 fof(f562,plain,(
% 0.11/0.53 ~sQ10_spl|sQ15_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f558,f533,f559])).
% 0.11/0.53 fof(f563,plain,(
% 0.11/0.53 $false|sQ10_spl),
% 0.11/0.53 inference(forward_subsumption_resolution,[status(thm)],[f535,f223])).
% 0.11/0.53 fof(f564,plain,(
% 0.11/0.53 sQ10_spl),
% 0.11/0.53 inference(contradiction_clause,[status(thm)],[f563])).
% 0.11/0.53 fof(f565,plain,(
% 0.11/0.53 ![X0]: (~ssItem(X0)|singletonP(cons(X0,nil))|~sQ15_spl)),
% 0.11/0.53 inference(duplicate_literals_removal,[status(thm)],[f560])).
% 0.11/0.53 fof(f567,plain,(
% 0.11/0.53 ~segmentP(nil,nil)|~sQ2_spl|~sQ1_spl|sQ3_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f538,f539])).
% 0.11/0.53 fof(f568,plain,(
% 0.11/0.53 ~ssList(nil)|~sQ2_spl|~sQ1_spl|sQ3_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f567,f323])).
% 0.11/0.53 fof(f570,plain,(
% 0.11/0.53 ~sQ10_spl|~sQ2_spl|~sQ1_spl|sQ3_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f568,f533,f458,f454,f462])).
% 0.11/0.53 fof(f572,plain,(
% 0.11/0.53 $false|sQ8_spl|~sQ0_spl),
% 0.11/0.53 inference(forward_subsumption_resolution,[status(thm)],[f514,f528])).
% 0.11/0.53 fof(f573,plain,(
% 0.11/0.53 sQ8_spl|~sQ0_spl),
% 0.11/0.53 inference(contradiction_clause,[status(thm)],[f572])).
% 0.11/0.53 fof(f575,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 0.11/0.53 inference(resolution,[status(thm)],[f123,f295])).
% 0.11/0.53 fof(f577,definition,(
% 0.11/0.53 ![X0]: (sQ16_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f580,plain,(
% 0.11/0.53 sQ16_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f575,f577,f533])).
% 0.11/0.53 fof(f583,plain,(
% 0.11/0.53 $false|sQ6_spl),
% 0.11/0.53 inference(forward_subsumption_resolution,[status(thm)],[f522,f420])).
% 0.11/0.53 fof(f584,plain,(
% 0.11/0.53 sQ6_spl),
% 0.11/0.53 inference(contradiction_clause,[status(thm)],[f583])).
% 0.11/0.53 fof(f606,plain,(
% 0.11/0.53 neq(nil,nil)|~sQ1_spl|~sQ4_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f537,f466])).
% 0.11/0.53 fof(f607,plain,(
% 0.11/0.53 ~ssList(nil)|~sQ1_spl|~sQ4_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f606,f489])).
% 0.11/0.53 fof(f608,plain,(
% 0.11/0.53 ~sQ10_spl|~sQ1_spl|~sQ4_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f607,f533,f454,f465])).
% 0.11/0.53 fof(f631,plain,(
% 0.11/0.53 app(app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),sK47_skl),sK53_skl(sK51_skl,sK48_skl,sK47_skl))=sK48_skl|~sQ0_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f513,f439])).
% 0.11/0.53 fof(f634,plain,(
% 0.11/0.53 singletonP(sK47_skl)|~sQ0_spl|~sQ7_spl),
% 0.11/0.53 inference(backward_demodulation,[status(thm)],[f517,f524])).
% 0.11/0.53 fof(f647,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|cons(sK4_skl(sK47_skl),nil)=sK47_skl|~sQ0_spl|~sQ7_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f634,f117])).
% 0.11/0.53 fof(f648,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|ssItem(sK4_skl(sK47_skl))|~sQ0_spl|~sQ7_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f634,f116])).
% 0.11/0.53 fof(f649,definition,(
% 0.11/0.53 sQ22_spl <=> (cons(sK4_skl(sK47_skl),nil)=sK47_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f650,plain,(
% 0.11/0.53 cons(sK4_skl(sK47_skl),nil)=sK47_skl|~sQ22_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f649])).
% 0.11/0.53 fof(f652,plain,(
% 0.11/0.53 ~sQ6_spl|sQ22_spl|~sQ0_spl|~sQ7_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f647,f520,f649,f451,f523])).
% 0.11/0.53 fof(f653,definition,(
% 0.11/0.53 sQ23_spl <=> (ssItem(sK4_skl(sK47_skl)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f656,plain,(
% 0.11/0.53 ~sQ6_spl|sQ23_spl|~sQ0_spl|~sQ7_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f648,f520,f653,f451,f523])).
% 0.11/0.53 fof(f663,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0)),
% 0.11/0.53 inference(resolution,[status(thm)],[f309,f129])).
% 0.11/0.53 fof(f664,definition,(
% 0.11/0.53 ![X0]: (sQ24_spl <=> (~ssList(X0)|~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f667,plain,(
% 0.11/0.53 sQ24_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f663,f664,f533])).
% 0.11/0.53 fof(f676,plain,(
% 0.11/0.53 app(nil,sK47_skl)=sK47_skl),
% 0.11/0.53 inference(resolution,[status(thm)],[f249,f420])).
% 0.11/0.53 fof(f678,plain,(
% 0.11/0.53 app(nil,sK48_skl)=sK48_skl),
% 0.11/0.53 inference(resolution,[status(thm)],[f249,f421])).
% 0.11/0.53 fof(f686,plain,(
% 0.11/0.53 app(nil,nil)=nil),
% 0.11/0.53 inference(resolution,[status(thm)],[f249,f223])).
% 0.11/0.53 fof(f687,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|~ssList(sK47_skl)|rearsegP(app(nil,sK47_skl),sK47_skl)|~ssList(nil)),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f676,f478])).
% 0.11/0.53 fof(f688,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f676,f477])).
% 0.11/0.53 fof(f689,plain,(
% 0.11/0.53 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f676,f479])).
% 0.11/0.53 fof(f690,definition,(
% 0.11/0.53 sQ25_spl <=> (rearsegP(app(nil,sK47_skl),sK47_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f691,plain,(
% 0.11/0.53 rearsegP(app(nil,sK47_skl),sK47_skl)|~sQ25_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f690])).
% 0.11/0.53 fof(f693,plain,(
% 0.11/0.53 ~sQ6_spl|sQ25_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f687,f520,f690,f533])).
% 0.11/0.53 fof(f694,definition,(
% 0.11/0.53 sQ26_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f695,plain,(
% 0.11/0.53 frontsegP(app(nil,sK47_skl),nil)|~sQ26_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f694])).
% 0.11/0.53 fof(f697,plain,(
% 0.11/0.53 ~sQ6_spl|~sQ10_spl|sQ26_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f688,f520,f533,f694])).
% 0.11/0.53 fof(f698,definition,(
% 0.11/0.53 ![X0]: (sQ27_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f701,plain,(
% 0.11/0.53 sQ27_spl|~sQ6_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f689,f698,f520,f533])).
% 0.11/0.53 fof(f702,plain,(
% 0.11/0.53 rearsegP(sK47_skl,sK47_skl)|~sQ25_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f676,f691])).
% 0.11/0.53 fof(f703,plain,(
% 0.11/0.53 frontsegP(sK47_skl,nil)|~sQ26_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f676,f695])).
% 0.11/0.53 fof(f705,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl|~sQ25_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f702,f129])).
% 0.11/0.53 fof(f706,definition,(
% 0.11/0.53 sQ28_spl <=> (app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f707,plain,(
% 0.11/0.53 app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl|~sQ28_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f706])).
% 0.11/0.53 fof(f709,plain,(
% 0.11/0.53 ~sQ6_spl|sQ28_spl|~sQ25_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f705,f520,f706,f690])).
% 0.11/0.53 fof(f710,plain,(
% 0.11/0.53 ~ssList(sK47_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ26_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f703,f123])).
% 0.11/0.53 fof(f711,definition,(
% 0.11/0.53 sQ29_spl <=> (app(nil,sK5_skl(nil,sK47_skl))=sK47_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f712,plain,(
% 0.11/0.53 app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ29_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f711])).
% 0.11/0.53 fof(f714,plain,(
% 0.11/0.53 ~sQ6_spl|~sQ10_spl|sQ29_spl|~sQ26_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f710,f520,f533,f711,f694])).
% 0.11/0.53 fof(f716,plain,(
% 0.11/0.53 ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 0.11/0.53 inference(resolution,[status(thm)],[f136,f323])).
% 0.11/0.53 fof(f718,definition,(
% 0.11/0.53 ![X0]: (sQ30_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f721,plain,(
% 0.11/0.53 sQ30_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f716,f718,f533])).
% 0.11/0.53 fof(f727,plain,(
% 0.11/0.53 ~ssList(sK48_skl)|~ssList(sK48_skl)|rearsegP(app(nil,sK48_skl),sK48_skl)|~ssList(nil)),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f678,f478])).
% 0.11/0.53 fof(f728,plain,(
% 0.11/0.53 ~ssList(sK48_skl)|~ssList(nil)|frontsegP(app(nil,sK48_skl),nil)|~ssList(sK48_skl)),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f678,f477])).
% 0.11/0.53 fof(f729,plain,(
% 0.11/0.53 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f678,f479])).
% 0.11/0.53 fof(f730,definition,(
% 0.11/0.53 sQ31_spl <=> (ssList(sK48_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f732,plain,(
% 0.11/0.53 ~ssList(sK48_skl)|sQ31_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f730])).
% 0.11/0.53 fof(f733,definition,(
% 0.11/0.53 sQ32_spl <=> (rearsegP(app(nil,sK48_skl),sK48_skl))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f734,plain,(
% 0.11/0.53 rearsegP(app(nil,sK48_skl),sK48_skl)|~sQ32_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f733])).
% 0.11/0.53 fof(f736,plain,(
% 0.11/0.53 ~sQ31_spl|sQ32_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f727,f730,f733,f533])).
% 0.11/0.53 fof(f737,definition,(
% 0.11/0.53 sQ33_spl <=> (frontsegP(app(nil,sK48_skl),nil))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f738,plain,(
% 0.11/0.53 frontsegP(app(nil,sK48_skl),nil)|~sQ33_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f737])).
% 0.11/0.53 fof(f740,plain,(
% 0.11/0.53 ~sQ31_spl|~sQ10_spl|sQ33_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f728,f730,f533,f737])).
% 0.11/0.53 fof(f741,definition,(
% 0.11/0.53 ![X0]: (sQ34_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f744,plain,(
% 0.11/0.53 sQ34_spl|~sQ31_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f729,f741,f730,f533])).
% 0.11/0.53 fof(f745,plain,(
% 0.11/0.53 $false|sQ31_spl),
% 0.11/0.53 inference(forward_subsumption_resolution,[status(thm)],[f732,f421])).
% 0.11/0.53 fof(f746,plain,(
% 0.11/0.53 sQ31_spl),
% 0.11/0.53 inference(contradiction_clause,[status(thm)],[f745])).
% 0.11/0.53 fof(f747,plain,(
% 0.11/0.53 rearsegP(sK48_skl,sK48_skl)|~sQ32_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f678,f734])).
% 0.11/0.53 fof(f748,plain,(
% 0.11/0.53 frontsegP(sK48_skl,nil)|~sQ33_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f678,f738])).
% 0.11/0.53 fof(f750,plain,(
% 0.11/0.53 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)=sK48_skl|~sQ32_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f747,f129])).
% 0.11/0.53 fof(f751,definition,(
% 0.11/0.53 sQ35_spl <=> (app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)=sK48_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f754,plain,(
% 0.11/0.53 ~sQ31_spl|sQ35_spl|~sQ32_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f750,f730,f751,f733])).
% 0.11/0.53 fof(f755,plain,(
% 0.11/0.53 ~ssList(sK48_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK48_skl))=sK48_skl|~sQ33_spl),
% 0.11/0.53 inference(resolution,[status(thm)],[f748,f123])).
% 0.11/0.53 fof(f756,definition,(
% 0.11/0.53 sQ36_spl <=> (app(nil,sK5_skl(nil,sK48_skl))=sK48_skl)),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f759,plain,(
% 0.11/0.53 ~sQ31_spl|~sQ10_spl|sQ36_spl|~sQ33_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f755,f730,f533,f756,f737])).
% 0.11/0.53 fof(f760,plain,(
% 0.11/0.53 ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f686,f478])).
% 0.11/0.53 fof(f761,plain,(
% 0.11/0.53 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f686,f477])).
% 0.11/0.53 fof(f762,plain,(
% 0.11/0.53 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 0.11/0.53 inference(paramodulation,[status(thm)],[f686,f479])).
% 0.11/0.53 fof(f763,definition,(
% 0.11/0.53 sQ37_spl <=> (rearsegP(app(nil,nil),nil))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f764,plain,(
% 0.11/0.53 rearsegP(app(nil,nil),nil)|~sQ37_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f763])).
% 0.11/0.53 fof(f766,plain,(
% 0.11/0.53 ~sQ10_spl|sQ37_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f760,f533,f763])).
% 0.11/0.53 fof(f767,definition,(
% 0.11/0.53 sQ38_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f768,plain,(
% 0.11/0.53 frontsegP(app(nil,nil),nil)|~sQ38_spl),
% 0.11/0.53 inference(component_clause,[status(thm)],[f767])).
% 0.11/0.53 fof(f770,plain,(
% 0.11/0.53 ~sQ10_spl|sQ38_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f761,f533,f767])).
% 0.11/0.53 fof(f771,definition,(
% 0.11/0.53 ![X0]: (sQ39_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 0.11/0.53 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.11/0.53 fof(f774,plain,(
% 0.11/0.53 sQ39_spl|~sQ10_spl),
% 0.11/0.53 inference(split_clause,[status(thm)],[f762,f771,f533])).
% 0.11/0.53 fof(f775,plain,(
% 0.11/0.53 rearsegP(nil,nil)|~sQ37_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f686,f764])).
% 0.11/0.53 fof(f776,plain,(
% 0.11/0.53 frontsegP(nil,nil)|~sQ38_spl),
% 0.11/0.53 inference(forward_demodulation,[status(thm)],[f686,f768])).
% 0.11/0.54 fof(f778,plain,(
% 0.11/0.54 ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil|~sQ37_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f775,f129])).
% 0.11/0.54 fof(f779,definition,(
% 0.11/0.54 sQ40_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f782,plain,(
% 0.11/0.54 ~sQ10_spl|sQ40_spl|~sQ37_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f778,f533,f779,f763])).
% 0.11/0.54 fof(f783,plain,(
% 0.11/0.54 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ38_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f776,f123])).
% 0.11/0.54 fof(f784,definition,(
% 0.11/0.54 sQ41_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f787,plain,(
% 0.11/0.54 ~sQ10_spl|sQ41_spl|~sQ38_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f783,f533,f784,f767])).
% 0.11/0.54 fof(f789,plain,(
% 0.11/0.54 app(sK47_skl,nil)=sK47_skl),
% 0.11/0.54 inference(resolution,[status(thm)],[f389,f420])).
% 0.11/0.54 fof(f791,plain,(
% 0.11/0.54 app(sK48_skl,nil)=sK48_skl),
% 0.11/0.54 inference(resolution,[status(thm)],[f389,f421])).
% 0.11/0.54 fof(f800,plain,(
% 0.11/0.54 ~ssList(sK47_skl)|~ssList(nil)|rearsegP(app(sK47_skl,nil),nil)|~ssList(sK47_skl)),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f789,f478])).
% 0.11/0.54 fof(f801,plain,(
% 0.11/0.54 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f789,f477])).
% 0.11/0.54 fof(f802,plain,(
% 0.11/0.54 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f789,f479])).
% 0.11/0.54 fof(f803,definition,(
% 0.11/0.54 sQ42_spl <=> (rearsegP(app(sK47_skl,nil),nil))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f804,plain,(
% 0.11/0.54 rearsegP(app(sK47_skl,nil),nil)|~sQ42_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f803])).
% 0.11/0.54 fof(f806,plain,(
% 0.11/0.54 ~sQ6_spl|~sQ10_spl|sQ42_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f800,f520,f533,f803])).
% 0.11/0.54 fof(f807,definition,(
% 0.11/0.54 sQ43_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f808,plain,(
% 0.11/0.54 frontsegP(app(sK47_skl,nil),sK47_skl)|~sQ43_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f807])).
% 0.11/0.54 fof(f810,plain,(
% 0.11/0.54 ~sQ6_spl|sQ43_spl|~sQ10_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f801,f520,f807,f533])).
% 0.11/0.54 fof(f811,definition,(
% 0.11/0.54 ![X0]: (sQ44_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f814,plain,(
% 0.11/0.54 sQ44_spl|~sQ10_spl|~sQ6_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f802,f811,f533,f520])).
% 0.11/0.54 fof(f815,plain,(
% 0.11/0.54 rearsegP(sK47_skl,nil)|~sQ42_spl),
% 0.11/0.54 inference(forward_demodulation,[status(thm)],[f789,f804])).
% 0.11/0.54 fof(f816,plain,(
% 0.11/0.54 frontsegP(sK47_skl,sK47_skl)|~sQ43_spl),
% 0.11/0.54 inference(forward_demodulation,[status(thm)],[f789,f808])).
% 0.11/0.54 fof(f818,plain,(
% 0.11/0.54 ~ssList(sK47_skl)|~ssList(nil)|app(sK6_skl(nil,sK47_skl),nil)=sK47_skl|~sQ42_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f815,f129])).
% 0.11/0.54 fof(f819,definition,(
% 0.11/0.54 sQ45_spl <=> (app(sK6_skl(nil,sK47_skl),nil)=sK47_skl)),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f822,plain,(
% 0.11/0.54 ~sQ6_spl|~sQ10_spl|sQ45_spl|~sQ42_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f818,f520,f533,f819,f803])).
% 0.11/0.54 fof(f845,plain,(
% 0.11/0.54 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ43_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f816,f123])).
% 0.11/0.54 fof(f846,definition,(
% 0.11/0.54 sQ46_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f849,plain,(
% 0.11/0.54 ~sQ6_spl|sQ46_spl|~sQ43_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f845,f520,f846,f807])).
% 0.11/0.54 fof(f851,plain,(
% 0.11/0.54 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f791,f479])).
% 0.11/0.54 fof(f853,definition,(
% 0.11/0.54 ![X0]: (sQ47_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f856,plain,(
% 0.11/0.54 sQ47_spl|~sQ10_spl|~sQ31_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f851,f853,f533,f730])).
% 0.11/0.54 fof(f1012,plain,(
% 0.11/0.54 ~ssItem(sK4_skl(sK47_skl))|singletonP(sK47_skl)|~sQ15_spl|~sQ22_spl),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f650,f565])).
% 0.11/0.54 fof(f1018,plain,(
% 0.11/0.54 ~sQ23_spl|sQ5_spl|~sQ15_spl|~sQ22_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1012,f653,f469,f559,f649])).
% 0.11/0.54 fof(f1083,plain,(
% 0.11/0.54 ![X0]: (~ssItem(X0)|~ssList(sK48_skl)|~ssList(nil)|~memberP(sK48_skl,X0)|memberP(sK48_skl,X0)|memberP(nil,X0))),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f791,f270])).
% 0.11/0.54 fof(f1084,plain,(
% 0.11/0.54 ![X0]: (~ssItem(X0)|~ssList(sK47_skl)|~ssList(nil)|~memberP(sK47_skl,X0)|memberP(sK47_skl,X0)|memberP(nil,X0))),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f789,f270])).
% 0.11/0.54 fof(f1085,plain,(
% 0.11/0.54 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f686,f270])).
% 0.11/0.54 fof(f1088,definition,(
% 0.11/0.54 ![X0]: (sQ59_spl <=> (~ssItem(X0)|~memberP(sK48_skl,X0)|memberP(sK48_skl,X0)|memberP(nil,X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1091,plain,(
% 0.11/0.54 sQ59_spl|~sQ31_spl|~sQ10_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1083,f1088,f730,f533])).
% 0.11/0.54 fof(f1092,definition,(
% 0.11/0.54 ![X0]: (sQ60_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(sK47_skl,X0)|memberP(nil,X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1095,plain,(
% 0.11/0.54 sQ60_spl|~sQ6_spl|~sQ10_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1084,f1092,f520,f533])).
% 0.11/0.54 fof(f1096,definition,(
% 0.11/0.54 ![X0]: (sQ61_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1099,plain,(
% 0.11/0.54 sQ61_spl|~sQ10_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1085,f1096,f533])).
% 0.11/0.54 fof(f1180,plain,(
% 0.11/0.54 ~ssList(nil)|nil=nil|~ssList(nil)),
% 0.11/0.54 inference(resolution,[status(thm)],[f326,f323])).
% 0.11/0.54 fof(f1182,definition,(
% 0.11/0.54 sQ70_spl <=> (nil=nil)),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1185,plain,(
% 0.11/0.54 ~sQ10_spl|sQ70_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1180,f533,f1182])).
% 0.11/0.54 fof(f1369,plain,(
% 0.11/0.54 ![X0]: (~ssItem(X0)|~ssList(sK6_skl(sK47_skl,sK47_skl))|~ssList(sK47_skl)|~memberP(sK47_skl,X0)|memberP(sK6_skl(sK47_skl,sK47_skl),X0)|memberP(sK47_skl,X0)|~sQ28_spl)),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f707,f270])).
% 0.11/0.54 fof(f1371,plain,(
% 0.11/0.54 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),X0),sK47_skl)|~ssList(sK6_skl(sK47_skl,sK47_skl))|~ssList(X0)|~sQ28_spl)),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f707,f479])).
% 0.11/0.54 fof(f1372,definition,(
% 0.11/0.54 ![X0]: (sQ80_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(sK6_skl(sK47_skl,sK47_skl),X0)|memberP(sK47_skl,X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1375,definition,(
% 0.11/0.54 sQ81_spl <=> (ssList(sK6_skl(sK47_skl,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1376,plain,(
% 0.11/0.54 ssList(sK6_skl(sK47_skl,sK47_skl))|~sQ81_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1375])).
% 0.11/0.54 fof(f1377,plain,(
% 0.11/0.54 ~ssList(sK6_skl(sK47_skl,sK47_skl))|sQ81_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1375])).
% 0.11/0.54 fof(f1378,plain,(
% 0.11/0.54 sQ80_spl|~sQ81_spl|~sQ6_spl|~sQ28_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1369,f1372,f1375,f520,f706])).
% 0.11/0.54 fof(f1380,definition,(
% 0.11/0.54 ![X0]: (sQ82_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1383,plain,(
% 0.11/0.54 sQ82_spl|~sQ6_spl|~sQ81_spl|~sQ28_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1371,f1380,f520,f1375,f706])).
% 0.11/0.54 fof(f1384,plain,(
% 0.11/0.54 ~ssList(sK47_skl)|~ssList(sK47_skl)|~rearsegP(sK47_skl,sK47_skl)|sQ81_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1377,f128])).
% 0.11/0.54 fof(f1385,definition,(
% 0.11/0.54 sQ83_spl <=> (rearsegP(sK47_skl,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1387,plain,(
% 0.11/0.54 ~rearsegP(sK47_skl,sK47_skl)|sQ83_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1385])).
% 0.11/0.54 fof(f1388,plain,(
% 0.11/0.54 ~sQ6_spl|~sQ83_spl|sQ81_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1384,f520,f1385,f1375])).
% 0.11/0.54 fof(f1390,plain,(
% 0.11/0.54 $false|~sQ25_spl|sQ83_spl),
% 0.11/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1387,f702])).
% 0.11/0.54 fof(f1391,plain,(
% 0.11/0.54 ~sQ25_spl|sQ83_spl),
% 0.11/0.54 inference(contradiction_clause,[status(thm)],[f1390])).
% 0.11/0.54 fof(f1393,plain,(
% 0.11/0.54 totalorderP(sK6_skl(sK47_skl,sK47_skl))|app(app(sK16_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK14_skl(sK6_skl(sK47_skl,sK47_skl)),sK17_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK15_skl(sK6_skl(sK47_skl,sK47_skl)),sK18_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl)|~sQ81_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1376,f159])).
% 0.11/0.54 fof(f1397,plain,(
% 0.11/0.54 cyclefreeP(sK6_skl(sK47_skl,sK47_skl))|app(app(sK11_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK9_skl(sK6_skl(sK47_skl,sK47_skl)),sK12_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK10_skl(sK6_skl(sK47_skl,sK47_skl)),sK13_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl)|~sQ81_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1376,f147])).
% 0.11/0.54 fof(f1404,definition,(
% 0.11/0.54 sQ84_spl <=> (totalorderP(sK6_skl(sK47_skl,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1407,definition,(
% 0.11/0.54 sQ85_spl <=> (app(app(sK16_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK14_skl(sK6_skl(sK47_skl,sK47_skl)),sK17_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK15_skl(sK6_skl(sK47_skl,sK47_skl)),sK18_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1410,plain,(
% 0.11/0.54 sQ84_spl|sQ85_spl|~sQ81_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1393,f1404,f1407,f1375])).
% 0.11/0.54 fof(f1411,definition,(
% 0.11/0.54 sQ86_spl <=> (cyclefreeP(sK6_skl(sK47_skl,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1414,definition,(
% 0.11/0.54 sQ87_spl <=> (app(app(sK11_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK9_skl(sK6_skl(sK47_skl,sK47_skl)),sK12_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK10_skl(sK6_skl(sK47_skl,sK47_skl)),sK13_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1417,plain,(
% 0.11/0.54 sQ86_spl|sQ87_spl|~sQ81_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1397,f1411,f1414,f1375])).
% 0.11/0.54 fof(f1556,plain,(
% 0.11/0.54 strictorderP(sK6_skl(sK47_skl,sK47_skl))|app(app(sK21_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK19_skl(sK6_skl(sK47_skl,sK47_skl)),sK22_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK20_skl(sK6_skl(sK47_skl,sK47_skl)),sK23_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl)|~sQ81_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f171,f1376])).
% 0.11/0.54 fof(f1576,definition,(
% 0.11/0.54 sQ104_spl <=> (strictorderP(sK6_skl(sK47_skl,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1579,definition,(
% 0.11/0.54 sQ105_spl <=> (app(app(sK21_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK19_skl(sK6_skl(sK47_skl,sK47_skl)),sK22_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK20_skl(sK6_skl(sK47_skl,sK47_skl)),sK23_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1582,plain,(
% 0.11/0.54 sQ104_spl|sQ105_spl|~sQ81_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1556,f1576,f1579,f1375])).
% 0.11/0.54 fof(f1590,plain,(
% 0.11/0.54 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK5_skl(nil,sK47_skl))|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK5_skl(nil,sK47_skl),X0)|~sQ29_spl)),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f712,f270])).
% 0.11/0.54 fof(f1592,plain,(
% 0.11/0.54 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK5_skl(nil,sK47_skl))|segmentP(app(app(nil,sK5_skl(nil,sK47_skl)),X0),sK5_skl(nil,sK47_skl))|~ssList(nil)|~ssList(X0)|~sQ29_spl)),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f712,f479])).
% 0.11/0.54 fof(f1593,definition,(
% 0.11/0.54 ![X0]: (sQ108_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK5_skl(nil,sK47_skl),X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1596,definition,(
% 0.11/0.54 sQ109_spl <=> (ssList(sK5_skl(nil,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1597,plain,(
% 0.11/0.54 ssList(sK5_skl(nil,sK47_skl))|~sQ109_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1596])).
% 0.11/0.54 fof(f1598,plain,(
% 0.11/0.54 ~ssList(sK5_skl(nil,sK47_skl))|sQ109_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1596])).
% 0.11/0.54 fof(f1599,plain,(
% 0.11/0.54 sQ108_spl|~sQ10_spl|~sQ109_spl|~sQ29_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1590,f1593,f533,f1596,f711])).
% 0.11/0.54 fof(f1601,definition,(
% 0.11/0.54 ![X0]: (sQ110_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK5_skl(nil,sK47_skl)),X0),sK5_skl(nil,sK47_skl))|~ssList(X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1604,plain,(
% 0.11/0.54 sQ110_spl|~sQ109_spl|~sQ10_spl|~sQ29_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1592,f1601,f1596,f533,f711])).
% 0.11/0.54 fof(f1605,plain,(
% 0.11/0.54 ~ssList(sK48_skl)|~ssList(sK47_skl)|segmentP(app(app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),sK47_skl),sK53_skl(sK51_skl,sK48_skl,sK47_skl)),sK47_skl)|~ssList(sK52_skl(sK51_skl,sK48_skl,sK47_skl))|~ssList(sK53_skl(sK51_skl,sK48_skl,sK47_skl))|~sQ0_spl),
% 0.11/0.54 inference(paramodulation,[status(thm)],[f631,f479])).
% 0.11/0.54 fof(f1609,definition,(
% 0.11/0.54 sQ111_spl <=> (segmentP(app(app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),sK47_skl),sK53_skl(sK51_skl,sK48_skl,sK47_skl)),sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1610,plain,(
% 0.11/0.54 segmentP(app(app(sK52_skl(sK51_skl,sK48_skl,sK47_skl),sK47_skl),sK53_skl(sK51_skl,sK48_skl,sK47_skl)),sK47_skl)|~sQ111_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1609])).
% 0.11/0.54 fof(f1612,definition,(
% 0.11/0.54 sQ112_spl <=> (ssList(sK52_skl(sK51_skl,sK48_skl,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1614,plain,(
% 0.11/0.54 ~ssList(sK52_skl(sK51_skl,sK48_skl,sK47_skl))|sQ112_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1612])).
% 0.11/0.54 fof(f1615,definition,(
% 0.11/0.54 sQ113_spl <=> (ssList(sK53_skl(sK51_skl,sK48_skl,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1617,plain,(
% 0.11/0.54 ~ssList(sK53_skl(sK51_skl,sK48_skl,sK47_skl))|sQ113_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1615])).
% 0.11/0.54 fof(f1618,plain,(
% 0.11/0.54 ~sQ31_spl|~sQ6_spl|sQ111_spl|~sQ112_spl|~sQ113_spl|~sQ0_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1605,f730,f520,f1609,f1612,f1615,f451])).
% 0.11/0.54 fof(f1631,plain,(
% 0.11/0.54 ~ssList(sK47_skl)|~ssList(nil)|~frontsegP(sK47_skl,nil)|sQ109_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1598,f122])).
% 0.11/0.54 fof(f1632,definition,(
% 0.11/0.54 sQ117_spl <=> (frontsegP(sK47_skl,nil))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1634,plain,(
% 0.11/0.54 ~frontsegP(sK47_skl,nil)|sQ117_spl),
% 0.11/0.54 inference(component_clause,[status(thm)],[f1632])).
% 0.11/0.54 fof(f1635,plain,(
% 0.11/0.54 ~sQ6_spl|~sQ10_spl|~sQ117_spl|sQ109_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1631,f520,f533,f1632,f1596])).
% 0.11/0.54 fof(f1636,plain,(
% 0.11/0.54 $false|~sQ26_spl|sQ117_spl),
% 0.11/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1634,f703])).
% 0.11/0.54 fof(f1637,plain,(
% 0.11/0.54 ~sQ26_spl|sQ117_spl),
% 0.11/0.54 inference(contradiction_clause,[status(thm)],[f1636])).
% 0.11/0.54 fof(f1640,plain,(
% 0.11/0.54 strictorderP(sK5_skl(nil,sK47_skl))|app(app(sK21_skl(sK5_skl(nil,sK47_skl)),cons(sK19_skl(sK5_skl(nil,sK47_skl)),sK22_skl(sK5_skl(nil,sK47_skl)))),cons(sK20_skl(sK5_skl(nil,sK47_skl)),sK23_skl(sK5_skl(nil,sK47_skl))))=sK5_skl(nil,sK47_skl)|~sQ109_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1597,f171])).
% 0.11/0.54 fof(f1641,plain,(
% 0.11/0.54 totalorderP(sK5_skl(nil,sK47_skl))|app(app(sK16_skl(sK5_skl(nil,sK47_skl)),cons(sK14_skl(sK5_skl(nil,sK47_skl)),sK17_skl(sK5_skl(nil,sK47_skl)))),cons(sK15_skl(sK5_skl(nil,sK47_skl)),sK18_skl(sK5_skl(nil,sK47_skl))))=sK5_skl(nil,sK47_skl)|~sQ109_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1597,f159])).
% 0.11/0.54 fof(f1644,plain,(
% 0.11/0.54 cyclefreeP(sK5_skl(nil,sK47_skl))|app(app(sK11_skl(sK5_skl(nil,sK47_skl)),cons(sK9_skl(sK5_skl(nil,sK47_skl)),sK12_skl(sK5_skl(nil,sK47_skl)))),cons(sK10_skl(sK5_skl(nil,sK47_skl)),sK13_skl(sK5_skl(nil,sK47_skl))))=sK5_skl(nil,sK47_skl)|~sQ109_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1597,f147])).
% 0.11/0.54 fof(f1651,definition,(
% 0.11/0.54 sQ118_spl <=> (strictorderP(sK5_skl(nil,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1654,definition,(
% 0.11/0.54 sQ119_spl <=> (app(app(sK21_skl(sK5_skl(nil,sK47_skl)),cons(sK19_skl(sK5_skl(nil,sK47_skl)),sK22_skl(sK5_skl(nil,sK47_skl)))),cons(sK20_skl(sK5_skl(nil,sK47_skl)),sK23_skl(sK5_skl(nil,sK47_skl))))=sK5_skl(nil,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1657,plain,(
% 0.11/0.54 sQ118_spl|sQ119_spl|~sQ109_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1640,f1651,f1654,f1596])).
% 0.11/0.54 fof(f1658,definition,(
% 0.11/0.54 sQ120_spl <=> (totalorderP(sK5_skl(nil,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1661,definition,(
% 0.11/0.54 sQ121_spl <=> (app(app(sK16_skl(sK5_skl(nil,sK47_skl)),cons(sK14_skl(sK5_skl(nil,sK47_skl)),sK17_skl(sK5_skl(nil,sK47_skl)))),cons(sK15_skl(sK5_skl(nil,sK47_skl)),sK18_skl(sK5_skl(nil,sK47_skl))))=sK5_skl(nil,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1664,plain,(
% 0.11/0.54 sQ120_spl|sQ121_spl|~sQ109_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1641,f1658,f1661,f1596])).
% 0.11/0.54 fof(f1665,definition,(
% 0.11/0.54 sQ122_spl <=> (cyclefreeP(sK5_skl(nil,sK47_skl)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1668,definition,(
% 0.11/0.54 sQ123_spl <=> (app(app(sK11_skl(sK5_skl(nil,sK47_skl)),cons(sK9_skl(sK5_skl(nil,sK47_skl)),sK12_skl(sK5_skl(nil,sK47_skl)))),cons(sK10_skl(sK5_skl(nil,sK47_skl)),sK13_skl(sK5_skl(nil,sK47_skl))))=sK5_skl(nil,sK47_skl))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1671,plain,(
% 0.11/0.54 sQ122_spl|sQ123_spl|~sQ109_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1644,f1665,f1668,f1596])).
% 0.11/0.54 fof(f1680,plain,(
% 0.11/0.54 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1))),
% 0.11/0.54 inference(resolution,[status(thm)],[f315,f323])).
% 0.11/0.54 fof(f1682,definition,(
% 0.11/0.54 ![X0,X1]: (sQ124_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1685,plain,(
% 0.11/0.54 sQ124_spl|~sQ10_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1680,f1682,f533])).
% 0.11/0.54 fof(f1687,plain,(
% 0.11/0.54 ![X0]: (~ssList(nil)|~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0))),
% 0.11/0.54 inference(resolution,[status(thm)],[f317,f323])).
% 0.11/0.54 fof(f1689,definition,(
% 0.11/0.54 ![X0]: (sQ125_spl <=> (~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0)))),
% 0.11/0.54 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.11/0.54 fof(f1692,plain,(
% 0.11/0.54 ~sQ10_spl|sQ125_spl),
% 0.11/0.54 inference(split_clause,[status(thm)],[f1687,f533,f1689])).
% 0.11/0.54 fof(f1694,plain,(
% 0.11/0.54 ~sP0_prd(sK51_skl,sK48_skl,sK47_skl)|sQ113_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1617,f437])).
% 0.11/0.54 fof(f1695,plain,(
% 0.11/0.54 $false|~sQ0_spl|sQ113_spl),
% 0.11/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1694,f513])).
% 0.11/0.54 fof(f1696,plain,(
% 0.11/0.54 ~sQ0_spl|sQ113_spl),
% 0.11/0.54 inference(contradiction_clause,[status(thm)],[f1695])).
% 0.11/0.54 fof(f1697,plain,(
% 0.11/0.54 segmentP(sK48_skl,sK47_skl)|~sQ0_spl|~sQ111_spl),
% 0.11/0.54 inference(forward_demodulation,[status(thm)],[f631,f1610])).
% 0.11/0.54 fof(f1698,plain,(
% 0.11/0.54 $false|sQ3_spl|~sQ0_spl|~sQ111_spl),
% 0.11/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1697,f464])).
% 0.11/0.54 fof(f1699,plain,(
% 0.11/0.54 sQ3_spl|~sQ0_spl|~sQ111_spl),
% 0.11/0.54 inference(contradiction_clause,[status(thm)],[f1698])).
% 0.11/0.54 fof(f1733,plain,(
% 0.11/0.54 ~sP0_prd(sK51_skl,sK48_skl,sK47_skl)|sQ112_spl),
% 0.11/0.54 inference(resolution,[status(thm)],[f1614,f436])).
% 0.11/0.54 fof(f1734,plain,(
% 0.11/0.54 $false|~sQ0_spl|sQ112_spl),
% 0.11/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1733,f513])).
% 0.11/0.54 fof(f1735,plain,(
% 0.11/0.54 ~sQ0_spl|sQ112_spl),
% 0.11/0.54 inference(contradiction_clause,[status(thm)],[f1734])).
% 0.11/0.54 fof(f1736,plain,(
% 0.11/0.54 $false),
% 0.11/0.54 inference(sat_refutation,[status(thm)],[f457,f461,f468,f472,f529,f562,f564,f570,f573,f580,f584,f608,f652,f656,f667,f693,f697,f701,f709,f714,f721,f736,f740,f744,f746,f754,f759,f766,f770,f774,f782,f787,f806,f810,f814,f822,f849,f856,f1018,f1091,f1095,f1099,f1185,f1378,f1383,f1388,f1391,f1410,f1417,f1582,f1599,f1604,f1618,f1635,f1637,f1657,f1664,f1671,f1685,f1692,f1696,f1699,f1735])).
% 0.11/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.35/0.55 % Elapsed time: 0.156339 seconds
% 0.35/0.55 % CPU time: 0.949195 seconds
% 0.35/0.55 % Total memory used: 125.503 MB
% 0.35/0.55 % Net memory used: 124.363 MB
%------------------------------------------------------------------------------