%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC110+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:37 PM UTC 2026
% Result : Theorem 1.44s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC110+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 07:51:13 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 1.44/0.77 % Refutation found
% 1.44/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.44/0.77 % SZS output start CNFRefutation for theBenchmark
% 1.44/0.77 fof(f1,axiom,(
% 1.44/0.77 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f2,axiom,(
% 1.44/0.77 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f5,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f7,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f15,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f16,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f17,axiom,(
% 1.44/0.77 ssList(nil) ),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f19,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssItem(X)=> ( cons(W,U) = cons(X,V)=> ( W = X& V = U ) ) ) )) )) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f26,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f28,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f53,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( segmentP(U,V)& segmentP(V,W) )=> segmentP(U,W) ) ) )) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f54,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( segmentP(U,V)& segmentP(V,U) )=> U = V ) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f55,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> segmentP(U,U) ) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f57,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f58,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> ( segmentP(nil,U)<=> nil = U ) ) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f79,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(W,V) = app(U,V)=> W = U ) ) )) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f80,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(V,W) = app(V,U)=> W = U ) ) )) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f81,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> cons(V,U) = app(cons(V,nil),U) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f83,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( nil = app(U,V)<=> ( nil = V& nil = U ) ) ) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f84,axiom,(
% 1.44/0.77 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f96,conjecture,(
% 1.44/0.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssList(Y)=> ( app(W,Y) != X| ~ equalelemsP(W)| (? [Z] :( ssItem(Z)& (? [X1] :( ssList(X1)& app(cons(Z,nil),X1) = Y& (? [X2] :( ssList(X2)& app(X2,cons(Z,nil)) = W ) )) )) )) ))| ( nil != X& nil = W )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| ( neq(U,nil)& segmentP(V,U) ) ) ) ) ) )) )) )) )),
% 1.44/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.44/0.77 fof(f97,negated_conjecture,(
% 1.44/0.77 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssList(Y)=> ( app(W,Y) != X| ~ equalelemsP(W)| (? [Z] :( ssItem(Z)& (? [X1] :( ssList(X1)& app(cons(Z,nil),X1) = Y& (? [X2] :( ssList(X2)& app(X2,cons(Z,nil)) = W ) )) )) )) ))| ( nil != X& nil = W )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| ( neq(U,nil)& segmentP(V,U) ) ) ) ) ) )) )) )) ))),
% 1.44/0.77 inference(negated_conjecture,[status(cth)],[f96])).
% 1.44/0.77 fof(f98,plain,(
% 1.44/0.77 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(neq(U,V)<=>~U=V))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 1.44/0.77 fof(f99,plain,(
% 1.44/0.77 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f98])).
% 1.44/0.77 fof(f100,plain,(
% 1.44/0.77 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~neq(X0,X1)|~X0=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f99])).
% 1.44/0.77 fof(f101,plain,(
% 1.44/0.77 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|neq(X0,X1)|X0=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f99])).
% 1.44/0.77 fof(f102,plain,(
% 1.44/0.77 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 1.44/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 1.44/0.77 fof(f103,plain,(
% 1.44/0.77 ssItem(sK0_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f102])).
% 1.44/0.77 fof(f104,plain,(
% 1.44/0.77 ssItem(sK1_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f102])).
% 1.44/0.77 fof(f105,plain,(
% 1.44/0.77 ~sK0_skl=sK1_skl),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f102])).
% 1.44/0.77 fof(f119,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 1.44/0.77 fof(f120,plain,(
% 1.44/0.77 ![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)))))))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f119])).
% 1.44/0.77 fof(f121,plain,(
% 1.44/0.77 ![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)))))))),
% 1.44/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 1.44/0.77 fof(f124,plain,(
% 1.44/0.77 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f121])).
% 1.44/0.77 fof(f131,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 1.44/0.77 fof(f132,plain,(
% 1.44/0.77 ![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)))))))))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f131])).
% 1.44/0.77 fof(f133,plain,(
% 1.44/0.77 ![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)))))))))),
% 1.44/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 1.44/0.77 fof(f134,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f133])).
% 1.44/0.77 fof(f135,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f133])).
% 1.44/0.77 fof(f136,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f133])).
% 1.44/0.77 fof(f137,plain,(
% 1.44/0.77 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f133])).
% 1.44/0.77 fof(f217,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 1.44/0.77 fof(f218,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f217])).
% 1.44/0.77 fof(f219,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f218])).
% 1.44/0.77 fof(f220,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X0,X1)|X0=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f218])).
% 1.44/0.77 fof(f221,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 1.44/0.77 fof(f222,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f221])).
% 1.44/0.77 fof(f223,plain,(
% 1.44/0.77 ssList(nil)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f17])).
% 1.44/0.77 fof(f226,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssItem(W)|(![X]: (~ssItem(X)|(~cons(W,U)=cons(X,V)|(W=X&V=U)))))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 1.44/0.77 fof(f227,plain,(
% 1.44/0.77 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X2=X3)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f226])).
% 1.44/0.77 fof(f244,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 1.44/0.77 fof(f245,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f244])).
% 1.44/0.77 fof(f248,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|app(nil,U)=U)),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 1.44/0.77 fof(f249,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f248])).
% 1.44/0.77 fof(f314,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~segmentP(U,V)|~segmentP(V,W))|segmentP(U,W)))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 1.44/0.77 fof(f315,plain,(
% 1.44/0.77 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(X0,X1)|~segmentP(X1,X2)|segmentP(X0,X2))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f314])).
% 1.44/0.77 fof(f316,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|~segmentP(V,U))|U=V))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 1.44/0.77 fof(f317,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|~segmentP(X1,X0)|X0=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f316])).
% 1.44/0.77 fof(f318,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|segmentP(U,U))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 1.44/0.77 fof(f319,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f318])).
% 1.44/0.77 fof(f322,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|segmentP(U,nil))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 1.44/0.77 fof(f323,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f322])).
% 1.44/0.77 fof(f324,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(segmentP(nil,U)<=>nil=U))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 1.44/0.77 fof(f325,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|((~segmentP(nil,U)|nil=U)&(segmentP(nil,U)|~nil=U)))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f324])).
% 1.44/0.77 fof(f326,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|~segmentP(nil,X0)|nil=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f325])).
% 1.44/0.77 fof(f375,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(W,V)=app(U,V)|W=U))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 1.44/0.77 fof(f376,plain,(
% 1.44/0.77 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X2,X1)=app(X0,X1)|X2=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f375])).
% 1.44/0.77 fof(f377,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(V,W)=app(V,U)|W=U))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 1.44/0.77 fof(f378,plain,(
% 1.44/0.77 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X1,X2)=app(X1,X0)|X2=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f377])).
% 1.44/0.77 fof(f379,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|cons(V,U)=app(cons(V,nil),U))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 1.44/0.77 fof(f380,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|cons(X1,X0)=app(cons(X1,nil),X0))),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f379])).
% 1.44/0.77 fof(f383,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(nil=app(U,V)<=>(nil=V&nil=U)))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 1.44/0.77 fof(f384,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~nil=app(U,V)|(nil=V&nil=U))&(nil=app(U,V)|(~nil=V|~nil=U))))))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f383])).
% 1.44/0.77 fof(f385,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~nil=app(X0,X1)|nil=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f384])).
% 1.44/0.77 fof(f386,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~nil=app(X0,X1)|nil=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f384])).
% 1.44/0.77 fof(f388,plain,(
% 1.44/0.77 ![U]: (~ssList(U)|app(U,nil)=U)),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 1.44/0.77 fof(f389,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f388])).
% 1.44/0.77 fof(f415,plain,(
% 1.44/0.77 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(?[Y]: (ssList(Y)&((app(W,Y)=X&equalelemsP(W))&(![Z]: (~ssItem(Z)|(![X1]: ((~ssList(X1)|~app(cons(Z,nil),X1)=Y)|(![X2]: (~ssList(X2)|~app(X2,cons(Z,nil))=W))))))))))&(nil=X|~nil=W))&((nil=V&~nil=U)|(neq(V,nil)&(~neq(U,nil)|~segmentP(V,U)))))))))))))),
% 1.44/0.77 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 1.44/0.77 fof(f416,definition,(
% 1.44/0.77 ![U,V]: (sP0_prd(V,U)<=>(nil=V&~nil=U))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 1.44/0.77 fof(f417,plain,(
% 1.44/0.77 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(?[Y]: (ssList(Y)&((app(W,Y)=X&equalelemsP(W))&(![Z]: (~ssItem(Z)|(![X1]: ((~ssList(X1)|~app(cons(Z,nil),X1)=Y)|(![X2]: (~ssList(X2)|~app(X2,cons(Z,nil))=W))))))))))&(nil=X|~nil=W))&(sP0_prd(V,U)|(neq(V,nil)&(~neq(U,nil)|~segmentP(V,U))))))))))))),
% 1.44/0.77 inference(formula_renaming,[status(thm)],[f415,f416])).
% 1.44/0.77 fof(f418,plain,(
% 1.44/0.77 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(?[Y]: (ssList(Y)&((app(W,Y)=X&equalelemsP(W))&(![Z]: (~ssItem(Z)|((![X1]: (~ssList(X1)|~app(cons(Z,nil),X1)=Y))|(![X2]: (~ssList(X2)|~app(X2,cons(Z,nil))=W)))))))))&(nil=X|~nil=W))&(sP0_prd(V,U)|(neq(V,nil)&(~neq(U,nil)|~segmentP(V,U))))))))))))),
% 1.44/0.77 inference(miniscoping,[status(thm)],[f417])).
% 1.44/0.77 fof(f419,plain,(
% 1.44/0.77 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&((((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(ssList(sK51_skl)&((app(sK49_skl,sK51_skl)=sK50_skl&equalelemsP(sK49_skl))&(![Z]: (~ssItem(Z)|((![X1]: (~ssList(X1)|~app(cons(Z,nil),X1)=sK51_skl))|(![X2]: (~ssList(X2)|~app(X2,cons(Z,nil))=sK49_skl))))))))&(nil=sK50_skl|~nil=sK49_skl))&(sP0_prd(sK48_skl,sK47_skl)|(neq(sK48_skl,nil)&(~neq(sK47_skl,nil)|~segmentP(sK48_skl,sK47_skl)))))))))),
% 1.44/0.77 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])).
% 1.44/0.77 fof(f420,plain,(
% 1.44/0.77 ssList(sK47_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f421,plain,(
% 1.44/0.77 ssList(sK48_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f422,plain,(
% 1.44/0.77 ssList(sK49_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f424,plain,(
% 1.44/0.77 sK48_skl=sK50_skl),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f425,plain,(
% 1.44/0.77 sK47_skl=sK49_skl),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f426,plain,(
% 1.44/0.77 ssList(sK51_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f427,plain,(
% 1.44/0.77 app(sK49_skl,sK51_skl)=sK50_skl),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f430,plain,(
% 1.44/0.77 nil=sK50_skl|~nil=sK49_skl),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f431,plain,(
% 1.44/0.77 sP0_prd(sK48_skl,sK47_skl)|neq(sK48_skl,nil)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f432,plain,(
% 1.44/0.77 sP0_prd(sK48_skl,sK47_skl)|~neq(sK47_skl,nil)|~segmentP(sK48_skl,sK47_skl)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f419])).
% 1.44/0.77 fof(f433,plain,(
% 1.44/0.77 ![U,V]: ((~sP0_prd(V,U)|(nil=V&~nil=U))&(sP0_prd(V,U)|(~nil=V|nil=U)))),
% 1.44/0.77 inference(NNF_transformation,[status(thm)],[f416])).
% 1.44/0.77 fof(f434,plain,(
% 1.44/0.77 (![U,V]: (~sP0_prd(V,U)|(nil=V&~nil=U)))&(![U,V]: (sP0_prd(V,U)|(~nil=V|nil=U)))),
% 1.44/0.77 inference(miniscoping,[status(thm)],[f433])).
% 1.44/0.77 fof(f435,plain,(
% 1.44/0.77 ![X0,X1]: (~sP0_prd(X0,X1)|nil=X0)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f434])).
% 1.44/0.77 fof(f436,plain,(
% 1.44/0.77 ![X0,X1]: (~sP0_prd(X0,X1)|~nil=X1)),
% 1.44/0.77 inference(cnf_transformation,[status(thm)],[f434])).
% 1.44/0.77 fof(f438,definition,(
% 1.44/0.77 sQ0_spl <=> (nil=sK50_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f439,plain,(
% 1.44/0.77 nil=sK50_skl|~sQ0_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f438])).
% 1.44/0.77 fof(f440,plain,(
% 1.44/0.77 ~nil=sK50_skl|sQ0_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f438])).
% 1.44/0.77 fof(f441,definition,(
% 1.44/0.77 sQ1_spl <=> (nil=sK49_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f443,plain,(
% 1.44/0.77 ~nil=sK49_skl|sQ1_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f441])).
% 1.44/0.77 fof(f444,plain,(
% 1.44/0.77 sQ0_spl|~sQ1_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f430,f438,f441])).
% 1.44/0.77 fof(f445,definition,(
% 1.44/0.77 sQ2_spl <=> (sP0_prd(sK48_skl,sK47_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f446,plain,(
% 1.44/0.77 sP0_prd(sK48_skl,sK47_skl)|~sQ2_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f445])).
% 1.44/0.77 fof(f448,definition,(
% 1.44/0.77 sQ3_spl <=> (neq(sK48_skl,nil))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f449,plain,(
% 1.44/0.77 neq(sK48_skl,nil)|~sQ3_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f448])).
% 1.44/0.77 fof(f451,plain,(
% 1.44/0.77 sQ2_spl|sQ3_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f431,f445,f448])).
% 1.44/0.77 fof(f452,definition,(
% 1.44/0.77 sQ4_spl <=> (neq(sK47_skl,nil))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f455,definition,(
% 1.44/0.77 sQ5_spl <=> (segmentP(sK48_skl,sK47_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f457,plain,(
% 1.44/0.77 ~segmentP(sK48_skl,sK47_skl)|sQ5_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f455])).
% 1.44/0.77 fof(f458,plain,(
% 1.44/0.77 sQ2_spl|~sQ4_spl|~sQ5_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f432,f445,f452,f455])).
% 1.44/0.77 fof(f459,plain,(
% 1.44/0.77 ![X1]: (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1))),
% 1.44/0.77 inference(destructive_equality_resolution,[status(thm)],[f100])).
% 1.44/0.77 fof(f460,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|~neq(X0,X0))),
% 1.44/0.77 inference(duplicate_literals_removal,[status(thm)],[f459])).
% 1.44/0.77 fof(f463,plain,(
% 1.44/0.77 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 1.44/0.77 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 1.44/0.77 fof(f465,plain,(
% 1.44/0.77 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 1.44/0.77 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 1.44/0.77 fof(f474,plain,(
% 1.44/0.77 ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 1.44/0.77 inference(destructive_equality_resolution,[status(thm)],[f219])).
% 1.44/0.77 fof(f475,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 1.44/0.77 inference(duplicate_literals_removal,[status(thm)],[f474])).
% 1.44/0.77 fof(f489,plain,(
% 1.44/0.77 ![X0]: (~sP0_prd(X0,nil))),
% 1.44/0.77 inference(destructive_equality_resolution,[status(thm)],[f436])).
% 1.44/0.77 fof(f495,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|ssList(app(sK49_skl,X0)))),
% 1.44/0.77 inference(resolution,[status(thm)],[f245,f422])).
% 1.44/0.77 fof(f498,plain,(
% 1.44/0.77 app(nil,sK49_skl)=sK49_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f249,f422])).
% 1.44/0.77 fof(f499,plain,(
% 1.44/0.77 app(nil,sK48_skl)=sK48_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f249,f421])).
% 1.44/0.77 fof(f501,plain,(
% 1.44/0.77 segmentP(sK49_skl,sK49_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f319,f422])).
% 1.44/0.77 fof(f502,plain,(
% 1.44/0.77 segmentP(sK48_skl,sK48_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f319,f421])).
% 1.44/0.77 fof(f504,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|neq(sK0_skl,X0)|sK0_skl=X0)),
% 1.44/0.77 inference(resolution,[status(thm)],[f103,f101])).
% 1.44/0.77 fof(f505,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|neq(sK1_skl,X0)|sK1_skl=X0)),
% 1.44/0.77 inference(resolution,[status(thm)],[f104,f101])).
% 1.44/0.77 fof(f508,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|cons(X0,sK49_skl)=app(cons(X0,nil),sK49_skl))),
% 1.44/0.77 inference(resolution,[status(thm)],[f380,f422])).
% 1.44/0.77 fof(f509,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|cons(X0,sK48_skl)=app(cons(X0,nil),sK48_skl))),
% 1.44/0.77 inference(resolution,[status(thm)],[f380,f421])).
% 1.44/0.77 fof(f511,plain,(
% 1.44/0.77 app(sK49_skl,nil)=sK49_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f389,f422])).
% 1.44/0.77 fof(f512,plain,(
% 1.44/0.77 app(sK48_skl,nil)=sK48_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f389,f421])).
% 1.44/0.77 fof(f515,plain,(
% 1.44/0.77 app(sK51_skl,nil)=sK51_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f426,f389])).
% 1.44/0.77 fof(f516,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|cons(X0,sK51_skl)=app(cons(X0,nil),sK51_skl))),
% 1.44/0.77 inference(resolution,[status(thm)],[f426,f380])).
% 1.44/0.77 fof(f517,plain,(
% 1.44/0.77 segmentP(sK51_skl,sK51_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f426,f319])).
% 1.44/0.77 fof(f518,plain,(
% 1.44/0.77 app(nil,sK51_skl)=sK51_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f426,f249])).
% 1.44/0.77 fof(f519,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|ssList(app(sK51_skl,X0)))),
% 1.44/0.77 inference(resolution,[status(thm)],[f426,f245])).
% 1.44/0.77 fof(f521,plain,(
% 1.44/0.77 app(sK47_skl,sK51_skl)=sK50_skl),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f427])).
% 1.44/0.77 fof(f522,plain,(
% 1.44/0.77 app(sK47_skl,sK51_skl)=sK48_skl),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f424,f521])).
% 1.44/0.77 fof(f523,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK51_skl)|segmentP(app(app(sK47_skl,sK51_skl),X0),sK51_skl)|~ssList(sK47_skl)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f522,f465])).
% 1.44/0.77 fof(f524,definition,(
% 1.44/0.77 ![X0]: (sQ6_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK47_skl,sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f527,definition,(
% 1.44/0.77 sQ7_spl <=> (ssList(sK51_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f529,plain,(
% 1.44/0.77 ~ssList(sK51_skl)|sQ7_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f527])).
% 1.44/0.77 fof(f530,definition,(
% 1.44/0.77 sQ8_spl <=> (ssList(sK47_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f532,plain,(
% 1.44/0.77 ~ssList(sK47_skl)|sQ8_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f530])).
% 1.44/0.77 fof(f533,plain,(
% 1.44/0.77 sQ6_spl|~sQ7_spl|~sQ8_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f523,f524,f527,f530])).
% 1.44/0.77 fof(f534,plain,(
% 1.44/0.77 $false|sQ8_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f532,f420])).
% 1.44/0.77 fof(f535,plain,(
% 1.44/0.77 sQ8_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f534])).
% 1.44/0.77 fof(f538,plain,(
% 1.44/0.77 sK48_skl=nil|~sQ0_spl),
% 1.44/0.77 inference(backward_demodulation,[status(thm)],[f439,f424])).
% 1.44/0.77 fof(f539,plain,(
% 1.44/0.77 app(nil,sK47_skl)=sK49_skl),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f498])).
% 1.44/0.77 fof(f540,plain,(
% 1.44/0.77 app(nil,sK47_skl)=sK47_skl),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f539])).
% 1.44/0.77 fof(f541,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f540,f465])).
% 1.44/0.77 fof(f542,definition,(
% 1.44/0.77 ![X0]: (sQ9_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f543,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)|~sQ9_spl)),
% 1.44/0.77 inference(component_clause,[status(thm)],[f542])).
% 1.44/0.77 fof(f545,definition,(
% 1.44/0.77 sQ10_spl <=> (ssList(nil))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f547,plain,(
% 1.44/0.77 ~ssList(nil)|sQ10_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f545])).
% 1.44/0.77 fof(f548,plain,(
% 1.44/0.77 sQ9_spl|~sQ8_spl|~sQ10_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f541,f542,f530,f545])).
% 1.44/0.77 fof(f549,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK47_skl,X0))|segmentP(app(sK47_skl,X0),sK47_skl)|~ssList(X0)|~sQ9_spl)),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f540,f543])).
% 1.44/0.77 fof(f550,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f499,f465])).
% 1.44/0.77 fof(f551,definition,(
% 1.44/0.77 ![X0]: (sQ11_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f554,definition,(
% 1.44/0.77 sQ12_spl <=> (ssList(sK48_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f556,plain,(
% 1.44/0.77 ~ssList(sK48_skl)|sQ12_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f554])).
% 1.44/0.77 fof(f557,plain,(
% 1.44/0.77 sQ11_spl|~sQ12_spl|~sQ10_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f550,f551,f554,f545])).
% 1.44/0.77 fof(f558,plain,(
% 1.44/0.77 segmentP(sK47_skl,sK49_skl)),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f501])).
% 1.44/0.77 fof(f559,plain,(
% 1.44/0.77 segmentP(sK47_skl,sK47_skl)),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f558])).
% 1.44/0.77 fof(f560,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(sK47_skl)|~segmentP(X0,sK47_skl)|segmentP(X0,sK47_skl))),
% 1.44/0.77 inference(resolution,[status(thm)],[f559,f315])).
% 1.44/0.77 fof(f561,definition,(
% 1.44/0.77 ![X0]: (sQ13_spl <=> (~ssList(X0)|~segmentP(X0,sK47_skl)|segmentP(X0,sK47_skl)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f564,plain,(
% 1.44/0.77 sQ13_spl|~sQ8_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f560,f561,f530])).
% 1.44/0.77 fof(f565,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(sK48_skl)|~segmentP(X0,sK48_skl)|segmentP(X0,sK48_skl))),
% 1.44/0.77 inference(resolution,[status(thm)],[f502,f315])).
% 1.44/0.77 fof(f566,definition,(
% 1.44/0.77 ![X0]: (sQ14_spl <=> (~ssList(X0)|~segmentP(X0,sK48_skl)|segmentP(X0,sK48_skl)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f569,plain,(
% 1.44/0.77 sQ14_spl|~sQ12_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f565,f566,f554])).
% 1.44/0.77 fof(f570,plain,(
% 1.44/0.77 $false|sQ12_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f556,f421])).
% 1.44/0.77 fof(f571,plain,(
% 1.44/0.77 sQ12_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f570])).
% 1.44/0.77 fof(f573,plain,(
% 1.44/0.77 neq(sK0_skl,sK1_skl)|sK0_skl=sK1_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f504,f104])).
% 1.44/0.77 fof(f574,plain,(
% 1.44/0.77 neq(sK0_skl,sK0_skl)|sK0_skl=sK0_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f504,f103])).
% 1.44/0.77 fof(f575,definition,(
% 1.44/0.77 sQ15_spl <=> (neq(sK0_skl,sK1_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f578,definition,(
% 1.44/0.77 sQ16_spl <=> (sK0_skl=sK1_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f579,plain,(
% 1.44/0.77 sK0_skl=sK1_skl|~sQ16_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f578])).
% 1.44/0.77 fof(f581,plain,(
% 1.44/0.77 sQ15_spl|sQ16_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f573,f575,f578])).
% 1.44/0.77 fof(f582,definition,(
% 1.44/0.77 sQ17_spl <=> (neq(sK0_skl,sK0_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f583,plain,(
% 1.44/0.77 neq(sK0_skl,sK0_skl)|~sQ17_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f582])).
% 1.44/0.77 fof(f585,definition,(
% 1.44/0.77 sQ18_spl <=> (sK0_skl=sK0_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f588,plain,(
% 1.44/0.77 sQ17_spl|sQ18_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f574,f582,f585])).
% 1.44/0.77 fof(f589,plain,(
% 1.44/0.77 neq(sK1_skl,sK1_skl)|sK1_skl=sK1_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f505,f104])).
% 1.44/0.77 fof(f590,plain,(
% 1.44/0.77 neq(sK1_skl,sK0_skl)|sK1_skl=sK0_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f505,f103])).
% 1.44/0.77 fof(f591,definition,(
% 1.44/0.77 sQ19_spl <=> (neq(sK1_skl,sK1_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f592,plain,(
% 1.44/0.77 neq(sK1_skl,sK1_skl)|~sQ19_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f591])).
% 1.44/0.77 fof(f594,definition,(
% 1.44/0.77 sQ20_spl <=> (sK1_skl=sK1_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f597,plain,(
% 1.44/0.77 sQ19_spl|sQ20_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f589,f591,f594])).
% 1.44/0.77 fof(f598,definition,(
% 1.44/0.77 sQ21_spl <=> (neq(sK1_skl,sK0_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f601,plain,(
% 1.44/0.77 sQ21_spl|sQ16_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f590,f598,f578])).
% 1.44/0.77 fof(f602,plain,(
% 1.44/0.77 $false|~sQ16_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f579,f105])).
% 1.44/0.77 fof(f603,plain,(
% 1.44/0.77 ~sQ16_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f602])).
% 1.44/0.77 fof(f604,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|cons(X0,sK47_skl)=app(cons(X0,nil),sK49_skl))),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f508])).
% 1.44/0.77 fof(f605,plain,(
% 1.44/0.77 ![X0]: (~ssItem(X0)|cons(X0,sK47_skl)=app(cons(X0,nil),sK47_skl))),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f604])).
% 1.44/0.77 fof(f606,plain,(
% 1.44/0.77 cons(sK1_skl,sK47_skl)=app(cons(sK1_skl,nil),sK47_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f605,f104])).
% 1.44/0.77 fof(f607,plain,(
% 1.44/0.77 cons(sK0_skl,sK47_skl)=app(cons(sK0_skl,nil),sK47_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f605,f103])).
% 1.44/0.77 fof(f608,plain,(
% 1.44/0.77 cons(sK1_skl,sK48_skl)=app(cons(sK1_skl,nil),sK48_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f509,f104])).
% 1.44/0.77 fof(f609,plain,(
% 1.44/0.77 cons(sK0_skl,sK48_skl)=app(cons(sK0_skl,nil),sK48_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f509,f103])).
% 1.44/0.77 fof(f610,plain,(
% 1.44/0.77 app(sK47_skl,nil)=sK49_skl),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f511])).
% 1.44/0.77 fof(f611,plain,(
% 1.44/0.77 app(sK47_skl,nil)=sK47_skl),
% 1.44/0.77 inference(forward_demodulation,[status(thm)],[f425,f610])).
% 1.44/0.77 fof(f612,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f611,f465])).
% 1.44/0.77 fof(f613,definition,(
% 1.44/0.77 ![X0]: (sQ22_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f616,plain,(
% 1.44/0.77 sQ22_spl|~sQ10_spl|~sQ8_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f612,f613,f545,f530])).
% 1.44/0.77 fof(f617,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f512,f465])).
% 1.44/0.77 fof(f618,definition,(
% 1.44/0.77 ![X0]: (sQ23_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f621,plain,(
% 1.44/0.77 sQ23_spl|~sQ10_spl|~sQ12_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f617,f618,f545,f554])).
% 1.44/0.77 fof(f622,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|neq(sK51_skl,X0)|sK51_skl=X0)),
% 1.44/0.77 inference(resolution,[status(thm)],[f220,f426])).
% 1.44/0.77 fof(f623,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|neq(sK48_skl,X0)|sK48_skl=X0)),
% 1.44/0.77 inference(resolution,[status(thm)],[f220,f421])).
% 1.44/0.77 fof(f624,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|neq(sK47_skl,X0)|sK47_skl=X0)),
% 1.44/0.77 inference(resolution,[status(thm)],[f220,f420])).
% 1.44/0.77 fof(f625,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(nil)|segmentP(app(app(sK51_skl,nil),X0),nil)|~ssList(sK51_skl)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f515,f465])).
% 1.44/0.77 fof(f626,definition,(
% 1.44/0.77 ![X0]: (sQ24_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(sK51_skl,nil),X0),nil)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f629,plain,(
% 1.44/0.77 sQ24_spl|~sQ10_spl|~sQ7_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f625,f626,f545,f527])).
% 1.44/0.77 fof(f630,plain,(
% 1.44/0.77 $false|sQ7_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f529,f426])).
% 1.44/0.77 fof(f631,plain,(
% 1.44/0.77 sQ7_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f630])).
% 1.44/0.77 fof(f632,plain,(
% 1.44/0.77 cons(sK1_skl,sK51_skl)=app(cons(sK1_skl,nil),sK51_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f516,f104])).
% 1.44/0.77 fof(f633,plain,(
% 1.44/0.77 cons(sK0_skl,sK51_skl)=app(cons(sK0_skl,nil),sK51_skl)),
% 1.44/0.77 inference(resolution,[status(thm)],[f516,f103])).
% 1.44/0.77 fof(f634,plain,(
% 1.44/0.77 ![X0]: (~ssList(X0)|~ssList(sK51_skl)|~ssList(sK51_skl)|~segmentP(X0,sK51_skl)|segmentP(X0,sK51_skl))),
% 1.44/0.77 inference(resolution,[status(thm)],[f517,f315])).
% 1.44/0.77 fof(f635,definition,(
% 1.44/0.77 ![X0]: (sQ25_spl <=> (~ssList(X0)|~segmentP(X0,sK51_skl)|segmentP(X0,sK51_skl)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f638,plain,(
% 1.44/0.77 sQ25_spl|~sQ7_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f634,f635,f527])).
% 1.44/0.77 fof(f639,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(sK51_skl)|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(nil)|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f518,f465])).
% 1.44/0.77 fof(f640,definition,(
% 1.44/0.77 ![X0]: (sQ26_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f641,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(sK51_skl,X0))|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(X0)|~sQ26_spl)),
% 1.44/0.77 inference(component_clause,[status(thm)],[f640])).
% 1.44/0.77 fof(f643,plain,(
% 1.44/0.77 sQ26_spl|~sQ7_spl|~sQ10_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f639,f640,f527,f545])).
% 1.44/0.77 fof(f648,plain,(
% 1.44/0.77 app(sK47_skl,sK51_skl)=nil|~sQ0_spl),
% 1.44/0.77 inference(backward_demodulation,[status(thm)],[f538,f522])).
% 1.44/0.77 fof(f655,plain,(
% 1.44/0.77 ~ssItem(sK0_skl)|~sQ17_spl),
% 1.44/0.77 inference(resolution,[status(thm)],[f583,f460])).
% 1.44/0.77 fof(f656,plain,(
% 1.44/0.77 $false|~sQ17_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f655,f103])).
% 1.44/0.77 fof(f657,plain,(
% 1.44/0.77 ~sQ17_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f656])).
% 1.44/0.77 fof(f659,plain,(
% 1.44/0.77 ~ssItem(sK1_skl)|~sQ19_spl),
% 1.44/0.77 inference(resolution,[status(thm)],[f592,f460])).
% 1.44/0.77 fof(f660,plain,(
% 1.44/0.77 $false|~sQ19_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f659,f104])).
% 1.44/0.77 fof(f661,plain,(
% 1.44/0.77 ~sQ19_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f660])).
% 1.44/0.77 fof(f663,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(cons(sK1_skl,sK47_skl),X0))|~ssList(sK47_skl)|segmentP(app(app(cons(sK1_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f606,f465])).
% 1.44/0.77 fof(f664,definition,(
% 1.44/0.77 sQ27_spl <=> (ssItem(sK1_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f666,plain,(
% 1.44/0.77 ~ssItem(sK1_skl)|sQ27_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f664])).
% 1.44/0.77 fof(f674,definition,(
% 1.44/0.77 ![X0]: (sQ30_spl <=> (~ssList(app(cons(sK1_skl,sK47_skl),X0))|segmentP(app(app(cons(sK1_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f677,definition,(
% 1.44/0.77 sQ31_spl <=> (ssList(cons(sK1_skl,nil)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f679,plain,(
% 1.44/0.77 ~ssList(cons(sK1_skl,nil))|sQ31_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f677])).
% 1.44/0.77 fof(f680,plain,(
% 1.44/0.77 sQ30_spl|~sQ8_spl|~sQ31_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f663,f674,f530,f677])).
% 1.44/0.77 fof(f683,plain,(
% 1.44/0.77 ![X0]: (~ssList(app(cons(sK0_skl,sK47_skl),X0))|~ssList(sK47_skl)|segmentP(app(app(cons(sK0_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 1.44/0.77 inference(paramodulation,[status(thm)],[f607,f465])).
% 1.44/0.77 fof(f684,definition,(
% 1.44/0.77 sQ32_spl <=> (ssItem(sK0_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f686,plain,(
% 1.44/0.77 ~ssItem(sK0_skl)|sQ32_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f684])).
% 1.44/0.77 fof(f694,definition,(
% 1.44/0.77 ![X0]: (sQ35_spl <=> (~ssList(app(cons(sK0_skl,sK47_skl),X0))|segmentP(app(app(cons(sK0_skl,nil),sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f697,definition,(
% 1.44/0.77 sQ36_spl <=> (ssList(cons(sK0_skl,nil)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f699,plain,(
% 1.44/0.77 ~ssList(cons(sK0_skl,nil))|sQ36_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f697])).
% 1.44/0.77 fof(f700,plain,(
% 1.44/0.77 sQ35_spl|~sQ8_spl|~sQ36_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f683,f694,f530,f697])).
% 1.44/0.77 fof(f702,plain,(
% 1.44/0.77 $false|sQ32_spl),
% 1.44/0.77 inference(forward_subsumption_resolution,[status(thm)],[f686,f103])).
% 1.44/0.77 fof(f703,plain,(
% 1.44/0.77 sQ32_spl),
% 1.44/0.77 inference(contradiction_clause,[status(thm)],[f702])).
% 1.44/0.77 fof(f712,definition,(
% 1.44/0.77 ![X0]: (sQ38_spl <=> (~ssList(app(cons(sK1_skl,nil),X0))|segmentP(app(app(cons(sK1_skl,nil),nil),X0),nil)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f724,definition,(
% 1.44/0.77 ![X0]: (sQ40_spl <=> (~ssList(app(cons(sK0_skl,nil),X0))|segmentP(app(app(cons(sK0_skl,nil),nil),X0),nil)|~ssList(X0)))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f728,plain,(
% 1.44/0.77 neq(sK51_skl,sK51_skl)|sK51_skl=sK51_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f622,f426])).
% 1.44/0.77 fof(f730,definition,(
% 1.44/0.77 sQ41_spl <=> (neq(sK51_skl,sK51_skl))),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f731,plain,(
% 1.44/0.77 neq(sK51_skl,sK51_skl)|~sQ41_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f730])).
% 1.44/0.77 fof(f733,definition,(
% 1.44/0.77 sQ42_spl <=> (sK51_skl=sK51_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f736,plain,(
% 1.44/0.77 sQ41_spl|sQ42_spl),
% 1.44/0.77 inference(split_clause,[status(thm)],[f728,f730,f733])).
% 1.44/0.77 fof(f751,definition,(
% 1.44/0.77 sQ46_spl <=> (nil=sK51_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f752,plain,(
% 1.44/0.77 nil=sK51_skl|~sQ46_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f751])).
% 1.44/0.77 fof(f758,definition,(
% 1.44/0.77 sQ48_spl <=> (nil=sK47_skl)),
% 1.44/0.77 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 1.44/0.77 fof(f759,plain,(
% 1.44/0.77 nil=sK47_skl|~sQ48_spl),
% 1.44/0.77 inference(component_clause,[status(thm)],[f758])).
% 1.44/0.77 fof(f763,plain,(
% 1.44/0.77 neq(sK47_skl,sK47_skl)|sK47_skl=sK47_skl),
% 1.44/0.77 inference(resolution,[status(thm)],[f624,f420])).
% 1.44/0.77 fof(f768,definition,(
% 1.44/0.77 sQ50_spl <=> (neq(sK47_skl,sK47_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f769,plain,(
% 1.44/0.79 neq(sK47_skl,sK47_skl)|~sQ50_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f768])).
% 1.44/0.79 fof(f771,definition,(
% 1.44/0.79 sQ51_spl <=> (sK47_skl=sK47_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f774,plain,(
% 1.44/0.79 sQ50_spl|sQ51_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f763,f768,f771])).
% 1.44/0.79 fof(f776,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(cons(sK1_skl,sK51_skl),X0))|~ssList(sK51_skl)|segmentP(app(app(cons(sK1_skl,nil),sK51_skl),X0),sK51_skl)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f632,f465])).
% 1.44/0.79 fof(f781,definition,(
% 1.44/0.79 ![X0]: (sQ53_spl <=> (~ssList(app(cons(sK1_skl,sK51_skl),X0))|segmentP(app(app(cons(sK1_skl,nil),sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f784,plain,(
% 1.44/0.79 sQ53_spl|~sQ7_spl|~sQ31_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f776,f781,f527,f677])).
% 1.44/0.79 fof(f786,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(cons(sK0_skl,sK51_skl),X0))|~ssList(sK51_skl)|segmentP(app(app(cons(sK0_skl,nil),sK51_skl),X0),sK51_skl)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f633,f465])).
% 1.44/0.79 fof(f791,definition,(
% 1.44/0.79 ![X0]: (sQ55_spl <=> (~ssList(app(cons(sK0_skl,sK51_skl),X0))|segmentP(app(app(cons(sK0_skl,nil),sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f794,plain,(
% 1.44/0.79 sQ55_spl|~sQ7_spl|~sQ36_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f786,f791,f527,f697])).
% 1.44/0.79 fof(f796,definition,(
% 1.44/0.79 ![X0]: (sQ56_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f803,definition,(
% 1.44/0.79 ![X0]: (sQ57_spl <=> (~ssList(X0)|~segmentP(X0,nil)|segmentP(X0,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f812,plain,(
% 1.44/0.79 ~nil=sK47_skl|sQ1_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f425,f443])).
% 1.44/0.79 fof(f813,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~sQ41_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f731,f475])).
% 1.44/0.79 fof(f815,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ41_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f813,f527,f730])).
% 1.44/0.79 fof(f816,plain,(
% 1.44/0.79 neq(sK47_skl,nil)|sK47_skl=nil),
% 1.44/0.79 inference(resolution,[status(thm)],[f223,f624])).
% 1.44/0.79 fof(f817,plain,(
% 1.44/0.79 neq(sK51_skl,nil)|sK51_skl=nil),
% 1.44/0.79 inference(resolution,[status(thm)],[f223,f622])).
% 1.44/0.79 fof(f819,plain,(
% 1.44/0.79 app(nil,nil)=nil),
% 1.44/0.79 inference(resolution,[status(thm)],[f223,f389])).
% 1.44/0.79 fof(f820,plain,(
% 1.44/0.79 ![X0]: (~ssItem(X0)|cons(X0,nil)=app(cons(X0,nil),nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f223,f380])).
% 1.44/0.79 fof(f821,plain,(
% 1.44/0.79 segmentP(nil,nil)),
% 1.44/0.79 inference(resolution,[status(thm)],[f223,f319])).
% 1.44/0.79 fof(f824,plain,(
% 1.44/0.79 ![X0]: (~ssItem(X0)|ssList(cons(X0,nil)))),
% 1.44/0.79 inference(resolution,[status(thm)],[f223,f222])).
% 1.44/0.79 fof(f825,plain,(
% 1.44/0.79 sQ4_spl|sQ48_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f816,f452,f758])).
% 1.44/0.79 fof(f826,definition,(
% 1.44/0.79 sQ59_spl <=> (neq(sK51_skl,nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f829,plain,(
% 1.44/0.79 sQ59_spl|sQ46_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f817,f826,f751])).
% 1.44/0.79 fof(f830,plain,(
% 1.44/0.79 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X1=X1)),
% 1.44/0.79 inference(equality_resolution,[status(thm)],[f227])).
% 1.44/0.79 fof(f831,definition,(
% 1.44/0.79 ![X0]: (sQ60_spl <=> (~ssList(X0)|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f832,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ60_spl)),
% 1.44/0.79 inference(component_clause,[status(thm)],[f831])).
% 1.44/0.79 fof(f834,definition,(
% 1.44/0.79 ![X1]: (sQ61_spl <=> (~ssItem(X1)|~ssItem(X1)|X1=X1))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f837,plain,(
% 1.44/0.79 sQ60_spl|sQ61_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f830,f831,f834])).
% 1.44/0.79 fof(f838,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~sQ60_spl)),
% 1.44/0.79 inference(duplicate_literals_removal,[status(thm)],[f832])).
% 1.44/0.79 fof(f855,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~sQ50_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f769,f475])).
% 1.44/0.79 fof(f857,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ50_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f855,f530,f768])).
% 1.44/0.79 fof(f860,definition,(
% 1.44/0.79 sQ62_spl <=> (sK48_skl=nil)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f862,plain,(
% 1.44/0.79 ~sK48_skl=nil|sQ62_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f860])).
% 1.44/0.79 fof(f867,definition,(
% 1.44/0.79 sQ64_spl <=> (sK48_skl=sK47_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f868,plain,(
% 1.44/0.79 sK48_skl=sK47_skl|~sQ64_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f867])).
% 1.44/0.79 fof(f871,plain,(
% 1.44/0.79 $false|sQ27_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f666,f104])).
% 1.44/0.79 fof(f872,plain,(
% 1.44/0.79 sQ27_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f871])).
% 1.44/0.79 fof(f873,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(cons(sK0_skl,sK48_skl),X0))|~ssList(sK48_skl)|segmentP(app(app(cons(sK0_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f609,f465])).
% 1.44/0.79 fof(f874,definition,(
% 1.44/0.79 ![X0]: (sQ65_spl <=> (~ssList(app(cons(sK0_skl,sK48_skl),X0))|segmentP(app(app(cons(sK0_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f877,plain,(
% 1.44/0.79 sQ65_spl|~sQ12_spl|~sQ36_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f873,f874,f554,f697])).
% 1.44/0.79 fof(f878,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(cons(sK1_skl,sK48_skl),X0))|~ssList(sK48_skl)|segmentP(app(app(cons(sK1_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f608,f465])).
% 1.44/0.79 fof(f879,definition,(
% 1.44/0.79 ![X0]: (sQ66_spl <=> (~ssList(app(cons(sK1_skl,sK48_skl),X0))|segmentP(app(app(cons(sK1_skl,nil),sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f882,plain,(
% 1.44/0.79 sQ66_spl|~sQ12_spl|~sQ31_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f878,f879,f554,f677])).
% 1.44/0.79 fof(f897,plain,(
% 1.44/0.79 neq(sK48_skl,sK48_skl)|sK48_skl=sK48_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f421,f623])).
% 1.44/0.79 fof(f906,definition,(
% 1.44/0.79 sQ68_spl <=> (neq(sK48_skl,sK48_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f907,plain,(
% 1.44/0.79 neq(sK48_skl,sK48_skl)|~sQ68_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f906])).
% 1.44/0.79 fof(f909,definition,(
% 1.44/0.79 sQ69_spl <=> (sK48_skl=sK48_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f912,plain,(
% 1.44/0.79 sQ68_spl|sQ69_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f897,f906,f909])).
% 1.44/0.79 fof(f917,plain,(
% 1.44/0.79 ~nil=sK48_skl|sQ0_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f424,f440])).
% 1.44/0.79 fof(f918,plain,(
% 1.44/0.79 $false|sQ1_spl|~sQ48_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f759,f812])).
% 1.44/0.79 fof(f919,plain,(
% 1.44/0.79 sQ1_spl|~sQ48_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f918])).
% 1.44/0.79 fof(f920,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f819,f465])).
% 1.44/0.79 fof(f921,plain,(
% 1.44/0.79 sQ56_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f920,f796,f545])).
% 1.44/0.79 fof(f922,plain,(
% 1.44/0.79 cons(sK1_skl,nil)=app(cons(sK1_skl,nil),nil)),
% 1.44/0.79 inference(resolution,[status(thm)],[f820,f104])).
% 1.44/0.79 fof(f923,plain,(
% 1.44/0.79 cons(sK0_skl,nil)=app(cons(sK0_skl,nil),nil)),
% 1.44/0.79 inference(resolution,[status(thm)],[f820,f103])).
% 1.44/0.79 fof(f924,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~segmentP(X0,nil)|segmentP(X0,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f821,f315])).
% 1.44/0.79 fof(f925,plain,(
% 1.44/0.79 sQ57_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f924,f803,f545])).
% 1.44/0.79 fof(f927,plain,(
% 1.44/0.79 ssList(cons(sK1_skl,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f824,f104])).
% 1.44/0.79 fof(f928,plain,(
% 1.44/0.79 ssList(cons(sK0_skl,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f824,f103])).
% 1.44/0.79 fof(f930,plain,(
% 1.44/0.79 $false|~sQ60_spl),
% 1.44/0.79 inference(backward_subsumption_resolution,[status(thm)],[f421,f838])).
% 1.44/0.79 fof(f933,plain,(
% 1.44/0.79 ~sQ60_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f930])).
% 1.44/0.79 fof(f944,plain,(
% 1.44/0.79 app(sK47_skl,nil)=sK48_skl|~sQ46_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f752,f522])).
% 1.44/0.79 fof(f945,plain,(
% 1.44/0.79 neq(sK47_skl,nil)|~sQ46_spl|~sQ3_spl),
% 1.44/0.79 inference(backward_demodulation,[status(thm)],[f954,f449])).
% 1.44/0.79 fof(f954,plain,(
% 1.44/0.79 sK47_skl=sK48_skl|~sQ46_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f611,f944])).
% 1.44/0.79 fof(f980,definition,(
% 1.44/0.79 sQ74_spl <=> (nil=nil)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f985,plain,(
% 1.44/0.79 neq(sK47_skl,sK48_skl)|~sQ64_spl|~sQ68_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f868,f907])).
% 1.44/0.79 fof(f986,plain,(
% 1.44/0.79 neq(sK47_skl,sK47_skl)|~sQ64_spl|~sQ68_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f868,f985])).
% 1.44/0.79 fof(f990,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f819,f463])).
% 1.44/0.79 fof(f991,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f540,f463])).
% 1.44/0.79 fof(f992,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f611,f463])).
% 1.44/0.79 fof(f1007,definition,(
% 1.44/0.79 sQ79_spl <=> (frontsegP(app(nil,nil),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1010,plain,(
% 1.44/0.79 ~sQ10_spl|sQ79_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f990,f545,f1007])).
% 1.44/0.79 fof(f1011,definition,(
% 1.44/0.79 sQ80_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1014,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ10_spl|sQ80_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f991,f530,f545,f1011])).
% 1.44/0.79 fof(f1015,definition,(
% 1.44/0.79 sQ81_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1018,plain,(
% 1.44/0.79 ~sQ8_spl|sQ81_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f992,f530,f1015,f545])).
% 1.44/0.79 fof(f1035,plain,(
% 1.44/0.79 ~ssList(cons(sK1_skl,nil))|~ssList(cons(sK1_skl,nil))|frontsegP(app(cons(sK1_skl,nil),nil),cons(sK1_skl,nil))|~ssList(nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f922,f463])).
% 1.44/0.79 fof(f1036,definition,(
% 1.44/0.79 sQ83_spl <=> (frontsegP(app(cons(sK1_skl,nil),nil),cons(sK1_skl,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1039,plain,(
% 1.44/0.79 ~sQ31_spl|sQ83_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1035,f677,f1036,f545])).
% 1.44/0.79 fof(f1040,plain,(
% 1.44/0.79 ~ssList(cons(sK0_skl,nil))|~ssList(cons(sK0_skl,nil))|frontsegP(app(cons(sK0_skl,nil),nil),cons(sK0_skl,nil))|~ssList(nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f923,f463])).
% 1.44/0.79 fof(f1041,definition,(
% 1.44/0.79 sQ84_spl <=> (frontsegP(app(cons(sK0_skl,nil),nil),cons(sK0_skl,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1044,plain,(
% 1.44/0.79 ~sQ36_spl|sQ84_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1040,f697,f1041,f545])).
% 1.44/0.79 fof(f1051,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~sQ64_spl|~sQ68_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f475,f986])).
% 1.44/0.79 fof(f1052,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ64_spl|~sQ68_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1051,f530,f867,f906])).
% 1.44/0.79 fof(f1095,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(sK51_skl)|ssList(sK7_skl(sK51_skl,sK51_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f134,f517])).
% 1.44/0.79 fof(f1096,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(nil)|ssList(sK7_skl(nil,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f134,f821])).
% 1.44/0.79 fof(f1097,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK47_skl)|ssList(sK7_skl(sK47_skl,sK47_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f134,f559])).
% 1.44/0.79 fof(f1098,definition,(
% 1.44/0.79 sQ88_spl <=> (ssList(sK7_skl(sK51_skl,sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1101,plain,(
% 1.44/0.79 ~sQ7_spl|sQ88_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1095,f527,f1098])).
% 1.44/0.79 fof(f1102,definition,(
% 1.44/0.79 sQ89_spl <=> (ssList(sK7_skl(nil,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1105,plain,(
% 1.44/0.79 ~sQ10_spl|sQ89_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1096,f545,f1102])).
% 1.44/0.79 fof(f1106,definition,(
% 1.44/0.79 sQ90_spl <=> (ssList(sK7_skl(sK47_skl,sK47_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1109,plain,(
% 1.44/0.79 ~sQ8_spl|sQ90_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1097,f530,f1106])).
% 1.44/0.79 fof(f1110,plain,(
% 1.44/0.79 nil=sK48_skl|~sQ2_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f446,f435])).
% 1.44/0.79 fof(f1111,plain,(
% 1.44/0.79 $false|sQ0_spl|~sQ2_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1110,f917])).
% 1.44/0.79 fof(f1112,plain,(
% 1.44/0.79 sQ0_spl|~sQ2_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f1111])).
% 1.44/0.79 fof(f1113,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(sK48_skl)|ssList(sK7_skl(sK48_skl,sK48_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f502,f134])).
% 1.44/0.79 fof(f1116,definition,(
% 1.44/0.79 sQ91_spl <=> (ssList(sK7_skl(sK48_skl,sK48_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1119,plain,(
% 1.44/0.79 ~sQ12_spl|sQ91_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1113,f554,f1116])).
% 1.44/0.79 fof(f1129,plain,(
% 1.44/0.79 segmentP(sK51_skl,nil)),
% 1.44/0.79 inference(resolution,[status(thm)],[f323,f426])).
% 1.44/0.79 fof(f1130,plain,(
% 1.44/0.79 segmentP(sK47_skl,nil)),
% 1.44/0.79 inference(resolution,[status(thm)],[f323,f420])).
% 1.44/0.79 fof(f1131,plain,(
% 1.44/0.79 segmentP(sK48_skl,nil)),
% 1.44/0.79 inference(resolution,[status(thm)],[f421,f323])).
% 1.44/0.79 fof(f1164,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(sK48_skl)|ssList(sK8_skl(sK48_skl,sK48_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f135,f502])).
% 1.44/0.79 fof(f1165,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(sK51_skl)|ssList(sK8_skl(sK51_skl,sK51_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f135,f517])).
% 1.44/0.79 fof(f1166,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(nil)|ssList(sK8_skl(nil,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f135,f821])).
% 1.44/0.79 fof(f1167,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK47_skl)|ssList(sK8_skl(sK47_skl,sK47_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f135,f559])).
% 1.44/0.79 fof(f1168,definition,(
% 1.44/0.79 sQ96_spl <=> (ssList(sK8_skl(sK48_skl,sK48_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1171,plain,(
% 1.44/0.79 ~sQ12_spl|sQ96_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1164,f554,f1168])).
% 1.44/0.79 fof(f1172,definition,(
% 1.44/0.79 sQ97_spl <=> (ssList(sK8_skl(sK51_skl,sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1175,plain,(
% 1.44/0.79 ~sQ7_spl|sQ97_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1165,f527,f1172])).
% 1.44/0.79 fof(f1176,definition,(
% 1.44/0.79 sQ98_spl <=> (ssList(sK8_skl(nil,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1179,plain,(
% 1.44/0.79 ~sQ10_spl|sQ98_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1166,f545,f1176])).
% 1.44/0.79 fof(f1180,definition,(
% 1.44/0.79 sQ99_spl <=> (ssList(sK8_skl(sK47_skl,sK47_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1183,plain,(
% 1.44/0.79 ~sQ8_spl|sQ99_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1167,f530,f1180])).
% 1.44/0.79 fof(f1184,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl))=sK48_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f136,f502])).
% 1.44/0.79 fof(f1185,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(sK51_skl)|app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl))=sK51_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f136,f517])).
% 1.44/0.79 fof(f1186,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(nil)|app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil))=nil),
% 1.44/0.79 inference(resolution,[status(thm)],[f136,f821])).
% 1.44/0.79 fof(f1187,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl))=sK47_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f136,f559])).
% 1.44/0.79 fof(f1188,definition,(
% 1.44/0.79 sQ100_spl <=> (app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl))=sK48_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1189,plain,(
% 1.44/0.79 app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl))=sK48_skl|~sQ100_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1188])).
% 1.44/0.79 fof(f1191,plain,(
% 1.44/0.79 ~sQ12_spl|sQ100_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1184,f554,f1188])).
% 1.44/0.79 fof(f1192,definition,(
% 1.44/0.79 sQ101_spl <=> (app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl))=sK51_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1193,plain,(
% 1.44/0.79 app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl))=sK51_skl|~sQ101_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1192])).
% 1.44/0.79 fof(f1195,plain,(
% 1.44/0.79 ~sQ7_spl|sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1185,f527,f1192])).
% 1.44/0.79 fof(f1196,definition,(
% 1.44/0.79 sQ102_spl <=> (app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil))=nil)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1197,plain,(
% 1.44/0.79 app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil))=nil|~sQ102_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1196])).
% 1.44/0.79 fof(f1199,plain,(
% 1.44/0.79 ~sQ10_spl|sQ102_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1186,f545,f1196])).
% 1.44/0.79 fof(f1200,definition,(
% 1.44/0.79 sQ103_spl <=> (app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1201,plain,(
% 1.44/0.79 app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ103_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1200])).
% 1.44/0.79 fof(f1203,plain,(
% 1.44/0.79 ~sQ8_spl|sQ103_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1187,f530,f1200])).
% 1.44/0.79 fof(f1204,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(nil)|app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl))=sK51_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1129,f136])).
% 1.44/0.79 fof(f1205,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(nil)|ssList(sK8_skl(nil,sK51_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1129,f135])).
% 1.44/0.79 fof(f1206,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(nil)|ssList(sK7_skl(nil,sK51_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1129,f134])).
% 1.44/0.79 fof(f1207,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(sK51_skl)|~segmentP(nil,sK51_skl)|nil=sK51_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1129,f317])).
% 1.44/0.79 fof(f1208,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK51_skl)|~ssList(nil)|~segmentP(X0,sK51_skl)|segmentP(X0,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1129,f315])).
% 1.44/0.79 fof(f1209,definition,(
% 1.44/0.79 sQ104_spl <=> (app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl))=sK51_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1210,plain,(
% 1.44/0.79 app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl))=sK51_skl|~sQ104_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1209])).
% 1.44/0.79 fof(f1212,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ10_spl|sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1204,f527,f545,f1209])).
% 1.44/0.79 fof(f1213,definition,(
% 1.44/0.79 sQ105_spl <=> (ssList(sK8_skl(nil,sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1216,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ10_spl|sQ105_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1205,f527,f545,f1213])).
% 1.44/0.79 fof(f1217,definition,(
% 1.44/0.79 sQ106_spl <=> (ssList(sK7_skl(nil,sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1220,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ10_spl|sQ106_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1206,f527,f545,f1217])).
% 1.44/0.79 fof(f1221,definition,(
% 1.44/0.79 sQ107_spl <=> (segmentP(nil,sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1224,plain,(
% 1.44/0.79 ~sQ10_spl|~sQ7_spl|~sQ107_spl|sQ46_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1207,f545,f527,f1221,f751])).
% 1.44/0.79 fof(f1225,definition,(
% 1.44/0.79 ![X0]: (sQ108_spl <=> (~ssList(X0)|~segmentP(X0,sK51_skl)|segmentP(X0,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1228,plain,(
% 1.44/0.79 sQ108_spl|~sQ7_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1208,f1225,f527,f545])).
% 1.44/0.79 fof(f1229,plain,(
% 1.44/0.79 sQ64_spl|~sQ46_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f954,f867,f751])).
% 1.44/0.79 fof(f1252,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(nil)|app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl))=sK47_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1130,f136])).
% 1.44/0.79 fof(f1253,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(nil)|ssList(sK8_skl(nil,sK47_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1130,f135])).
% 1.44/0.79 fof(f1254,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(nil)|ssList(sK7_skl(nil,sK47_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1130,f134])).
% 1.44/0.79 fof(f1256,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~segmentP(X0,sK47_skl)|segmentP(X0,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1130,f315])).
% 1.44/0.79 fof(f1257,definition,(
% 1.44/0.79 sQ111_spl <=> (app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl))=sK47_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1258,plain,(
% 1.44/0.79 app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl))=sK47_skl|~sQ111_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1257])).
% 1.44/0.79 fof(f1260,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ10_spl|sQ111_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1252,f530,f545,f1257])).
% 1.44/0.79 fof(f1261,definition,(
% 1.44/0.79 sQ112_spl <=> (ssList(sK8_skl(nil,sK47_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1264,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ10_spl|sQ112_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1253,f530,f545,f1261])).
% 1.44/0.79 fof(f1265,definition,(
% 1.44/0.79 sQ113_spl <=> (ssList(sK7_skl(nil,sK47_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1268,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ10_spl|sQ113_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1254,f530,f545,f1265])).
% 1.44/0.79 fof(f1273,definition,(
% 1.44/0.79 ![X0]: (sQ115_spl <=> (~ssList(X0)|~segmentP(X0,sK47_skl)|segmentP(X0,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1276,plain,(
% 1.44/0.79 sQ115_spl|~sQ8_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1256,f1273,f530,f545])).
% 1.44/0.79 fof(f1277,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(nil)|app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl))=sK48_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1131,f136])).
% 1.44/0.79 fof(f1278,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(nil)|ssList(sK8_skl(nil,sK48_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1131,f135])).
% 1.44/0.79 fof(f1279,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(nil)|ssList(sK7_skl(nil,sK48_skl))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1131,f134])).
% 1.44/0.79 fof(f1280,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(sK48_skl)|~segmentP(nil,sK48_skl)|nil=sK48_skl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1131,f317])).
% 1.44/0.79 fof(f1281,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~segmentP(X0,sK48_skl)|segmentP(X0,nil))),
% 1.44/0.79 inference(resolution,[status(thm)],[f1131,f315])).
% 1.44/0.79 fof(f1282,definition,(
% 1.44/0.79 sQ116_spl <=> (app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl))=sK48_skl)),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1283,plain,(
% 1.44/0.79 app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl))=sK48_skl|~sQ116_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1282])).
% 1.44/0.79 fof(f1285,plain,(
% 1.44/0.79 ~sQ12_spl|~sQ10_spl|sQ116_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1277,f554,f545,f1282])).
% 1.44/0.79 fof(f1286,definition,(
% 1.44/0.79 sQ117_spl <=> (ssList(sK8_skl(nil,sK48_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1289,plain,(
% 1.44/0.79 ~sQ12_spl|~sQ10_spl|sQ117_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1278,f554,f545,f1286])).
% 1.44/0.79 fof(f1290,definition,(
% 1.44/0.79 sQ118_spl <=> (ssList(sK7_skl(nil,sK48_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1293,plain,(
% 1.44/0.79 ~sQ12_spl|~sQ10_spl|sQ118_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1279,f554,f545,f1290])).
% 1.44/0.79 fof(f1294,definition,(
% 1.44/0.79 sQ119_spl <=> (segmentP(nil,sK48_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1296,plain,(
% 1.44/0.79 ~segmentP(nil,sK48_skl)|sQ119_spl),
% 1.44/0.79 inference(component_clause,[status(thm)],[f1294])).
% 1.44/0.79 fof(f1297,plain,(
% 1.44/0.79 ~sQ10_spl|~sQ12_spl|~sQ119_spl|sQ62_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1280,f545,f554,f1294,f860])).
% 1.44/0.79 fof(f1298,definition,(
% 1.44/0.79 ![X0]: (sQ120_spl <=> (~ssList(X0)|~segmentP(X0,sK48_skl)|segmentP(X0,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1301,plain,(
% 1.44/0.79 sQ120_spl|~sQ12_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1281,f1298,f554,f545])).
% 1.44/0.79 fof(f1330,plain,(
% 1.44/0.79 ~ssList(nil)|nil=nil),
% 1.44/0.79 inference(resolution,[status(thm)],[f326,f821])).
% 1.44/0.79 fof(f1331,plain,(
% 1.44/0.79 ~sQ10_spl|sQ74_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1330,f545,f980])).
% 1.44/0.79 fof(f1479,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|ssList(app(sK47_skl,X0)))),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f425,f495])).
% 1.44/0.79 fof(f1483,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK8_skl(sK48_skl,sK48_skl))|~ssList(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl))|~sK48_skl=app(X0,sK8_skl(sK48_skl,sK48_skl))|app(sK7_skl(sK48_skl,sK48_skl),sK48_skl)=X0|~sQ100_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1189,f376])).
% 1.44/0.79 fof(f1484,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK8_skl(sK47_skl,sK47_skl))|~ssList(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl))|~sK47_skl=app(X0,sK8_skl(sK47_skl,sK47_skl))|app(sK7_skl(sK47_skl,sK47_skl),sK47_skl)=X0|~sQ103_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1201,f376])).
% 1.44/0.79 fof(f1485,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK48_skl)|~sK48_skl=app(X0,nil)|sK48_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f512,f376])).
% 1.44/0.79 fof(f1486,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(cons(sK0_skl,nil))|~cons(sK0_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK0_skl,nil)=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f609,f376])).
% 1.44/0.79 fof(f1487,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(cons(sK0_skl,nil))|~cons(sK0_skl,nil)=app(X0,nil)|cons(sK0_skl,nil)=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f923,f376])).
% 1.44/0.79 fof(f1488,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(cons(sK0_skl,nil))|~cons(sK0_skl,sK47_skl)=app(X0,sK47_skl)|cons(sK0_skl,nil)=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f607,f376])).
% 1.44/0.79 fof(f1489,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(cons(sK1_skl,nil))|~cons(sK1_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK1_skl,nil)=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f608,f376])).
% 1.44/0.79 fof(f1490,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(cons(sK1_skl,nil))|~cons(sK1_skl,nil)=app(X0,nil)|cons(sK1_skl,nil)=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f922,f376])).
% 1.44/0.79 fof(f1491,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(cons(sK1_skl,nil))|~cons(sK1_skl,sK47_skl)=app(X0,sK47_skl)|cons(sK1_skl,nil)=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f606,f376])).
% 1.44/0.79 fof(f1492,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~sK48_skl=app(X0,sK48_skl)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f499,f376])).
% 1.44/0.79 fof(f1493,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~nil=app(X0,nil)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f819,f376])).
% 1.44/0.79 fof(f1494,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~sK47_skl=app(X0,sK47_skl)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f540,f376])).
% 1.44/0.79 fof(f1496,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK47_skl)|~sK47_skl=app(X0,nil)|sK47_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f611,f376])).
% 1.44/0.79 fof(f1512,definition,(
% 1.44/0.79 ![X0]: (sQ151_spl <=> (~ssList(X0)|~sK48_skl=app(X0,sK8_skl(sK48_skl,sK48_skl))|app(sK7_skl(sK48_skl,sK48_skl),sK48_skl)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1515,definition,(
% 1.44/0.79 sQ152_spl <=> (ssList(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1518,plain,(
% 1.44/0.79 sQ151_spl|~sQ96_spl|~sQ152_spl|~sQ100_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1483,f1512,f1168,f1515,f1188])).
% 1.44/0.79 fof(f1519,definition,(
% 1.44/0.79 ![X0]: (sQ153_spl <=> (~ssList(X0)|~sK47_skl=app(X0,sK8_skl(sK47_skl,sK47_skl))|app(sK7_skl(sK47_skl,sK47_skl),sK47_skl)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1522,definition,(
% 1.44/0.79 sQ154_spl <=> (ssList(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1525,plain,(
% 1.44/0.79 sQ153_spl|~sQ99_spl|~sQ154_spl|~sQ103_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1484,f1519,f1180,f1522,f1200])).
% 1.44/0.79 fof(f1526,definition,(
% 1.44/0.79 ![X0]: (sQ155_spl <=> (~ssList(X0)|~sK48_skl=app(X0,nil)|sK48_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1529,plain,(
% 1.44/0.79 sQ155_spl|~sQ10_spl|~sQ12_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1485,f1526,f545,f554])).
% 1.44/0.79 fof(f1530,definition,(
% 1.44/0.79 ![X0]: (sQ156_spl <=> (~ssList(X0)|~cons(sK0_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK0_skl,nil)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1533,plain,(
% 1.44/0.79 sQ156_spl|~sQ12_spl|~sQ36_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1486,f1530,f554,f697])).
% 1.44/0.79 fof(f1534,definition,(
% 1.44/0.79 ![X0]: (sQ157_spl <=> (~ssList(X0)|~cons(sK0_skl,nil)=app(X0,nil)|cons(sK0_skl,nil)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1537,plain,(
% 1.44/0.79 sQ157_spl|~sQ10_spl|~sQ36_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1487,f1534,f545,f697])).
% 1.44/0.79 fof(f1538,definition,(
% 1.44/0.79 ![X0]: (sQ158_spl <=> (~ssList(X0)|~cons(sK0_skl,sK47_skl)=app(X0,sK47_skl)|cons(sK0_skl,nil)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1541,plain,(
% 1.44/0.79 sQ158_spl|~sQ8_spl|~sQ36_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1488,f1538,f530,f697])).
% 1.44/0.79 fof(f1542,definition,(
% 1.44/0.79 ![X0]: (sQ159_spl <=> (~ssList(X0)|~cons(sK1_skl,sK48_skl)=app(X0,sK48_skl)|cons(sK1_skl,nil)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1545,plain,(
% 1.44/0.79 sQ159_spl|~sQ12_spl|~sQ31_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1489,f1542,f554,f677])).
% 1.44/0.79 fof(f1546,definition,(
% 1.44/0.79 ![X0]: (sQ160_spl <=> (~ssList(X0)|~cons(sK1_skl,nil)=app(X0,nil)|cons(sK1_skl,nil)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1549,plain,(
% 1.44/0.79 sQ160_spl|~sQ10_spl|~sQ31_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1490,f1546,f545,f677])).
% 1.44/0.79 fof(f1550,definition,(
% 1.44/0.79 ![X0]: (sQ161_spl <=> (~ssList(X0)|~cons(sK1_skl,sK47_skl)=app(X0,sK47_skl)|cons(sK1_skl,nil)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1553,plain,(
% 1.44/0.79 sQ161_spl|~sQ8_spl|~sQ31_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1491,f1550,f530,f677])).
% 1.44/0.79 fof(f1554,definition,(
% 1.44/0.79 ![X0]: (sQ162_spl <=> (~ssList(X0)|~sK48_skl=app(X0,sK48_skl)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1557,plain,(
% 1.44/0.79 sQ162_spl|~sQ12_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1492,f1554,f554,f545])).
% 1.44/0.79 fof(f1558,definition,(
% 1.44/0.79 ![X0]: (sQ163_spl <=> (~ssList(X0)|~nil=app(X0,nil)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1561,plain,(
% 1.44/0.79 sQ163_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1493,f1558,f545])).
% 1.44/0.79 fof(f1562,definition,(
% 1.44/0.79 ![X0]: (sQ164_spl <=> (~ssList(X0)|~sK47_skl=app(X0,sK47_skl)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1565,plain,(
% 1.44/0.79 sQ164_spl|~sQ8_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1494,f1562,f530,f545])).
% 1.44/0.79 fof(f1570,definition,(
% 1.44/0.79 ![X0]: (sQ166_spl <=> (~ssList(X0)|~sK47_skl=app(X0,nil)|sK47_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1573,plain,(
% 1.44/0.79 sQ166_spl|~sQ10_spl|~sQ8_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1496,f1570,f545,f530])).
% 1.44/0.79 fof(f1592,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl))|~ssList(sK8_skl(sK51_skl,sK51_skl))|~ssList(X0)|~app(X0,sK8_skl(sK51_skl,sK51_skl))=sK51_skl|X0=app(sK7_skl(sK51_skl,sK51_skl),sK51_skl)|~sQ101_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1193,f376])).
% 1.44/0.79 fof(f1594,definition,(
% 1.44/0.79 sQ168_spl <=> (ssList(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1597,definition,(
% 1.44/0.79 ![X0]: (sQ169_spl <=> (~ssList(X0)|~app(X0,sK8_skl(sK51_skl,sK51_skl))=sK51_skl|X0=app(sK7_skl(sK51_skl,sK51_skl),sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1600,plain,(
% 1.44/0.79 ~sQ168_spl|~sQ97_spl|sQ169_spl|~sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1592,f1594,f1172,f1597,f1192])).
% 1.44/0.79 fof(f1612,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl))|~ssList(sK8_skl(sK51_skl,sK51_skl))|~sK51_skl=app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),X0)|sK8_skl(sK51_skl,sK51_skl)=X0|~sQ101_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1193,f378])).
% 1.44/0.79 fof(f1613,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl))|~ssList(sK8_skl(sK48_skl,sK48_skl))|~sK48_skl=app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),X0)|sK8_skl(sK48_skl,sK48_skl)=X0|~sQ100_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1189,f378])).
% 1.44/0.79 fof(f1614,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl))|~ssList(sK8_skl(sK47_skl,sK47_skl))|~sK47_skl=app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),X0)|sK8_skl(sK47_skl,sK47_skl)=X0|~sQ103_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1201,f378])).
% 1.44/0.79 fof(f1615,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(nil)|~sK48_skl=app(sK48_skl,X0)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f512,f378])).
% 1.44/0.79 fof(f1616,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(cons(sK0_skl,nil))|~ssList(sK48_skl)|~cons(sK0_skl,sK48_skl)=app(cons(sK0_skl,nil),X0)|sK48_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f609,f378])).
% 1.44/0.79 fof(f1617,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(cons(sK0_skl,nil))|~ssList(nil)|~cons(sK0_skl,nil)=app(cons(sK0_skl,nil),X0)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f923,f378])).
% 1.44/0.79 fof(f1618,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(cons(sK0_skl,nil))|~ssList(sK47_skl)|~cons(sK0_skl,sK47_skl)=app(cons(sK0_skl,nil),X0)|sK47_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f607,f378])).
% 1.44/0.79 fof(f1619,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(cons(sK1_skl,nil))|~ssList(sK48_skl)|~cons(sK1_skl,sK48_skl)=app(cons(sK1_skl,nil),X0)|sK48_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f608,f378])).
% 1.44/0.79 fof(f1620,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(cons(sK1_skl,nil))|~ssList(nil)|~cons(sK1_skl,nil)=app(cons(sK1_skl,nil),X0)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f922,f378])).
% 1.44/0.79 fof(f1621,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(cons(sK1_skl,nil))|~ssList(sK47_skl)|~cons(sK1_skl,sK47_skl)=app(cons(sK1_skl,nil),X0)|sK47_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f606,f378])).
% 1.44/0.79 fof(f1622,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK48_skl)|~sK48_skl=app(nil,X0)|sK48_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f499,f378])).
% 1.44/0.79 fof(f1623,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~nil=app(nil,X0)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f819,f378])).
% 1.44/0.79 fof(f1624,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sK47_skl)|~sK47_skl=app(nil,X0)|sK47_skl=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f540,f378])).
% 1.44/0.79 fof(f1625,plain,(
% 1.44/0.79 ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~sK47_skl=app(sK47_skl,X0)|nil=X0)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f611,f378])).
% 1.44/0.79 fof(f1641,definition,(
% 1.44/0.79 ![X0]: (sQ170_spl <=> (~ssList(X0)|~sK51_skl=app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),X0)|sK8_skl(sK51_skl,sK51_skl)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1644,plain,(
% 1.44/0.79 sQ170_spl|~sQ168_spl|~sQ97_spl|~sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1612,f1641,f1594,f1172,f1192])).
% 1.44/0.79 fof(f1645,definition,(
% 1.44/0.79 ![X0]: (sQ171_spl <=> (~ssList(X0)|~sK48_skl=app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),X0)|sK8_skl(sK48_skl,sK48_skl)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1648,plain,(
% 1.44/0.79 sQ171_spl|~sQ152_spl|~sQ96_spl|~sQ100_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1613,f1645,f1515,f1168,f1188])).
% 1.44/0.79 fof(f1649,definition,(
% 1.44/0.79 ![X0]: (sQ172_spl <=> (~ssList(X0)|~sK47_skl=app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),X0)|sK8_skl(sK47_skl,sK47_skl)=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1652,plain,(
% 1.44/0.79 sQ172_spl|~sQ154_spl|~sQ99_spl|~sQ103_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1614,f1649,f1522,f1180,f1200])).
% 1.44/0.79 fof(f1653,definition,(
% 1.44/0.79 ![X0]: (sQ173_spl <=> (~ssList(X0)|~sK48_skl=app(sK48_skl,X0)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1656,plain,(
% 1.44/0.79 sQ173_spl|~sQ12_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1615,f1653,f554,f545])).
% 1.44/0.79 fof(f1657,definition,(
% 1.44/0.79 ![X0]: (sQ174_spl <=> (~ssList(X0)|~cons(sK0_skl,sK48_skl)=app(cons(sK0_skl,nil),X0)|sK48_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1660,plain,(
% 1.44/0.79 sQ174_spl|~sQ36_spl|~sQ12_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1616,f1657,f697,f554])).
% 1.44/0.79 fof(f1661,definition,(
% 1.44/0.79 ![X0]: (sQ175_spl <=> (~ssList(X0)|~cons(sK0_skl,nil)=app(cons(sK0_skl,nil),X0)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1664,plain,(
% 1.44/0.79 sQ175_spl|~sQ36_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1617,f1661,f697,f545])).
% 1.44/0.79 fof(f1665,definition,(
% 1.44/0.79 ![X0]: (sQ176_spl <=> (~ssList(X0)|~cons(sK0_skl,sK47_skl)=app(cons(sK0_skl,nil),X0)|sK47_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1668,plain,(
% 1.44/0.79 sQ176_spl|~sQ36_spl|~sQ8_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1618,f1665,f697,f530])).
% 1.44/0.79 fof(f1669,definition,(
% 1.44/0.79 ![X0]: (sQ177_spl <=> (~ssList(X0)|~cons(sK1_skl,sK48_skl)=app(cons(sK1_skl,nil),X0)|sK48_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1672,plain,(
% 1.44/0.79 sQ177_spl|~sQ31_spl|~sQ12_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1619,f1669,f677,f554])).
% 1.44/0.79 fof(f1673,definition,(
% 1.44/0.79 ![X0]: (sQ178_spl <=> (~ssList(X0)|~cons(sK1_skl,nil)=app(cons(sK1_skl,nil),X0)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1676,plain,(
% 1.44/0.79 sQ178_spl|~sQ31_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1620,f1673,f677,f545])).
% 1.44/0.79 fof(f1677,definition,(
% 1.44/0.79 ![X0]: (sQ179_spl <=> (~ssList(X0)|~cons(sK1_skl,sK47_skl)=app(cons(sK1_skl,nil),X0)|sK47_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1680,plain,(
% 1.44/0.79 sQ179_spl|~sQ31_spl|~sQ8_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1621,f1677,f677,f530])).
% 1.44/0.79 fof(f1681,definition,(
% 1.44/0.79 ![X0]: (sQ180_spl <=> (~ssList(X0)|~sK48_skl=app(nil,X0)|sK48_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1684,plain,(
% 1.44/0.79 sQ180_spl|~sQ10_spl|~sQ12_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1622,f1681,f545,f554])).
% 1.44/0.79 fof(f1685,definition,(
% 1.44/0.79 ![X0]: (sQ181_spl <=> (~ssList(X0)|~nil=app(nil,X0)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1688,plain,(
% 1.44/0.79 sQ181_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1623,f1685,f545])).
% 1.44/0.79 fof(f1689,definition,(
% 1.44/0.79 ![X0]: (sQ182_spl <=> (~ssList(X0)|~sK47_skl=app(nil,X0)|sK47_skl=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1692,plain,(
% 1.44/0.79 sQ182_spl|~sQ10_spl|~sQ8_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1624,f1689,f545,f530])).
% 1.44/0.79 fof(f1693,definition,(
% 1.44/0.79 ![X0]: (sQ183_spl <=> (~ssList(X0)|~sK47_skl=app(sK47_skl,X0)|nil=X0))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1696,plain,(
% 1.44/0.79 sQ183_spl|~sQ8_spl|~sQ10_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1625,f1693,f530,f545])).
% 1.44/0.79 fof(f1718,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK51_skl)|~ssList(sK47_skl)|~ssList(X0)|~app(sK47_skl,X0)=sK48_skl|X0=sK51_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f522,f378])).
% 1.44/0.79 fof(f1720,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK47_skl)|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=sK48_skl|X0=sK47_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f522,f376])).
% 1.44/0.79 fof(f1722,definition,(
% 1.44/0.79 ![X0]: (sQ184_spl <=> (~ssList(X0)|~app(sK47_skl,X0)=sK48_skl|X0=sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1725,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ8_spl|sQ184_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1718,f527,f530,f1722])).
% 1.44/0.79 fof(f1727,definition,(
% 1.44/0.79 ![X0]: (sQ185_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=sK48_skl|X0=sK47_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1730,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ7_spl|sQ185_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1720,f530,f527,f1727])).
% 1.44/0.79 fof(f1732,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK51_skl)|~ssList(cons(sK0_skl,nil))|~ssList(X0)|~app(cons(sK0_skl,nil),X0)=cons(sK0_skl,sK51_skl)|X0=sK51_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f633,f378])).
% 1.44/0.79 fof(f1734,plain,(
% 1.44/0.79 ![X0]: (~ssList(cons(sK0_skl,nil))|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=cons(sK0_skl,sK51_skl)|X0=cons(sK0_skl,nil))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f633,f376])).
% 1.44/0.79 fof(f1736,definition,(
% 1.44/0.79 ![X0]: (sQ186_spl <=> (~ssList(X0)|~app(cons(sK0_skl,nil),X0)=cons(sK0_skl,sK51_skl)|X0=sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1739,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ36_spl|sQ186_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1732,f527,f697,f1736])).
% 1.44/0.79 fof(f1741,definition,(
% 1.44/0.79 ![X0]: (sQ187_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=cons(sK0_skl,sK51_skl)|X0=cons(sK0_skl,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1744,plain,(
% 1.44/0.79 ~sQ36_spl|~sQ7_spl|sQ187_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1734,f697,f527,f1741])).
% 1.44/0.79 fof(f1746,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK51_skl)|~ssList(cons(sK1_skl,nil))|~ssList(X0)|~app(cons(sK1_skl,nil),X0)=cons(sK1_skl,sK51_skl)|X0=sK51_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f632,f378])).
% 1.44/0.79 fof(f1748,plain,(
% 1.44/0.79 ![X0]: (~ssList(cons(sK1_skl,nil))|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=cons(sK1_skl,sK51_skl)|X0=cons(sK1_skl,nil))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f632,f376])).
% 1.44/0.79 fof(f1750,definition,(
% 1.44/0.79 ![X0]: (sQ188_spl <=> (~ssList(X0)|~app(cons(sK1_skl,nil),X0)=cons(sK1_skl,sK51_skl)|X0=sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1753,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ31_spl|sQ188_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1746,f527,f677,f1750])).
% 1.44/0.79 fof(f1755,definition,(
% 1.44/0.79 ![X0]: (sQ189_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=cons(sK1_skl,sK51_skl)|X0=cons(sK1_skl,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1758,plain,(
% 1.44/0.79 ~sQ31_spl|~sQ7_spl|sQ189_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1748,f677,f527,f1755])).
% 1.44/0.79 fof(f1764,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK51_skl)|~ssList(nil)|~ssList(X0)|~app(nil,X0)=sK51_skl|X0=sK51_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f518,f378])).
% 1.44/0.79 fof(f1766,plain,(
% 1.44/0.79 ![X0]: (~ssList(nil)|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=sK51_skl|X0=nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f518,f376])).
% 1.44/0.79 fof(f1768,definition,(
% 1.44/0.79 ![X0]: (sQ190_spl <=> (~ssList(X0)|~app(nil,X0)=sK51_skl|X0=sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1771,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ10_spl|sQ190_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1764,f527,f545,f1768])).
% 1.44/0.79 fof(f1773,definition,(
% 1.44/0.79 ![X0]: (sQ191_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=sK51_skl|X0=nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1776,plain,(
% 1.44/0.79 ~sQ10_spl|~sQ7_spl|sQ191_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1766,f545,f527,f1773])).
% 1.44/0.79 fof(f1790,plain,(
% 1.44/0.79 ![X0]: (~ssList(nil)|~ssList(sK51_skl)|~ssList(X0)|~app(sK51_skl,X0)=sK51_skl|X0=nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f515,f378])).
% 1.44/0.79 fof(f1792,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK51_skl)|~ssList(nil)|~ssList(X0)|~app(X0,nil)=sK51_skl|X0=sK51_skl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f515,f376])).
% 1.44/0.79 fof(f1794,definition,(
% 1.44/0.79 ![X0]: (sQ192_spl <=> (~ssList(X0)|~app(sK51_skl,X0)=sK51_skl|X0=nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1797,plain,(
% 1.44/0.79 ~sQ10_spl|~sQ7_spl|sQ192_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1790,f545,f527,f1794])).
% 1.44/0.79 fof(f1799,definition,(
% 1.44/0.79 ![X0]: (sQ193_spl <=> (~ssList(X0)|~app(X0,nil)=sK51_skl|X0=sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1802,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ10_spl|sQ193_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1792,f527,f545,f1799])).
% 1.44/0.79 fof(f1922,plain,(
% 1.44/0.79 ~ssList(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl))|~ssList(sK8_skl(sK51_skl,sK51_skl))|~nil=sK51_skl|nil=sK8_skl(sK51_skl,sK51_skl)|~sQ101_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1193,f385])).
% 1.44/0.79 fof(f1926,plain,(
% 1.44/0.79 ~ssList(cons(sK0_skl,nil))|~ssList(sK51_skl)|~nil=cons(sK0_skl,sK51_skl)|nil=sK51_skl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f633,f385])).
% 1.44/0.79 fof(f1930,plain,(
% 1.44/0.79 ~ssList(cons(sK1_skl,nil))|~ssList(sK51_skl)|~nil=cons(sK1_skl,sK51_skl)|nil=sK51_skl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f632,f385])).
% 1.44/0.79 fof(f1938,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK51_skl)|~nil=sK48_skl|nil=sK51_skl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f522,f385])).
% 1.44/0.79 fof(f1942,definition,(
% 1.44/0.79 sQ212_spl <=> (nil=sK8_skl(sK51_skl,sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1945,plain,(
% 1.44/0.79 ~sQ168_spl|~sQ97_spl|~sQ46_spl|sQ212_spl|~sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1922,f1594,f1172,f751,f1942,f1192])).
% 1.44/0.79 fof(f1955,definition,(
% 1.44/0.79 sQ215_spl <=> (nil=cons(sK0_skl,sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1958,plain,(
% 1.44/0.79 ~sQ36_spl|~sQ7_spl|~sQ215_spl|sQ46_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1926,f697,f527,f1955,f751])).
% 1.44/0.79 fof(f1963,definition,(
% 1.44/0.79 sQ217_spl <=> (nil=cons(sK0_skl,nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1971,definition,(
% 1.44/0.79 sQ219_spl <=> (nil=cons(sK1_skl,sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1974,plain,(
% 1.44/0.79 ~sQ31_spl|~sQ7_spl|~sQ219_spl|sQ46_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1930,f677,f527,f1971,f751])).
% 1.44/0.79 fof(f1979,definition,(
% 1.44/0.79 sQ221_spl <=> (nil=cons(sK1_skl,nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f1991,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ7_spl|~sQ62_spl|sQ46_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1938,f530,f527,f860,f751])).
% 1.44/0.79 fof(f1995,plain,(
% 1.44/0.79 ~ssList(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl))|~ssList(sK8_skl(sK51_skl,sK51_skl))|~nil=sK51_skl|nil=app(sK7_skl(sK51_skl,sK51_skl),sK51_skl)|~sQ101_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1193,f386])).
% 1.44/0.79 fof(f1999,plain,(
% 1.44/0.79 ~ssList(cons(sK0_skl,nil))|~ssList(sK51_skl)|~nil=cons(sK0_skl,sK51_skl)|nil=cons(sK0_skl,nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f633,f386])).
% 1.44/0.79 fof(f2003,plain,(
% 1.44/0.79 ~ssList(cons(sK1_skl,nil))|~ssList(sK51_skl)|~nil=cons(sK1_skl,sK51_skl)|nil=cons(sK1_skl,nil)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f632,f386])).
% 1.44/0.79 fof(f2011,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK51_skl)|~nil=sK48_skl|nil=sK47_skl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f522,f386])).
% 1.44/0.79 fof(f2015,definition,(
% 1.44/0.79 sQ223_spl <=> (nil=app(sK7_skl(sK51_skl,sK51_skl),sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2018,plain,(
% 1.44/0.79 ~sQ168_spl|~sQ97_spl|~sQ46_spl|sQ223_spl|~sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1995,f1594,f1172,f751,f2015,f1192])).
% 1.44/0.79 fof(f2028,plain,(
% 1.44/0.79 ~sQ36_spl|~sQ7_spl|~sQ215_spl|sQ217_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f1999,f697,f527,f1955,f1963])).
% 1.44/0.79 fof(f2032,plain,(
% 1.44/0.79 ~sQ31_spl|~sQ7_spl|~sQ219_spl|sQ221_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2003,f677,f527,f1971,f1979])).
% 1.44/0.79 fof(f2040,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ7_spl|~sQ62_spl|sQ48_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2011,f530,f527,f860,f758])).
% 1.44/0.79 fof(f2532,plain,(
% 1.44/0.79 $false|sQ31_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f927,f679])).
% 1.44/0.79 fof(f2533,plain,(
% 1.44/0.79 sQ31_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f2532])).
% 1.44/0.79 fof(f2536,plain,(
% 1.44/0.79 $false|sQ36_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f928,f699])).
% 1.44/0.79 fof(f2537,plain,(
% 1.44/0.79 sQ36_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f2536])).
% 1.44/0.79 fof(f2540,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(sK51_skl)|segmentP(app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl)),sK51_skl)|~ssList(sK7_skl(sK51_skl,sK51_skl))|~ssList(sK8_skl(sK51_skl,sK51_skl))|~sQ101_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1193,f465])).
% 1.44/0.79 fof(f2541,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(sK48_skl)|segmentP(app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl)),sK48_skl)|~ssList(sK7_skl(sK48_skl,sK48_skl))|~ssList(sK8_skl(sK48_skl,sK48_skl))|~sQ100_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1189,f465])).
% 1.44/0.79 fof(f2542,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(sK47_skl)|segmentP(app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl)),sK47_skl)|~ssList(sK7_skl(sK47_skl,sK47_skl))|~ssList(sK8_skl(sK47_skl,sK47_skl))|~sQ103_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1201,f465])).
% 1.44/0.79 fof(f2544,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(sK8_skl(sK51_skl,sK51_skl))|segmentP(app(app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl)),X0),sK8_skl(sK51_skl,sK51_skl))|~ssList(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl))|~ssList(X0)|~sQ101_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1193,f465])).
% 1.44/0.79 fof(f2545,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK8_skl(sK48_skl,sK48_skl))|segmentP(app(app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl)),X0),sK8_skl(sK48_skl,sK48_skl))|~ssList(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl))|~ssList(X0)|~sQ100_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1189,f465])).
% 1.44/0.79 fof(f2546,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK8_skl(sK47_skl,sK47_skl))|segmentP(app(app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl)),X0),sK8_skl(sK47_skl,sK47_skl))|~ssList(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl))|~ssList(X0)|~sQ103_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1201,f465])).
% 1.44/0.79 fof(f2550,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(cons(sK0_skl,nil),X0))|~ssList(nil)|segmentP(app(app(cons(sK0_skl,nil),nil),X0),nil)|~ssList(cons(sK0_skl,nil))|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f923,f465])).
% 1.44/0.79 fof(f2554,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(cons(sK1_skl,nil),X0))|~ssList(nil)|segmentP(app(app(cons(sK1_skl,nil),nil),X0),nil)|~ssList(cons(sK1_skl,nil))|~ssList(X0))),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f922,f465])).
% 1.44/0.79 fof(f2562,definition,(
% 1.44/0.79 sQ323_spl <=> (segmentP(app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl)),sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2565,plain,(
% 1.44/0.79 ~sQ7_spl|sQ323_spl|~sQ88_spl|~sQ97_spl|~sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2540,f527,f2562,f1098,f1172,f1192])).
% 1.44/0.79 fof(f2566,definition,(
% 1.44/0.79 sQ324_spl <=> (segmentP(app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl)),sK48_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2569,plain,(
% 1.44/0.79 ~sQ12_spl|sQ324_spl|~sQ91_spl|~sQ96_spl|~sQ100_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2541,f554,f2566,f1116,f1168,f1188])).
% 1.44/0.79 fof(f2570,definition,(
% 1.44/0.79 sQ325_spl <=> (segmentP(app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl)),sK47_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2573,plain,(
% 1.44/0.79 ~sQ8_spl|sQ325_spl|~sQ90_spl|~sQ99_spl|~sQ103_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2542,f530,f2570,f1106,f1180,f1200])).
% 1.44/0.79 fof(f2575,definition,(
% 1.44/0.79 ![X0]: (sQ326_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(app(sK7_skl(sK51_skl,sK51_skl),sK51_skl),sK8_skl(sK51_skl,sK51_skl)),X0),sK8_skl(sK51_skl,sK51_skl))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2578,plain,(
% 1.44/0.79 sQ326_spl|~sQ97_spl|~sQ168_spl|~sQ101_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2544,f2575,f1172,f1594,f1192])).
% 1.44/0.79 fof(f2579,definition,(
% 1.44/0.79 ![X0]: (sQ327_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl)),X0),sK8_skl(sK48_skl,sK48_skl))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2582,plain,(
% 1.44/0.79 sQ327_spl|~sQ96_spl|~sQ152_spl|~sQ100_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2545,f2579,f1168,f1515,f1188])).
% 1.44/0.79 fof(f2583,definition,(
% 1.44/0.79 ![X0]: (sQ328_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(app(sK7_skl(sK47_skl,sK47_skl),sK47_skl),sK8_skl(sK47_skl,sK47_skl)),X0),sK8_skl(sK47_skl,sK47_skl))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2586,plain,(
% 1.44/0.79 sQ328_spl|~sQ99_spl|~sQ154_spl|~sQ103_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2546,f2583,f1180,f1522,f1200])).
% 1.44/0.79 fof(f2590,plain,(
% 1.44/0.79 sQ40_spl|~sQ10_spl|~sQ36_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2550,f724,f545,f697])).
% 1.44/0.79 fof(f2594,plain,(
% 1.44/0.79 sQ38_spl|~sQ10_spl|~sQ31_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2554,f712,f545,f677])).
% 1.44/0.79 fof(f2605,plain,(
% 1.44/0.79 $false|sQ10_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f223,f547])).
% 1.44/0.79 fof(f2606,plain,(
% 1.44/0.79 sQ10_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f2605])).
% 1.44/0.79 fof(f2609,plain,(
% 1.44/0.79 ![X0]: (segmentP(app(sK47_skl,X0),sK47_skl)|~ssList(X0)|~sQ9_spl)),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f549,f1479])).
% 1.44/0.79 fof(f2615,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK51_skl,X0))|segmentP(app(sK51_skl,X0),sK51_skl)|~ssList(X0)|~sQ26_spl)),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f518,f641])).
% 1.44/0.79 fof(f2616,plain,(
% 1.44/0.79 ![X0]: (segmentP(app(sK51_skl,X0),sK51_skl)|~ssList(X0)|~sQ26_spl)),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2615,f519])).
% 1.44/0.79 fof(f2619,plain,(
% 1.44/0.79 segmentP(app(sK47_skl,sK51_skl),sK47_skl)|~sQ9_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f2609,f426])).
% 1.44/0.79 fof(f2622,plain,(
% 1.44/0.79 segmentP(sK48_skl,sK47_skl)|~sQ9_spl),
% 1.44/0.79 inference(forward_demodulation,[status(thm)],[f522,f2619])).
% 1.44/0.79 fof(f2623,plain,(
% 1.44/0.79 $false|sQ5_spl|~sQ9_spl),
% 1.44/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2622,f457])).
% 1.44/0.79 fof(f2624,plain,(
% 1.44/0.79 sQ5_spl|~sQ9_spl),
% 1.44/0.79 inference(contradiction_clause,[status(thm)],[f2623])).
% 1.44/0.79 fof(f2626,plain,(
% 1.44/0.79 ~ssList(sK47_skl)|~ssList(nil)|segmentP(app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl)),nil)|~ssList(sK7_skl(nil,sK47_skl))|~ssList(sK8_skl(nil,sK47_skl))|~sQ111_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1258,f465])).
% 1.44/0.79 fof(f2627,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK8_skl(nil,sK47_skl))|segmentP(app(app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl)),X0),sK8_skl(nil,sK47_skl))|~ssList(app(sK7_skl(nil,sK47_skl),nil))|~ssList(X0)|~sQ111_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1258,f465])).
% 1.44/0.79 fof(f2630,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK8_skl(nil,sK47_skl))|~ssList(app(sK7_skl(nil,sK47_skl),nil))|~ssList(X0)|~app(app(sK7_skl(nil,sK47_skl),nil),X0)=sK47_skl|X0=sK8_skl(nil,sK47_skl)|~sQ111_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1258,f378])).
% 1.44/0.79 fof(f2632,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK7_skl(nil,sK47_skl),nil))|~ssList(sK8_skl(nil,sK47_skl))|~ssList(X0)|~app(X0,sK8_skl(nil,sK47_skl))=sK47_skl|X0=app(sK7_skl(nil,sK47_skl),nil)|~sQ111_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1258,f376])).
% 1.44/0.79 fof(f2634,definition,(
% 1.44/0.79 sQ329_spl <=> (segmentP(app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl)),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2637,plain,(
% 1.44/0.79 ~sQ8_spl|~sQ10_spl|sQ329_spl|~sQ113_spl|~sQ112_spl|~sQ111_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2626,f530,f545,f2634,f1265,f1261,f1257])).
% 1.44/0.79 fof(f2638,definition,(
% 1.44/0.79 ![X0]: (sQ330_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl)),X0),sK8_skl(nil,sK47_skl))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2641,definition,(
% 1.44/0.79 sQ331_spl <=> (ssList(app(sK7_skl(nil,sK47_skl),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2644,plain,(
% 1.44/0.79 sQ330_spl|~sQ112_spl|~sQ331_spl|~sQ111_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2627,f2638,f1261,f2641,f1257])).
% 1.44/0.79 fof(f2653,definition,(
% 1.44/0.79 ![X0]: (sQ334_spl <=> (~ssList(X0)|~app(app(sK7_skl(nil,sK47_skl),nil),X0)=sK47_skl|X0=sK8_skl(nil,sK47_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2656,plain,(
% 1.44/0.79 ~sQ112_spl|~sQ331_spl|sQ334_spl|~sQ111_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2630,f1261,f2641,f2653,f1257])).
% 1.44/0.79 fof(f2658,definition,(
% 1.44/0.79 ![X0]: (sQ335_spl <=> (~ssList(X0)|~app(X0,sK8_skl(nil,sK47_skl))=sK47_skl|X0=app(sK7_skl(nil,sK47_skl),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2661,plain,(
% 1.44/0.79 ~sQ331_spl|~sQ112_spl|sQ335_spl|~sQ111_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2632,f2641,f1261,f2658,f1257])).
% 1.44/0.79 fof(f2667,plain,(
% 1.44/0.79 ~ssList(sK48_skl)|~ssList(nil)|segmentP(app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl)),nil)|~ssList(sK7_skl(nil,sK48_skl))|~ssList(sK8_skl(nil,sK48_skl))|~sQ116_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1283,f465])).
% 1.44/0.79 fof(f2668,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK8_skl(nil,sK48_skl))|segmentP(app(app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl)),X0),sK8_skl(nil,sK48_skl))|~ssList(app(sK7_skl(nil,sK48_skl),nil))|~ssList(X0)|~sQ116_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1283,f465])).
% 1.44/0.79 fof(f2671,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK8_skl(nil,sK48_skl))|~ssList(app(sK7_skl(nil,sK48_skl),nil))|~ssList(X0)|~app(app(sK7_skl(nil,sK48_skl),nil),X0)=sK48_skl|X0=sK8_skl(nil,sK48_skl)|~sQ116_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1283,f378])).
% 1.44/0.79 fof(f2673,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK7_skl(nil,sK48_skl),nil))|~ssList(sK8_skl(nil,sK48_skl))|~ssList(X0)|~app(X0,sK8_skl(nil,sK48_skl))=sK48_skl|X0=app(sK7_skl(nil,sK48_skl),nil)|~sQ116_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1283,f376])).
% 1.44/0.79 fof(f2675,definition,(
% 1.44/0.79 sQ336_spl <=> (segmentP(app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl)),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2678,plain,(
% 1.44/0.79 ~sQ12_spl|~sQ10_spl|sQ336_spl|~sQ118_spl|~sQ117_spl|~sQ116_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2667,f554,f545,f2675,f1290,f1286,f1282])).
% 1.44/0.79 fof(f2679,definition,(
% 1.44/0.79 ![X0]: (sQ337_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(app(sK7_skl(nil,sK48_skl),nil),sK8_skl(nil,sK48_skl)),X0),sK8_skl(nil,sK48_skl))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2682,definition,(
% 1.44/0.79 sQ338_spl <=> (ssList(app(sK7_skl(nil,sK48_skl),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2685,plain,(
% 1.44/0.79 sQ337_spl|~sQ117_spl|~sQ338_spl|~sQ116_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2668,f2679,f1286,f2682,f1282])).
% 1.44/0.79 fof(f2694,definition,(
% 1.44/0.79 ![X0]: (sQ341_spl <=> (~ssList(X0)|~app(app(sK7_skl(nil,sK48_skl),nil),X0)=sK48_skl|X0=sK8_skl(nil,sK48_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2697,plain,(
% 1.44/0.79 ~sQ117_spl|~sQ338_spl|sQ341_spl|~sQ116_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2671,f1286,f2682,f2694,f1282])).
% 1.44/0.79 fof(f2699,definition,(
% 1.44/0.79 ![X0]: (sQ342_spl <=> (~ssList(X0)|~app(X0,sK8_skl(nil,sK48_skl))=sK48_skl|X0=app(sK7_skl(nil,sK48_skl),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2702,plain,(
% 1.44/0.79 ~sQ338_spl|~sQ117_spl|sQ342_spl|~sQ116_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2673,f2682,f1286,f2699,f1282])).
% 1.44/0.79 fof(f2943,plain,(
% 1.44/0.79 segmentP(app(sK51_skl,sK51_skl),sK51_skl)|~sQ26_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f2616,f426])).
% 1.44/0.79 fof(f2947,plain,(
% 1.44/0.79 ~ssList(sK51_skl)|~ssList(nil)|segmentP(app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl)),nil)|~ssList(sK7_skl(nil,sK51_skl))|~ssList(sK8_skl(nil,sK51_skl))|~sQ104_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1210,f465])).
% 1.44/0.79 fof(f2948,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(sK8_skl(nil,sK51_skl))|segmentP(app(app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl)),X0),sK8_skl(nil,sK51_skl))|~ssList(app(sK7_skl(nil,sK51_skl),nil))|~ssList(X0)|~sQ104_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1210,f465])).
% 1.44/0.79 fof(f2949,plain,(
% 1.44/0.79 ~ssList(app(sK7_skl(nil,sK51_skl),nil))|~ssList(sK8_skl(nil,sK51_skl))|~nil=sK51_skl|nil=app(sK7_skl(nil,sK51_skl),nil)|~sQ104_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1210,f386])).
% 1.44/0.79 fof(f2950,plain,(
% 1.44/0.79 ~ssList(app(sK7_skl(nil,sK51_skl),nil))|~ssList(sK8_skl(nil,sK51_skl))|~nil=sK51_skl|nil=sK8_skl(nil,sK51_skl)|~sQ104_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1210,f385])).
% 1.44/0.79 fof(f2951,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK8_skl(nil,sK51_skl))|~ssList(app(sK7_skl(nil,sK51_skl),nil))|~ssList(X0)|~app(app(sK7_skl(nil,sK51_skl),nil),X0)=sK51_skl|X0=sK8_skl(nil,sK51_skl)|~sQ104_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1210,f378])).
% 1.44/0.79 fof(f2953,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK7_skl(nil,sK51_skl),nil))|~ssList(sK8_skl(nil,sK51_skl))|~ssList(X0)|~app(X0,sK8_skl(nil,sK51_skl))=sK51_skl|X0=app(sK7_skl(nil,sK51_skl),nil)|~sQ104_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1210,f376])).
% 1.44/0.79 fof(f2955,definition,(
% 1.44/0.79 sQ384_spl <=> (segmentP(app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl)),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2958,plain,(
% 1.44/0.79 ~sQ7_spl|~sQ10_spl|sQ384_spl|~sQ106_spl|~sQ105_spl|~sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2947,f527,f545,f2955,f1217,f1213,f1209])).
% 1.44/0.79 fof(f2959,definition,(
% 1.44/0.79 ![X0]: (sQ385_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(app(sK7_skl(nil,sK51_skl),nil),sK8_skl(nil,sK51_skl)),X0),sK8_skl(nil,sK51_skl))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2962,definition,(
% 1.44/0.79 sQ386_spl <=> (ssList(app(sK7_skl(nil,sK51_skl),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2965,plain,(
% 1.44/0.79 sQ385_spl|~sQ105_spl|~sQ386_spl|~sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2948,f2959,f1213,f2962,f1209])).
% 1.44/0.79 fof(f2966,definition,(
% 1.44/0.79 sQ387_spl <=> (nil=app(sK7_skl(nil,sK51_skl),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2969,plain,(
% 1.44/0.79 ~sQ386_spl|~sQ105_spl|~sQ46_spl|sQ387_spl|~sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2949,f2962,f1213,f751,f2966,f1209])).
% 1.44/0.79 fof(f2970,definition,(
% 1.44/0.79 sQ388_spl <=> (nil=sK8_skl(nil,sK51_skl))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2973,plain,(
% 1.44/0.79 ~sQ386_spl|~sQ105_spl|~sQ46_spl|sQ388_spl|~sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2950,f2962,f1213,f751,f2970,f1209])).
% 1.44/0.79 fof(f2974,definition,(
% 1.44/0.79 ![X0]: (sQ389_spl <=> (~ssList(X0)|~app(app(sK7_skl(nil,sK51_skl),nil),X0)=sK51_skl|X0=sK8_skl(nil,sK51_skl)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2977,plain,(
% 1.44/0.79 ~sQ105_spl|~sQ386_spl|sQ389_spl|~sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2951,f1213,f2962,f2974,f1209])).
% 1.44/0.79 fof(f2979,definition,(
% 1.44/0.79 ![X0]: (sQ390_spl <=> (~ssList(X0)|~app(X0,sK8_skl(nil,sK51_skl))=sK51_skl|X0=app(sK7_skl(nil,sK51_skl),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2982,plain,(
% 1.44/0.79 ~sQ386_spl|~sQ105_spl|sQ390_spl|~sQ104_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2953,f2962,f1213,f2979,f1209])).
% 1.44/0.79 fof(f2985,plain,(
% 1.44/0.79 ~ssList(app(sK7_skl(nil,nil),nil))|~ssList(sK8_skl(nil,nil))|nil=app(sK7_skl(nil,nil),nil)|~sQ102_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1197,f386])).
% 1.44/0.79 fof(f2986,plain,(
% 1.44/0.79 ~ssList(app(sK7_skl(nil,nil),nil))|~ssList(sK8_skl(nil,nil))|nil=sK8_skl(nil,nil)|~sQ102_spl),
% 1.44/0.79 inference(resolution,[status(thm)],[f1197,f385])).
% 1.44/0.79 fof(f2987,plain,(
% 1.44/0.79 ~ssList(nil)|~ssList(nil)|segmentP(app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil)),nil)|~ssList(sK7_skl(nil,nil))|~ssList(sK8_skl(nil,nil))|~sQ102_spl),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1197,f465])).
% 1.44/0.79 fof(f2988,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(nil,X0))|~ssList(sK8_skl(nil,nil))|segmentP(app(app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil)),X0),sK8_skl(nil,nil))|~ssList(app(sK7_skl(nil,nil),nil))|~ssList(X0)|~sQ102_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1197,f465])).
% 1.44/0.79 fof(f2991,plain,(
% 1.44/0.79 ![X0]: (~ssList(sK8_skl(nil,nil))|~ssList(app(sK7_skl(nil,nil),nil))|~ssList(X0)|~app(app(sK7_skl(nil,nil),nil),X0)=nil|X0=sK8_skl(nil,nil)|~sQ102_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1197,f378])).
% 1.44/0.79 fof(f2993,plain,(
% 1.44/0.79 ![X0]: (~ssList(app(sK7_skl(nil,nil),nil))|~ssList(sK8_skl(nil,nil))|~ssList(X0)|~app(X0,sK8_skl(nil,nil))=nil|X0=app(sK7_skl(nil,nil),nil)|~sQ102_spl)),
% 1.44/0.79 inference(paramodulation,[status(thm)],[f1197,f376])).
% 1.44/0.79 fof(f2995,definition,(
% 1.44/0.79 sQ391_spl <=> (ssList(app(sK7_skl(nil,nil),nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f2998,definition,(
% 1.44/0.79 sQ392_spl <=> (nil=app(sK7_skl(nil,nil),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f3001,plain,(
% 1.44/0.79 ~sQ391_spl|~sQ98_spl|sQ392_spl|~sQ102_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2985,f2995,f1176,f2998,f1196])).
% 1.44/0.79 fof(f3002,definition,(
% 1.44/0.79 sQ393_spl <=> (nil=sK8_skl(nil,nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ393_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f3005,plain,(
% 1.44/0.79 ~sQ391_spl|~sQ98_spl|sQ393_spl|~sQ102_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2986,f2995,f1176,f3002,f1196])).
% 1.44/0.79 fof(f3006,definition,(
% 1.44/0.79 sQ394_spl <=> (segmentP(app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil)),nil))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f3009,plain,(
% 1.44/0.79 ~sQ10_spl|sQ394_spl|~sQ89_spl|~sQ98_spl|~sQ102_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2987,f545,f3006,f1102,f1176,f1196])).
% 1.44/0.79 fof(f3010,definition,(
% 1.44/0.79 ![X0]: (sQ395_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(app(sK7_skl(nil,nil),nil),sK8_skl(nil,nil)),X0),sK8_skl(nil,nil))|~ssList(X0)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f3013,plain,(
% 1.44/0.79 sQ395_spl|~sQ98_spl|~sQ391_spl|~sQ102_spl),
% 1.44/0.79 inference(split_clause,[status(thm)],[f2988,f3010,f1176,f2995,f1196])).
% 1.44/0.79 fof(f3016,definition,(
% 1.44/0.79 ![X0]: (sQ396_spl <=> (~ssList(X0)|~app(app(sK7_skl(nil,nil),nil),X0)=nil|X0=sK8_skl(nil,nil)))),
% 1.44/0.79 introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition])).
% 1.44/0.79 fof(f3019,plain,(
% 1.44/0.79 ~sQ98_spl|~sQ391_spl|sQ396_spl|~sQ102_spl),
% 0.21/0.79 inference(split_clause,[status(thm)],[f2991,f1176,f2995,f3016,f1196])).
% 0.21/0.79 fof(f3021,definition,(
% 0.21/0.79 ![X0]: (sQ397_spl <=> (~ssList(X0)|~app(X0,sK8_skl(nil,nil))=nil|X0=app(sK7_skl(nil,nil),nil)))),
% 0.21/0.79 introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition])).
% 0.21/0.79 fof(f3024,plain,(
% 0.21/0.79 ~sQ391_spl|~sQ98_spl|sQ397_spl|~sQ102_spl),
% 0.21/0.79 inference(split_clause,[status(thm)],[f2993,f2995,f1176,f3021,f1196])).
% 0.21/0.79 fof(f3089,plain,(
% 0.21/0.79 $false|sQ62_spl|~sQ2_spl),
% 0.21/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1110,f862])).
% 0.21/0.79 fof(f3090,plain,(
% 0.21/0.79 sQ62_spl|~sQ2_spl),
% 0.21/0.79 inference(contradiction_clause,[status(thm)],[f3089])).
% 0.21/0.79 fof(f3134,plain,(
% 0.21/0.79 ~ssList(sK47_skl)|~ssList(sK51_skl)|nil=sK47_skl|~sQ0_spl),
% 0.21/0.79 inference(resolution,[status(thm)],[f648,f386])).
% 0.21/0.79 fof(f3135,plain,(
% 0.21/0.79 ~ssList(sK47_skl)|~ssList(sK51_skl)|nil=sK51_skl|~sQ0_spl),
% 0.21/0.79 inference(resolution,[status(thm)],[f648,f385])).
% 0.21/0.79 fof(f3143,plain,(
% 0.21/0.79 ~sQ8_spl|~sQ7_spl|sQ48_spl|~sQ0_spl),
% 0.21/0.79 inference(split_clause,[status(thm)],[f3134,f530,f527,f758,f438])).
% 0.21/0.80 fof(f3144,plain,(
% 0.21/0.80 ~sQ8_spl|~sQ7_spl|sQ46_spl|~sQ0_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3135,f530,f527,f751,f438])).
% 0.21/0.80 fof(f3158,plain,(
% 0.21/0.80 segmentP(nil,sK47_skl)|~sQ0_spl|~sQ9_spl),
% 0.21/0.80 inference(forward_demodulation,[status(thm)],[f538,f2622])).
% 0.21/0.80 fof(f3159,plain,(
% 0.21/0.80 ~ssList(sK47_skl)|nil=sK47_skl|~sQ0_spl|~sQ9_spl),
% 0.21/0.80 inference(resolution,[status(thm)],[f3158,f326])).
% 0.21/0.80 fof(f3165,plain,(
% 0.21/0.80 ~sQ8_spl|sQ48_spl|~sQ0_spl|~sQ9_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3159,f530,f758,f438,f542])).
% 0.21/0.80 fof(f3327,plain,(
% 0.21/0.80 ~ssList(app(sK51_skl,sK51_skl))|~ssList(sK51_skl)|app(app(sK7_skl(sK51_skl,app(sK51_skl,sK51_skl)),sK51_skl),sK8_skl(sK51_skl,app(sK51_skl,sK51_skl)))=app(sK51_skl,sK51_skl)|~sQ26_spl),
% 0.21/0.80 inference(resolution,[status(thm)],[f2943,f136])).
% 0.21/0.80 fof(f3328,plain,(
% 0.21/0.80 ~ssList(app(sK51_skl,sK51_skl))|~ssList(sK51_skl)|ssList(sK8_skl(sK51_skl,app(sK51_skl,sK51_skl)))|~sQ26_spl),
% 0.21/0.80 inference(resolution,[status(thm)],[f2943,f135])).
% 0.21/0.80 fof(f3329,plain,(
% 0.21/0.80 ~ssList(app(sK51_skl,sK51_skl))|~ssList(sK51_skl)|ssList(sK7_skl(sK51_skl,app(sK51_skl,sK51_skl)))|~sQ26_spl),
% 0.21/0.80 inference(resolution,[status(thm)],[f2943,f134])).
% 0.21/0.80 fof(f3330,plain,(
% 0.21/0.80 ~ssList(sK51_skl)|~ssList(app(sK51_skl,sK51_skl))|~segmentP(sK51_skl,app(sK51_skl,sK51_skl))|sK51_skl=app(sK51_skl,sK51_skl)|~sQ26_spl),
% 0.21/0.80 inference(resolution,[status(thm)],[f2943,f317])).
% 0.21/0.80 fof(f3331,plain,(
% 0.21/0.80 ![X0]: (~ssList(X0)|~ssList(app(sK51_skl,sK51_skl))|~ssList(sK51_skl)|~segmentP(X0,app(sK51_skl,sK51_skl))|segmentP(X0,sK51_skl)|~sQ26_spl)),
% 0.21/0.80 inference(resolution,[status(thm)],[f2943,f315])).
% 0.21/0.80 fof(f3332,definition,(
% 0.21/0.80 sQ433_spl <=> (ssList(app(sK51_skl,sK51_skl)))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3335,definition,(
% 0.21/0.80 sQ434_spl <=> (app(app(sK7_skl(sK51_skl,app(sK51_skl,sK51_skl)),sK51_skl),sK8_skl(sK51_skl,app(sK51_skl,sK51_skl)))=app(sK51_skl,sK51_skl))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3338,plain,(
% 0.21/0.80 ~sQ433_spl|~sQ7_spl|sQ434_spl|~sQ26_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3327,f3332,f527,f3335,f640])).
% 0.21/0.80 fof(f3339,definition,(
% 0.21/0.80 sQ435_spl <=> (ssList(sK8_skl(sK51_skl,app(sK51_skl,sK51_skl))))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3342,plain,(
% 0.21/0.80 ~sQ433_spl|~sQ7_spl|sQ435_spl|~sQ26_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3328,f3332,f527,f3339,f640])).
% 0.21/0.80 fof(f3343,definition,(
% 0.21/0.80 sQ436_spl <=> (ssList(sK7_skl(sK51_skl,app(sK51_skl,sK51_skl))))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3346,plain,(
% 0.21/0.80 ~sQ433_spl|~sQ7_spl|sQ436_spl|~sQ26_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3329,f3332,f527,f3343,f640])).
% 0.21/0.80 fof(f3347,definition,(
% 0.21/0.80 sQ437_spl <=> (segmentP(sK51_skl,app(sK51_skl,sK51_skl)))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3350,definition,(
% 0.21/0.80 sQ438_spl <=> (sK51_skl=app(sK51_skl,sK51_skl))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3353,plain,(
% 0.21/0.80 ~sQ7_spl|~sQ433_spl|~sQ437_spl|sQ438_spl|~sQ26_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3330,f527,f3332,f3347,f3350,f640])).
% 0.21/0.80 fof(f3354,definition,(
% 0.21/0.80 ![X0]: (sQ439_spl <=> (~ssList(X0)|~segmentP(X0,app(sK51_skl,sK51_skl))|segmentP(X0,sK51_skl)))),
% 0.21/0.80 introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition])).
% 0.21/0.80 fof(f3357,plain,(
% 0.21/0.80 sQ439_spl|~sQ433_spl|~sQ7_spl|~sQ26_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f3331,f3354,f3332,f527,f640])).
% 0.21/0.80 fof(f3362,plain,(
% 0.21/0.80 sP0_prd(nil,sK47_skl)|~sQ0_spl|~sQ2_spl),
% 0.21/0.80 inference(forward_demodulation,[status(thm)],[f538,f446])).
% 0.21/0.80 fof(f3363,plain,(
% 0.21/0.80 sP0_prd(nil,nil)|~sQ48_spl|~sQ0_spl|~sQ2_spl),
% 0.21/0.80 inference(forward_demodulation,[status(thm)],[f759,f3362])).
% 0.21/0.80 fof(f3364,plain,(
% 0.21/0.80 $false|~sQ48_spl|~sQ0_spl|~sQ2_spl),
% 0.21/0.80 inference(forward_subsumption_resolution,[status(thm)],[f3363,f489])).
% 0.21/0.80 fof(f3365,plain,(
% 0.21/0.80 ~sQ48_spl|~sQ0_spl|~sQ2_spl),
% 0.21/0.80 inference(contradiction_clause,[status(thm)],[f3364])).
% 0.21/0.80 fof(f3367,plain,(
% 0.21/0.80 ~segmentP(nil,nil)|~sQ0_spl|sQ119_spl),
% 0.21/0.80 inference(forward_demodulation,[status(thm)],[f538,f1296])).
% 0.21/0.80 fof(f3368,plain,(
% 0.21/0.80 $false|~sQ0_spl|sQ119_spl),
% 0.21/0.80 inference(forward_subsumption_resolution,[status(thm)],[f3367,f821])).
% 0.21/0.80 fof(f3369,plain,(
% 0.21/0.80 ~sQ0_spl|sQ119_spl),
% 0.21/0.80 inference(contradiction_clause,[status(thm)],[f3368])).
% 0.21/0.80 fof(f3416,plain,(
% 0.21/0.80 sQ4_spl|~sQ46_spl|~sQ3_spl),
% 0.21/0.80 inference(split_clause,[status(thm)],[f945,f452,f751,f448])).
% 0.21/0.80 fof(f3425,plain,(
% 0.21/0.80 $false),
% 0.21/0.80 inference(sat_refutation,[status(thm)],[f444,f451,f458,f533,f535,f548,f557,f564,f569,f571,f581,f588,f597,f601,f603,f616,f621,f629,f631,f638,f643,f657,f661,f680,f700,f703,f736,f774,f784,f794,f815,f825,f829,f837,f857,f872,f877,f882,f912,f919,f921,f925,f933,f1010,f1014,f1018,f1039,f1044,f1052,f1101,f1105,f1109,f1112,f1119,f1171,f1175,f1179,f1183,f1191,f1195,f1199,f1203,f1212,f1216,f1220,f1224,f1228,f1229,f1260,f1264,f1268,f1276,f1285,f1289,f1293,f1297,f1301,f1331,f1518,f1525,f1529,f1533,f1537,f1541,f1545,f1549,f1553,f1557,f1561,f1565,f1573,f1600,f1644,f1648,f1652,f1656,f1660,f1664,f1668,f1672,f1676,f1680,f1684,f1688,f1692,f1696,f1725,f1730,f1739,f1744,f1753,f1758,f1771,f1776,f1797,f1802,f1945,f1958,f1974,f1991,f2018,f2028,f2032,f2040,f2533,f2537,f2565,f2569,f2573,f2578,f2582,f2586,f2590,f2594,f2606,f2624,f2637,f2644,f2656,f2661,f2678,f2685,f2697,f2702,f2958,f2965,f2969,f2973,f2977,f2982,f3001,f3005,f3009,f3013,f3019,f3024,f3090,f3143,f3144,f3165,f3338,f3342,f3346,f3353,f3357,f3365,f3369,f3416])).
% 0.21/0.80 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.80 % Elapsed time: 0.436477 seconds
% 0.21/0.80 % CPU time: 3.161297 seconds
% 0.21/0.80 % Total memory used: 155.004 MB
% 0.21/0.80 % Net memory used: 151.922 MB
%------------------------------------------------------------------------------