%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC067+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 : n001.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:41:29 PM UTC 2026
% Result : Theorem 0.24s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC067+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n001.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 07:58:43 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 0.24/0.60 % Refutation found
% 0.24/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.24/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.24/0.60 fof(f2,axiom,(
% 0.24/0.60 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f4,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f5,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f6,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f7,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f15,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f16,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f17,axiom,(
% 0.24/0.60 ssList(nil) ),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f26,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f28,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f45,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f51,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.24/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.60 fof(f53,axiom,(
% 0.24/0.60 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( segmentP(U,V)& segmentP(V,W) )=> segmentP(U,W) ) ) )) )) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f54,axiom,(
% 0.24/0.61 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( segmentP(U,V)& segmentP(V,U) )=> U = V ) ) )) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f55,axiom,(
% 0.24/0.61 (! [U] :( ssList(U)=> segmentP(U,U) ) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f56,axiom,(
% 0.24/0.61 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( segmentP(U,V)=> segmentP(app(app(W,U),X),V) ) ) )) )) )) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f57,axiom,(
% 0.24/0.61 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f84,axiom,(
% 0.24/0.61 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f96,conjecture,(
% 0.24/0.61 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(Y,W),Z) != X| ~ strictorderedP(W)| (? [X1] :( ssItem(X1)& (? [X2] :( ssList(X2)& app(X2,cons(X1,nil)) = Y& (? [X3] :( ssItem(X3)& (? [X4] :( ssList(X4)& app(cons(X3,nil),X4) = W& lt(X1,X3) ) )) )) )))| (? [X5] :( ssItem(X5)& (? [X6] :( ssList(X6)& app(cons(X5,nil),X6) = Z& (? [X7] :( ssItem(X7)& (? [X8] :( ssList(X8)& app(X8,cons(X7,nil)) = W& lt(X7,X5) ) )) )) )) )) ) )))| ( nil != X& nil = W )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| (? [X9] :( ssList(X9)& neq(X9,nil)& segmentP(V,X9)& segmentP(U,X9) ) )) ) ) ) )) )) )) )),
% 0.24/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.61 fof(f97,negated_conjecture,(
% 0.24/0.61 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(Y,W),Z) != X| ~ strictorderedP(W)| (? [X1] :( ssItem(X1)& (? [X2] :( ssList(X2)& app(X2,cons(X1,nil)) = Y& (? [X3] :( ssItem(X3)& (? [X4] :( ssList(X4)& app(cons(X3,nil),X4) = W& lt(X1,X3) ) )) )) )))| (? [X5] :( ssItem(X5)& (? [X6] :( ssList(X6)& app(cons(X5,nil),X6) = Z& (? [X7] :( ssItem(X7)& (? [X8] :( ssList(X8)& app(X8,cons(X7,nil)) = W& lt(X7,X5) ) )) )) )) )) ) )))| ( nil != X& nil = W )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| (? [X9] :( ssList(X9)& neq(X9,nil)& segmentP(V,X9)& segmentP(U,X9) ) )) ) ) ) )) )) )) ))),
% 0.24/0.61 inference(negated_conjecture,[status(cth)],[f96])).
% 0.24/0.61 fof(f102,plain,(
% 0.24/0.61 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.24/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.24/0.61 fof(f105,plain,(
% 0.24/0.61 ~sK0_skl=sK1_skl),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f102])).
% 0.24/0.61 fof(f113,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.24/0.61 fof(f114,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.24/0.61 inference(NNF_transformation,[status(thm)],[f113])).
% 0.24/0.61 fof(f115,plain,(
% 0.24/0.61 ![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.24/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 0.24/0.61 fof(f118,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|singletonP(X0)|~ssItem(X1)|~cons(X1,nil)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f115])).
% 0.24/0.61 fof(f119,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.24/0.61 fof(f120,plain,(
% 0.24/0.61 ![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.24/0.61 inference(NNF_transformation,[status(thm)],[f119])).
% 0.24/0.61 fof(f121,plain,(
% 0.24/0.61 ![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.24/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.24/0.61 fof(f123,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f121])).
% 0.24/0.61 fof(f124,plain,(
% 0.24/0.61 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f121])).
% 0.24/0.61 fof(f125,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.24/0.61 fof(f126,plain,(
% 0.24/0.61 ![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.24/0.61 inference(NNF_transformation,[status(thm)],[f125])).
% 0.24/0.61 fof(f127,plain,(
% 0.24/0.61 ![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.24/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.24/0.61 fof(f128,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f127])).
% 0.24/0.61 fof(f129,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f127])).
% 0.24/0.61 fof(f130,plain,(
% 0.24/0.61 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f127])).
% 0.24/0.61 fof(f131,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.24/0.61 fof(f132,plain,(
% 0.24/0.61 ![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.24/0.61 inference(NNF_transformation,[status(thm)],[f131])).
% 0.24/0.61 fof(f133,plain,(
% 0.24/0.61 ![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.24/0.61 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.24/0.61 fof(f134,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f133])).
% 0.24/0.61 fof(f135,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f133])).
% 0.24/0.61 fof(f136,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f133])).
% 0.24/0.61 fof(f137,plain,(
% 0.24/0.61 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f133])).
% 0.24/0.61 fof(f217,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.24/0.61 fof(f218,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 0.24/0.61 inference(NNF_transformation,[status(thm)],[f217])).
% 0.24/0.61 fof(f219,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f218])).
% 0.24/0.61 fof(f220,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X0,X1)|X0=X1)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f218])).
% 0.24/0.61 fof(f221,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.24/0.61 fof(f222,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f221])).
% 0.24/0.61 fof(f223,plain,(
% 0.24/0.61 ssList(nil)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f17])).
% 0.24/0.61 fof(f244,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.24/0.61 fof(f245,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f244])).
% 0.24/0.61 fof(f248,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.24/0.61 fof(f249,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f248])).
% 0.24/0.61 fof(f294,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.24/0.61 fof(f295,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f294])).
% 0.24/0.61 fof(f308,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.24/0.61 fof(f309,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f308])).
% 0.24/0.61 fof(f314,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~segmentP(U,V)|~segmentP(V,W))|segmentP(U,W)))))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.24/0.61 fof(f315,plain,(
% 0.24/0.61 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(X0,X1)|~segmentP(X1,X2)|segmentP(X0,X2))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f314])).
% 0.24/0.61 fof(f316,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|~segmentP(V,U))|U=V))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.24/0.61 fof(f317,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|~segmentP(X1,X0)|X0=X1)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f316])).
% 0.24/0.61 fof(f318,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|segmentP(U,U))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.24/0.61 fof(f319,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f318])).
% 0.24/0.61 fof(f320,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|(~segmentP(U,V)|segmentP(app(app(W,U),X),V)))))))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.24/0.61 fof(f321,plain,(
% 0.24/0.61 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X0,X1)|segmentP(app(app(X2,X0),X3),X1))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f320])).
% 0.24/0.61 fof(f322,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|segmentP(U,nil))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.24/0.61 fof(f323,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f322])).
% 0.24/0.61 fof(f388,plain,(
% 0.24/0.61 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.24/0.61 fof(f389,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f388])).
% 0.24/0.61 fof(f415,plain,(
% 0.24/0.61 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(((app(app(Y,W),Z)=X&strictorderedP(W))&(![X1]: (~ssItem(X1)|(![X2]: ((~ssList(X2)|~app(X2,cons(X1,nil))=Y)|(![X3]: (~ssItem(X3)|(![X4]: ((~ssList(X4)|~app(cons(X3,nil),X4)=W)|~lt(X1,X3))))))))))&(![X5]: (~ssItem(X5)|(![X6]: ((~ssList(X6)|~app(cons(X5,nil),X6)=Z)|(![X7]: (~ssItem(X7)|(![X8]: ((~ssList(X8)|~app(X8,cons(X7,nil))=W)|~lt(X7,X5)))))))))))))))&(nil=X|~nil=W))&((nil=V&~nil=U)|(neq(V,nil)&(![X9]: (((~ssList(X9)|~neq(X9,nil))|~segmentP(V,X9))|~segmentP(U,X9))))))))))))))),
% 0.24/0.61 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.24/0.61 fof(f416,definition,(
% 0.24/0.61 ![U,V]: (sP0_prd(V,U)<=>(nil=V&~nil=U))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.24/0.61 fof(f417,plain,(
% 0.24/0.61 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(((app(app(Y,W),Z)=X&strictorderedP(W))&(![X1]: (~ssItem(X1)|(![X2]: ((~ssList(X2)|~app(X2,cons(X1,nil))=Y)|(![X3]: (~ssItem(X3)|(![X4]: ((~ssList(X4)|~app(cons(X3,nil),X4)=W)|~lt(X1,X3))))))))))&(![X5]: (~ssItem(X5)|(![X6]: ((~ssList(X6)|~app(cons(X5,nil),X6)=Z)|(![X7]: (~ssItem(X7)|(![X8]: ((~ssList(X8)|~app(X8,cons(X7,nil))=W)|~lt(X7,X5)))))))))))))))&(nil=X|~nil=W))&(sP0_prd(V,U)|(neq(V,nil)&(![X9]: (((~ssList(X9)|~neq(X9,nil))|~segmentP(V,X9))|~segmentP(U,X9)))))))))))))),
% 0.24/0.61 inference(formula_renaming,[status(thm)],[f415,f416])).
% 0.24/0.61 fof(f418,plain,(
% 0.24/0.61 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(((app(app(Y,W),Z)=X&strictorderedP(W))&(![X1]: (~ssItem(X1)|((![X2]: (~ssList(X2)|~app(X2,cons(X1,nil))=Y))|(![X3]: (~ssItem(X3)|((![X4]: (~ssList(X4)|~app(cons(X3,nil),X4)=W))|~lt(X1,X3))))))))&(![X5]: (~ssItem(X5)|((![X6]: (~ssList(X6)|~app(cons(X5,nil),X6)=Z))|(![X7]: (~ssItem(X7)|((![X8]: (~ssList(X8)|~app(X8,cons(X7,nil))=W))|~lt(X7,X5)))))))))))))&(nil=X|~nil=W))&(sP0_prd(V,U)|(neq(V,nil)&(![X9]: (((~ssList(X9)|~neq(X9,nil))|~segmentP(V,X9))|~segmentP(U,X9)))))))))))))),
% 0.24/0.61 inference(miniscoping,[status(thm)],[f417])).
% 0.24/0.61 fof(f419,plain,(
% 0.24/0.61 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&((((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(ssList(sK51_skl)&(ssList(sK52_skl)&(((app(app(sK51_skl,sK49_skl),sK52_skl)=sK50_skl&strictorderedP(sK49_skl))&(![X1]: (~ssItem(X1)|((![X2]: (~ssList(X2)|~app(X2,cons(X1,nil))=sK51_skl))|(![X3]: (~ssItem(X3)|((![X4]: (~ssList(X4)|~app(cons(X3,nil),X4)=sK49_skl))|~lt(X1,X3))))))))&(![X5]: (~ssItem(X5)|((![X6]: (~ssList(X6)|~app(cons(X5,nil),X6)=sK52_skl))|(![X7]: (~ssItem(X7)|((![X8]: (~ssList(X8)|~app(X8,cons(X7,nil))=sK49_skl))|~lt(X7,X5)))))))))))&(nil=sK50_skl|~nil=sK49_skl))&(sP0_prd(sK48_skl,sK47_skl)|(neq(sK48_skl,nil)&(![X9]: (((~ssList(X9)|~neq(X9,nil))|~segmentP(sK48_skl,X9))|~segmentP(sK47_skl,X9))))))))))),
% 0.24/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl),skolemize(Z,sK52_skl)],[f418])).
% 0.24/0.61 fof(f420,plain,(
% 0.24/0.61 ssList(sK47_skl)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f423,plain,(
% 0.24/0.61 ssList(sK50_skl)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f424,plain,(
% 0.24/0.61 sK48_skl=sK50_skl),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f425,plain,(
% 0.24/0.61 sK47_skl=sK49_skl),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f426,plain,(
% 0.24/0.61 ssList(sK51_skl)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f427,plain,(
% 0.24/0.61 ssList(sK52_skl)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f428,plain,(
% 0.24/0.61 app(app(sK51_skl,sK49_skl),sK52_skl)=sK50_skl),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f432,plain,(
% 0.24/0.61 nil=sK50_skl|~nil=sK49_skl),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f433,plain,(
% 0.24/0.61 sP0_prd(sK48_skl,sK47_skl)|neq(sK48_skl,nil)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f434,plain,(
% 0.24/0.61 ![X0]: (sP0_prd(sK48_skl,sK47_skl)|~ssList(X0)|~neq(X0,nil)|~segmentP(sK48_skl,X0)|~segmentP(sK47_skl,X0))),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f419])).
% 0.24/0.61 fof(f435,plain,(
% 0.24/0.61 ![U,V]: ((~sP0_prd(V,U)|(nil=V&~nil=U))&(sP0_prd(V,U)|(~nil=V|nil=U)))),
% 0.24/0.61 inference(NNF_transformation,[status(thm)],[f416])).
% 0.24/0.61 fof(f436,plain,(
% 0.24/0.61 (![U,V]: (~sP0_prd(V,U)|(nil=V&~nil=U)))&(![U,V]: (sP0_prd(V,U)|(~nil=V|nil=U)))),
% 0.24/0.61 inference(miniscoping,[status(thm)],[f435])).
% 0.24/0.61 fof(f437,plain,(
% 0.24/0.61 ![X0,X1]: (~sP0_prd(X0,X1)|nil=X0)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f436])).
% 0.24/0.61 fof(f438,plain,(
% 0.24/0.61 ![X0,X1]: (~sP0_prd(X0,X1)|~nil=X1)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f436])).
% 0.24/0.61 fof(f439,plain,(
% 0.24/0.61 ![X0,X1]: (sP0_prd(X0,X1)|~nil=X0|nil=X1)),
% 0.24/0.61 inference(cnf_transformation,[status(thm)],[f436])).
% 0.24/0.61 fof(f440,definition,(
% 0.24/0.61 sQ0_spl <=> (nil=sK50_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f441,plain,(
% 0.24/0.61 nil=sK50_skl|~sQ0_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f440])).
% 0.24/0.61 fof(f443,definition,(
% 0.24/0.61 sQ1_spl <=> (nil=sK49_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f445,plain,(
% 0.24/0.61 ~nil=sK49_skl|sQ1_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f443])).
% 0.24/0.61 fof(f446,plain,(
% 0.24/0.61 sQ0_spl|~sQ1_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f432,f440,f443])).
% 0.24/0.61 fof(f447,definition,(
% 0.24/0.61 sQ2_spl <=> (sP0_prd(sK48_skl,sK47_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f448,plain,(
% 0.24/0.61 sP0_prd(sK48_skl,sK47_skl)|~sQ2_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f447])).
% 0.24/0.61 fof(f450,definition,(
% 0.24/0.61 sQ3_spl <=> (neq(sK48_skl,nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f451,plain,(
% 0.24/0.61 neq(sK48_skl,nil)|~sQ3_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f450])).
% 0.24/0.61 fof(f453,plain,(
% 0.24/0.61 sQ2_spl|sQ3_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f433,f447,f450])).
% 0.24/0.61 fof(f454,definition,(
% 0.24/0.61 ![X0]: (sQ4_spl <=> (~ssList(X0)|~neq(X0,nil)|~segmentP(sK48_skl,X0)|~segmentP(sK47_skl,X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f455,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sK48_skl,X0)|~segmentP(sK47_skl,X0)|~sQ4_spl)),
% 0.24/0.61 inference(component_clause,[status(thm)],[f454])).
% 0.24/0.61 fof(f457,plain,(
% 0.24/0.61 sQ2_spl|sQ4_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f434,f447,f454])).
% 0.24/0.61 fof(f461,plain,(
% 0.24/0.61 ![X0]: (~ssList(cons(X0,nil))|singletonP(cons(X0,nil))|~ssItem(X0))),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.24/0.61 fof(f462,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.24/0.61 fof(f463,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.24/0.61 fof(f464,plain,(
% 0.24/0.61 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 0.24/0.61 fof(f473,plain,(
% 0.24/0.61 ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f219])).
% 0.24/0.61 fof(f474,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 0.24/0.61 inference(duplicate_literals_removal,[status(thm)],[f473])).
% 0.24/0.61 fof(f488,plain,(
% 0.24/0.61 ![X0]: (~sP0_prd(X0,nil))),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f438])).
% 0.24/0.61 fof(f489,plain,(
% 0.24/0.61 ![X0]: (sP0_prd(nil,X0)|nil=X0)),
% 0.24/0.61 inference(destructive_equality_resolution,[status(thm)],[f439])).
% 0.24/0.61 fof(f497,plain,(
% 0.24/0.61 sK48_skl=nil|~sQ0_spl),
% 0.24/0.61 inference(backward_demodulation,[status(thm)],[f441,f424])).
% 0.24/0.61 fof(f499,plain,(
% 0.24/0.61 app(app(sK51_skl,sK47_skl),sK52_skl)=sK50_skl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f425,f428])).
% 0.24/0.61 fof(f500,plain,(
% 0.24/0.61 app(app(sK51_skl,sK47_skl),sK52_skl)=nil|~sQ0_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f441,f499])).
% 0.24/0.61 fof(f501,plain,(
% 0.24/0.61 sP0_prd(nil,sK47_skl)|~sQ0_spl|~sQ2_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f497,f448])).
% 0.24/0.61 fof(f504,definition,(
% 0.24/0.61 sQ5_spl <=> (ssList(nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f506,plain,(
% 0.24/0.61 ~ssList(nil)|sQ5_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f504])).
% 0.24/0.61 fof(f507,definition,(
% 0.24/0.61 sQ6_spl <=> (ssList(sK47_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f509,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|sQ6_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f507])).
% 0.24/0.61 fof(f510,definition,(
% 0.24/0.61 sQ7_spl <=> (segmentP(app(app(sK51_skl,sK47_skl),sK52_skl),sK47_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f511,plain,(
% 0.24/0.61 segmentP(app(app(sK51_skl,sK47_skl),sK52_skl),sK47_skl)|~sQ7_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f510])).
% 0.24/0.61 fof(f513,definition,(
% 0.24/0.61 sQ8_spl <=> (ssList(sK51_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f515,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|sQ8_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f513])).
% 0.24/0.61 fof(f516,definition,(
% 0.24/0.61 sQ9_spl <=> (ssList(sK52_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f518,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|sQ9_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f516])).
% 0.24/0.61 fof(f527,plain,(
% 0.24/0.61 $false|sQ9_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f518,f427])).
% 0.24/0.61 fof(f528,plain,(
% 0.24/0.61 sQ9_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f527])).
% 0.24/0.61 fof(f530,plain,(
% 0.24/0.61 $false|sQ8_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f515,f426])).
% 0.24/0.61 fof(f531,plain,(
% 0.24/0.61 sQ8_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f530])).
% 0.24/0.61 fof(f532,plain,(
% 0.24/0.61 segmentP(nil,sK47_skl)|~sQ0_spl|~sQ7_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f500,f511])).
% 0.24/0.61 fof(f535,plain,(
% 0.24/0.61 ![X0]: (nil=X0|nil=nil)),
% 0.24/0.61 inference(resolution,[status(thm)],[f489,f437])).
% 0.24/0.61 fof(f536,definition,(
% 0.24/0.61 ![X0]: (sQ12_spl <=> (nil=X0))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f537,plain,(
% 0.24/0.61 ![X0]: (nil=X0|~sQ12_spl)),
% 0.24/0.61 inference(component_clause,[status(thm)],[f536])).
% 0.24/0.61 fof(f539,definition,(
% 0.24/0.61 sQ13_spl <=> (nil=nil)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f542,plain,(
% 0.24/0.61 sQ12_spl|sQ13_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f535,f536,f539])).
% 0.24/0.61 fof(f543,plain,(
% 0.24/0.61 ![X0,X1]: (X0=X1|~sQ12_spl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f537,f537])).
% 0.24/0.61 fof(f556,plain,(
% 0.24/0.61 $false|~sQ12_spl),
% 0.24/0.61 inference(backward_subsumption_resolution,[status(thm)],[f105,f543])).
% 0.24/0.61 fof(f557,plain,(
% 0.24/0.61 ~sQ12_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f556])).
% 0.24/0.61 fof(f583,plain,(
% 0.24/0.61 app(nil,sK52_skl)=sK52_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f249,f427])).
% 0.24/0.61 fof(f584,plain,(
% 0.24/0.61 app(nil,sK51_skl)=sK51_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f249,f426])).
% 0.24/0.61 fof(f585,plain,(
% 0.24/0.61 app(nil,nil)=nil),
% 0.24/0.61 inference(resolution,[status(thm)],[f249,f223])).
% 0.24/0.61 fof(f586,plain,(
% 0.24/0.61 app(nil,sK47_skl)=sK47_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f249,f420])).
% 0.24/0.61 fof(f587,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK52_skl,X0))|~ssList(sK52_skl)|segmentP(app(app(nil,sK52_skl),X0),sK52_skl)|~ssList(nil)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f583,f464])).
% 0.24/0.61 fof(f588,definition,(
% 0.24/0.61 ![X0]: (sQ18_spl <=> (~ssList(app(sK52_skl,X0))|segmentP(app(app(nil,sK52_skl),X0),sK52_skl)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f591,plain,(
% 0.24/0.61 sQ18_spl|~sQ9_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f587,f588,f516,f504])).
% 0.24/0.61 fof(f592,plain,(
% 0.24/0.61 $false|sQ5_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f506,f223])).
% 0.24/0.61 fof(f593,plain,(
% 0.24/0.61 sQ5_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f592])).
% 0.24/0.61 fof(f595,plain,(
% 0.24/0.61 $false|sQ6_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f509,f420])).
% 0.24/0.61 fof(f596,plain,(
% 0.24/0.61 sQ6_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f595])).
% 0.24/0.61 fof(f597,plain,(
% 0.24/0.61 ![X0]: (singletonP(cons(X0,nil))|~ssItem(X0)|~ssList(nil)|~ssItem(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f461,f222])).
% 0.24/0.61 fof(f598,definition,(
% 0.24/0.61 ![X0]: (sQ19_spl <=> (singletonP(cons(X0,nil))|~ssItem(X0)|~ssItem(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f601,plain,(
% 0.24/0.61 sQ19_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f597,f598,f504])).
% 0.24/0.61 fof(f604,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f123,f295])).
% 0.24/0.61 fof(f606,definition,(
% 0.24/0.61 ![X0]: (sQ20_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f609,plain,(
% 0.24/0.61 sQ20_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f604,f606,f504])).
% 0.24/0.61 fof(f612,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(sK51_skl)|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(nil)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f584,f464])).
% 0.24/0.61 fof(f613,definition,(
% 0.24/0.61 ![X0]: (sQ21_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f616,plain,(
% 0.24/0.61 sQ21_spl|~sQ8_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f612,f613,f513,f504])).
% 0.24/0.61 fof(f618,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f586,f464])).
% 0.24/0.61 fof(f619,definition,(
% 0.24/0.61 ![X0]: (sQ22_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f622,plain,(
% 0.24/0.61 sQ22_spl|~sQ6_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f618,f619,f507,f504])).
% 0.24/0.61 fof(f625,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f585,f464])).
% 0.24/0.61 fof(f626,definition,(
% 0.24/0.61 ![X0]: (sQ23_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f629,plain,(
% 0.24/0.61 sQ23_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f625,f626,f504])).
% 0.24/0.61 fof(f635,plain,(
% 0.24/0.61 app(sK52_skl,nil)=sK52_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f389,f427])).
% 0.24/0.61 fof(f636,plain,(
% 0.24/0.61 app(sK51_skl,nil)=sK51_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f389,f426])).
% 0.24/0.61 fof(f638,plain,(
% 0.24/0.61 app(sK47_skl,nil)=sK47_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f389,f420])).
% 0.24/0.61 fof(f639,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK52_skl,X0))|~ssList(nil)|segmentP(app(app(sK52_skl,nil),X0),nil)|~ssList(sK52_skl)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f635,f464])).
% 0.24/0.61 fof(f640,definition,(
% 0.24/0.61 ![X0]: (sQ24_spl <=> (~ssList(app(sK52_skl,X0))|segmentP(app(app(sK52_skl,nil),X0),nil)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f643,plain,(
% 0.24/0.61 sQ24_spl|~sQ5_spl|~sQ9_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f639,f640,f504,f516])).
% 0.24/0.61 fof(f645,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(nil)|segmentP(app(app(sK51_skl,nil),X0),nil)|~ssList(sK51_skl)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f636,f464])).
% 0.24/0.61 fof(f646,definition,(
% 0.24/0.61 ![X0]: (sQ25_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(sK51_skl,nil),X0),nil)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f649,plain,(
% 0.24/0.61 sQ25_spl|~sQ5_spl|~sQ8_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f645,f646,f504,f513])).
% 0.24/0.61 fof(f651,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f638,f464])).
% 0.24/0.61 fof(f652,definition,(
% 0.24/0.61 ![X0]: (sQ26_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f655,plain,(
% 0.24/0.61 sQ26_spl|~sQ5_spl|~sQ6_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f651,f652,f504,f507])).
% 0.24/0.61 fof(f677,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f638,f462])).
% 0.24/0.61 fof(f678,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(sK51_skl)|frontsegP(app(sK51_skl,nil),sK51_skl)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f636,f462])).
% 0.24/0.61 fof(f679,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(sK52_skl)|frontsegP(app(sK52_skl,nil),sK52_skl)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f635,f462])).
% 0.24/0.61 fof(f680,plain,(
% 0.24/0.61 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f585,f462])).
% 0.24/0.61 fof(f681,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f586,f462])).
% 0.24/0.61 fof(f682,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(nil)|frontsegP(app(nil,sK51_skl),nil)|~ssList(sK51_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f584,f462])).
% 0.24/0.61 fof(f683,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(nil)|frontsegP(app(nil,sK52_skl),nil)|~ssList(sK52_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f583,f462])).
% 0.24/0.61 fof(f684,definition,(
% 0.24/0.61 sQ27_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f685,plain,(
% 0.24/0.61 frontsegP(app(sK47_skl,nil),sK47_skl)|~sQ27_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f684])).
% 0.24/0.61 fof(f687,plain,(
% 0.24/0.61 ~sQ6_spl|sQ27_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f677,f507,f684,f504])).
% 0.24/0.61 fof(f688,definition,(
% 0.24/0.61 sQ28_spl <=> (frontsegP(app(sK51_skl,nil),sK51_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f689,plain,(
% 0.24/0.61 frontsegP(app(sK51_skl,nil),sK51_skl)|~sQ28_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f688])).
% 0.24/0.61 fof(f691,plain,(
% 0.24/0.61 ~sQ8_spl|sQ28_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f678,f513,f688,f504])).
% 0.24/0.61 fof(f692,definition,(
% 0.24/0.61 sQ29_spl <=> (frontsegP(app(sK52_skl,nil),sK52_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f693,plain,(
% 0.24/0.61 frontsegP(app(sK52_skl,nil),sK52_skl)|~sQ29_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f692])).
% 0.24/0.61 fof(f695,plain,(
% 0.24/0.61 ~sQ9_spl|sQ29_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f679,f516,f692,f504])).
% 0.24/0.61 fof(f696,definition,(
% 0.24/0.61 sQ30_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f697,plain,(
% 0.24/0.61 frontsegP(app(nil,nil),nil)|~sQ30_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f696])).
% 0.24/0.61 fof(f699,plain,(
% 0.24/0.61 ~sQ5_spl|sQ30_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f680,f504,f696])).
% 0.24/0.61 fof(f700,definition,(
% 0.24/0.61 sQ31_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f701,plain,(
% 0.24/0.61 frontsegP(app(nil,sK47_skl),nil)|~sQ31_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f700])).
% 0.24/0.61 fof(f703,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|sQ31_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f681,f507,f504,f700])).
% 0.24/0.61 fof(f704,definition,(
% 0.24/0.61 sQ32_spl <=> (frontsegP(app(nil,sK51_skl),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f705,plain,(
% 0.24/0.61 frontsegP(app(nil,sK51_skl),nil)|~sQ32_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f704])).
% 0.24/0.61 fof(f707,plain,(
% 0.24/0.61 ~sQ8_spl|~sQ5_spl|sQ32_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f682,f513,f504,f704])).
% 0.24/0.61 fof(f708,definition,(
% 0.24/0.61 sQ33_spl <=> (frontsegP(app(nil,sK52_skl),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f709,plain,(
% 0.24/0.61 frontsegP(app(nil,sK52_skl),nil)|~sQ33_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f708])).
% 0.24/0.61 fof(f711,plain,(
% 0.24/0.61 ~sQ9_spl|~sQ5_spl|sQ33_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f683,f516,f504,f708])).
% 0.24/0.61 fof(f712,plain,(
% 0.24/0.61 frontsegP(sK52_skl,sK52_skl)|~sQ29_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f635,f693])).
% 0.24/0.61 fof(f713,plain,(
% 0.24/0.61 frontsegP(sK52_skl,nil)|~sQ33_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f583,f709])).
% 0.24/0.61 fof(f714,plain,(
% 0.24/0.61 frontsegP(sK51_skl,sK51_skl)|~sQ28_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f636,f689])).
% 0.24/0.61 fof(f715,plain,(
% 0.24/0.61 frontsegP(sK51_skl,nil)|~sQ32_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f584,f705])).
% 0.24/0.61 fof(f716,plain,(
% 0.24/0.61 frontsegP(sK47_skl,sK47_skl)|~sQ27_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f638,f685])).
% 0.24/0.61 fof(f717,plain,(
% 0.24/0.61 frontsegP(nil,nil)|~sQ30_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f585,f697])).
% 0.24/0.61 fof(f718,plain,(
% 0.24/0.61 frontsegP(sK47_skl,nil)|~sQ31_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f586,f701])).
% 0.24/0.61 fof(f719,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK6_skl(nil,X0))|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f128,f309])).
% 0.24/0.61 fof(f721,definition,(
% 0.24/0.61 ![X0]: (sQ34_spl <=> (~ssList(X0)|ssList(sK6_skl(nil,X0))|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f724,plain,(
% 0.24/0.61 sQ34_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f719,f721,f504])).
% 0.24/0.61 fof(f727,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f129,f309])).
% 0.24/0.61 fof(f729,definition,(
% 0.24/0.61 ![X0]: (sQ35_spl <=> (~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f732,plain,(
% 0.24/0.61 sQ35_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f727,f729,f504])).
% 0.24/0.61 fof(f735,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(sK52_skl)|app(sK52_skl,sK5_skl(sK52_skl,sK52_skl))=sK52_skl|~sQ29_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f712,f123])).
% 0.24/0.61 fof(f736,definition,(
% 0.24/0.61 sQ36_spl <=> (app(sK52_skl,sK5_skl(sK52_skl,sK52_skl))=sK52_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f739,plain,(
% 0.24/0.61 ~sQ9_spl|sQ36_spl|~sQ29_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f735,f516,f736,f692])).
% 0.24/0.61 fof(f740,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK52_skl))=sK52_skl|~sQ33_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f713,f123])).
% 0.24/0.61 fof(f741,definition,(
% 0.24/0.61 sQ37_spl <=> (app(nil,sK5_skl(nil,sK52_skl))=sK52_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f744,plain,(
% 0.24/0.61 ~sQ9_spl|~sQ5_spl|sQ37_spl|~sQ33_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f740,f516,f504,f741,f708])).
% 0.24/0.61 fof(f745,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(sK51_skl)|app(sK51_skl,sK5_skl(sK51_skl,sK51_skl))=sK51_skl|~sQ28_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f714,f123])).
% 0.24/0.61 fof(f746,definition,(
% 0.24/0.61 sQ38_spl <=> (app(sK51_skl,sK5_skl(sK51_skl,sK51_skl))=sK51_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f749,plain,(
% 0.24/0.61 ~sQ8_spl|sQ38_spl|~sQ28_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f745,f513,f746,f688])).
% 0.24/0.61 fof(f759,plain,(
% 0.24/0.61 ~nil=sK47_skl|sQ1_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f425,f445])).
% 0.24/0.61 fof(f762,plain,(
% 0.24/0.61 app(sK50_skl,nil)=sK50_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f423,f389])).
% 0.24/0.61 fof(f763,plain,(
% 0.24/0.61 app(nil,sK50_skl)=sK50_skl),
% 0.24/0.61 inference(resolution,[status(thm)],[f423,f249])).
% 0.24/0.61 fof(f764,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK51_skl))=sK51_skl|~sQ32_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f715,f123])).
% 0.24/0.61 fof(f765,definition,(
% 0.24/0.61 sQ40_spl <=> (app(nil,sK5_skl(nil,sK51_skl))=sK51_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f768,plain,(
% 0.24/0.61 ~sQ8_spl|~sQ5_spl|sQ40_spl|~sQ32_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f764,f513,f504,f765,f704])).
% 0.24/0.61 fof(f769,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ27_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f716,f123])).
% 0.24/0.61 fof(f770,definition,(
% 0.24/0.61 sQ41_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f773,plain,(
% 0.24/0.61 ~sQ6_spl|sQ41_spl|~sQ27_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f769,f507,f770,f684])).
% 0.24/0.61 fof(f778,plain,(
% 0.24/0.61 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ30_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f717,f123])).
% 0.24/0.61 fof(f779,definition,(
% 0.24/0.61 sQ42_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f782,plain,(
% 0.24/0.61 ~sQ5_spl|sQ42_spl|~sQ30_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f778,f504,f779,f696])).
% 0.24/0.61 fof(f783,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ31_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f718,f123])).
% 0.24/0.61 fof(f784,definition,(
% 0.24/0.61 sQ43_spl <=> (app(nil,sK5_skl(nil,sK47_skl))=sK47_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f787,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|sQ43_spl|~sQ31_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f783,f507,f504,f784,f700])).
% 0.24/0.61 fof(f788,plain,(
% 0.24/0.61 sP0_prd(sK50_skl,sK47_skl)|~sQ2_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f424,f448])).
% 0.24/0.61 fof(f789,plain,(
% 0.24/0.61 nil=sK50_skl|~sQ2_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f788,f437])).
% 0.24/0.61 fof(f790,plain,(
% 0.24/0.61 sQ0_spl|~sQ2_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f789,f440,f447])).
% 0.24/0.61 fof(f795,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|rearsegP(app(sK47_skl,nil),nil)|~ssList(sK47_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f638,f463])).
% 0.24/0.61 fof(f796,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(nil)|rearsegP(app(sK51_skl,nil),nil)|~ssList(sK51_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f636,f463])).
% 0.24/0.61 fof(f797,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(nil)|rearsegP(app(sK52_skl,nil),nil)|~ssList(sK52_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f635,f463])).
% 0.24/0.61 fof(f798,plain,(
% 0.24/0.61 ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f585,f463])).
% 0.24/0.61 fof(f799,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(sK47_skl)|rearsegP(app(nil,sK47_skl),sK47_skl)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f586,f463])).
% 0.24/0.61 fof(f800,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(sK51_skl)|rearsegP(app(nil,sK51_skl),sK51_skl)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f584,f463])).
% 0.24/0.61 fof(f801,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(sK52_skl)|rearsegP(app(nil,sK52_skl),sK52_skl)|~ssList(nil)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f583,f463])).
% 0.24/0.61 fof(f802,definition,(
% 0.24/0.61 sQ44_spl <=> (rearsegP(app(sK47_skl,nil),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f803,plain,(
% 0.24/0.61 rearsegP(app(sK47_skl,nil),nil)|~sQ44_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f802])).
% 0.24/0.61 fof(f805,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|sQ44_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f795,f507,f504,f802])).
% 0.24/0.61 fof(f806,definition,(
% 0.24/0.61 sQ45_spl <=> (rearsegP(app(sK51_skl,nil),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f807,plain,(
% 0.24/0.61 rearsegP(app(sK51_skl,nil),nil)|~sQ45_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f806])).
% 0.24/0.61 fof(f809,plain,(
% 0.24/0.61 ~sQ8_spl|~sQ5_spl|sQ45_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f796,f513,f504,f806])).
% 0.24/0.61 fof(f810,definition,(
% 0.24/0.61 sQ46_spl <=> (rearsegP(app(sK52_skl,nil),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f811,plain,(
% 0.24/0.61 rearsegP(app(sK52_skl,nil),nil)|~sQ46_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f810])).
% 0.24/0.61 fof(f813,plain,(
% 0.24/0.61 ~sQ9_spl|~sQ5_spl|sQ46_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f797,f516,f504,f810])).
% 0.24/0.61 fof(f814,definition,(
% 0.24/0.61 sQ47_spl <=> (rearsegP(app(nil,nil),nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f815,plain,(
% 0.24/0.61 rearsegP(app(nil,nil),nil)|~sQ47_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f814])).
% 0.24/0.61 fof(f817,plain,(
% 0.24/0.61 ~sQ5_spl|sQ47_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f798,f504,f814])).
% 0.24/0.61 fof(f818,definition,(
% 0.24/0.61 sQ48_spl <=> (rearsegP(app(nil,sK47_skl),sK47_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f819,plain,(
% 0.24/0.61 rearsegP(app(nil,sK47_skl),sK47_skl)|~sQ48_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f818])).
% 0.24/0.61 fof(f821,plain,(
% 0.24/0.61 ~sQ6_spl|sQ48_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f799,f507,f818,f504])).
% 0.24/0.61 fof(f822,definition,(
% 0.24/0.61 sQ49_spl <=> (rearsegP(app(nil,sK51_skl),sK51_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f823,plain,(
% 0.24/0.61 rearsegP(app(nil,sK51_skl),sK51_skl)|~sQ49_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f822])).
% 0.24/0.61 fof(f825,plain,(
% 0.24/0.61 ~sQ8_spl|sQ49_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f800,f513,f822,f504])).
% 0.24/0.61 fof(f826,definition,(
% 0.24/0.61 sQ50_spl <=> (rearsegP(app(nil,sK52_skl),sK52_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f827,plain,(
% 0.24/0.61 rearsegP(app(nil,sK52_skl),sK52_skl)|~sQ50_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f826])).
% 0.24/0.61 fof(f829,plain,(
% 0.24/0.61 ~sQ9_spl|sQ50_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f801,f516,f826,f504])).
% 0.24/0.61 fof(f830,plain,(
% 0.24/0.61 rearsegP(sK52_skl,nil)|~sQ46_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f635,f811])).
% 0.24/0.61 fof(f831,plain,(
% 0.24/0.61 rearsegP(sK52_skl,sK52_skl)|~sQ50_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f583,f827])).
% 0.24/0.61 fof(f832,plain,(
% 0.24/0.61 rearsegP(sK51_skl,nil)|~sQ45_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f636,f807])).
% 0.24/0.61 fof(f833,plain,(
% 0.24/0.61 rearsegP(sK51_skl,sK51_skl)|~sQ49_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f584,f823])).
% 0.24/0.61 fof(f834,plain,(
% 0.24/0.61 rearsegP(sK47_skl,nil)|~sQ44_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f638,f803])).
% 0.24/0.61 fof(f835,plain,(
% 0.24/0.61 rearsegP(nil,nil)|~sQ47_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f585,f815])).
% 0.24/0.61 fof(f836,plain,(
% 0.24/0.61 rearsegP(sK47_skl,sK47_skl)|~sQ48_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f586,f819])).
% 0.24/0.61 fof(f838,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK7_skl(nil,X0))|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f134,f323])).
% 0.24/0.61 fof(f844,definition,(
% 0.24/0.61 ![X0]: (sQ52_spl <=> (~ssList(X0)|ssList(sK7_skl(nil,X0))|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f847,plain,(
% 0.24/0.61 sQ52_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f838,f844,f504])).
% 0.24/0.61 fof(f850,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK8_skl(nil,X0))|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f135,f323])).
% 0.24/0.61 fof(f852,definition,(
% 0.24/0.61 ![X0]: (sQ53_spl <=> (~ssList(X0)|ssList(sK8_skl(nil,X0))|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f855,plain,(
% 0.24/0.61 sQ53_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f850,f852,f504])).
% 0.24/0.61 fof(f862,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(nil)|app(sK6_skl(nil,sK52_skl),nil)=sK52_skl|~sQ46_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f830,f129])).
% 0.24/0.61 fof(f863,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK52_skl))|~sQ46_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f830,f128])).
% 0.24/0.61 fof(f864,definition,(
% 0.24/0.61 sQ54_spl <=> (app(sK6_skl(nil,sK52_skl),nil)=sK52_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f867,plain,(
% 0.24/0.61 ~sQ9_spl|~sQ5_spl|sQ54_spl|~sQ46_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f862,f516,f504,f864,f810])).
% 0.24/0.61 fof(f868,definition,(
% 0.24/0.61 sQ55_spl <=> (ssList(sK6_skl(nil,sK52_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f871,plain,(
% 0.24/0.61 ~sQ9_spl|~sQ5_spl|sQ55_spl|~sQ46_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f863,f516,f504,f868,f810])).
% 0.24/0.61 fof(f872,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(sK52_skl)|app(sK6_skl(sK52_skl,sK52_skl),sK52_skl)=sK52_skl|~sQ50_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f831,f129])).
% 0.24/0.61 fof(f873,plain,(
% 0.24/0.61 ~ssList(sK52_skl)|~ssList(sK52_skl)|ssList(sK6_skl(sK52_skl,sK52_skl))|~sQ50_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f831,f128])).
% 0.24/0.61 fof(f874,definition,(
% 0.24/0.61 sQ56_spl <=> (app(sK6_skl(sK52_skl,sK52_skl),sK52_skl)=sK52_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f877,plain,(
% 0.24/0.61 ~sQ9_spl|sQ56_spl|~sQ50_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f872,f516,f874,f826])).
% 0.24/0.61 fof(f878,definition,(
% 0.24/0.61 sQ57_spl <=> (ssList(sK6_skl(sK52_skl,sK52_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f881,plain,(
% 0.24/0.61 ~sQ9_spl|sQ57_spl|~sQ50_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f873,f516,f878,f826])).
% 0.24/0.61 fof(f882,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(nil)|app(sK6_skl(nil,sK51_skl),nil)=sK51_skl|~sQ45_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f832,f129])).
% 0.24/0.61 fof(f883,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK51_skl))|~sQ45_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f832,f128])).
% 0.24/0.61 fof(f884,definition,(
% 0.24/0.61 sQ58_spl <=> (app(sK6_skl(nil,sK51_skl),nil)=sK51_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f887,plain,(
% 0.24/0.61 ~sQ8_spl|~sQ5_spl|sQ58_spl|~sQ45_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f882,f513,f504,f884,f806])).
% 0.24/0.61 fof(f888,definition,(
% 0.24/0.61 sQ59_spl <=> (ssList(sK6_skl(nil,sK51_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f891,plain,(
% 0.24/0.61 ~sQ8_spl|~sQ5_spl|sQ59_spl|~sQ45_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f883,f513,f504,f888,f806])).
% 0.24/0.61 fof(f892,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(sK51_skl)|app(sK6_skl(sK51_skl,sK51_skl),sK51_skl)=sK51_skl|~sQ49_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f833,f129])).
% 0.24/0.61 fof(f893,plain,(
% 0.24/0.61 ~ssList(sK51_skl)|~ssList(sK51_skl)|ssList(sK6_skl(sK51_skl,sK51_skl))|~sQ49_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f833,f128])).
% 0.24/0.61 fof(f894,definition,(
% 0.24/0.61 sQ60_spl <=> (app(sK6_skl(sK51_skl,sK51_skl),sK51_skl)=sK51_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f897,plain,(
% 0.24/0.61 ~sQ8_spl|sQ60_spl|~sQ49_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f892,f513,f894,f822])).
% 0.24/0.61 fof(f898,definition,(
% 0.24/0.61 sQ61_spl <=> (ssList(sK6_skl(sK51_skl,sK51_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f901,plain,(
% 0.24/0.61 ~sQ8_spl|sQ61_spl|~sQ49_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f893,f513,f898,f822])).
% 0.24/0.61 fof(f902,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|app(sK6_skl(nil,sK47_skl),nil)=sK47_skl|~sQ44_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f834,f129])).
% 0.24/0.61 fof(f903,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK47_skl))|~sQ44_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f834,f128])).
% 0.24/0.61 fof(f904,definition,(
% 0.24/0.61 sQ62_spl <=> (app(sK6_skl(nil,sK47_skl),nil)=sK47_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f907,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|sQ62_spl|~sQ44_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f902,f507,f504,f904,f802])).
% 0.24/0.61 fof(f908,definition,(
% 0.24/0.61 sQ63_spl <=> (ssList(sK6_skl(nil,sK47_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f911,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|sQ63_spl|~sQ44_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f903,f507,f504,f908,f802])).
% 0.24/0.61 fof(f914,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|ssList(app(X0,sK50_skl)))),
% 0.24/0.61 inference(resolution,[status(thm)],[f245,f423])).
% 0.24/0.61 fof(f919,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|ssList(app(X0,sK52_skl)))),
% 0.24/0.61 inference(resolution,[status(thm)],[f245,f427])).
% 0.24/0.61 fof(f920,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|ssList(app(X0,sK51_skl)))),
% 0.24/0.61 inference(resolution,[status(thm)],[f245,f426])).
% 0.24/0.61 fof(f925,plain,(
% 0.24/0.61 ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil|~sQ47_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f835,f129])).
% 0.24/0.61 fof(f926,plain,(
% 0.24/0.61 ~ssList(nil)|~ssList(nil)|ssList(sK6_skl(nil,nil))|~sQ47_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f835,f128])).
% 0.24/0.61 fof(f927,definition,(
% 0.24/0.61 sQ64_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f930,plain,(
% 0.24/0.61 ~sQ5_spl|sQ64_spl|~sQ47_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f925,f504,f927,f814])).
% 0.24/0.61 fof(f931,definition,(
% 0.24/0.61 sQ65_spl <=> (ssList(sK6_skl(nil,nil)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f934,plain,(
% 0.24/0.61 ~sQ5_spl|sQ65_spl|~sQ47_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f926,f504,f931,f814])).
% 0.24/0.61 fof(f935,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl|~sQ48_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f836,f129])).
% 0.24/0.61 fof(f936,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(sK47_skl)|ssList(sK6_skl(sK47_skl,sK47_skl))|~sQ48_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f836,f128])).
% 0.24/0.61 fof(f937,definition,(
% 0.24/0.61 sQ66_spl <=> (app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f940,plain,(
% 0.24/0.61 ~sQ6_spl|sQ66_spl|~sQ48_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f935,f507,f937,f818])).
% 0.24/0.61 fof(f941,definition,(
% 0.24/0.61 sQ67_spl <=> (ssList(sK6_skl(sK47_skl,sK47_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f944,plain,(
% 0.24/0.61 ~sQ6_spl|sQ67_spl|~sQ48_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f936,f507,f941,f818])).
% 0.24/0.61 fof(f945,plain,(
% 0.24/0.61 neq(sK50_skl,nil)|~sQ3_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f424,f451])).
% 0.24/0.61 fof(f947,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK50_skl,X0))|~ssList(nil)|segmentP(app(app(sK50_skl,nil),X0),nil)|~ssList(sK50_skl)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f762,f464])).
% 0.24/0.61 fof(f948,definition,(
% 0.24/0.61 ![X0]: (sQ68_spl <=> (~ssList(app(sK50_skl,X0))|segmentP(app(app(sK50_skl,nil),X0),nil)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f951,definition,(
% 0.24/0.61 sQ69_spl <=> (ssList(sK50_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f953,plain,(
% 0.24/0.61 ~ssList(sK50_skl)|sQ69_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f951])).
% 0.24/0.61 fof(f954,plain,(
% 0.24/0.61 sQ68_spl|~sQ5_spl|~sQ69_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f947,f948,f504,f951])).
% 0.24/0.61 fof(f956,plain,(
% 0.24/0.61 ![X0]: (~ssList(app(sK50_skl,X0))|~ssList(sK50_skl)|segmentP(app(app(nil,sK50_skl),X0),sK50_skl)|~ssList(nil)|~ssList(X0))),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f763,f464])).
% 0.24/0.61 fof(f957,definition,(
% 0.24/0.61 ![X0]: (sQ70_spl <=> (~ssList(app(sK50_skl,X0))|segmentP(app(app(nil,sK50_skl),X0),sK50_skl)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f960,plain,(
% 0.24/0.61 sQ70_spl|~sQ69_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f956,f957,f951,f504])).
% 0.24/0.61 fof(f961,plain,(
% 0.24/0.61 $false|sQ69_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f953,f423])).
% 0.24/0.61 fof(f962,plain,(
% 0.24/0.61 sQ69_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f961])).
% 0.24/0.61 fof(f964,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f136,f323])).
% 0.24/0.61 fof(f966,definition,(
% 0.24/0.61 ![X0]: (sQ71_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f969,plain,(
% 0.24/0.61 sQ71_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f964,f966,f504])).
% 0.24/0.61 fof(f978,plain,(
% 0.24/0.61 ~ssList(sK50_skl)|~ssList(sK47_skl)|segmentP(app(app(sK51_skl,sK47_skl),sK52_skl),sK47_skl)|~ssList(sK51_skl)|~ssList(sK52_skl)),
% 0.24/0.61 inference(paramodulation,[status(thm)],[f499,f464])).
% 0.24/0.61 fof(f980,plain,(
% 0.24/0.61 ~sQ69_spl|~sQ6_spl|sQ7_spl|~sQ8_spl|~sQ9_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f978,f951,f507,f510,f513,f516])).
% 0.24/0.61 fof(f985,plain,(
% 0.24/0.61 segmentP(sK50_skl,sK47_skl)|~sQ7_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f499,f511])).
% 0.24/0.61 fof(f986,plain,(
% 0.24/0.61 ~ssList(sK50_skl)|~ssList(sK47_skl)|app(app(sK7_skl(sK47_skl,sK50_skl),sK47_skl),sK8_skl(sK47_skl,sK50_skl))=sK50_skl|~sQ7_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f985,f136])).
% 0.24/0.61 fof(f987,plain,(
% 0.24/0.61 ~ssList(sK50_skl)|~ssList(sK47_skl)|ssList(sK8_skl(sK47_skl,sK50_skl))|~sQ7_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f985,f135])).
% 0.24/0.61 fof(f988,plain,(
% 0.24/0.61 ~ssList(sK50_skl)|~ssList(sK47_skl)|ssList(sK7_skl(sK47_skl,sK50_skl))|~sQ7_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f985,f134])).
% 0.24/0.61 fof(f989,definition,(
% 0.24/0.61 sQ73_spl <=> (app(app(sK7_skl(sK47_skl,sK50_skl),sK47_skl),sK8_skl(sK47_skl,sK50_skl))=sK50_skl)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f992,plain,(
% 0.24/0.61 ~sQ69_spl|~sQ6_spl|sQ73_spl|~sQ7_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f986,f951,f507,f989,f510])).
% 0.24/0.61 fof(f993,definition,(
% 0.24/0.61 sQ74_spl <=> (ssList(sK8_skl(sK47_skl,sK50_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f996,plain,(
% 0.24/0.61 ~sQ69_spl|~sQ6_spl|sQ74_spl|~sQ7_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f987,f951,f507,f993,f510])).
% 0.24/0.61 fof(f997,definition,(
% 0.24/0.61 sQ75_spl <=> (ssList(sK7_skl(sK47_skl,sK50_skl)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1000,plain,(
% 0.24/0.61 ~sQ69_spl|~sQ6_spl|sQ75_spl|~sQ7_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f988,f951,f507,f997,f510])).
% 0.24/0.61 fof(f1077,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK50_skl),X1)|~ssList(X0)|~ssList(sK50_skl))),
% 0.24/0.61 inference(resolution,[status(thm)],[f914,f464])).
% 0.24/0.61 fof(f1084,definition,(
% 0.24/0.61 ![X0,X1]: (sQ76_spl <=> (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK50_skl),X1)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1087,plain,(
% 0.24/0.61 sQ76_spl|~sQ69_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1077,f1084,f951])).
% 0.24/0.61 fof(f1090,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK52_skl),X1)|~ssList(X0)|~ssList(sK52_skl))),
% 0.24/0.61 inference(resolution,[status(thm)],[f919,f464])).
% 0.24/0.61 fof(f1098,definition,(
% 0.24/0.61 ![X0,X1]: (sQ77_spl <=> (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK52_skl),X1)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1101,plain,(
% 0.24/0.61 sQ77_spl|~sQ9_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1090,f1098,f516])).
% 0.24/0.61 fof(f1105,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK51_skl),X1)|~ssList(X0)|~ssList(sK51_skl))),
% 0.24/0.61 inference(resolution,[status(thm)],[f920,f464])).
% 0.24/0.61 fof(f1112,definition,(
% 0.24/0.61 ![X0,X1]: (sQ78_spl <=> (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK51_skl),X1)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1115,plain,(
% 0.24/0.61 sQ78_spl|~sQ8_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1105,f1112,f513])).
% 0.24/0.61 fof(f1118,plain,(
% 0.24/0.61 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sK50_skl,X0)|~segmentP(sK47_skl,X0)|~sQ4_spl)),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f424,f455])).
% 0.24/0.61 fof(f1120,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~neq(sK47_skl,nil)|~segmentP(sK50_skl,sK47_skl)|~ssList(sK47_skl)|~sQ4_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f1118,f319])).
% 0.24/0.61 fof(f1128,definition,(
% 0.24/0.61 sQ81_spl <=> (neq(sK47_skl,nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1130,plain,(
% 0.24/0.61 ~neq(sK47_skl,nil)|sQ81_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f1128])).
% 0.24/0.61 fof(f1131,definition,(
% 0.24/0.61 sQ82_spl <=> (segmentP(sK50_skl,sK47_skl))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1133,plain,(
% 0.24/0.61 ~segmentP(sK50_skl,sK47_skl)|sQ82_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f1131])).
% 0.24/0.61 fof(f1134,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ81_spl|~sQ82_spl|~sQ4_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1120,f507,f1128,f1131,f454])).
% 0.24/0.61 fof(f1137,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|sK47_skl=nil|sQ81_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f1130,f220])).
% 0.24/0.61 fof(f1138,definition,(
% 0.24/0.61 sQ83_spl <=> (sK47_skl=nil)),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1139,plain,(
% 0.24/0.61 sK47_skl=nil|~sQ83_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f1138])).
% 0.24/0.61 fof(f1141,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|sQ83_spl|sQ81_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1137,f507,f504,f1138,f1128])).
% 0.24/0.61 fof(f1142,plain,(
% 0.24/0.61 $false|~sQ7_spl|sQ82_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f1133,f985])).
% 0.24/0.61 fof(f1143,plain,(
% 0.24/0.61 ~sQ7_spl|sQ82_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f1142])).
% 0.24/0.61 fof(f1178,plain,(
% 0.24/0.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1))),
% 0.24/0.61 inference(resolution,[status(thm)],[f315,f323])).
% 0.24/0.61 fof(f1180,definition,(
% 0.24/0.61 ![X0,X1]: (sQ84_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1183,plain,(
% 0.24/0.61 sQ84_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1178,f1180,f504])).
% 0.24/0.61 fof(f1185,plain,(
% 0.24/0.61 ![X0]: (~ssList(nil)|~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f317,f323])).
% 0.24/0.61 fof(f1187,definition,(
% 0.24/0.61 ![X0]: (sQ85_spl <=> (~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1190,plain,(
% 0.24/0.61 ~sQ5_spl|sQ85_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1185,f504,f1187])).
% 0.24/0.61 fof(f1197,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|~ssList(nil)|~segmentP(sK47_skl,nil)|sK47_skl=nil|~sQ0_spl|~sQ7_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f532,f317])).
% 0.24/0.61 fof(f1202,definition,(
% 0.24/0.61 sQ86_spl <=> (segmentP(sK47_skl,nil))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1204,plain,(
% 0.24/0.61 ~segmentP(sK47_skl,nil)|sQ86_spl),
% 0.24/0.61 inference(component_clause,[status(thm)],[f1202])).
% 0.24/0.61 fof(f1205,plain,(
% 0.24/0.61 ~sQ6_spl|~sQ5_spl|~sQ86_spl|sQ83_spl|~sQ0_spl|~sQ7_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1197,f507,f504,f1202,f1138,f440,f510])).
% 0.24/0.61 fof(f1330,plain,(
% 0.24/0.61 ~ssList(sK47_skl)|sQ86_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f1204,f323])).
% 0.24/0.61 fof(f1331,plain,(
% 0.24/0.61 ~sQ6_spl|sQ86_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1330,f507,f1202])).
% 0.24/0.61 fof(f1332,plain,(
% 0.24/0.61 ~sQ83_spl|sQ1_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f759,f1138,f443])).
% 0.24/0.61 fof(f1334,plain,(
% 0.24/0.61 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X0),X2),nil)|~ssList(X0))),
% 0.24/0.61 inference(resolution,[status(thm)],[f321,f323])).
% 0.24/0.61 fof(f1336,definition,(
% 0.24/0.61 ![X0,X1,X2]: (sQ108_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X0),X2),nil)|~ssList(X0)))),
% 0.24/0.61 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.24/0.61 fof(f1339,plain,(
% 0.24/0.61 sQ108_spl|~sQ5_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1334,f1336,f504])).
% 0.24/0.61 fof(f1426,plain,(
% 0.24/0.61 sP0_prd(nil,nil)|~sQ83_spl|~sQ0_spl|~sQ2_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f1139,f501])).
% 0.24/0.61 fof(f1427,plain,(
% 0.24/0.61 $false|~sQ83_spl|~sQ0_spl|~sQ2_spl),
% 0.24/0.61 inference(forward_subsumption_resolution,[status(thm)],[f1426,f488])).
% 0.24/0.61 fof(f1428,plain,(
% 0.24/0.61 ~sQ83_spl|~sQ0_spl|~sQ2_spl),
% 0.24/0.61 inference(contradiction_clause,[status(thm)],[f1427])).
% 0.24/0.61 fof(f1429,plain,(
% 0.24/0.61 neq(nil,nil)|~sQ0_spl|~sQ3_spl),
% 0.24/0.61 inference(forward_demodulation,[status(thm)],[f441,f945])).
% 0.24/0.61 fof(f1440,plain,(
% 0.24/0.61 ~ssList(nil)|~sQ0_spl|~sQ3_spl),
% 0.24/0.61 inference(resolution,[status(thm)],[f1429,f474])).
% 0.24/0.61 fof(f1441,plain,(
% 0.24/0.61 ~sQ5_spl|~sQ0_spl|~sQ3_spl),
% 0.24/0.61 inference(split_clause,[status(thm)],[f1440,f504,f440,f450])).
% 0.24/0.61 fof(f1442,plain,(
% 0.24/0.61 $false),
% 0.24/0.61 inference(sat_refutation,[status(thm)],[f446,f453,f457,f528,f531,f542,f557,f591,f593,f596,f601,f609,f616,f622,f629,f643,f649,f655,f687,f691,f695,f699,f703,f707,f711,f724,f732,f739,f744,f749,f768,f773,f782,f787,f790,f805,f809,f813,f817,f821,f825,f829,f847,f855,f867,f871,f877,f881,f887,f891,f897,f901,f907,f911,f930,f934,f940,f944,f954,f960,f962,f969,f980,f992,f996,f1000,f1087,f1101,f1115,f1134,f1141,f1143,f1183,f1190,f1205,f1331,f1332,f1339,f1428,f1441])).
% 0.24/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.64 % Elapsed time: 0.181391 seconds
% 0.24/0.64 % CPU time: 0.780129 seconds
% 0.24/0.64 % Total memory used: 93.037 MB
% 0.24/0.64 % Net memory used: 92.521 MB
%------------------------------------------------------------------------------