Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SWC070+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 : n026.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:30 PM UTC 2026

% Result   : Theorem 5.51s 1.16s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWC070+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 : n026.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:55:51 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.37  % Drodi V4.1.1
% 5.51/1.16  % Refutation found
% 5.51/1.16  % SZS status Theorem for theBenchmark: Theorem is valid
% 5.51/1.16  % SZS output start CNFRefutation for theBenchmark
% 5.51/1.16  fof(f1,axiom,(
% 5.51/1.16    (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f2,axiom,(
% 5.51/1.16    (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f5,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f6,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f7,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f8,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> ( cyclefreeP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ~ ( leq(V,W)& leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f9,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> ( totalorderP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ( leq(V,W)| leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f10,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> ( strictorderP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ( lt(V,W)| lt(W,V) ) ) ) )) )) )) )) )) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f11,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> ( totalorderedP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> leq(V,W) ) ) )) )) )) )) )) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f13,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> ( duplicatefreeP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> V != W ) ) )) )) )) )) )) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f15,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f17,axiom,(
% 5.51/1.16    ssList(nil) ),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f26,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f28,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f40,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( frontsegP(U,V)& frontsegP(V,W) )=> frontsegP(U,W) ) ) )) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f41,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( frontsegP(U,V)& frontsegP(V,U) )=> U = V ) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f42,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> frontsegP(U,U) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f43,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( frontsegP(U,V)=> frontsegP(app(U,W),V) ) ) )) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f44,axiom,(
% 5.51/1.16    (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( frontsegP(cons(U,W),cons(V,X))<=> ( U = V& frontsegP(W,X) ) ) ) )) )) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f45,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f46,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> ( frontsegP(nil,U)<=> nil = U ) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f51,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f53,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( segmentP(U,V)& segmentP(V,W) )=> segmentP(U,W) ) ) )) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f54,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( segmentP(U,V)& segmentP(V,U) )=> U = V ) ) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f55,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> segmentP(U,U) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f56,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( segmentP(U,V)=> segmentP(app(app(W,U),X),V) ) ) )) )) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f57,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f84,axiom,(
% 5.51/1.16    (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f96,conjecture,(
% 5.51/1.16    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssList(Y)& neq(Y,nil)& segmentP(V,Y)& segmentP(U,Y) ))| ( nil = V& nil = U )| ( ( nil != X| nil != W )& ( ~ neq(W,nil)| ~ frontsegP(X,W) ) ) ) ) )) )) )) )),
% 5.51/1.16    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.51/1.16  fof(f97,negated_conjecture,(
% 5.51/1.16    ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssList(Y)& neq(Y,nil)& segmentP(V,Y)& segmentP(U,Y) ))| ( nil = V& nil = U )| ( ( nil != X| nil != W )& ( ~ neq(W,nil)| ~ frontsegP(X,W) ) ) ) ) )) )) )) ))),
% 5.51/1.16    inference(negated_conjecture,[status(cth)],[f96])).
% 5.51/1.16  fof(f98,plain,(
% 5.51/1.16    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(neq(U,V)<=>~U=V))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f1])).
% 5.51/1.16  fof(f99,plain,(
% 5.51/1.16    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f98])).
% 5.51/1.16  fof(f101,plain,(
% 5.51/1.16    ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|neq(X0,X1)|X0=X1)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f99])).
% 5.51/1.16  fof(f102,plain,(
% 5.51/1.16    (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 5.51/1.16  fof(f103,plain,(
% 5.51/1.16    ssItem(sK0_skl)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f102])).
% 5.51/1.16  fof(f104,plain,(
% 5.51/1.16    ssItem(sK1_skl)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f102])).
% 5.51/1.16  fof(f105,plain,(
% 5.51/1.16    ~sK0_skl=sK1_skl),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f102])).
% 5.51/1.16  fof(f119,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f5])).
% 5.51/1.16  fof(f120,plain,(
% 5.51/1.16    ![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)))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f119])).
% 5.51/1.16  fof(f121,plain,(
% 5.51/1.16    ![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)))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 5.51/1.16  fof(f122,plain,(
% 5.51/1.16    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f121])).
% 5.51/1.16  fof(f123,plain,(
% 5.51/1.16    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f121])).
% 5.51/1.16  fof(f124,plain,(
% 5.51/1.16    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f121])).
% 5.51/1.16  fof(f125,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f6])).
% 5.51/1.16  fof(f126,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(?[W]: (ssList(W)&app(W,V)=U)))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f125])).
% 5.51/1.16  fof(f127,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(ssList(sK6_skl(V,U))&app(sK6_skl(V,U),V)=U))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 5.51/1.16  fof(f129,plain,(
% 5.51/1.16    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f127])).
% 5.51/1.16  fof(f131,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f7])).
% 5.51/1.16  fof(f132,plain,(
% 5.51/1.16    ![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)))))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f131])).
% 5.51/1.16  fof(f133,plain,(
% 5.51/1.16    ![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)))))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 5.51/1.16  fof(f136,plain,(
% 5.51/1.16    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f133])).
% 5.51/1.16  fof(f137,plain,(
% 5.51/1.16    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f133])).
% 5.51/1.16  fof(f138,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(cyclefreeP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V)))))))))))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f8])).
% 5.51/1.16  fof(f139,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(leq(V,W)&leq(W,V))))))))))))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f138])).
% 5.51/1.16  fof(f140,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(ssItem(sK9_skl(U))&(ssItem(sK10_skl(U))&(ssList(sK11_skl(U))&(ssList(sK12_skl(U))&(ssList(sK13_skl(U))&(app(app(sK11_skl(U),cons(sK9_skl(U),sK12_skl(U))),cons(sK10_skl(U),sK13_skl(U)))=U&(leq(sK9_skl(U),sK10_skl(U))&leq(sK10_skl(U),sK9_skl(U))))))))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(V,sK9_skl(U)),skolemize(W,sK10_skl(U)),skolemize(X,sK11_skl(U)),skolemize(Y,sK12_skl(U)),skolemize(Z,sK13_skl(U))],[f139])).
% 5.51/1.16  fof(f147,plain,(
% 5.51/1.16    ![X0]: (~ssList(X0)|cyclefreeP(X0)|app(app(sK11_skl(X0),cons(sK9_skl(X0),sK12_skl(X0))),cons(sK10_skl(X0),sK13_skl(X0)))=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f140])).
% 5.51/1.16  fof(f150,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(totalorderP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(leq(V,W)|leq(W,V)))))))))))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f9])).
% 5.51/1.16  fof(f151,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~totalorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(leq(V,W)|leq(W,V))))))))))))))&(totalorderP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(~leq(V,W)&~leq(W,V))))))))))))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f150])).
% 5.51/1.16  fof(f152,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~totalorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(leq(V,W)|leq(W,V))))))))))))))&(totalorderP(U)|(ssItem(sK14_skl(U))&(ssItem(sK15_skl(U))&(ssList(sK16_skl(U))&(ssList(sK17_skl(U))&(ssList(sK18_skl(U))&(app(app(sK16_skl(U),cons(sK14_skl(U),sK17_skl(U))),cons(sK15_skl(U),sK18_skl(U)))=U&(~leq(sK14_skl(U),sK15_skl(U))&~leq(sK15_skl(U),sK14_skl(U))))))))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(V,sK14_skl(U)),skolemize(W,sK15_skl(U)),skolemize(X,sK16_skl(U)),skolemize(Y,sK17_skl(U)),skolemize(Z,sK18_skl(U))],[f151])).
% 5.51/1.16  fof(f159,plain,(
% 5.51/1.16    ![X0]: (~ssList(X0)|totalorderP(X0)|app(app(sK16_skl(X0),cons(sK14_skl(X0),sK17_skl(X0))),cons(sK15_skl(X0),sK18_skl(X0)))=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f152])).
% 5.51/1.16  fof(f162,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(strictorderP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(lt(V,W)|lt(W,V)))))))))))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f10])).
% 5.51/1.16  fof(f163,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~strictorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(lt(V,W)|lt(W,V))))))))))))))&(strictorderP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(~lt(V,W)&~lt(W,V))))))))))))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f162])).
% 5.51/1.16  fof(f164,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~strictorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(lt(V,W)|lt(W,V))))))))))))))&(strictorderP(U)|(ssItem(sK19_skl(U))&(ssItem(sK20_skl(U))&(ssList(sK21_skl(U))&(ssList(sK22_skl(U))&(ssList(sK23_skl(U))&(app(app(sK21_skl(U),cons(sK19_skl(U),sK22_skl(U))),cons(sK20_skl(U),sK23_skl(U)))=U&(~lt(sK19_skl(U),sK20_skl(U))&~lt(sK20_skl(U),sK19_skl(U))))))))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl]),skolemize(V,sK19_skl(U)),skolemize(W,sK20_skl(U)),skolemize(X,sK21_skl(U)),skolemize(Y,sK22_skl(U)),skolemize(Z,sK23_skl(U))],[f163])).
% 5.51/1.16  fof(f171,plain,(
% 5.51/1.16    ![X0]: (~ssList(X0)|strictorderP(X0)|app(app(sK21_skl(X0),cons(sK19_skl(X0),sK22_skl(X0))),cons(sK20_skl(X0),sK23_skl(X0)))=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f164])).
% 5.51/1.16  fof(f174,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(totalorderedP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W))))))))))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f11])).
% 5.51/1.16  fof(f175,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~totalorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W)))))))))))))&(totalorderedP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&~leq(V,W)))))))))))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f174])).
% 5.51/1.16  fof(f176,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~totalorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W)))))))))))))&(totalorderedP(U)|(ssItem(sK24_skl(U))&(ssItem(sK25_skl(U))&(ssList(sK26_skl(U))&(ssList(sK27_skl(U))&(ssList(sK28_skl(U))&(app(app(sK26_skl(U),cons(sK24_skl(U),sK27_skl(U))),cons(sK25_skl(U),sK28_skl(U)))=U&~leq(sK24_skl(U),sK25_skl(U)))))))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(V,sK24_skl(U)),skolemize(W,sK25_skl(U)),skolemize(X,sK26_skl(U)),skolemize(Y,sK27_skl(U)),skolemize(Z,sK28_skl(U))],[f175])).
% 5.51/1.16  fof(f183,plain,(
% 5.51/1.16    ![X0]: (~ssList(X0)|totalorderedP(X0)|app(app(sK26_skl(X0),cons(sK24_skl(X0),sK27_skl(X0))),cons(sK25_skl(X0),sK28_skl(X0)))=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f176])).
% 5.51/1.16  fof(f196,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(duplicatefreeP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|~V=W)))))))))))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f13])).
% 5.51/1.16  fof(f197,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~duplicatefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|~V=W))))))))))))&(duplicatefreeP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&V=W))))))))))))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f196])).
% 5.51/1.16  fof(f198,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|((~duplicatefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|~V=W))))))))))))&(duplicatefreeP(U)|(ssItem(sK34_skl(U))&(ssItem(sK35_skl(U))&(ssList(sK36_skl(U))&(ssList(sK37_skl(U))&(ssList(sK38_skl(U))&(app(app(sK36_skl(U),cons(sK34_skl(U),sK37_skl(U))),cons(sK35_skl(U),sK38_skl(U)))=U&sK34_skl(U)=sK35_skl(U))))))))))),
% 5.51/1.16    inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl,sK36_skl,sK37_skl,sK38_skl]),skolemize(V,sK34_skl(U)),skolemize(W,sK35_skl(U)),skolemize(X,sK36_skl(U)),skolemize(Y,sK37_skl(U)),skolemize(Z,sK38_skl(U))],[f197])).
% 5.51/1.16  fof(f206,plain,(
% 5.51/1.16    ![X0]: (~ssList(X0)|duplicatefreeP(X0)|sK34_skl(X0)=sK35_skl(X0))),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f198])).
% 5.51/1.16  fof(f217,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f15])).
% 5.51/1.16  fof(f218,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 5.51/1.16    inference(NNF_transformation,[status(thm)],[f217])).
% 5.51/1.16  fof(f220,plain,(
% 5.51/1.16    ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X0,X1)|X0=X1)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f218])).
% 5.51/1.16  fof(f223,plain,(
% 5.51/1.16    ssList(nil)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f17])).
% 5.51/1.16  fof(f244,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f26])).
% 5.51/1.16  fof(f245,plain,(
% 5.51/1.16    ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f244])).
% 5.51/1.16  fof(f248,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|app(nil,U)=U)),
% 5.51/1.16    inference(pre_NNF_transformation,[status(thm)],[f28])).
% 5.51/1.16  fof(f249,plain,(
% 5.51/1.16    ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 5.51/1.16    inference(cnf_transformation,[status(thm)],[f248])).
% 5.51/1.16  fof(f281,plain,(
% 5.51/1.16    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~frontsegP(U,V)|~frontsegP(V,W))|frontsegP(U,W)))))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f40])).
% 5.51/1.17  fof(f282,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|~frontsegP(X1,X2)|frontsegP(X0,X2))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f281])).
% 5.51/1.17  fof(f283,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|~frontsegP(V,U))|U=V))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f41])).
% 5.51/1.17  fof(f284,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|~frontsegP(X1,X0)|X0=X1)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f283])).
% 5.51/1.17  fof(f285,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|frontsegP(U,U))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f42])).
% 5.51/1.17  fof(f286,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f285])).
% 5.51/1.17  fof(f287,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~frontsegP(U,V)|frontsegP(app(U,W),V)))))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f43])).
% 5.51/1.17  fof(f288,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|frontsegP(app(X0,X2),X1))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f287])).
% 5.51/1.17  fof(f289,plain,(
% 5.51/1.17    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|(frontsegP(cons(U,W),cons(V,X))<=>(U=V&frontsegP(W,X))))))))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f44])).
% 5.51/1.17  fof(f290,plain,(
% 5.51/1.17    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|((~frontsegP(cons(U,W),cons(V,X))|(U=V&frontsegP(W,X)))&(frontsegP(cons(U,W),cons(V,X))|(~U=V|~frontsegP(W,X)))))))))))),
% 5.51/1.17    inference(NNF_transformation,[status(thm)],[f289])).
% 5.51/1.17  fof(f292,plain,(
% 5.51/1.17    ![X0,X1,X2,X3]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(cons(X0,X2),cons(X1,X3))|frontsegP(X2,X3))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f290])).
% 5.51/1.17  fof(f293,plain,(
% 5.51/1.17    ![X0,X1,X2,X3]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|frontsegP(cons(X0,X2),cons(X1,X3))|~X0=X1|~frontsegP(X2,X3))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f290])).
% 5.51/1.17  fof(f294,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|frontsegP(U,nil))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f45])).
% 5.51/1.17  fof(f295,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f294])).
% 5.51/1.17  fof(f296,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|(frontsegP(nil,U)<=>nil=U))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f46])).
% 5.51/1.17  fof(f297,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|((~frontsegP(nil,U)|nil=U)&(frontsegP(nil,U)|~nil=U)))),
% 5.51/1.17    inference(NNF_transformation,[status(thm)],[f296])).
% 5.51/1.17  fof(f298,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|nil=X0)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f297])).
% 5.51/1.17  fof(f308,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|rearsegP(U,nil))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f51])).
% 5.51/1.17  fof(f309,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f308])).
% 5.51/1.17  fof(f314,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~segmentP(U,V)|~segmentP(V,W))|segmentP(U,W)))))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f53])).
% 5.51/1.17  fof(f315,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(X0,X1)|~segmentP(X1,X2)|segmentP(X0,X2))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f314])).
% 5.51/1.17  fof(f316,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|~segmentP(V,U))|U=V))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f54])).
% 5.51/1.17  fof(f317,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|~segmentP(X1,X0)|X0=X1)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f316])).
% 5.51/1.17  fof(f318,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|segmentP(U,U))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f55])).
% 5.51/1.17  fof(f319,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f318])).
% 5.51/1.17  fof(f320,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|(~segmentP(U,V)|segmentP(app(app(W,U),X),V)))))))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f56])).
% 5.51/1.17  fof(f321,plain,(
% 5.51/1.17    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X0,X1)|segmentP(app(app(X2,X0),X3),X1))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f320])).
% 5.51/1.17  fof(f322,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|segmentP(U,nil))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f57])).
% 5.51/1.17  fof(f323,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f322])).
% 5.51/1.17  fof(f388,plain,(
% 5.51/1.17    ![U]: (~ssList(U)|app(U,nil)=U)),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f84])).
% 5.51/1.17  fof(f389,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f388])).
% 5.51/1.17  fof(f415,plain,(
% 5.51/1.17    (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(![Y]: (((~ssList(Y)|~neq(Y,nil))|~segmentP(V,Y))|~segmentP(U,Y))))&(~nil=V|~nil=U))&((nil=X&nil=W)|(neq(W,nil)&frontsegP(X,W))))))))))))),
% 5.51/1.17    inference(pre_NNF_transformation,[status(thm)],[f97])).
% 5.51/1.17  fof(f416,definition,(
% 5.51/1.17    ![W,X]: (sP0_prd(X,W)<=>(nil=X&nil=W))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 5.51/1.17  fof(f417,plain,(
% 5.51/1.17    ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&((((V=X&U=W)&(![Y]: (((~ssList(Y)|~neq(Y,nil))|~segmentP(V,Y))|~segmentP(U,Y))))&(~nil=V|~nil=U))&(sP0_prd(X,W)|(neq(W,nil)&frontsegP(X,W)))))))))))),
% 5.51/1.17    inference(formula_renaming,[status(thm)],[f415,f416])).
% 5.51/1.17  fof(f418,plain,(
% 5.51/1.17    (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&((((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(![Y]: (((~ssList(Y)|~neq(Y,nil))|~segmentP(sK48_skl,Y))|~segmentP(sK47_skl,Y))))&(~nil=sK48_skl|~nil=sK47_skl))&(sP0_prd(sK50_skl,sK49_skl)|(neq(sK49_skl,nil)&frontsegP(sK50_skl,sK49_skl))))))))),
% 5.51/1.17    inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl)],[f417])).
% 5.51/1.17  fof(f419,plain,(
% 5.51/1.17    ssList(sK47_skl)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f420,plain,(
% 5.51/1.17    ssList(sK48_skl)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f423,plain,(
% 5.51/1.17    sK48_skl=sK50_skl),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f424,plain,(
% 5.51/1.17    sK47_skl=sK49_skl),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f425,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sK48_skl,X0)|~segmentP(sK47_skl,X0))),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f426,plain,(
% 5.51/1.17    ~nil=sK48_skl|~nil=sK47_skl),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f427,plain,(
% 5.51/1.17    sP0_prd(sK50_skl,sK49_skl)|neq(sK49_skl,nil)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f428,plain,(
% 5.51/1.17    sP0_prd(sK50_skl,sK49_skl)|frontsegP(sK50_skl,sK49_skl)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f418])).
% 5.51/1.17  fof(f429,plain,(
% 5.51/1.17    ![W,X]: ((~sP0_prd(X,W)|(nil=X&nil=W))&(sP0_prd(X,W)|(~nil=X|~nil=W)))),
% 5.51/1.17    inference(NNF_transformation,[status(thm)],[f416])).
% 5.51/1.17  fof(f430,plain,(
% 5.51/1.17    (![W,X]: (~sP0_prd(X,W)|(nil=X&nil=W)))&(![W,X]: (sP0_prd(X,W)|(~nil=X|~nil=W)))),
% 5.51/1.17    inference(miniscoping,[status(thm)],[f429])).
% 5.51/1.17  fof(f431,plain,(
% 5.51/1.17    ![X0,X1]: (~sP0_prd(X0,X1)|nil=X0)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f430])).
% 5.51/1.17  fof(f432,plain,(
% 5.51/1.17    ![X0,X1]: (~sP0_prd(X0,X1)|nil=X1)),
% 5.51/1.17    inference(cnf_transformation,[status(thm)],[f430])).
% 5.51/1.17  fof(f434,definition,(
% 5.51/1.17    sQ0_spl <=> (nil=sK48_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f436,plain,(
% 5.51/1.17    ~nil=sK48_skl|sQ0_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f434])).
% 5.51/1.17  fof(f437,definition,(
% 5.51/1.17    sQ1_spl <=> (nil=sK47_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f438,plain,(
% 5.51/1.17    nil=sK47_skl|~sQ1_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f437])).
% 5.51/1.17  fof(f440,plain,(
% 5.51/1.17    ~sQ0_spl|~sQ1_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f426,f434,f437])).
% 5.51/1.17  fof(f441,definition,(
% 5.51/1.17    sQ2_spl <=> (sP0_prd(sK50_skl,sK49_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f442,plain,(
% 5.51/1.17    sP0_prd(sK50_skl,sK49_skl)|~sQ2_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f441])).
% 5.51/1.17  fof(f444,definition,(
% 5.51/1.17    sQ3_spl <=> (neq(sK49_skl,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f445,plain,(
% 5.51/1.17    neq(sK49_skl,nil)|~sQ3_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f444])).
% 5.51/1.17  fof(f447,plain,(
% 5.51/1.17    sQ2_spl|sQ3_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f427,f441,f444])).
% 5.51/1.17  fof(f448,definition,(
% 5.51/1.17    sQ4_spl <=> (frontsegP(sK50_skl,sK49_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f449,plain,(
% 5.51/1.17    frontsegP(sK50_skl,sK49_skl)|~sQ4_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f448])).
% 5.51/1.17  fof(f451,plain,(
% 5.51/1.17    sQ2_spl|sQ4_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f428,f441,f448])).
% 5.51/1.17  fof(f456,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 5.51/1.17    inference(destructive_equality_resolution,[status(thm)],[f124])).
% 5.51/1.17  fof(f458,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 5.51/1.17    inference(destructive_equality_resolution,[status(thm)],[f137])).
% 5.51/1.17  fof(f470,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 5.51/1.17    inference(backward_subsumption_resolution,[status(thm)],[f456,f245])).
% 5.51/1.17  fof(f473,plain,(
% 5.51/1.17    ![X1,X2,X3]: (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|frontsegP(cons(X1,X2),cons(X1,X3))|~frontsegP(X2,X3))),
% 5.51/1.17    inference(destructive_equality_resolution,[status(thm)],[f293])).
% 5.51/1.17  fof(f474,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|frontsegP(cons(X0,X1),cons(X0,X2))|~frontsegP(X1,X2))),
% 5.51/1.17    inference(duplicate_literals_removal,[status(thm)],[f473])).
% 5.51/1.17  fof(f487,plain,(
% 5.51/1.17    sP0_prd(sK48_skl,sK49_skl)|~sQ2_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f423,f442])).
% 5.51/1.17  fof(f488,plain,(
% 5.51/1.17    sP0_prd(sK48_skl,sK47_skl)|~sQ2_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f424,f487])).
% 5.51/1.17  fof(f489,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(sK47_skl)|~neq(sK47_skl,nil)|~segmentP(sK48_skl,sK47_skl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f319,f425])).
% 5.51/1.17  fof(f491,definition,(
% 5.51/1.17    sQ5_spl <=> (ssList(sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f493,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|sQ5_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f491])).
% 5.51/1.17  fof(f494,definition,(
% 5.51/1.17    sQ6_spl <=> (neq(sK47_skl,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f496,plain,(
% 5.51/1.17    ~neq(sK47_skl,nil)|sQ6_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f494])).
% 5.51/1.17  fof(f497,definition,(
% 5.51/1.17    sQ7_spl <=> (segmentP(sK48_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f499,plain,(
% 5.51/1.17    ~segmentP(sK48_skl,sK47_skl)|sQ7_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f497])).
% 5.51/1.17  fof(f500,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f489,f491,f494,f497])).
% 5.51/1.17  fof(f501,definition,(
% 5.51/1.17    sQ8_spl <=> (ssList(sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f503,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|sQ8_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f501])).
% 5.51/1.17  fof(f511,plain,(
% 5.51/1.17    $false|sQ8_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f503,f420])).
% 5.51/1.17  fof(f512,plain,(
% 5.51/1.17    sQ8_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f511])).
% 5.51/1.17  fof(f513,plain,(
% 5.51/1.17    ![X0]: (~ssItem(X0)|neq(X0,sK0_skl)|X0=sK0_skl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f103,f101])).
% 5.51/1.17  fof(f515,plain,(
% 5.51/1.17    ![X0]: (~ssItem(X0)|neq(X0,sK1_skl)|X0=sK1_skl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f104,f101])).
% 5.51/1.17  fof(f517,plain,(
% 5.51/1.17    nil=sK48_skl|~sQ2_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f431,f488])).
% 5.51/1.17  fof(f519,plain,(
% 5.51/1.17    $false|sQ0_spl|~sQ2_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f517,f436])).
% 5.51/1.17  fof(f520,plain,(
% 5.51/1.17    sQ0_spl|~sQ2_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f519])).
% 5.51/1.17  fof(f521,plain,(
% 5.51/1.17    neq(sK47_skl,nil)|~sQ3_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f424,f445])).
% 5.51/1.17  fof(f522,plain,(
% 5.51/1.17    frontsegP(sK48_skl,sK49_skl)|~sQ4_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f423,f449])).
% 5.51/1.17  fof(f523,plain,(
% 5.51/1.17    frontsegP(sK48_skl,sK47_skl)|~sQ4_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f424,f522])).
% 5.51/1.17  fof(f528,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(nil)|~neq(nil,nil)|~segmentP(sK47_skl,nil)),
% 5.51/1.17    inference(resolution,[status(thm)],[f323,f425])).
% 5.51/1.17  fof(f529,definition,(
% 5.51/1.17    sQ11_spl <=> (ssList(nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f531,plain,(
% 5.51/1.17    ~ssList(nil)|sQ11_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f529])).
% 5.51/1.17  fof(f532,definition,(
% 5.51/1.17    sQ12_spl <=> (neq(nil,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f534,plain,(
% 5.51/1.17    ~neq(nil,nil)|sQ12_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f532])).
% 5.51/1.17  fof(f539,definition,(
% 5.51/1.17    sQ14_spl <=> (segmentP(sK47_skl,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f540,plain,(
% 5.51/1.17    segmentP(sK47_skl,nil)|~sQ14_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f539])).
% 5.51/1.17  fof(f541,plain,(
% 5.51/1.17    ~segmentP(sK47_skl,nil)|sQ14_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f539])).
% 5.51/1.17  fof(f542,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ11_spl|~sQ12_spl|~sQ14_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f528,f501,f529,f532,f539])).
% 5.51/1.17  fof(f543,plain,(
% 5.51/1.17    $false|sQ11_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f531,f223])).
% 5.51/1.17  fof(f544,plain,(
% 5.51/1.17    sQ11_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f543])).
% 5.51/1.17  fof(f545,plain,(
% 5.51/1.17    $false|sQ5_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f493,f419])).
% 5.51/1.17  fof(f546,plain,(
% 5.51/1.17    sQ5_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f545])).
% 5.51/1.17  fof(f551,plain,(
% 5.51/1.17    sP0_prd(nil,sK47_skl)|~sQ2_spl),
% 5.51/1.17    inference(backward_demodulation,[status(thm)],[f517,f488])).
% 5.51/1.17  fof(f570,definition,(
% 5.51/1.17    sQ19_spl <=> (nil=nil)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f574,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(nil)|sK47_skl=nil|sQ6_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f496,f220])).
% 5.51/1.17  fof(f575,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ11_spl|sQ1_spl|sQ6_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f574,f491,f529,f437,f494])).
% 5.51/1.17  fof(f582,plain,(
% 5.51/1.17    neq(nil,nil)|~sQ1_spl|~sQ3_spl),
% 5.51/1.17    inference(backward_demodulation,[status(thm)],[f438,f521])).
% 5.51/1.17  fof(f583,plain,(
% 5.51/1.17    $false|sQ12_spl|~sQ1_spl|~sQ3_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f582,f534])).
% 5.51/1.17  fof(f584,plain,(
% 5.51/1.17    sQ12_spl|~sQ1_spl|~sQ3_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f583])).
% 5.51/1.17  fof(f605,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|sQ14_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f541,f323])).
% 5.51/1.17  fof(f606,plain,(
% 5.51/1.17    ~sQ5_spl|sQ14_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f605,f491,f539])).
% 5.51/1.17  fof(f610,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f284,f295])).
% 5.51/1.17  fof(f611,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~ssList(X1)|~ssList(X2)|~ssList(X0)|~frontsegP(X1,X2)|~frontsegP(X2,X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f284,f282])).
% 5.51/1.17  fof(f613,definition,(
% 5.51/1.17    ![X0]: (sQ21_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f616,plain,(
% 5.51/1.17    ~sQ11_spl|sQ21_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f610,f529,f613])).
% 5.51/1.17  fof(f617,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~ssList(X2)|~frontsegP(X1,X2)|~frontsegP(X2,X0))),
% 5.51/1.17    inference(duplicate_literals_removal,[status(thm)],[f611])).
% 5.51/1.17  fof(f619,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|~ssList(X1)|~ssList(app(X0,X2))|~frontsegP(X1,app(X0,X2))|X1=app(X0,X2))),
% 5.51/1.17    inference(resolution,[status(thm)],[f288,f284])).
% 5.51/1.17  fof(f620,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|~ssList(app(X0,X2))|~frontsegP(X1,app(X0,X2))|X1=app(X0,X2))),
% 5.51/1.17    inference(duplicate_literals_removal,[status(thm)],[f619])).
% 5.51/1.17  fof(f621,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|~frontsegP(X1,app(X0,X2))|X1=app(X0,X2))),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f620,f245])).
% 5.51/1.17  fof(f648,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(app(X0,X1))|~ssList(X2)|app(X2,sK5_skl(X2,app(X0,X1)))=app(X0,X1)|~ssList(X0)|~ssList(X2)|~ssList(X1)|~frontsegP(X0,X2))),
% 5.51/1.17    inference(resolution,[status(thm)],[f123,f288])).
% 5.51/1.17  fof(f649,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f123,f295])).
% 5.51/1.17  fof(f650,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|app(X1,sK5_skl(X1,X0))=X0|~ssList(X0)|~ssList(X2)|~ssList(X1)|~frontsegP(X0,X2)|~frontsegP(X2,X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f123,f282])).
% 5.51/1.17  fof(f651,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(X0)|app(X0,sK5_skl(X0,X0))=X0|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f123,f286])).
% 5.51/1.17  fof(f652,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(app(X0,X1))|~ssList(X2)|app(X2,sK5_skl(X2,app(X0,X1)))=app(X0,X1)|~ssList(X0)|~ssList(X1)|~frontsegP(X0,X2))),
% 5.51/1.17    inference(duplicate_literals_removal,[status(thm)],[f648])).
% 5.51/1.17  fof(f653,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|app(X0,sK5_skl(X0,app(X1,X2)))=app(X1,X2)|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X0))),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f652,f245])).
% 5.51/1.17  fof(f654,definition,(
% 5.51/1.17    ![X0]: (sQ25_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f657,plain,(
% 5.51/1.17    sQ25_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f649,f654,f529])).
% 5.51/1.17  fof(f658,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|app(X1,sK5_skl(X1,X0))=X0|~ssList(X2)|~frontsegP(X0,X2)|~frontsegP(X2,X1))),
% 5.51/1.17    inference(duplicate_literals_removal,[status(thm)],[f650])).
% 5.51/1.17  fof(f659,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|app(X0,sK5_skl(X0,X0))=X0)),
% 5.51/1.17    inference(duplicate_literals_removal,[status(thm)],[f651])).
% 5.51/1.17  fof(f661,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK48_skl))=sK48_skl|~sQ4_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f523,f123])).
% 5.51/1.17  fof(f663,definition,(
% 5.51/1.17    sQ26_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK48_skl))=sK48_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f664,plain,(
% 5.51/1.17    app(sK47_skl,sK5_skl(sK47_skl,sK48_skl))=sK48_skl|~sQ26_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f663])).
% 5.51/1.17  fof(f666,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ5_spl|sQ26_spl|~sQ4_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f661,f501,f491,f663,f448])).
% 5.51/1.17  fof(f706,definition,(
% 5.51/1.17    sQ29_spl <=> (ssList(sK5_skl(sK47_skl,sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f708,plain,(
% 5.51/1.17    ~ssList(sK5_skl(sK47_skl,sK48_skl))|sQ29_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f706])).
% 5.51/1.17  fof(f714,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(sK47_skl)|~frontsegP(sK48_skl,sK47_skl)|sQ29_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f708,f122])).
% 5.51/1.17  fof(f715,definition,(
% 5.51/1.17    sQ31_spl <=> (frontsegP(sK48_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f717,plain,(
% 5.51/1.17    ~frontsegP(sK48_skl,sK47_skl)|sQ31_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f715])).
% 5.51/1.17  fof(f718,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ5_spl|~sQ31_spl|sQ29_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f714,f501,f491,f715,f706])).
% 5.51/1.17  fof(f720,plain,(
% 5.51/1.17    $false|~sQ4_spl|sQ31_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f717,f523])).
% 5.51/1.17  fof(f721,plain,(
% 5.51/1.17    ~sQ4_spl|sQ31_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f720])).
% 5.51/1.17  fof(f744,plain,(
% 5.51/1.17    nil=sK47_skl|~sQ2_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f551,f432])).
% 5.51/1.17  fof(f746,plain,(
% 5.51/1.17    sQ1_spl|~sQ2_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f744,f437,f441])).
% 5.51/1.17  fof(f748,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|frontsegP(cons(sK1_skl,X0),cons(sK1_skl,X1))|~frontsegP(X0,X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f474,f104])).
% 5.51/1.17  fof(f750,plain,(
% 5.51/1.17    ~ssList(nil)|nil=nil|~ssList(nil)),
% 5.51/1.17    inference(resolution,[status(thm)],[f298,f295])).
% 5.51/1.17  fof(f751,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|nil=X0|~ssList(nil)|~ssList(X1)|~ssList(X0)|~frontsegP(nil,X1)|~frontsegP(X1,X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f298,f282])).
% 5.51/1.17  fof(f753,plain,(
% 5.51/1.17    ~sQ11_spl|sQ19_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f750,f529,f570])).
% 5.51/1.17  fof(f754,definition,(
% 5.51/1.17    ![X0,X1]: (sQ32_spl <=> (~ssList(X0)|nil=X0|~ssList(X1)|~ssList(X0)|~frontsegP(nil,X1)|~frontsegP(X1,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f757,plain,(
% 5.51/1.17    sQ32_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f751,f754,f529])).
% 5.51/1.17  fof(f766,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0)),
% 5.51/1.17    inference(resolution,[status(thm)],[f309,f129])).
% 5.51/1.17  fof(f767,definition,(
% 5.51/1.17    ![X0]: (sQ33_spl <=> (~ssList(X0)|~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f770,plain,(
% 5.51/1.17    sQ33_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f766,f767,f529])).
% 5.51/1.17  fof(f772,plain,(
% 5.51/1.17    app(nil,sK48_skl)=sK48_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f249,f420])).
% 5.51/1.17  fof(f777,plain,(
% 5.51/1.17    app(nil,sK47_skl)=sK47_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f249,f419])).
% 5.51/1.17  fof(f780,plain,(
% 5.51/1.17    app(nil,nil)=nil),
% 5.51/1.17    inference(resolution,[status(thm)],[f249,f223])).
% 5.51/1.17  fof(f781,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(sK48_skl)|~frontsegP(nil,X0)|frontsegP(sK48_skl,X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f772,f288])).
% 5.51/1.17  fof(f782,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f772,f458])).
% 5.51/1.17  fof(f783,definition,(
% 5.51/1.17    ![X0]: (sQ34_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|frontsegP(sK48_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f784,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|frontsegP(sK48_skl,X0)|~sQ34_spl)),
% 5.51/1.17    inference(component_clause,[status(thm)],[f783])).
% 5.51/1.17  fof(f786,plain,(
% 5.51/1.17    ~sQ11_spl|sQ34_spl|~sQ8_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f781,f529,f783,f501])).
% 5.51/1.17  fof(f787,definition,(
% 5.51/1.17    ![X0]: (sQ35_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f788,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)|~sQ35_spl)),
% 5.51/1.17    inference(component_clause,[status(thm)],[f787])).
% 5.51/1.17  fof(f790,plain,(
% 5.51/1.17    sQ35_spl|~sQ8_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f782,f787,f501,f529])).
% 5.51/1.17  fof(f791,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK48_skl,X0))|segmentP(app(sK48_skl,X0),sK48_skl)|~ssList(X0)|~sQ35_spl)),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f772,f788])).
% 5.51/1.17  fof(f792,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(sK47_skl)|~frontsegP(nil,X0)|frontsegP(sK47_skl,X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f777,f288])).
% 5.51/1.17  fof(f793,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f777,f458])).
% 5.51/1.17  fof(f794,definition,(
% 5.51/1.17    ![X0]: (sQ36_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|frontsegP(sK47_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f795,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|frontsegP(sK47_skl,X0)|~sQ36_spl)),
% 5.51/1.17    inference(component_clause,[status(thm)],[f794])).
% 5.51/1.17  fof(f797,plain,(
% 5.51/1.17    ~sQ11_spl|sQ36_spl|~sQ5_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f792,f529,f794,f491])).
% 5.51/1.17  fof(f798,definition,(
% 5.51/1.17    ![X0]: (sQ37_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f799,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)|~sQ37_spl)),
% 5.51/1.17    inference(component_clause,[status(thm)],[f798])).
% 5.51/1.17  fof(f801,plain,(
% 5.51/1.17    sQ37_spl|~sQ5_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f793,f798,f491,f529])).
% 5.51/1.17  fof(f802,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK47_skl,X0))|segmentP(app(sK47_skl,X0),sK47_skl)|~ssList(X0)|~sQ37_spl)),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f777,f799])).
% 5.51/1.17  fof(f803,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(nil)|~frontsegP(nil,X0)|frontsegP(nil,X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f780,f288])).
% 5.51/1.17  fof(f804,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f780,f458])).
% 5.51/1.17  fof(f805,definition,(
% 5.51/1.17    ![X0]: (sQ38_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f808,plain,(
% 5.51/1.17    ~sQ11_spl|sQ38_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f803,f529,f805])).
% 5.51/1.17  fof(f809,definition,(
% 5.51/1.17    ![X0]: (sQ39_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f812,plain,(
% 5.51/1.17    sQ39_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f804,f809,f529])).
% 5.51/1.17  fof(f815,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(nil)|app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl))=sK47_skl|~sQ14_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f136,f540])).
% 5.51/1.17  fof(f816,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f136,f323])).
% 5.51/1.17  fof(f818,definition,(
% 5.51/1.17    sQ40_spl <=> (app(app(sK7_skl(nil,sK47_skl),nil),sK8_skl(nil,sK47_skl))=sK47_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f821,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ11_spl|sQ40_spl|~sQ14_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f815,f491,f529,f818,f539])).
% 5.51/1.17  fof(f822,definition,(
% 5.51/1.17    ![X0]: (sQ41_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f825,plain,(
% 5.51/1.17    sQ41_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f816,f822,f529])).
% 5.51/1.17  fof(f870,plain,(
% 5.51/1.17    neq(sK1_skl,sK0_skl)|sK1_skl=sK0_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f513,f104])).
% 5.51/1.17  fof(f872,definition,(
% 5.51/1.17    sQ47_spl <=> (neq(sK1_skl,sK0_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f875,definition,(
% 5.51/1.17    sQ48_spl <=> (sK1_skl=sK0_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f876,plain,(
% 5.51/1.17    sK1_skl=sK0_skl|~sQ48_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f875])).
% 5.51/1.17  fof(f878,plain,(
% 5.51/1.17    sQ47_spl|sQ48_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f870,f872,f875])).
% 5.51/1.17  fof(f884,plain,(
% 5.51/1.17    neq(sK0_skl,sK1_skl)|sK0_skl=sK1_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f515,f103])).
% 5.51/1.17  fof(f889,definition,(
% 5.51/1.17    sQ51_spl <=> (neq(sK0_skl,sK1_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f892,plain,(
% 5.51/1.17    sQ51_spl|sQ48_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f884,f889,f875])).
% 5.51/1.17  fof(f893,plain,(
% 5.51/1.17    $false|~sQ48_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f876,f105])).
% 5.51/1.17  fof(f894,plain,(
% 5.51/1.17    ~sQ48_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f893])).
% 5.51/1.17  fof(f896,plain,(
% 5.51/1.17    app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f659,f420])).
% 5.51/1.17  fof(f901,plain,(
% 5.51/1.17    app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f659,f419])).
% 5.51/1.17  fof(f905,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK48_skl)|~ssList(X0)|~ssList(sK5_skl(sK48_skl,sK48_skl))|~frontsegP(sK48_skl,X0)|frontsegP(sK48_skl,X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f896,f288])).
% 5.51/1.17  fof(f906,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK5_skl(sK48_skl,sK48_skl))|segmentP(app(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),X0),sK5_skl(sK48_skl,sK48_skl))|~ssList(sK48_skl)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f896,f458])).
% 5.51/1.17  fof(f907,definition,(
% 5.51/1.17    ![X0]: (sQ52_spl <=> (~ssList(X0)|~frontsegP(sK48_skl,X0)|frontsegP(sK48_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f910,definition,(
% 5.51/1.17    sQ53_spl <=> (ssList(sK5_skl(sK48_skl,sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f911,plain,(
% 5.51/1.17    ssList(sK5_skl(sK48_skl,sK48_skl))|~sQ53_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f910])).
% 5.51/1.17  fof(f912,plain,(
% 5.51/1.17    ~ssList(sK5_skl(sK48_skl,sK48_skl))|sQ53_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f910])).
% 5.51/1.17  fof(f913,plain,(
% 5.51/1.17    ~sQ8_spl|sQ52_spl|~sQ53_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f905,f501,f907,f910])).
% 5.51/1.17  fof(f914,definition,(
% 5.51/1.17    ![X0]: (sQ54_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),X0),sK5_skl(sK48_skl,sK48_skl))|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f917,plain,(
% 5.51/1.17    sQ54_spl|~sQ53_spl|~sQ8_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f906,f914,f910,f501])).
% 5.51/1.17  fof(f918,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~ssList(nil)|~segmentP(X0,sK47_skl)|segmentP(X0,nil)|~sQ14_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f315,f540])).
% 5.51/1.17  fof(f919,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f315,f323])).
% 5.51/1.17  fof(f921,definition,(
% 5.51/1.17    ![X0]: (sQ55_spl <=> (~ssList(X0)|~segmentP(X0,sK47_skl)|segmentP(X0,nil)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f924,plain,(
% 5.51/1.17    sQ55_spl|~sQ5_spl|~sQ11_spl|~sQ14_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f918,f921,f491,f529,f539])).
% 5.51/1.17  fof(f925,definition,(
% 5.51/1.17    ![X0,X1]: (sQ56_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f928,plain,(
% 5.51/1.17    sQ56_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f919,f925,f529])).
% 5.51/1.17  fof(f931,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f317,f323])).
% 5.51/1.17  fof(f937,definition,(
% 5.51/1.17    ![X0]: (sQ58_spl <=> (~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f940,plain,(
% 5.51/1.17    ~sQ11_spl|sQ58_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f931,f529,f937])).
% 5.51/1.17  fof(f942,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(sK48_skl)|~frontsegP(sK48_skl,sK48_skl)|sQ53_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f912,f122])).
% 5.51/1.17  fof(f943,definition,(
% 5.51/1.17    sQ59_spl <=> (frontsegP(sK48_skl,sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f944,plain,(
% 5.51/1.17    frontsegP(sK48_skl,sK48_skl)|~sQ59_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f943])).
% 5.51/1.17  fof(f945,plain,(
% 5.51/1.17    ~frontsegP(sK48_skl,sK48_skl)|sQ59_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f943])).
% 5.51/1.17  fof(f946,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ59_spl|sQ53_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f942,f501,f943,f910])).
% 5.51/1.17  fof(f950,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|sQ59_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f945,f286])).
% 5.51/1.17  fof(f956,plain,(
% 5.51/1.17    ~sQ8_spl|sQ59_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f950,f501,f943])).
% 5.51/1.17  fof(f957,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl|~sQ59_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f944,f123])).
% 5.51/1.17  fof(f958,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(sK48_skl)|~frontsegP(sK48_skl,sK48_skl)|sK48_skl=sK48_skl|~sQ59_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f944,f284])).
% 5.51/1.17  fof(f959,definition,(
% 5.51/1.17    sQ61_spl <=> (app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f962,plain,(
% 5.51/1.17    ~sQ8_spl|sQ61_spl|~sQ59_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f957,f501,f959,f943])).
% 5.51/1.17  fof(f963,definition,(
% 5.51/1.17    sQ62_spl <=> (sK48_skl=sK48_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f966,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ59_spl|sQ62_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f958,f501,f943,f963])).
% 5.51/1.17  fof(f968,plain,(
% 5.51/1.17    app(nil,sK5_skl(sK48_skl,sK48_skl))=sK5_skl(sK48_skl,sK48_skl)|~sQ53_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f911,f249])).
% 5.51/1.17  fof(f970,plain,(
% 5.51/1.17    app(sK48_skl,nil)=sK48_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f389,f420])).
% 5.51/1.17  fof(f976,plain,(
% 5.51/1.17    app(sK47_skl,nil)=sK47_skl),
% 5.51/1.17    inference(resolution,[status(thm)],[f389,f419])).
% 5.51/1.17  fof(f981,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f970,f458])).
% 5.51/1.17  fof(f983,definition,(
% 5.51/1.17    ![X0]: (sQ63_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f986,plain,(
% 5.51/1.17    sQ63_spl|~sQ11_spl|~sQ8_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f981,f983,f529,f501])).
% 5.51/1.17  fof(f988,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK47_skl)|~ssList(X0)|~ssList(nil)|~frontsegP(sK47_skl,X0)|frontsegP(sK47_skl,X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f976,f288])).
% 5.51/1.17  fof(f989,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f976,f458])).
% 5.51/1.17  fof(f990,definition,(
% 5.51/1.17    ![X0]: (sQ64_spl <=> (~ssList(X0)|~frontsegP(sK47_skl,X0)|frontsegP(sK47_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f993,plain,(
% 5.51/1.17    ~sQ5_spl|sQ64_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f988,f491,f990,f529])).
% 5.51/1.17  fof(f994,definition,(
% 5.51/1.17    ![X0]: (sQ65_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f997,plain,(
% 5.51/1.17    sQ65_spl|~sQ11_spl|~sQ5_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f989,f994,f529,f491])).
% 5.51/1.17  fof(f1013,plain,(
% 5.51/1.17    ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK5_skl(sK47_skl,sK47_skl))|segmentP(app(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),X0),sK5_skl(sK47_skl,sK47_skl))|~ssList(sK47_skl)|~ssList(X0))),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f901,f458])).
% 5.51/1.17  fof(f1014,definition,(
% 5.51/1.17    sQ66_spl <=> (ssList(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1015,plain,(
% 5.51/1.17    ssList(sK5_skl(sK47_skl,sK47_skl))|~sQ66_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1014])).
% 5.51/1.17  fof(f1016,plain,(
% 5.51/1.17    ~ssList(sK5_skl(sK47_skl,sK47_skl))|sQ66_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1014])).
% 5.51/1.17  fof(f1018,definition,(
% 5.51/1.17    ![X0]: (sQ67_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),X0),sK5_skl(sK47_skl,sK47_skl))|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1021,plain,(
% 5.51/1.17    sQ67_spl|~sQ66_spl|~sQ5_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1013,f1018,f1014,f491])).
% 5.51/1.17  fof(f1022,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(sK47_skl)|~frontsegP(sK47_skl,sK47_skl)|sQ66_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1016,f122])).
% 5.51/1.17  fof(f1023,definition,(
% 5.51/1.17    sQ68_spl <=> (frontsegP(sK47_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1024,plain,(
% 5.51/1.17    frontsegP(sK47_skl,sK47_skl)|~sQ68_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1023])).
% 5.51/1.17  fof(f1025,plain,(
% 5.51/1.17    ~frontsegP(sK47_skl,sK47_skl)|sQ68_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1023])).
% 5.51/1.17  fof(f1026,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ68_spl|sQ66_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1022,f491,f1023,f1014])).
% 5.51/1.17  fof(f1029,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|sQ68_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1025,f286])).
% 5.51/1.17  fof(f1034,plain,(
% 5.51/1.17    ~sQ5_spl|sQ68_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1029,f491,f1023])).
% 5.51/1.17  fof(f1036,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ68_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1024,f123])).
% 5.51/1.17  fof(f1037,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(sK47_skl)|~frontsegP(sK47_skl,sK47_skl)|sK47_skl=sK47_skl|~sQ68_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1024,f284])).
% 5.51/1.17  fof(f1039,definition,(
% 5.51/1.17    sQ70_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1042,plain,(
% 5.51/1.17    ~sQ5_spl|sQ70_spl|~sQ68_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1036,f491,f1039,f1023])).
% 5.51/1.17  fof(f1043,definition,(
% 5.51/1.17    sQ71_spl <=> (sK47_skl=sK47_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1046,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ68_spl|sQ71_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1037,f491,f1023,f1043])).
% 5.51/1.17  fof(f1119,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(sK47_skl)|~ssList(nil)|~ssList(X0)|~ssList(X1)|segmentP(app(app(X0,sK47_skl),X1),nil)|~sQ14_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f321,f540])).
% 5.51/1.17  fof(f1120,plain,(
% 5.51/1.17    ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X0),X2),nil)|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f321,f323])).
% 5.51/1.17  fof(f1126,definition,(
% 5.51/1.17    ![X0,X1]: (sQ82_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X0,sK47_skl),X1),nil)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1129,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ11_spl|sQ82_spl|~sQ14_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1119,f491,f529,f1126,f539])).
% 5.51/1.17  fof(f1130,definition,(
% 5.51/1.17    ![X0,X1,X2]: (sQ83_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X0),X2),nil)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1133,plain,(
% 5.51/1.17    sQ83_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1120,f1130,f529])).
% 5.51/1.17  fof(f1142,plain,(
% 5.51/1.17    ~ssList(nil)|frontsegP(nil,nil)|~ssList(nil)),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f780,f470])).
% 5.51/1.17  fof(f1143,plain,(
% 5.51/1.17    ~ssList(nil)|frontsegP(sK47_skl,nil)|~ssList(sK47_skl)),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f777,f470])).
% 5.51/1.17  fof(f1144,plain,(
% 5.51/1.17    ~ssList(nil)|frontsegP(sK48_skl,nil)|~ssList(sK48_skl)),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f772,f470])).
% 5.51/1.17  fof(f1153,definition,(
% 5.51/1.17    sQ84_spl <=> (frontsegP(nil,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1154,plain,(
% 5.51/1.17    frontsegP(nil,nil)|~sQ84_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1153])).
% 5.51/1.17  fof(f1156,plain,(
% 5.51/1.17    ~sQ11_spl|sQ84_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1142,f529,f1153])).
% 5.51/1.17  fof(f1157,definition,(
% 5.51/1.17    sQ85_spl <=> (frontsegP(sK47_skl,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1158,plain,(
% 5.51/1.17    frontsegP(sK47_skl,nil)|~sQ85_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1157])).
% 5.51/1.17  fof(f1160,plain,(
% 5.51/1.17    ~sQ11_spl|sQ85_spl|~sQ5_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1143,f529,f1157,f491])).
% 5.51/1.17  fof(f1161,definition,(
% 5.51/1.17    sQ86_spl <=> (frontsegP(sK48_skl,nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1162,plain,(
% 5.51/1.17    frontsegP(sK48_skl,nil)|~sQ86_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1161])).
% 5.51/1.17  fof(f1164,plain,(
% 5.51/1.17    ~sQ11_spl|sQ86_spl|~sQ8_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1144,f529,f1161,f501])).
% 5.51/1.17  fof(f1165,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK48_skl))=sK48_skl|~sQ86_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1162,f123])).
% 5.51/1.17  fof(f1167,definition,(
% 5.51/1.17    sQ87_spl <=> (app(nil,sK5_skl(nil,sK48_skl))=sK48_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1170,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ11_spl|sQ87_spl|~sQ86_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1165,f501,f529,f1167,f1161])).
% 5.51/1.17  fof(f1173,plain,(
% 5.51/1.17    ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ84_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1154,f123])).
% 5.51/1.17  fof(f1176,definition,(
% 5.51/1.17    sQ88_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1179,plain,(
% 5.51/1.17    ~sQ11_spl|sQ88_spl|~sQ84_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1173,f529,f1176,f1153])).
% 5.51/1.17  fof(f1182,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ85_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1158,f123])).
% 5.51/1.17  fof(f1185,definition,(
% 5.51/1.17    sQ89_spl <=> (app(nil,sK5_skl(nil,sK47_skl))=sK47_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1188,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ11_spl|sQ89_spl|~sQ85_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1182,f491,f529,f1185,f1157])).
% 5.51/1.17  fof(f1220,plain,(
% 5.51/1.17    cyclefreeP(sK5_skl(sK47_skl,sK47_skl))|app(app(sK11_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK9_skl(sK5_skl(sK47_skl,sK47_skl)),sK12_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK10_skl(sK5_skl(sK47_skl,sK47_skl)),sK13_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl)|~sQ66_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f147,f1015])).
% 5.51/1.17  fof(f1247,definition,(
% 5.51/1.17    sQ97_spl <=> (cyclefreeP(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1250,definition,(
% 5.51/1.17    sQ98_spl <=> (app(app(sK11_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK9_skl(sK5_skl(sK47_skl,sK47_skl)),sK12_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK10_skl(sK5_skl(sK47_skl,sK47_skl)),sK13_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1253,plain,(
% 5.51/1.17    sQ97_spl|sQ98_spl|~sQ66_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1220,f1247,f1250,f1014])).
% 5.51/1.17  fof(f1308,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|~ssList(sK48_skl)|~ssList(X0)|app(X0,sK5_skl(X0,sK48_skl))=sK48_skl|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f784,f123])).
% 5.51/1.17  fof(f1309,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f784,f284])).
% 5.51/1.17  fof(f1310,definition,(
% 5.51/1.17    ![X0]: (sQ106_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|app(X0,sK5_skl(X0,sK48_skl))=sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1313,plain,(
% 5.51/1.17    sQ106_spl|~sQ8_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1308,f1310,f501,f783])).
% 5.51/1.17  fof(f1314,definition,(
% 5.51/1.17    ![X0]: (sQ107_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|~frontsegP(X0,sK48_skl)|X0=sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1317,plain,(
% 5.51/1.17    sQ107_spl|~sQ8_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1309,f1314,f501,f783])).
% 5.51/1.17  fof(f1322,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|~ssList(sK47_skl)|~ssList(X0)|app(X0,sK5_skl(X0,sK47_skl))=sK47_skl|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f795,f123])).
% 5.51/1.17  fof(f1323,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f795,f284])).
% 5.51/1.17  fof(f1326,definition,(
% 5.51/1.17    ![X0]: (sQ108_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|app(X0,sK5_skl(X0,sK47_skl))=sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1329,plain,(
% 5.51/1.17    sQ108_spl|~sQ5_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1322,f1326,f491,f794])).
% 5.51/1.17  fof(f1330,definition,(
% 5.51/1.17    ![X0]: (sQ109_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|~frontsegP(X0,sK47_skl)|X0=sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1333,plain,(
% 5.51/1.17    sQ109_spl|~sQ5_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1323,f1330,f491,f794])).
% 5.51/1.17  fof(f1349,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|~frontsegP(X0,nil)|X0=nil|~ssList(nil)|~frontsegP(nil,X0)|~sQ84_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f1154])).
% 5.51/1.17  fof(f1350,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~ssList(nil)|~frontsegP(nil,X0)|~sQ85_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f1158])).
% 5.51/1.17  fof(f1352,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~ssList(sK47_skl)|~frontsegP(sK47_skl,X0)|~sQ68_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f1024])).
% 5.51/1.17  fof(f1354,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~ssList(X1)|~frontsegP(X1,X0)|~ssList(X1)|~frontsegP(nil,X1)|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f795])).
% 5.51/1.17  fof(f1355,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~ssList(nil)|~frontsegP(nil,X0)|~sQ86_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f1162])).
% 5.51/1.17  fof(f1357,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~ssList(sK48_skl)|~frontsegP(sK48_skl,X0)|~sQ59_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f944])).
% 5.51/1.17  fof(f1360,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~ssList(X1)|~frontsegP(X1,X0)|~ssList(X1)|~frontsegP(nil,X1)|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f784])).
% 5.51/1.17  fof(f1367,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~ssList(nil)|~frontsegP(nil,X0)|~ssList(X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f295])).
% 5.51/1.17  fof(f1373,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|~sQ85_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f1158])).
% 5.51/1.17  fof(f1375,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~ssList(sK47_skl)|~frontsegP(X1,sK47_skl)|~ssList(X0)|~frontsegP(nil,X0)|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f795])).
% 5.51/1.17  fof(f1376,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|~sQ86_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f1162])).
% 5.51/1.17  fof(f1379,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~ssList(sK48_skl)|~frontsegP(X1,sK48_skl)|~ssList(X0)|~frontsegP(nil,X0)|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f784])).
% 5.51/1.17  fof(f1383,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(nil)|~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(X1)|~frontsegP(X0,X1)|~ssList(X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f617,f295])).
% 5.51/1.17  fof(f1388,definition,(
% 5.51/1.17    ![X0]: (sQ111_spl <=> (~ssList(X0)|~frontsegP(X0,nil)|X0=nil|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1391,plain,(
% 5.51/1.17    sQ111_spl|~sQ11_spl|~sQ84_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1349,f1388,f529,f1153])).
% 5.51/1.17  fof(f1392,definition,(
% 5.51/1.17    ![X0]: (sQ112_spl <=> (~ssList(X0)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1395,plain,(
% 5.51/1.17    sQ112_spl|~sQ5_spl|~sQ11_spl|~sQ85_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1350,f1392,f491,f529,f1157])).
% 5.51/1.17  fof(f1397,definition,(
% 5.51/1.17    ![X0]: (sQ113_spl <=> (~ssList(X0)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~frontsegP(sK47_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1400,plain,(
% 5.51/1.17    sQ113_spl|~sQ5_spl|~sQ68_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1352,f1397,f491,f1023])).
% 5.51/1.17  fof(f1402,definition,(
% 5.51/1.17    ![X0,X1]: (sQ114_spl <=> (~ssList(X0)|~frontsegP(X0,sK47_skl)|X0=sK47_skl|~ssList(X1)|~frontsegP(X1,X0)|~ssList(X1)|~frontsegP(nil,X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1405,plain,(
% 5.51/1.17    sQ114_spl|~sQ5_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1354,f1402,f491,f794])).
% 5.51/1.17  fof(f1406,definition,(
% 5.51/1.17    ![X0]: (sQ115_spl <=> (~ssList(X0)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1409,plain,(
% 5.51/1.17    sQ115_spl|~sQ8_spl|~sQ11_spl|~sQ86_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1355,f1406,f501,f529,f1161])).
% 5.51/1.17  fof(f1411,definition,(
% 5.51/1.17    ![X0]: (sQ116_spl <=> (~ssList(X0)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~frontsegP(sK48_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1414,plain,(
% 5.51/1.17    sQ116_spl|~sQ8_spl|~sQ59_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1357,f1411,f501,f943])).
% 5.51/1.17  fof(f1420,definition,(
% 5.51/1.17    ![X0,X1]: (sQ118_spl <=> (~ssList(X0)|~frontsegP(X0,sK48_skl)|X0=sK48_skl|~ssList(X1)|~frontsegP(X1,X0)|~ssList(X1)|~frontsegP(nil,X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1423,plain,(
% 5.51/1.17    sQ118_spl|~sQ8_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1360,f1420,f501,f783])).
% 5.51/1.17  fof(f1433,definition,(
% 5.51/1.17    ![X0,X1]: (sQ120_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~frontsegP(nil,X0)|~ssList(X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1436,plain,(
% 5.51/1.17    sQ120_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1367,f1433,f529])).
% 5.51/1.17  fof(f1440,definition,(
% 5.51/1.17    ![X0]: (sQ121_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~frontsegP(X0,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1443,plain,(
% 5.51/1.17    ~sQ11_spl|sQ121_spl|~sQ5_spl|~sQ85_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1373,f529,f1440,f491,f1157])).
% 5.51/1.17  fof(f1445,definition,(
% 5.51/1.17    ![X0,X1]: (sQ122_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~frontsegP(X1,sK47_skl)|~ssList(X0)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1448,plain,(
% 5.51/1.17    sQ122_spl|~sQ5_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1375,f1445,f491,f794])).
% 5.51/1.17  fof(f1449,definition,(
% 5.51/1.17    ![X0]: (sQ123_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~frontsegP(X0,sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1452,plain,(
% 5.51/1.17    ~sQ11_spl|sQ123_spl|~sQ8_spl|~sQ86_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1376,f529,f1449,f501,f1161])).
% 5.51/1.17  fof(f1458,definition,(
% 5.51/1.17    ![X0,X1]: (sQ125_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|X0=X1|~frontsegP(X1,sK48_skl)|~ssList(X0)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1461,plain,(
% 5.51/1.17    sQ125_spl|~sQ8_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1379,f1458,f501,f783])).
% 5.51/1.17  fof(f1470,definition,(
% 5.51/1.17    ![X0,X1]: (sQ127_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(X1)|~frontsegP(X0,X1)|~ssList(X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1473,plain,(
% 5.51/1.17    ~sQ11_spl|sQ127_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1383,f529,f1470])).
% 5.51/1.17  fof(f1484,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(nil)|~ssList(X0)|~frontsegP(nil,app(nil,X0))|nil=app(nil,X0)|~sQ84_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f1154])).
% 5.51/1.17  fof(f1485,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK47_skl)|~ssList(nil)|~ssList(X0)|~frontsegP(nil,app(sK47_skl,X0))|nil=app(sK47_skl,X0)|~sQ85_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f1158])).
% 5.51/1.17  fof(f1486,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK47_skl)|~ssList(sK47_skl)|~ssList(X0)|~frontsegP(sK47_skl,app(sK47_skl,X0))|sK47_skl=app(sK47_skl,X0)|~sQ68_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f1024])).
% 5.51/1.17  fof(f1487,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(sK47_skl)|~ssList(X0)|~ssList(X1)|~frontsegP(X0,app(sK47_skl,X1))|X0=app(sK47_skl,X1)|~ssList(X0)|~frontsegP(nil,X0)|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f795])).
% 5.51/1.17  fof(f1488,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK48_skl)|~ssList(nil)|~ssList(X0)|~frontsegP(nil,app(sK48_skl,X0))|nil=app(sK48_skl,X0)|~sQ86_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f1162])).
% 5.51/1.17  fof(f1489,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK48_skl)|~ssList(sK48_skl)|~ssList(X0)|~frontsegP(sK48_skl,app(sK48_skl,X0))|sK48_skl=app(sK48_skl,X0)|~sQ59_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f944])).
% 5.51/1.17  fof(f1491,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(sK48_skl)|~ssList(X0)|~ssList(X1)|~frontsegP(X0,app(sK48_skl,X1))|X0=app(sK48_skl,X1)|~ssList(X0)|~frontsegP(nil,X0)|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f784])).
% 5.51/1.17  fof(f1495,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|~frontsegP(nil,app(X0,X1))|nil=app(X0,X1)|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f621,f295])).
% 5.51/1.17  fof(f1498,definition,(
% 5.51/1.17    ![X0]: (sQ128_spl <=> (~ssList(X0)|~frontsegP(nil,app(nil,X0))|nil=app(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1501,plain,(
% 5.51/1.17    ~sQ11_spl|sQ128_spl|~sQ84_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1484,f529,f1498,f1153])).
% 5.51/1.17  fof(f1502,definition,(
% 5.51/1.17    ![X0]: (sQ129_spl <=> (~ssList(X0)|~frontsegP(nil,app(sK47_skl,X0))|nil=app(sK47_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1505,plain,(
% 5.51/1.17    ~sQ5_spl|~sQ11_spl|sQ129_spl|~sQ85_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1485,f491,f529,f1502,f1157])).
% 5.51/1.17  fof(f1506,definition,(
% 5.51/1.17    ![X0]: (sQ130_spl <=> (~ssList(X0)|~frontsegP(sK47_skl,app(sK47_skl,X0))|sK47_skl=app(sK47_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1509,plain,(
% 5.51/1.17    ~sQ5_spl|sQ130_spl|~sQ68_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1486,f491,f1506,f1023])).
% 5.51/1.17  fof(f1510,definition,(
% 5.51/1.17    ![X0,X1]: (sQ131_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(X0,app(sK47_skl,X1))|X0=app(sK47_skl,X1)|~ssList(X0)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1513,plain,(
% 5.51/1.17    ~sQ5_spl|sQ131_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1487,f491,f1510,f794])).
% 5.51/1.17  fof(f1514,definition,(
% 5.51/1.17    ![X0]: (sQ132_spl <=> (~ssList(X0)|~frontsegP(nil,app(sK48_skl,X0))|nil=app(sK48_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1517,plain,(
% 5.51/1.17    ~sQ8_spl|~sQ11_spl|sQ132_spl|~sQ86_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1488,f501,f529,f1514,f1161])).
% 5.51/1.17  fof(f1518,definition,(
% 5.51/1.17    ![X0]: (sQ133_spl <=> (~ssList(X0)|~frontsegP(sK48_skl,app(sK48_skl,X0))|sK48_skl=app(sK48_skl,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1521,plain,(
% 5.51/1.17    ~sQ8_spl|sQ133_spl|~sQ59_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1489,f501,f1518,f943])).
% 5.51/1.17  fof(f1526,definition,(
% 5.51/1.17    ![X0,X1]: (sQ135_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(X0,app(sK48_skl,X1))|X0=app(sK48_skl,X1)|~ssList(X0)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1529,plain,(
% 5.51/1.17    ~sQ8_spl|sQ135_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1491,f501,f1526,f783])).
% 5.51/1.17  fof(f1538,definition,(
% 5.51/1.17    ![X0,X1]: (sQ137_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(nil,app(X0,X1))|nil=app(X0,X1)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1541,plain,(
% 5.51/1.17    sQ137_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1495,f1538,f529])).
% 5.51/1.17  fof(f1625,plain,(
% 5.51/1.17    totalorderP(sK5_skl(sK47_skl,sK47_skl))|app(app(sK16_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK14_skl(sK5_skl(sK47_skl,sK47_skl)),sK17_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK15_skl(sK5_skl(sK47_skl,sK47_skl)),sK18_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl)|~sQ66_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f159,f1015])).
% 5.51/1.17  fof(f1652,definition,(
% 5.51/1.17    sQ144_spl <=> (totalorderP(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1655,definition,(
% 5.51/1.17    sQ145_spl <=> (app(app(sK16_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK14_skl(sK5_skl(sK47_skl,sK47_skl)),sK17_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK15_skl(sK5_skl(sK47_skl,sK47_skl)),sK18_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1658,plain,(
% 5.51/1.17    sQ144_spl|sQ145_spl|~sQ66_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1625,f1652,f1655,f1014])).
% 5.51/1.17  fof(f1692,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|app(nil,sK5_skl(nil,app(nil,X0)))=app(nil,X0)|~ssList(nil)|~ssList(X0)|~sQ84_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f1154])).
% 5.51/1.17  fof(f1693,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|app(nil,sK5_skl(nil,app(sK47_skl,X0)))=app(sK47_skl,X0)|~ssList(sK47_skl)|~ssList(X0)|~sQ85_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f1158])).
% 5.51/1.17  fof(f1694,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,app(sK47_skl,X0)))=app(sK47_skl,X0)|~ssList(sK47_skl)|~ssList(X0)|~sQ68_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f1024])).
% 5.51/1.17  fof(f1695,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|app(X0,sK5_skl(X0,app(sK47_skl,X1)))=app(sK47_skl,X1)|~ssList(sK47_skl)|~ssList(X1)|~ssList(X0)|~frontsegP(nil,X0)|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f795])).
% 5.51/1.17  fof(f1696,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|app(nil,sK5_skl(nil,app(sK48_skl,X0)))=app(sK48_skl,X0)|~ssList(sK48_skl)|~ssList(X0)|~sQ86_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f1162])).
% 5.51/1.17  fof(f1697,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK48_skl)|app(sK48_skl,sK5_skl(sK48_skl,app(sK48_skl,X0)))=app(sK48_skl,X0)|~ssList(sK48_skl)|~ssList(X0)|~sQ59_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f944])).
% 5.51/1.17  fof(f1699,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|app(X0,sK5_skl(X0,app(sK48_skl,X1)))=app(sK48_skl,X1)|~ssList(sK48_skl)|~ssList(X1)|~ssList(X0)|~frontsegP(nil,X0)|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f784])).
% 5.51/1.17  fof(f1703,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(nil)|app(nil,sK5_skl(nil,app(X0,X1)))=app(X0,X1)|~ssList(X0)|~ssList(X1)|~ssList(X0))),
% 5.51/1.17    inference(resolution,[status(thm)],[f653,f295])).
% 5.51/1.17  fof(f1706,definition,(
% 5.51/1.17    ![X0]: (sQ151_spl <=> (app(nil,sK5_skl(nil,app(nil,X0)))=app(nil,X0)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1709,plain,(
% 5.51/1.17    ~sQ11_spl|sQ151_spl|~sQ84_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1692,f529,f1706,f1153])).
% 5.51/1.17  fof(f1710,definition,(
% 5.51/1.17    ![X0]: (sQ152_spl <=> (app(nil,sK5_skl(nil,app(sK47_skl,X0)))=app(sK47_skl,X0)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1713,plain,(
% 5.51/1.17    ~sQ11_spl|sQ152_spl|~sQ5_spl|~sQ85_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1693,f529,f1710,f491,f1157])).
% 5.51/1.17  fof(f1714,definition,(
% 5.51/1.17    ![X0]: (sQ153_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,app(sK47_skl,X0)))=app(sK47_skl,X0)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1717,plain,(
% 5.51/1.17    ~sQ5_spl|sQ153_spl|~sQ68_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1694,f491,f1714,f1023])).
% 5.51/1.17  fof(f1718,definition,(
% 5.51/1.17    ![X0,X1]: (sQ154_spl <=> (~ssList(X0)|app(X0,sK5_skl(X0,app(sK47_skl,X1)))=app(sK47_skl,X1)|~ssList(X1)|~ssList(X0)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1721,plain,(
% 5.51/1.17    sQ154_spl|~sQ5_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1695,f1718,f491,f794])).
% 5.51/1.17  fof(f1722,definition,(
% 5.51/1.17    ![X0]: (sQ155_spl <=> (app(nil,sK5_skl(nil,app(sK48_skl,X0)))=app(sK48_skl,X0)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1725,plain,(
% 5.51/1.17    ~sQ11_spl|sQ155_spl|~sQ8_spl|~sQ86_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1696,f529,f1722,f501,f1161])).
% 5.51/1.17  fof(f1726,definition,(
% 5.51/1.17    ![X0]: (sQ156_spl <=> (app(sK48_skl,sK5_skl(sK48_skl,app(sK48_skl,X0)))=app(sK48_skl,X0)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1729,plain,(
% 5.51/1.17    ~sQ8_spl|sQ156_spl|~sQ59_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1697,f501,f1726,f943])).
% 5.51/1.17  fof(f1734,definition,(
% 5.51/1.17    ![X0,X1]: (sQ158_spl <=> (~ssList(X0)|app(X0,sK5_skl(X0,app(sK48_skl,X1)))=app(sK48_skl,X1)|~ssList(X1)|~ssList(X0)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1737,plain,(
% 5.51/1.17    sQ158_spl|~sQ8_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1699,f1734,f501,f783])).
% 5.51/1.17  fof(f1746,definition,(
% 5.51/1.17    ![X0,X1]: (sQ160_spl <=> (app(nil,sK5_skl(nil,app(X0,X1)))=app(X0,X1)|~ssList(X0)|~ssList(X1)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1749,plain,(
% 5.51/1.17    ~sQ11_spl|sQ160_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1703,f529,f1746])).
% 5.51/1.17  fof(f1756,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(nil)|~frontsegP(X0,nil)|~sQ84_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f1154])).
% 5.51/1.17  fof(f1757,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|~sQ85_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f1158])).
% 5.51/1.17  fof(f1758,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,X0))=X0|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|~sQ68_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f1024])).
% 5.51/1.17  fof(f1759,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|app(X1,sK5_skl(X1,X0))=X0|~ssList(sK47_skl)|~frontsegP(X0,sK47_skl)|~ssList(X1)|~frontsegP(nil,X1)|~sQ36_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f795])).
% 5.51/1.17  fof(f1760,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|~sQ86_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f1162])).
% 5.51/1.17  fof(f1761,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK48_skl)|app(sK48_skl,sK5_skl(sK48_skl,X0))=X0|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|~sQ59_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f944])).
% 5.51/1.17  fof(f1763,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|app(X1,sK5_skl(X1,X0))=X0|~ssList(sK48_skl)|~frontsegP(X0,sK48_skl)|~ssList(X1)|~frontsegP(nil,X1)|~sQ34_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f784])).
% 5.51/1.17  fof(f1767,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X1)|~frontsegP(X0,X1)|~ssList(X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f658,f295])).
% 5.51/1.17  fof(f1770,definition,(
% 5.51/1.17    ![X0]: (sQ161_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~frontsegP(X0,nil)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1773,plain,(
% 5.51/1.17    sQ161_spl|~sQ11_spl|~sQ84_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1756,f1770,f529,f1153])).
% 5.51/1.17  fof(f1774,definition,(
% 5.51/1.17    ![X0]: (sQ162_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~frontsegP(X0,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1777,plain,(
% 5.51/1.17    sQ162_spl|~sQ11_spl|~sQ5_spl|~sQ85_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1757,f1774,f529,f491,f1157])).
% 5.51/1.17  fof(f1778,definition,(
% 5.51/1.17    ![X0]: (sQ163_spl <=> (~ssList(X0)|app(sK47_skl,sK5_skl(sK47_skl,X0))=X0|~frontsegP(X0,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1781,plain,(
% 5.51/1.17    sQ163_spl|~sQ5_spl|~sQ68_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1758,f1778,f491,f1023])).
% 5.51/1.17  fof(f1782,definition,(
% 5.51/1.17    ![X0,X1]: (sQ164_spl <=> (~ssList(X0)|~ssList(X1)|app(X1,sK5_skl(X1,X0))=X0|~frontsegP(X0,sK47_skl)|~ssList(X1)|~frontsegP(nil,X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1785,plain,(
% 5.51/1.17    sQ164_spl|~sQ5_spl|~sQ36_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1759,f1782,f491,f794])).
% 5.51/1.17  fof(f1786,definition,(
% 5.51/1.17    ![X0]: (sQ165_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~frontsegP(X0,sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1789,plain,(
% 5.51/1.17    sQ165_spl|~sQ11_spl|~sQ8_spl|~sQ86_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1760,f1786,f529,f501,f1161])).
% 5.51/1.17  fof(f1790,definition,(
% 5.51/1.17    ![X0]: (sQ166_spl <=> (~ssList(X0)|app(sK48_skl,sK5_skl(sK48_skl,X0))=X0|~frontsegP(X0,sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1793,plain,(
% 5.51/1.17    sQ166_spl|~sQ8_spl|~sQ59_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1761,f1790,f501,f943])).
% 5.51/1.17  fof(f1798,definition,(
% 5.51/1.17    ![X0,X1]: (sQ168_spl <=> (~ssList(X0)|~ssList(X1)|app(X1,sK5_skl(X1,X0))=X0|~frontsegP(X0,sK48_skl)|~ssList(X1)|~frontsegP(nil,X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1801,plain,(
% 5.51/1.17    sQ168_spl|~sQ8_spl|~sQ34_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1763,f1798,f501,f783])).
% 5.51/1.17  fof(f1810,definition,(
% 5.51/1.17    ![X0,X1]: (sQ170_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X1)|~frontsegP(X0,X1)|~ssList(X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1813,plain,(
% 5.51/1.17    sQ170_spl|~sQ11_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1767,f1810,f529])).
% 5.51/1.17  fof(f1911,plain,(
% 5.51/1.17    strictorderP(sK5_skl(sK47_skl,sK47_skl))|app(app(sK21_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK19_skl(sK5_skl(sK47_skl,sK47_skl)),sK22_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK20_skl(sK5_skl(sK47_skl,sK47_skl)),sK23_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl)|~sQ66_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f171,f1015])).
% 5.51/1.17  fof(f1938,definition,(
% 5.51/1.17    sQ177_spl <=> (strictorderP(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1941,definition,(
% 5.51/1.17    sQ178_spl <=> (app(app(sK21_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK19_skl(sK5_skl(sK47_skl,sK47_skl)),sK22_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK20_skl(sK5_skl(sK47_skl,sK47_skl)),sK23_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1944,plain,(
% 5.51/1.17    sQ177_spl|sQ178_spl|~sQ66_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1911,f1938,f1941,f1014])).
% 5.51/1.17  fof(f1959,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|segmentP(app(sK48_skl,nil),sK48_skl)|~ssList(nil)|~sQ35_spl),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f970,f791])).
% 5.51/1.17  fof(f1960,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|segmentP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK48_skl)|~ssList(sK5_skl(sK48_skl,sK48_skl))|~sQ35_spl),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f896,f791])).
% 5.51/1.17  fof(f1961,definition,(
% 5.51/1.17    sQ183_spl <=> (segmentP(app(sK48_skl,nil),sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1962,plain,(
% 5.51/1.17    segmentP(app(sK48_skl,nil),sK48_skl)|~sQ183_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f1961])).
% 5.51/1.17  fof(f1964,plain,(
% 5.51/1.17    ~sQ8_spl|sQ183_spl|~sQ11_spl|~sQ35_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1959,f501,f1961,f529,f787])).
% 5.51/1.17  fof(f1965,definition,(
% 5.51/1.17    sQ184_spl <=> (segmentP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1968,plain,(
% 5.51/1.17    ~sQ8_spl|sQ184_spl|~sQ53_spl|~sQ35_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1960,f501,f1965,f910,f787])).
% 5.51/1.17  fof(f1969,plain,(
% 5.51/1.17    segmentP(sK48_skl,sK48_skl)|~sQ183_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f970,f1962])).
% 5.51/1.17  fof(f1972,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(sK48_skl)|~ssList(sK48_skl)|~ssList(X0)|~ssList(X1)|segmentP(app(app(X0,sK48_skl),X1),sK48_skl)|~sQ183_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f1969,f321])).
% 5.51/1.17  fof(f1974,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK48_skl)|~ssList(sK48_skl)|~segmentP(X0,sK48_skl)|segmentP(X0,sK48_skl)|~sQ183_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f1969,f315])).
% 5.51/1.17  fof(f1975,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|~ssList(sK48_skl)|app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl))=sK48_skl|~sQ183_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f1969,f136])).
% 5.51/1.17  fof(f1977,definition,(
% 5.51/1.17    ![X0,X1]: (sQ185_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X0,sK48_skl),X1),sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1980,plain,(
% 5.51/1.17    ~sQ8_spl|sQ185_spl|~sQ183_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1972,f501,f1977,f1961])).
% 5.51/1.17  fof(f1985,definition,(
% 5.51/1.17    ![X0]: (sQ187_spl <=> (~ssList(X0)|~segmentP(X0,sK48_skl)|segmentP(X0,sK48_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1988,plain,(
% 5.51/1.17    sQ187_spl|~sQ8_spl|~sQ183_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1974,f1985,f501,f1961])).
% 5.51/1.17  fof(f1989,definition,(
% 5.51/1.17    sQ188_spl <=> (app(app(sK7_skl(sK48_skl,sK48_skl),sK48_skl),sK8_skl(sK48_skl,sK48_skl))=sK48_skl)),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f1992,plain,(
% 5.51/1.17    ~sQ8_spl|sQ188_spl|~sQ183_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f1975,f501,f1989,f1961])).
% 5.51/1.17  fof(f2098,plain,(
% 5.51/1.17    ~ssList(nil)|frontsegP(sK5_skl(sK48_skl,sK48_skl),nil)|~ssList(sK5_skl(sK48_skl,sK48_skl))|~sQ53_spl),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f968,f470])).
% 5.51/1.17  fof(f2099,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(sK5_skl(sK48_skl,sK48_skl))|~frontsegP(nil,X0)|frontsegP(sK5_skl(sK48_skl,sK48_skl),X0)|~sQ53_spl)),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f968,f288])).
% 5.51/1.17  fof(f2100,definition,(
% 5.51/1.17    sQ189_spl <=> (frontsegP(sK5_skl(sK48_skl,sK48_skl),nil))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2101,plain,(
% 5.51/1.17    frontsegP(sK5_skl(sK48_skl,sK48_skl),nil)|~sQ189_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f2100])).
% 5.51/1.17  fof(f2103,plain,(
% 5.51/1.17    ~sQ11_spl|sQ189_spl|~sQ53_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2098,f529,f2100,f910])).
% 5.51/1.17  fof(f2104,definition,(
% 5.51/1.17    ![X0]: (sQ190_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|frontsegP(sK5_skl(sK48_skl,sK48_skl),X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2107,plain,(
% 5.51/1.17    ~sQ11_spl|sQ190_spl|~sQ53_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2099,f529,f2104,f910])).
% 5.51/1.17  fof(f2108,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(sK5_skl(sK48_skl,sK48_skl))|~frontsegP(X0,sK5_skl(sK48_skl,sK48_skl))|~sQ189_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f2101,f658])).
% 5.51/1.17  fof(f2109,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|app(nil,sK5_skl(nil,app(sK5_skl(sK48_skl,sK48_skl),X0)))=app(sK5_skl(sK48_skl,sK48_skl),X0)|~ssList(sK5_skl(sK48_skl,sK48_skl))|~ssList(X0)|~sQ189_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f2101,f653])).
% 5.51/1.17  fof(f2110,plain,(
% 5.51/1.17    ![X0]: (~ssList(sK5_skl(sK48_skl,sK48_skl))|~ssList(nil)|~ssList(X0)|~frontsegP(nil,app(sK5_skl(sK48_skl,sK48_skl),X0))|nil=app(sK5_skl(sK48_skl,sK48_skl),X0)|~sQ189_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f2101,f621])).
% 5.51/1.17  fof(f2111,plain,(
% 5.51/1.17    ![X0]: (~ssList(nil)|~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(sK5_skl(sK48_skl,sK48_skl))|~frontsegP(X0,sK5_skl(sK48_skl,sK48_skl))|~sQ189_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f2101,f617])).
% 5.51/1.17  fof(f2112,plain,(
% 5.51/1.17    ![X0]: (~ssList(X0)|~ssList(sK5_skl(sK48_skl,sK48_skl))|~frontsegP(X0,sK5_skl(sK48_skl,sK48_skl))|X0=sK5_skl(sK48_skl,sK48_skl)|~ssList(nil)|~frontsegP(nil,X0)|~sQ189_spl)),
% 5.51/1.17    inference(resolution,[status(thm)],[f2101,f617])).
% 5.51/1.17  fof(f2113,plain,(
% 5.51/1.17    ~ssList(sK5_skl(sK48_skl,sK48_skl))|~ssList(nil)|app(nil,sK5_skl(nil,sK5_skl(sK48_skl,sK48_skl)))=sK5_skl(sK48_skl,sK48_skl)|~sQ189_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f2101,f123])).
% 5.51/1.17  fof(f2115,definition,(
% 5.51/1.17    ![X0]: (sQ191_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~frontsegP(X0,sK5_skl(sK48_skl,sK48_skl))))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2118,plain,(
% 5.51/1.17    sQ191_spl|~sQ11_spl|~sQ53_spl|~sQ189_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2108,f2115,f529,f910,f2100])).
% 5.51/1.17  fof(f2119,definition,(
% 5.51/1.17    ![X0]: (sQ192_spl <=> (app(nil,sK5_skl(nil,app(sK5_skl(sK48_skl,sK48_skl),X0)))=app(sK5_skl(sK48_skl,sK48_skl),X0)|~ssList(X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2122,plain,(
% 5.51/1.17    ~sQ11_spl|sQ192_spl|~sQ53_spl|~sQ189_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2109,f529,f2119,f910,f2100])).
% 5.51/1.17  fof(f2123,definition,(
% 5.51/1.17    ![X0]: (sQ193_spl <=> (~ssList(X0)|~frontsegP(nil,app(sK5_skl(sK48_skl,sK48_skl),X0))|nil=app(sK5_skl(sK48_skl,sK48_skl),X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2126,plain,(
% 5.51/1.17    ~sQ53_spl|~sQ11_spl|sQ193_spl|~sQ189_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2110,f910,f529,f2123,f2100])).
% 5.51/1.17  fof(f2127,definition,(
% 5.51/1.17    ![X0]: (sQ194_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~frontsegP(X0,sK5_skl(sK48_skl,sK48_skl))))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2130,plain,(
% 5.51/1.17    ~sQ11_spl|sQ194_spl|~sQ53_spl|~sQ189_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2111,f529,f2127,f910,f2100])).
% 5.51/1.17  fof(f2131,definition,(
% 5.51/1.17    ![X0]: (sQ195_spl <=> (~ssList(X0)|~frontsegP(X0,sK5_skl(sK48_skl,sK48_skl))|X0=sK5_skl(sK48_skl,sK48_skl)|~frontsegP(nil,X0)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2134,plain,(
% 5.51/1.17    sQ195_spl|~sQ53_spl|~sQ11_spl|~sQ189_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2112,f2131,f910,f529,f2100])).
% 5.51/1.17  fof(f2135,definition,(
% 5.51/1.17    sQ196_spl <=> (app(nil,sK5_skl(nil,sK5_skl(sK48_skl,sK48_skl)))=sK5_skl(sK48_skl,sK48_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2138,plain,(
% 5.51/1.17    ~sQ53_spl|~sQ11_spl|sQ196_spl|~sQ189_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2113,f910,f529,f2135,f2100])).
% 5.51/1.17  fof(f2233,plain,(
% 5.51/1.17    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|~ssItem(sK1_skl)|~ssItem(sK1_skl)|~ssList(X0)|~ssList(X1)|frontsegP(X0,X1))),
% 5.51/1.17    inference(resolution,[status(thm)],[f748,f292])).
% 5.51/1.17  fof(f2244,definition,(
% 5.51/1.17    ![X0,X1]: (sQ200_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2247,definition,(
% 5.51/1.17    sQ201_spl <=> (ssItem(sK1_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2249,plain,(
% 5.51/1.17    ~ssItem(sK1_skl)|sQ201_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f2247])).
% 5.51/1.17  fof(f2250,plain,(
% 5.51/1.17    sQ200_spl|~sQ201_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2233,f2244,f2247])).
% 5.51/1.17  fof(f2255,plain,(
% 5.51/1.17    $false|sQ201_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f2249,f104])).
% 5.51/1.17  fof(f2256,plain,(
% 5.51/1.17    sQ201_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f2255])).
% 5.51/1.17  fof(f2386,plain,(
% 5.51/1.17    duplicatefreeP(sK5_skl(sK47_skl,sK47_skl))|sK34_skl(sK5_skl(sK47_skl,sK47_skl))=sK35_skl(sK5_skl(sK47_skl,sK47_skl))|~sQ66_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f206,f1015])).
% 5.51/1.17  fof(f2413,definition,(
% 5.51/1.17    sQ210_spl <=> (duplicatefreeP(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2416,definition,(
% 5.51/1.17    sQ211_spl <=> (sK34_skl(sK5_skl(sK47_skl,sK47_skl))=sK35_skl(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2419,plain,(
% 5.51/1.17    sQ210_spl|sQ211_spl|~sQ66_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2386,f2413,f2416,f1014])).
% 5.51/1.17  fof(f2463,plain,(
% 5.51/1.17    totalorderedP(sK5_skl(sK47_skl,sK47_skl))|app(app(sK26_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK24_skl(sK5_skl(sK47_skl,sK47_skl)),sK27_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK25_skl(sK5_skl(sK47_skl,sK47_skl)),sK28_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl)|~sQ66_spl),
% 5.51/1.17    inference(resolution,[status(thm)],[f183,f1015])).
% 5.51/1.17  fof(f2490,definition,(
% 5.51/1.17    sQ222_spl <=> (totalorderedP(sK5_skl(sK47_skl,sK47_skl)))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2493,definition,(
% 5.51/1.17    sQ223_spl <=> (app(app(sK26_skl(sK5_skl(sK47_skl,sK47_skl)),cons(sK24_skl(sK5_skl(sK47_skl,sK47_skl)),sK27_skl(sK5_skl(sK47_skl,sK47_skl)))),cons(sK25_skl(sK5_skl(sK47_skl,sK47_skl)),sK28_skl(sK5_skl(sK47_skl,sK47_skl))))=sK5_skl(sK47_skl,sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2496,plain,(
% 5.51/1.17    sQ222_spl|sQ223_spl|~sQ66_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2463,f2490,f2493,f1014])).
% 5.51/1.17  fof(f2511,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|segmentP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)|~sQ37_spl),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f976,f802])).
% 5.51/1.17  fof(f2512,plain,(
% 5.51/1.17    ~ssList(sK48_skl)|segmentP(app(sK47_skl,sK5_skl(sK47_skl,sK48_skl)),sK47_skl)|~ssList(sK5_skl(sK47_skl,sK48_skl))|~sQ37_spl|~sQ26_spl),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f664,f802])).
% 5.51/1.17  fof(f2513,plain,(
% 5.51/1.17    ~ssList(sK47_skl)|segmentP(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),sK47_skl)|~ssList(sK5_skl(sK47_skl,sK47_skl))|~sQ37_spl),
% 5.51/1.17    inference(paramodulation,[status(thm)],[f901,f802])).
% 5.51/1.17  fof(f2514,definition,(
% 5.51/1.17    sQ228_spl <=> (segmentP(app(sK47_skl,nil),sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2517,plain,(
% 5.51/1.17    ~sQ5_spl|sQ228_spl|~sQ11_spl|~sQ37_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2511,f491,f2514,f529,f798])).
% 5.51/1.17  fof(f2518,definition,(
% 5.51/1.17    sQ229_spl <=> (segmentP(app(sK47_skl,sK5_skl(sK47_skl,sK48_skl)),sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2519,plain,(
% 5.51/1.17    segmentP(app(sK47_skl,sK5_skl(sK47_skl,sK48_skl)),sK47_skl)|~sQ229_spl),
% 5.51/1.17    inference(component_clause,[status(thm)],[f2518])).
% 5.51/1.17  fof(f2521,plain,(
% 5.51/1.17    ~sQ8_spl|sQ229_spl|~sQ29_spl|~sQ37_spl|~sQ26_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2512,f501,f2518,f706,f798,f663])).
% 5.51/1.17  fof(f2522,definition,(
% 5.51/1.17    sQ230_spl <=> (segmentP(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),sK47_skl))),
% 5.51/1.17    introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition])).
% 5.51/1.17  fof(f2525,plain,(
% 5.51/1.17    ~sQ5_spl|sQ230_spl|~sQ66_spl|~sQ37_spl),
% 5.51/1.17    inference(split_clause,[status(thm)],[f2513,f491,f2522,f1014,f798])).
% 5.51/1.17  fof(f2528,plain,(
% 5.51/1.17    segmentP(sK48_skl,sK47_skl)|~sQ26_spl|~sQ229_spl),
% 5.51/1.17    inference(forward_demodulation,[status(thm)],[f664,f2519])).
% 5.51/1.17  fof(f2529,plain,(
% 5.51/1.17    $false|sQ7_spl|~sQ26_spl|~sQ229_spl),
% 5.51/1.17    inference(forward_subsumption_resolution,[status(thm)],[f2528,f499])).
% 5.51/1.17  fof(f2530,plain,(
% 5.51/1.17    sQ7_spl|~sQ26_spl|~sQ229_spl),
% 5.51/1.17    inference(contradiction_clause,[status(thm)],[f2529])).
% 5.51/1.18  fof(f2531,plain,(
% 5.51/1.18    $false),
% 5.51/1.18    inference(sat_refutation,[status(thm)],[f440,f447,f451,f500,f512,f520,f542,f544,f546,f575,f584,f606,f616,f657,f666,f718,f721,f746,f753,f757,f770,f786,f790,f797,f801,f808,f812,f821,f825,f878,f892,f894,f913,f917,f924,f928,f940,f946,f956,f962,f966,f986,f993,f997,f1021,f1026,f1034,f1042,f1046,f1129,f1133,f1156,f1160,f1164,f1170,f1179,f1188,f1253,f1313,f1317,f1329,f1333,f1391,f1395,f1400,f1405,f1409,f1414,f1423,f1436,f1443,f1448,f1452,f1461,f1473,f1501,f1505,f1509,f1513,f1517,f1521,f1529,f1541,f1658,f1709,f1713,f1717,f1721,f1725,f1729,f1737,f1749,f1773,f1777,f1781,f1785,f1789,f1793,f1801,f1813,f1944,f1964,f1968,f1980,f1988,f1992,f2103,f2107,f2118,f2122,f2126,f2130,f2134,f2138,f2250,f2256,f2419,f2496,f2517,f2521,f2525,f2530])).
% 5.51/1.18  % SZS output end CNFRefutation for theBenchmark.p
% 5.51/1.18  % Elapsed time: 0.816890 seconds
% 5.51/1.18  % CPU time: 6.112392 seconds
% 5.51/1.18  % Total memory used: 183.625 MB
% 5.51/1.18  % Net memory used: 178.397 MB
%------------------------------------------------------------------------------