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

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SWC109+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 : n011.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 02:41:36 PM UTC 2026

% Result   : Theorem 10.14s 1.76s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWC109+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.10/0.36  % Computer : n011.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Mon Sep 21 07:55:56 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.38  % Drodi V4.1.1
% 10.14/1.76  % Refutation found
% 10.14/1.76  % SZS status Theorem for theBenchmark: Theorem is valid
% 10.14/1.76  % SZS output start CNFRefutation for theBenchmark
% 10.14/1.76  fof(f1,axiom,(
% 10.14/1.76    (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f2,axiom,(
% 10.14/1.76    (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f4,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f5,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f6,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f7,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f8,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( cyclefreeP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ~ ( leq(V,W)& leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f9,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( totalorderP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ( leq(V,W)| leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f10,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( strictorderP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> ( lt(V,W)| lt(W,V) ) ) ) )) )) )) )) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f11,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( totalorderedP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> leq(V,W) ) ) )) )) )) )) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f12,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( strictorderedP(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) ) ) )) )) )) )) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f13,axiom,(
% 10.14/1.76    (! [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 ) ) )) )) )) )) )) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f15,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f16,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f17,axiom,(
% 10.14/1.76    ssList(nil) ),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f18,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> cons(V,U) != U ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f21,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> nil != cons(V,U) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f26,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f28,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f36,axiom,(
% 10.14/1.76    (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f38,axiom,(
% 10.14/1.76    (! [U] :( ssItem(U)=> ~ memberP(nil,U) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f40,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( frontsegP(U,V)& frontsegP(V,W) )=> frontsegP(U,W) ) ) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f41,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( frontsegP(U,V)& frontsegP(V,U) )=> U = V ) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f43,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( frontsegP(U,V)=> frontsegP(app(U,W),V) ) ) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f44,axiom,(
% 10.14/1.76    (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( frontsegP(cons(U,W),cons(V,X))<=> ( U = V& frontsegP(W,X) ) ) ) )) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f45,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f46,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( frontsegP(nil,U)<=> nil = U ) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f47,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( rearsegP(U,V)& rearsegP(V,W) )=> rearsegP(U,W) ) ) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f48,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( rearsegP(U,V)& rearsegP(V,U) )=> U = V ) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f50,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( rearsegP(U,V)=> rearsegP(app(W,U),V) ) ) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f51,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f52,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( rearsegP(nil,U)<=> nil = U ) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f53,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( ( segmentP(U,V)& segmentP(V,W) )=> segmentP(U,W) ) ) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f54,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( segmentP(U,V)& segmentP(V,U) )=> U = V ) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f56,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( segmentP(U,V)=> segmentP(app(app(W,U),X),V) ) ) )) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f57,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f58,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> ( segmentP(nil,U)<=> nil = U ) ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f83,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( nil = app(U,V)<=> ( nil = V& nil = U ) ) ) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f84,axiom,(
% 10.14/1.76    (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f96,conjecture,(
% 10.14/1.76    (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ( (! [Y] :( ssItem(Y)=> (! [Z] :( ssList(Z)=> (! [X1] :( ~ ssList(X1)| cons(Y,nil) != W| app(app(Z,W),X1) != X| (? [X2] :( ssItem(X2)& memberP(Z,X2)& lt(Y,X2) ))| (? [X3] :( ssItem(X3)& memberP(X1,X3)& lt(X3,Y) ) )) )) )))& ( nil != X| nil != W ) )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| ( neq(U,nil)& segmentP(V,U) ) ) ) ) )) )) )) )),
% 10.14/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.14/1.76  fof(f97,negated_conjecture,(
% 10.14/1.76    ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ( (! [Y] :( ssItem(Y)=> (! [Z] :( ssList(Z)=> (! [X1] :( ~ ssList(X1)| cons(Y,nil) != W| app(app(Z,W),X1) != X| (? [X2] :( ssItem(X2)& memberP(Z,X2)& lt(Y,X2) ))| (? [X3] :( ssItem(X3)& memberP(X1,X3)& lt(X3,Y) ) )) )) )))& ( nil != X| nil != W ) )| ( ( nil != V| nil = U )& ( ~ neq(V,nil)| ( neq(U,nil)& segmentP(V,U) ) ) ) ) )) )) )) ))),
% 10.14/1.76    inference(negated_conjecture,[status(cth)],[f96])).
% 10.14/1.76  fof(f98,plain,(
% 10.14/1.76    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(neq(U,V)<=>~U=V))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f1])).
% 10.14/1.76  fof(f99,plain,(
% 10.14/1.76    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f98])).
% 10.14/1.76  fof(f100,plain,(
% 10.14/1.76    ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~neq(X0,X1)|~X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f99])).
% 10.14/1.76  fof(f101,plain,(
% 10.14/1.76    ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|neq(X0,X1)|X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f99])).
% 10.14/1.76  fof(f102,plain,(
% 10.14/1.76    (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 10.14/1.76  fof(f103,plain,(
% 10.14/1.76    ssItem(sK0_skl)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f102])).
% 10.14/1.76  fof(f104,plain,(
% 10.14/1.76    ssItem(sK1_skl)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f102])).
% 10.14/1.76  fof(f105,plain,(
% 10.14/1.76    ~sK0_skl=sK1_skl),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f102])).
% 10.14/1.76  fof(f113,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f4])).
% 10.14/1.76  fof(f114,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f113])).
% 10.14/1.76  fof(f115,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~singletonP(U)|(ssItem(sK4_skl(U))&cons(sK4_skl(U),nil)=U))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 10.14/1.76  fof(f118,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|singletonP(X0)|~ssItem(X1)|~cons(X1,nil)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f115])).
% 10.14/1.76  fof(f119,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f5])).
% 10.14/1.76  fof(f120,plain,(
% 10.14/1.76    ![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)))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f119])).
% 10.14/1.76  fof(f121,plain,(
% 10.14/1.76    ![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)))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 10.14/1.76  fof(f122,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f121])).
% 10.14/1.76  fof(f123,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f121])).
% 10.14/1.76  fof(f124,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f121])).
% 10.14/1.76  fof(f125,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f6])).
% 10.14/1.76  fof(f126,plain,(
% 10.14/1.76    ![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)))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f125])).
% 10.14/1.76  fof(f127,plain,(
% 10.14/1.76    ![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)))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 10.14/1.76  fof(f128,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f127])).
% 10.14/1.76  fof(f129,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f127])).
% 10.14/1.76  fof(f130,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f127])).
% 10.14/1.76  fof(f131,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f7])).
% 10.14/1.76  fof(f132,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U)))))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f131])).
% 10.14/1.76  fof(f133,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(ssList(sK7_skl(V,U))&(ssList(sK8_skl(V,U))&app(app(sK7_skl(V,U),V),sK8_skl(V,U))=U)))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 10.14/1.76  fof(f134,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f133])).
% 10.14/1.76  fof(f135,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f133])).
% 10.14/1.76  fof(f136,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f133])).
% 10.14/1.76  fof(f137,plain,(
% 10.14/1.76    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f133])).
% 10.14/1.76  fof(f138,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(cyclefreeP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V)))))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f8])).
% 10.14/1.76  fof(f139,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(leq(V,W)&leq(W,V))))))))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f138])).
% 10.14/1.76  fof(f140,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~cyclefreeP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(~leq(V,W)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(ssItem(sK9_skl(U))&(ssItem(sK10_skl(U))&(ssList(sK11_skl(U))&(ssList(sK12_skl(U))&(ssList(sK13_skl(U))&(app(app(sK11_skl(U),cons(sK9_skl(U),sK12_skl(U))),cons(sK10_skl(U),sK13_skl(U)))=U&(leq(sK9_skl(U),sK10_skl(U))&leq(sK10_skl(U),sK9_skl(U))))))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(V,sK9_skl(U)),skolemize(W,sK10_skl(U)),skolemize(X,sK11_skl(U)),skolemize(Y,sK12_skl(U)),skolemize(Z,sK13_skl(U))],[f139])).
% 10.14/1.76  fof(f147,plain,(
% 10.14/1.76    ![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)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f140])).
% 10.14/1.76  fof(f150,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(totalorderP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(leq(V,W)|leq(W,V)))))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f9])).
% 10.14/1.76  fof(f151,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~totalorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(leq(V,W)|leq(W,V))))))))))))))&(totalorderP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(~leq(V,W)&~leq(W,V))))))))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f150])).
% 10.14/1.76  fof(f152,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~totalorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(leq(V,W)|leq(W,V))))))))))))))&(totalorderP(U)|(ssItem(sK14_skl(U))&(ssItem(sK15_skl(U))&(ssList(sK16_skl(U))&(ssList(sK17_skl(U))&(ssList(sK18_skl(U))&(app(app(sK16_skl(U),cons(sK14_skl(U),sK17_skl(U))),cons(sK15_skl(U),sK18_skl(U)))=U&(~leq(sK14_skl(U),sK15_skl(U))&~leq(sK15_skl(U),sK14_skl(U))))))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(V,sK14_skl(U)),skolemize(W,sK15_skl(U)),skolemize(X,sK16_skl(U)),skolemize(Y,sK17_skl(U)),skolemize(Z,sK18_skl(U))],[f151])).
% 10.14/1.76  fof(f159,plain,(
% 10.14/1.76    ![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)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f152])).
% 10.14/1.76  fof(f162,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(strictorderP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(lt(V,W)|lt(W,V)))))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f10])).
% 10.14/1.76  fof(f163,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~strictorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(lt(V,W)|lt(W,V))))))))))))))&(strictorderP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&(~lt(V,W)&~lt(W,V))))))))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f162])).
% 10.14/1.76  fof(f164,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~strictorderP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|(lt(V,W)|lt(W,V))))))))))))))&(strictorderP(U)|(ssItem(sK19_skl(U))&(ssItem(sK20_skl(U))&(ssList(sK21_skl(U))&(ssList(sK22_skl(U))&(ssList(sK23_skl(U))&(app(app(sK21_skl(U),cons(sK19_skl(U),sK22_skl(U))),cons(sK20_skl(U),sK23_skl(U)))=U&(~lt(sK19_skl(U),sK20_skl(U))&~lt(sK20_skl(U),sK19_skl(U))))))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl]),skolemize(V,sK19_skl(U)),skolemize(W,sK20_skl(U)),skolemize(X,sK21_skl(U)),skolemize(Y,sK22_skl(U)),skolemize(Z,sK23_skl(U))],[f163])).
% 10.14/1.76  fof(f171,plain,(
% 10.14/1.76    ![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)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f164])).
% 10.14/1.76  fof(f174,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(totalorderedP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W))))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f11])).
% 10.14/1.76  fof(f175,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~totalorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W)))))))))))))&(totalorderedP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&~leq(V,W)))))))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f174])).
% 10.14/1.76  fof(f176,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~totalorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W)))))))))))))&(totalorderedP(U)|(ssItem(sK24_skl(U))&(ssItem(sK25_skl(U))&(ssList(sK26_skl(U))&(ssList(sK27_skl(U))&(ssList(sK28_skl(U))&(app(app(sK26_skl(U),cons(sK24_skl(U),sK27_skl(U))),cons(sK25_skl(U),sK28_skl(U)))=U&~leq(sK24_skl(U),sK25_skl(U)))))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(V,sK24_skl(U)),skolemize(W,sK25_skl(U)),skolemize(X,sK26_skl(U)),skolemize(Y,sK27_skl(U)),skolemize(Z,sK28_skl(U))],[f175])).
% 10.14/1.76  fof(f183,plain,(
% 10.14/1.76    ![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)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f176])).
% 10.14/1.76  fof(f185,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(strictorderedP(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))))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f12])).
% 10.14/1.76  fof(f186,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~strictorderedP(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)))))))))))))&(strictorderedP(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)))))))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f185])).
% 10.14/1.76  fof(f187,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~strictorderedP(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)))))))))))))&(strictorderedP(U)|(ssItem(sK29_skl(U))&(ssItem(sK30_skl(U))&(ssList(sK31_skl(U))&(ssList(sK32_skl(U))&(ssList(sK33_skl(U))&(app(app(sK31_skl(U),cons(sK29_skl(U),sK32_skl(U))),cons(sK30_skl(U),sK33_skl(U)))=U&~lt(sK29_skl(U),sK30_skl(U)))))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl]),skolemize(V,sK29_skl(U)),skolemize(W,sK30_skl(U)),skolemize(X,sK31_skl(U)),skolemize(Y,sK32_skl(U)),skolemize(Z,sK33_skl(U))],[f186])).
% 10.14/1.76  fof(f194,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|strictorderedP(X0)|app(app(sK31_skl(X0),cons(sK29_skl(X0),sK32_skl(X0))),cons(sK30_skl(X0),sK33_skl(X0)))=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f187])).
% 10.14/1.76  fof(f196,plain,(
% 10.14/1.76    ![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)))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f13])).
% 10.14/1.76  fof(f197,plain,(
% 10.14/1.76    ![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))))))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f196])).
% 10.14/1.76  fof(f198,plain,(
% 10.14/1.76    ![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))))))))))),
% 10.14/1.76    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])).
% 10.14/1.76  fof(f205,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|duplicatefreeP(X0)|app(app(sK36_skl(X0),cons(sK34_skl(X0),sK37_skl(X0))),cons(sK35_skl(X0),sK38_skl(X0)))=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f198])).
% 10.14/1.76  fof(f206,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|duplicatefreeP(X0)|sK34_skl(X0)=sK35_skl(X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f198])).
% 10.14/1.76  fof(f217,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f15])).
% 10.14/1.76  fof(f218,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f217])).
% 10.14/1.76  fof(f219,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f218])).
% 10.14/1.76  fof(f220,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X0,X1)|X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f218])).
% 10.14/1.76  fof(f221,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f16])).
% 10.14/1.76  fof(f222,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f221])).
% 10.14/1.76  fof(f223,plain,(
% 10.14/1.76    ssList(nil)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f17])).
% 10.14/1.76  fof(f224,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssItem(V)|~cons(V,U)=U)))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f18])).
% 10.14/1.76  fof(f225,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~cons(X1,X0)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f224])).
% 10.14/1.76  fof(f234,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssItem(V)|~nil=cons(V,U))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f21])).
% 10.14/1.76  fof(f235,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~nil=cons(X1,X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f234])).
% 10.14/1.76  fof(f244,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f26])).
% 10.14/1.76  fof(f245,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f244])).
% 10.14/1.76  fof(f248,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|app(nil,U)=U)),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f28])).
% 10.14/1.76  fof(f249,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f248])).
% 10.14/1.76  fof(f268,plain,(
% 10.14/1.76    ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f36])).
% 10.14/1.76  fof(f269,plain,(
% 10.14/1.76    ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~memberP(app(V,W),U)|(memberP(V,U)|memberP(W,U)))&(memberP(app(V,W),U)|(~memberP(V,U)&~memberP(W,U)))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f268])).
% 10.14/1.76  fof(f270,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~memberP(app(X1,X2),X0)|memberP(X1,X0)|memberP(X2,X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f269])).
% 10.14/1.76  fof(f278,plain,(
% 10.14/1.76    ![U]: (~ssItem(U)|~memberP(nil,U))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f38])).
% 10.14/1.76  fof(f279,plain,(
% 10.14/1.76    ![X0]: (~ssItem(X0)|~memberP(nil,X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f278])).
% 10.14/1.76  fof(f281,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~frontsegP(U,V)|~frontsegP(V,W))|frontsegP(U,W)))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f40])).
% 10.14/1.76  fof(f282,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|~frontsegP(X1,X2)|frontsegP(X0,X2))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f281])).
% 10.14/1.76  fof(f283,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|~frontsegP(V,U))|U=V))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f41])).
% 10.14/1.76  fof(f284,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|~frontsegP(X1,X0)|X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f283])).
% 10.14/1.76  fof(f287,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~frontsegP(U,V)|frontsegP(app(U,W),V)))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f43])).
% 10.14/1.76  fof(f288,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~frontsegP(X0,X1)|frontsegP(app(X0,X2),X1))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f287])).
% 10.14/1.76  fof(f289,plain,(
% 10.14/1.76    ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|(frontsegP(cons(U,W),cons(V,X))<=>(U=V&frontsegP(W,X))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f44])).
% 10.14/1.76  fof(f290,plain,(
% 10.14/1.76    ![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)))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f289])).
% 10.14/1.76  fof(f293,plain,(
% 10.14/1.76    ![X0,X1,X2,X3]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|frontsegP(cons(X0,X2),cons(X1,X3))|~X0=X1|~frontsegP(X2,X3))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f290])).
% 10.14/1.76  fof(f294,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|frontsegP(U,nil))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f45])).
% 10.14/1.76  fof(f295,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f294])).
% 10.14/1.76  fof(f296,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(frontsegP(nil,U)<=>nil=U))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f46])).
% 10.14/1.76  fof(f297,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~frontsegP(nil,U)|nil=U)&(frontsegP(nil,U)|~nil=U)))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f296])).
% 10.14/1.76  fof(f298,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|nil=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f297])).
% 10.14/1.76  fof(f300,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~rearsegP(U,V)|~rearsegP(V,W))|rearsegP(U,W)))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f47])).
% 10.14/1.76  fof(f301,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~rearsegP(X0,X1)|~rearsegP(X1,X2)|rearsegP(X0,X2))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f300])).
% 10.14/1.76  fof(f302,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|~rearsegP(V,U))|U=V))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f48])).
% 10.14/1.76  fof(f303,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|~rearsegP(X1,X0)|X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f302])).
% 10.14/1.76  fof(f306,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~rearsegP(U,V)|rearsegP(app(W,U),V)))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f50])).
% 10.14/1.76  fof(f307,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~rearsegP(X0,X1)|rearsegP(app(X2,X0),X1))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f306])).
% 10.14/1.76  fof(f308,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|rearsegP(U,nil))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f51])).
% 10.14/1.76  fof(f309,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f308])).
% 10.14/1.76  fof(f310,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(rearsegP(nil,U)<=>nil=U))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f52])).
% 10.14/1.76  fof(f311,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~rearsegP(nil,U)|nil=U)&(rearsegP(nil,U)|~nil=U)))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f310])).
% 10.14/1.76  fof(f312,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|~rearsegP(nil,X0)|nil=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f311])).
% 10.14/1.76  fof(f314,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~segmentP(U,V)|~segmentP(V,W))|segmentP(U,W)))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f53])).
% 10.14/1.76  fof(f315,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(X0,X1)|~segmentP(X1,X2)|segmentP(X0,X2))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f314])).
% 10.14/1.76  fof(f316,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|~segmentP(V,U))|U=V))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f54])).
% 10.14/1.76  fof(f317,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|~segmentP(X1,X0)|X0=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f316])).
% 10.14/1.76  fof(f320,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|(~segmentP(U,V)|segmentP(app(app(W,U),X),V)))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f56])).
% 10.14/1.76  fof(f321,plain,(
% 10.14/1.76    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X0,X1)|segmentP(app(app(X2,X0),X3),X1))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f320])).
% 10.14/1.76  fof(f322,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|segmentP(U,nil))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f57])).
% 10.14/1.76  fof(f323,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f322])).
% 10.14/1.76  fof(f324,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(segmentP(nil,U)<=>nil=U))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f58])).
% 10.14/1.76  fof(f325,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|((~segmentP(nil,U)|nil=U)&(segmentP(nil,U)|~nil=U)))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f324])).
% 10.14/1.76  fof(f326,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|~segmentP(nil,X0)|nil=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f325])).
% 10.14/1.76  fof(f383,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|(nil=app(U,V)<=>(nil=V&nil=U)))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f83])).
% 10.14/1.76  fof(f384,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~nil=app(U,V)|(nil=V&nil=U))&(nil=app(U,V)|(~nil=V|~nil=U))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f383])).
% 10.14/1.76  fof(f385,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~nil=app(X0,X1)|nil=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f384])).
% 10.14/1.76  fof(f388,plain,(
% 10.14/1.76    ![U]: (~ssList(U)|app(U,nil)=U)),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f84])).
% 10.14/1.76  fof(f389,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f388])).
% 10.14/1.76  fof(f415,plain,(
% 10.14/1.76    (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((ssList(X)&V=X)&U=W)&((?[Y]: (ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: ((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2))))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))|(nil=X&nil=W)))&((nil=V&~nil=U)|(neq(V,nil)&(~neq(U,nil)|~segmentP(V,U))))))))))))),
% 10.14/1.76    inference(pre_NNF_transformation,[status(thm)],[f97])).
% 10.14/1.76  fof(f416,definition,(
% 10.14/1.76    ![W,X,Y]: (sP0_prd(Y,X,W)<=>(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: ((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2))))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 10.14/1.76  fof(f417,definition,(
% 10.14/1.76    ![U,V]: (sP1_prd(V,U)<=>(nil=V&~nil=U))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 10.14/1.76  fof(f418,plain,(
% 10.14/1.76    ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((ssList(X)&V=X)&U=W)&((?[Y]: sP0_prd(Y,X,W))|(nil=X&nil=W)))&(sP1_prd(V,U)|(neq(V,nil)&(~neq(U,nil)|~segmentP(V,U)))))))))))),
% 10.14/1.76    inference(formula_renaming,[status(thm)],[f415,f417,f416])).
% 10.14/1.76  fof(f419,plain,(
% 10.14/1.76    ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&((?[X]: (((ssList(X)&V=X)&U=W)&((?[Y]: sP0_prd(Y,X,W))|(nil=X&nil=W))))&(sP1_prd(V,U)|(neq(V,nil)&(~neq(U,nil)|~segmentP(V,U))))))))))),
% 10.14/1.76    inference(miniscoping,[status(thm)],[f418])).
% 10.14/1.76  fof(f420,plain,(
% 10.14/1.76    (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&(sP0_prd(sK51_skl,sK50_skl,sK49_skl)|(nil=sK50_skl&nil=sK49_skl)))&(sP1_prd(sK48_skl,sK47_skl)|(neq(sK48_skl,nil)&(~neq(sK47_skl,nil)|~segmentP(sK48_skl,sK47_skl))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl)],[f419])).
% 10.14/1.76  fof(f423,plain,(
% 10.14/1.76    ssList(sK49_skl)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f424,plain,(
% 10.14/1.76    ssList(sK50_skl)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f425,plain,(
% 10.14/1.76    sK48_skl=sK50_skl),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f426,plain,(
% 10.14/1.76    sK47_skl=sK49_skl),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f427,plain,(
% 10.14/1.76    sP0_prd(sK51_skl,sK50_skl,sK49_skl)|nil=sK50_skl),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f428,plain,(
% 10.14/1.76    sP0_prd(sK51_skl,sK50_skl,sK49_skl)|nil=sK49_skl),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f429,plain,(
% 10.14/1.76    sP1_prd(sK48_skl,sK47_skl)|neq(sK48_skl,nil)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f430,plain,(
% 10.14/1.76    sP1_prd(sK48_skl,sK47_skl)|~neq(sK47_skl,nil)|~segmentP(sK48_skl,sK47_skl)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f420])).
% 10.14/1.76  fof(f431,definition,(
% 10.14/1.76    ![Y,Z,X2]: (sP2_prd(X2,Z,Y)<=>((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2)))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 10.14/1.76  fof(f432,plain,(
% 10.14/1.76    ![W,X,Y]: (sP0_prd(Y,X,W)<=>(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: sP2_prd(X2,Z,Y)))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))),
% 10.14/1.76    inference(formula_renaming,[status(thm)],[f416,f431])).
% 10.14/1.76  fof(f433,plain,(
% 10.14/1.76    ![W,X,Y]: ((~sP0_prd(Y,X,W)|(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: sP2_prd(X2,Z,Y)))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y)))))))))&(sP0_prd(Y,X,W)|(~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~cons(Y,nil)=W)|~app(app(Z,W),X1)=X)|(?[X2]: ~sP2_prd(X2,Z,Y)))|(?[X3]: ((ssItem(X3)&memberP(X1,X3))&lt(X3,Y))))))))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f432])).
% 10.14/1.76  fof(f434,plain,(
% 10.14/1.76    (![W,X,Y]: (~sP0_prd(Y,X,W)|(ssItem(Y)&(?[Z]: (ssList(Z)&(?[X1]: ((((ssList(X1)&cons(Y,nil)=W)&app(app(Z,W),X1)=X)&(![X2]: sP2_prd(X2,Z,Y)))&(![X3]: ((~ssItem(X3)|~memberP(X1,X3))|~lt(X3,Y))))))))))&(![W,X,Y]: (sP0_prd(Y,X,W)|(~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~cons(Y,nil)=W)|~app(app(Z,W),X1)=X)|(?[X2]: ~sP2_prd(X2,Z,Y)))|(?[X3]: ((ssItem(X3)&memberP(X1,X3))&lt(X3,Y))))))))))),
% 10.14/1.76    inference(miniscoping,[status(thm)],[f433])).
% 10.14/1.76  fof(f435,plain,(
% 10.14/1.76    (![W,X,Y]: (~sP0_prd(Y,X,W)|(ssItem(Y)&(ssList(sK52_skl(Y,X,W))&((((ssList(sK53_skl(Y,X,W))&cons(Y,nil)=W)&app(app(sK52_skl(Y,X,W),W),sK53_skl(Y,X,W))=X)&(![X2]: sP2_prd(X2,sK52_skl(Y,X,W),Y)))&(![X3]: ((~ssItem(X3)|~memberP(sK53_skl(Y,X,W),X3))|~lt(X3,Y))))))))&(![W,X,Y]: (sP0_prd(Y,X,W)|(~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~cons(Y,nil)=W)|~app(app(Z,W),X1)=X)|~sP2_prd(sK54_skl(X1,Z,Y,X,W),Z,Y))|((ssItem(sK55_skl(X1,Z,Y,X,W))&memberP(X1,sK55_skl(X1,Z,Y,X,W)))&lt(sK55_skl(X1,Z,Y,X,W),Y)))))))))),
% 10.14/1.76    inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl,sK53_skl,sK54_skl,sK55_skl]),skolemize(Z,sK52_skl(Y,X,W)),skolemize(X1,sK53_skl(Y,X,W)),skolemize(X2,sK54_skl(X1,Z,Y,X,W)),skolemize(X3,sK55_skl(X1,Z,Y,X,W))],[f434])).
% 10.14/1.76  fof(f436,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssItem(X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f437,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssList(sK52_skl(X0,X1,X2)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f438,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssList(sK53_skl(X0,X1,X2)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f439,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|cons(X0,nil)=X2)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f440,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|app(app(sK52_skl(X0,X1,X2),X2),sK53_skl(X0,X1,X2))=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f443,plain,(
% 10.14/1.76    ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2)|~ssItem(X0)|~ssList(X3)|~ssList(X4)|~cons(X0,nil)=X2|~app(app(X3,X2),X4)=X1|~sP2_prd(sK54_skl(X4,X3,X0,X1,X2),X3,X0)|ssItem(sK55_skl(X4,X3,X0,X1,X2)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f444,plain,(
% 10.14/1.76    ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2)|~ssItem(X0)|~ssList(X3)|~ssList(X4)|~cons(X0,nil)=X2|~app(app(X3,X2),X4)=X1|~sP2_prd(sK54_skl(X4,X3,X0,X1,X2),X3,X0)|memberP(X4,sK55_skl(X4,X3,X0,X1,X2)))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f435])).
% 10.14/1.76  fof(f446,plain,(
% 10.14/1.76    ![U,V]: ((~sP1_prd(V,U)|(nil=V&~nil=U))&(sP1_prd(V,U)|(~nil=V|nil=U)))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f417])).
% 10.14/1.76  fof(f447,plain,(
% 10.14/1.76    (![U,V]: (~sP1_prd(V,U)|(nil=V&~nil=U)))&(![U,V]: (sP1_prd(V,U)|(~nil=V|nil=U)))),
% 10.14/1.76    inference(miniscoping,[status(thm)],[f446])).
% 10.14/1.76  fof(f448,plain,(
% 10.14/1.76    ![X0,X1]: (~sP1_prd(X0,X1)|nil=X0)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f447])).
% 10.14/1.76  fof(f449,plain,(
% 10.14/1.76    ![X0,X1]: (~sP1_prd(X0,X1)|~nil=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f447])).
% 10.14/1.76  fof(f450,plain,(
% 10.14/1.76    ![X0,X1]: (sP1_prd(X0,X1)|~nil=X0|nil=X1)),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f447])).
% 10.14/1.76  fof(f451,plain,(
% 10.14/1.76    ![Y,Z,X2]: ((~sP2_prd(X2,Z,Y)|((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2)))&(sP2_prd(X2,Z,Y)|((ssItem(X2)&memberP(Z,X2))&lt(Y,X2))))),
% 10.14/1.76    inference(NNF_transformation,[status(thm)],[f431])).
% 10.14/1.76  fof(f452,plain,(
% 10.14/1.76    (![Y,Z,X2]: (~sP2_prd(X2,Z,Y)|((~ssItem(X2)|~memberP(Z,X2))|~lt(Y,X2))))&(![Y,Z,X2]: (sP2_prd(X2,Z,Y)|((ssItem(X2)&memberP(Z,X2))&lt(Y,X2))))),
% 10.14/1.76    inference(miniscoping,[status(thm)],[f451])).
% 10.14/1.76  fof(f454,plain,(
% 10.14/1.76    ![X0,X1,X2]: (sP2_prd(X0,X1,X2)|ssItem(X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f452])).
% 10.14/1.76  fof(f455,plain,(
% 10.14/1.76    ![X0,X1,X2]: (sP2_prd(X0,X1,X2)|memberP(X1,X0))),
% 10.14/1.76    inference(cnf_transformation,[status(thm)],[f452])).
% 10.14/1.76  fof(f457,definition,(
% 10.14/1.76    sQ0_spl <=> (sP0_prd(sK51_skl,sK50_skl,sK49_skl))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f458,plain,(
% 10.14/1.76    sP0_prd(sK51_skl,sK50_skl,sK49_skl)|~sQ0_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f457])).
% 10.14/1.76  fof(f460,definition,(
% 10.14/1.76    sQ1_spl <=> (nil=sK50_skl)),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f461,plain,(
% 10.14/1.76    nil=sK50_skl|~sQ1_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f460])).
% 10.14/1.76  fof(f463,plain,(
% 10.14/1.76    sQ0_spl|sQ1_spl),
% 10.14/1.76    inference(split_clause,[status(thm)],[f427,f457,f460])).
% 10.14/1.76  fof(f464,definition,(
% 10.14/1.76    sQ2_spl <=> (nil=sK49_skl)),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f465,plain,(
% 10.14/1.76    nil=sK49_skl|~sQ2_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f464])).
% 10.14/1.76  fof(f467,plain,(
% 10.14/1.76    sQ0_spl|sQ2_spl),
% 10.14/1.76    inference(split_clause,[status(thm)],[f428,f457,f464])).
% 10.14/1.76  fof(f468,definition,(
% 10.14/1.76    sQ3_spl <=> (sP1_prd(sK48_skl,sK47_skl))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f469,plain,(
% 10.14/1.76    sP1_prd(sK48_skl,sK47_skl)|~sQ3_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f468])).
% 10.14/1.76  fof(f471,definition,(
% 10.14/1.76    sQ4_spl <=> (neq(sK48_skl,nil))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f472,plain,(
% 10.14/1.76    neq(sK48_skl,nil)|~sQ4_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f471])).
% 10.14/1.76  fof(f474,plain,(
% 10.14/1.76    sQ3_spl|sQ4_spl),
% 10.14/1.76    inference(split_clause,[status(thm)],[f429,f468,f471])).
% 10.14/1.76  fof(f475,definition,(
% 10.14/1.76    sQ5_spl <=> (neq(sK47_skl,nil))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f477,plain,(
% 10.14/1.76    ~neq(sK47_skl,nil)|sQ5_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f475])).
% 10.14/1.76  fof(f478,definition,(
% 10.14/1.76    sQ6_spl <=> (segmentP(sK48_skl,sK47_skl))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f480,plain,(
% 10.14/1.76    ~segmentP(sK48_skl,sK47_skl)|sQ6_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f478])).
% 10.14/1.76  fof(f481,plain,(
% 10.14/1.76    sQ3_spl|~sQ5_spl|~sQ6_spl),
% 10.14/1.76    inference(split_clause,[status(thm)],[f430,f468,f475,f478])).
% 10.14/1.76  fof(f482,plain,(
% 10.14/1.76    ![X1]: (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f100])).
% 10.14/1.76  fof(f483,plain,(
% 10.14/1.76    ![X0]: (~ssItem(X0)|~neq(X0,X0))),
% 10.14/1.76    inference(duplicate_literals_removal,[status(thm)],[f482])).
% 10.14/1.76  fof(f485,plain,(
% 10.14/1.76    ![X0]: (~ssList(cons(X0,nil))|singletonP(cons(X0,nil))|~ssItem(X0))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f118])).
% 10.14/1.76  fof(f486,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f124])).
% 10.14/1.76  fof(f487,plain,(
% 10.14/1.76    ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f130])).
% 10.14/1.76  fof(f488,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f137])).
% 10.14/1.76  fof(f497,plain,(
% 10.14/1.76    ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f219])).
% 10.14/1.76  fof(f498,plain,(
% 10.14/1.76    ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 10.14/1.76    inference(duplicate_literals_removal,[status(thm)],[f497])).
% 10.14/1.76  fof(f501,plain,(
% 10.14/1.76    ![X1,X2,X3]: (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|frontsegP(cons(X1,X2),cons(X1,X3))|~frontsegP(X2,X3))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f293])).
% 10.14/1.76  fof(f502,plain,(
% 10.14/1.76    ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|frontsegP(cons(X0,X1),cons(X0,X2))|~frontsegP(X1,X2))),
% 10.14/1.76    inference(duplicate_literals_removal,[status(thm)],[f501])).
% 10.14/1.76  fof(f512,plain,(
% 10.14/1.76    ![X0,X1,X2]: (sP0_prd(X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|~ssList(X2)|~sP2_prd(sK54_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil)),X1,X0)|ssItem(sK55_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f443])).
% 10.14/1.76  fof(f513,plain,(
% 10.14/1.76    ![X0,X1,X2]: (sP0_prd(X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|~ssList(X2)|~sP2_prd(sK54_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil)),X1,X0)|memberP(X2,sK55_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f444])).
% 10.14/1.76  fof(f515,plain,(
% 10.14/1.76    ![X0]: (~sP1_prd(X0,nil))),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f449])).
% 10.14/1.76  fof(f516,plain,(
% 10.14/1.76    ![X0]: (sP1_prd(nil,X0)|nil=X0)),
% 10.14/1.76    inference(destructive_equality_resolution,[status(thm)],[f450])).
% 10.14/1.76  fof(f519,plain,(
% 10.14/1.76    sP1_prd(sK50_skl,sK47_skl)|~sQ3_spl),
% 10.14/1.76    inference(forward_demodulation,[status(thm)],[f425,f469])).
% 10.14/1.76  fof(f520,plain,(
% 10.14/1.76    sP1_prd(sK50_skl,sK49_skl)|~sQ3_spl),
% 10.14/1.76    inference(forward_demodulation,[status(thm)],[f426,f519])).
% 10.14/1.76  fof(f521,plain,(
% 10.14/1.76    ![X0]: (~ssItem(X0)|neq(X0,sK0_skl)|X0=sK0_skl)),
% 10.14/1.76    inference(resolution,[status(thm)],[f103,f101])).
% 10.14/1.76  fof(f522,plain,(
% 10.14/1.76    ~neq(sK0_skl,sK0_skl)),
% 10.14/1.76    inference(resolution,[status(thm)],[f103,f483])).
% 10.14/1.76  fof(f523,plain,(
% 10.14/1.76    ![X0]: (~ssItem(X0)|neq(X0,sK1_skl)|X0=sK1_skl)),
% 10.14/1.76    inference(resolution,[status(thm)],[f104,f101])).
% 10.14/1.76  fof(f524,plain,(
% 10.14/1.76    ~neq(sK1_skl,sK1_skl)),
% 10.14/1.76    inference(resolution,[status(thm)],[f104,f483])).
% 10.14/1.76  fof(f525,plain,(
% 10.14/1.76    nil=sK50_skl|~sQ3_spl),
% 10.14/1.76    inference(resolution,[status(thm)],[f448,f520])).
% 10.14/1.76  fof(f526,plain,(
% 10.14/1.76    sP1_prd(nil,sK49_skl)|~sQ3_spl),
% 10.14/1.76    inference(backward_demodulation,[status(thm)],[f525,f520])).
% 10.14/1.76  fof(f536,definition,(
% 10.14/1.76    sQ8_spl <=> (sK1_skl=sK1_skl)),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f543,definition,(
% 10.14/1.76    sQ10_spl <=> (sK0_skl=sK0_skl)),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f548,plain,(
% 10.14/1.76    ![X0]: (nil=X0|nil=nil)),
% 10.14/1.76    inference(resolution,[status(thm)],[f516,f448])).
% 10.14/1.76  fof(f549,definition,(
% 10.14/1.76    ![X0]: (sQ11_spl <=> (nil=X0))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f550,plain,(
% 10.14/1.76    ![X0]: (nil=X0|~sQ11_spl)),
% 10.14/1.76    inference(component_clause,[status(thm)],[f549])).
% 10.14/1.76  fof(f552,definition,(
% 10.14/1.76    sQ12_spl <=> (nil=nil)),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f555,plain,(
% 10.14/1.76    sQ11_spl|sQ12_spl),
% 10.14/1.76    inference(split_clause,[status(thm)],[f548,f549,f552])).
% 10.14/1.76  fof(f556,plain,(
% 10.14/1.76    ![X0,X1]: (X0=X1|~sQ11_spl)),
% 10.14/1.76    inference(paramodulation,[status(thm)],[f550,f550])).
% 10.14/1.76  fof(f569,plain,(
% 10.14/1.76    $false|~sQ11_spl),
% 10.14/1.76    inference(backward_subsumption_resolution,[status(thm)],[f105,f556])).
% 10.14/1.76  fof(f570,plain,(
% 10.14/1.76    ~sQ11_spl),
% 10.14/1.76    inference(contradiction_clause,[status(thm)],[f569])).
% 10.14/1.76  fof(f572,plain,(
% 10.14/1.76    ![X0]: (~ssList(nil)|~ssItem(X0)|singletonP(cons(X0,nil))|~ssItem(X0))),
% 10.14/1.76    inference(resolution,[status(thm)],[f222,f485])).
% 10.14/1.76  fof(f573,definition,(
% 10.14/1.76    sQ13_spl <=> (ssList(nil))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f575,plain,(
% 10.14/1.76    ~ssList(nil)|sQ13_spl),
% 10.14/1.76    inference(component_clause,[status(thm)],[f573])).
% 10.14/1.76  fof(f576,definition,(
% 10.14/1.76    ![X0]: (sQ14_spl <=> (~ssItem(X0)|singletonP(cons(X0,nil))|~ssItem(X0)))),
% 10.14/1.76    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 10.14/1.76  fof(f579,plain,(
% 10.14/1.76    ~sQ13_spl|sQ14_spl),
% 10.14/1.76    inference(split_clause,[status(thm)],[f572,f573,f576])).
% 10.14/1.77  fof(f580,plain,(
% 10.14/1.77    $false|sQ13_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f575,f223])).
% 10.14/1.77  fof(f581,plain,(
% 10.14/1.77    sQ13_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f580])).
% 10.14/1.77  fof(f583,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~cons(sK1_skl,X0)=X0)),
% 10.14/1.77    inference(resolution,[status(thm)],[f225,f104])).
% 10.14/1.77  fof(f596,plain,(
% 10.14/1.77    app(nil,nil)=nil),
% 10.14/1.77    inference(resolution,[status(thm)],[f249,f223])).
% 10.14/1.77  fof(f597,plain,(
% 10.14/1.77    app(nil,sK49_skl)=sK49_skl),
% 10.14/1.77    inference(resolution,[status(thm)],[f249,f423])).
% 10.14/1.77  fof(f598,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(nil,sK5_skl(X1,X0))=sK5_skl(X1,X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f122,f249])).
% 10.14/1.77  fof(f599,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f123,f295])).
% 10.14/1.77  fof(f601,definition,(
% 10.14/1.77    ![X0]: (sQ15_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f604,plain,(
% 10.14/1.77    sQ15_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f599,f601,f573])).
% 10.14/1.77  fof(f607,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|frontsegP(app(nil,sK49_skl),nil)|~ssList(sK49_skl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f597,f486])).
% 10.14/1.77  fof(f608,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(sK49_skl)|segmentP(app(app(nil,sK49_skl),X0),sK49_skl)|~ssList(nil)|~ssList(X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f597,f488])).
% 10.14/1.77  fof(f609,definition,(
% 10.14/1.77    sQ16_spl <=> (ssList(sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f611,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|sQ16_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f609])).
% 10.14/1.77  fof(f612,definition,(
% 10.14/1.77    sQ17_spl <=> (frontsegP(app(nil,sK49_skl),nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f613,plain,(
% 10.14/1.77    frontsegP(app(nil,sK49_skl),nil)|~sQ17_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f612])).
% 10.14/1.77  fof(f615,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f607,f609,f573,f612])).
% 10.14/1.77  fof(f616,definition,(
% 10.14/1.77    ![X0]: (sQ18_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(nil,sK49_skl),X0),sK49_skl)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f619,plain,(
% 10.14/1.77    sQ18_spl|~sQ16_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f608,f616,f609,f573])).
% 10.14/1.77  fof(f620,plain,(
% 10.14/1.77    $false|sQ16_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f611,f423])).
% 10.14/1.77  fof(f621,plain,(
% 10.14/1.77    sQ16_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f620])).
% 10.14/1.77  fof(f622,plain,(
% 10.14/1.77    frontsegP(sK49_skl,nil)|~sQ17_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f597,f613])).
% 10.14/1.77  fof(f624,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK49_skl))=sK49_skl|~sQ17_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f622,f123])).
% 10.14/1.77  fof(f625,definition,(
% 10.14/1.77    sQ19_spl <=> (app(nil,sK5_skl(nil,sK49_skl))=sK49_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f626,plain,(
% 10.14/1.77    app(nil,sK5_skl(nil,sK49_skl))=sK49_skl|~sQ19_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f625])).
% 10.14/1.77  fof(f628,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ19_spl|~sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f624,f609,f573,f625,f612])).
% 10.14/1.77  fof(f630,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f486])).
% 10.14/1.77  fof(f631,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f488])).
% 10.14/1.77  fof(f632,definition,(
% 10.14/1.77    sQ20_spl <=> (frontsegP(app(nil,nil),nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f633,plain,(
% 10.14/1.77    frontsegP(app(nil,nil),nil)|~sQ20_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f632])).
% 10.14/1.77  fof(f635,plain,(
% 10.14/1.77    ~sQ13_spl|sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f630,f573,f632])).
% 10.14/1.77  fof(f636,definition,(
% 10.14/1.77    ![X0]: (sQ21_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f639,plain,(
% 10.14/1.77    sQ21_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f631,f636,f573])).
% 10.14/1.77  fof(f640,plain,(
% 10.14/1.77    frontsegP(nil,nil)|~sQ20_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f596,f633])).
% 10.14/1.77  fof(f642,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ20_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f640,f123])).
% 10.14/1.77  fof(f643,definition,(
% 10.14/1.77    sQ22_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f644,plain,(
% 10.14/1.77    app(nil,sK5_skl(nil,nil))=nil|~sQ22_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f643])).
% 10.14/1.77  fof(f646,plain,(
% 10.14/1.77    ~sQ13_spl|sQ22_spl|~sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f642,f573,f643,f632])).
% 10.14/1.77  fof(f648,plain,(
% 10.14/1.77    ![X0,X1]: (app(sK5_skl(X0,X1),nil)=sK5_skl(X0,X1)|~ssList(X1)|~ssList(X0)|~frontsegP(X1,X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f389,f122])).
% 10.14/1.77  fof(f654,plain,(
% 10.14/1.77    app(sK49_skl,nil)=sK49_skl),
% 10.14/1.77    inference(resolution,[status(thm)],[f389,f423])).
% 10.14/1.77  fof(f655,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|frontsegP(app(sK49_skl,nil),sK49_skl)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f486])).
% 10.14/1.77  fof(f656,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(nil)|segmentP(app(app(sK49_skl,nil),X0),nil)|~ssList(sK49_skl)|~ssList(X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f488])).
% 10.14/1.77  fof(f657,definition,(
% 10.14/1.77    sQ23_spl <=> (frontsegP(app(sK49_skl,nil),sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f658,plain,(
% 10.14/1.77    frontsegP(app(sK49_skl,nil),sK49_skl)|~sQ23_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f657])).
% 10.14/1.77  fof(f660,plain,(
% 10.14/1.77    ~sQ16_spl|sQ23_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f655,f609,f657,f573])).
% 10.14/1.77  fof(f661,definition,(
% 10.14/1.77    ![X0]: (sQ24_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(sK49_skl,nil),X0),nil)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f664,plain,(
% 10.14/1.77    sQ24_spl|~sQ13_spl|~sQ16_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f656,f661,f573,f609])).
% 10.14/1.77  fof(f665,plain,(
% 10.14/1.77    frontsegP(sK49_skl,sK49_skl)|~sQ23_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f654,f658])).
% 10.14/1.77  fof(f667,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl|~sQ23_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f665,f123])).
% 10.14/1.77  fof(f668,definition,(
% 10.14/1.77    sQ25_spl <=> (app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f669,plain,(
% 10.14/1.77    app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl|~sQ25_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f668])).
% 10.14/1.77  fof(f671,plain,(
% 10.14/1.77    ~sQ16_spl|sQ25_spl|~sQ23_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f667,f609,f668,f657])).
% 10.14/1.77  fof(f684,plain,(
% 10.14/1.77    ~cons(sK1_skl,nil)=nil),
% 10.14/1.77    inference(resolution,[status(thm)],[f583,f223])).
% 10.14/1.77  fof(f702,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK6_skl(nil,X0))|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f128,f309])).
% 10.14/1.77  fof(f704,definition,(
% 10.14/1.77    ![X0]: (sQ26_spl <=> (~ssList(X0)|ssList(sK6_skl(nil,X0))|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f707,plain,(
% 10.14/1.77    sQ26_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f702,f704,f573])).
% 10.14/1.77  fof(f710,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f129,f309])).
% 10.14/1.77  fof(f712,definition,(
% 10.14/1.77    ![X0]: (sQ27_spl <=> (~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f715,plain,(
% 10.14/1.77    sQ27_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f710,f712,f573])).
% 10.14/1.77  fof(f718,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|rearsegP(app(sK49_skl,nil),nil)|~ssList(sK49_skl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f487])).
% 10.14/1.77  fof(f719,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f487])).
% 10.14/1.77  fof(f720,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|rearsegP(app(nil,sK49_skl),sK49_skl)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f597,f487])).
% 10.14/1.77  fof(f721,definition,(
% 10.14/1.77    sQ28_spl <=> (rearsegP(app(sK49_skl,nil),nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f722,plain,(
% 10.14/1.77    rearsegP(app(sK49_skl,nil),nil)|~sQ28_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f721])).
% 10.14/1.77  fof(f724,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ28_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f718,f609,f573,f721])).
% 10.14/1.77  fof(f725,definition,(
% 10.14/1.77    sQ29_spl <=> (rearsegP(app(nil,nil),nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f726,plain,(
% 10.14/1.77    rearsegP(app(nil,nil),nil)|~sQ29_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f725])).
% 10.14/1.77  fof(f728,plain,(
% 10.14/1.77    ~sQ13_spl|sQ29_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f719,f573,f725])).
% 10.14/1.77  fof(f729,definition,(
% 10.14/1.77    sQ30_spl <=> (rearsegP(app(nil,sK49_skl),sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f730,plain,(
% 10.14/1.77    rearsegP(app(nil,sK49_skl),sK49_skl)|~sQ30_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f729])).
% 10.14/1.77  fof(f732,plain,(
% 10.14/1.77    ~sQ16_spl|sQ30_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f720,f609,f729,f573])).
% 10.14/1.77  fof(f733,plain,(
% 10.14/1.77    rearsegP(sK49_skl,nil)|~sQ28_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f654,f722])).
% 10.14/1.77  fof(f734,plain,(
% 10.14/1.77    rearsegP(nil,nil)|~sQ29_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f596,f726])).
% 10.14/1.77  fof(f735,plain,(
% 10.14/1.77    rearsegP(sK49_skl,sK49_skl)|~sQ30_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f597,f730])).
% 10.14/1.77  fof(f736,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|app(sK6_skl(nil,sK49_skl),nil)=sK49_skl|~sQ28_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f733,f129])).
% 10.14/1.77  fof(f737,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK49_skl))|~sQ28_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f733,f128])).
% 10.14/1.77  fof(f738,definition,(
% 10.14/1.77    sQ31_spl <=> (app(sK6_skl(nil,sK49_skl),nil)=sK49_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f741,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ31_spl|~sQ28_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f736,f609,f573,f738,f721])).
% 10.14/1.77  fof(f742,definition,(
% 10.14/1.77    sQ32_spl <=> (ssList(sK6_skl(nil,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f745,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ32_spl|~sQ28_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f737,f609,f573,f742,f721])).
% 10.14/1.77  fof(f746,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)=sK49_skl|~sQ30_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f735,f129])).
% 10.14/1.77  fof(f747,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK6_skl(sK49_skl,sK49_skl))|~sQ30_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f735,f128])).
% 10.14/1.77  fof(f748,definition,(
% 10.14/1.77    sQ33_spl <=> (app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)=sK49_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f751,plain,(
% 10.14/1.77    ~sQ16_spl|sQ33_spl|~sQ30_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f746,f609,f748,f729])).
% 10.14/1.77  fof(f752,definition,(
% 10.14/1.77    sQ34_spl <=> (ssList(sK6_skl(sK49_skl,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f755,plain,(
% 10.14/1.77    ~sQ16_spl|sQ34_spl|~sQ30_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f747,f609,f752,f729])).
% 10.14/1.77  fof(f762,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil|~sQ29_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f734,f129])).
% 10.14/1.77  fof(f763,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|ssList(sK6_skl(nil,nil))|~sQ29_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f734,f128])).
% 10.14/1.77  fof(f764,definition,(
% 10.14/1.77    sQ35_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f767,plain,(
% 10.14/1.77    ~sQ13_spl|sQ35_spl|~sQ29_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f762,f573,f764,f725])).
% 10.14/1.77  fof(f768,definition,(
% 10.14/1.77    sQ36_spl <=> (ssList(sK6_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f771,plain,(
% 10.14/1.77    ~sQ13_spl|sQ36_spl|~sQ29_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f763,f573,f768,f725])).
% 10.14/1.77  fof(f807,plain,(
% 10.14/1.77    sP1_prd(nil,nil)|~sQ2_spl|~sQ3_spl),
% 10.14/1.77    inference(backward_demodulation,[status(thm)],[f465,f526])).
% 10.14/1.77  fof(f816,plain,(
% 10.14/1.77    $false|~sQ2_spl|~sQ3_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f807,f515])).
% 10.14/1.77  fof(f817,plain,(
% 10.14/1.77    ~sQ2_spl|~sQ3_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f816])).
% 10.14/1.77  fof(f820,plain,(
% 10.14/1.77    app(sK50_skl,nil)=sK50_skl),
% 10.14/1.77    inference(resolution,[status(thm)],[f424,f389])).
% 10.14/1.77  fof(f821,plain,(
% 10.14/1.77    app(nil,sK50_skl)=sK50_skl),
% 10.14/1.77    inference(resolution,[status(thm)],[f424,f249])).
% 10.14/1.77  fof(f822,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~nil=cons(sK1_skl,X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f235,f104])).
% 10.14/1.77  fof(f824,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(X0)|rearsegP(app(X1,X0),X0)|~ssList(X1))),
% 10.14/1.77    inference(backward_subsumption_resolution,[status(thm)],[f487,f245])).
% 10.14/1.77  fof(f825,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 10.14/1.77    inference(backward_subsumption_resolution,[status(thm)],[f486,f245])).
% 10.14/1.77  fof(f826,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK50_skl)))),
% 10.14/1.77    inference(resolution,[status(thm)],[f245,f424])).
% 10.14/1.77  fof(f828,plain,(
% 10.14/1.77    ![X0,X1,X2]: (~ssList(X0)|ssList(app(X0,sK5_skl(X1,X2)))|~ssList(X2)|~ssList(X1)|~frontsegP(X2,X1))),
% 10.14/1.77    inference(resolution,[status(thm)],[f245,f122])).
% 10.14/1.77  fof(f833,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,nil)))),
% 10.14/1.77    inference(resolution,[status(thm)],[f245,f223])).
% 10.14/1.77  fof(f834,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK49_skl)))),
% 10.14/1.77    inference(resolution,[status(thm)],[f423,f245])).
% 10.14/1.77  fof(f839,plain,(
% 10.14/1.77    neq(sK50_skl,nil)|~sQ4_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f425,f472])).
% 10.14/1.77  fof(f840,plain,(
% 10.14/1.77    ~neq(sK49_skl,nil)|sQ5_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f426,f477])).
% 10.14/1.77  fof(f854,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK7_skl(nil,X0))|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f134,f323])).
% 10.14/1.77  fof(f856,definition,(
% 10.14/1.77    ![X0]: (sQ40_spl <=> (~ssList(X0)|ssList(sK7_skl(nil,X0))|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f859,plain,(
% 10.14/1.77    sQ40_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f854,f856,f573])).
% 10.14/1.77  fof(f862,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK8_skl(nil,X0))|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f135,f323])).
% 10.14/1.77  fof(f864,definition,(
% 10.14/1.77    ![X0]: (sQ41_spl <=> (~ssList(X0)|ssList(sK8_skl(nil,X0))|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f867,plain,(
% 10.14/1.77    sQ41_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f862,f864,f573])).
% 10.14/1.77  fof(f870,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f136,f323])).
% 10.14/1.77  fof(f872,definition,(
% 10.14/1.77    ![X0]: (sQ42_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f875,plain,(
% 10.14/1.77    sQ42_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f870,f872,f573])).
% 10.14/1.77  fof(f895,plain,(
% 10.14/1.77    sP0_prd(sK51_skl,nil,sK49_skl)|~sQ3_spl|~sQ0_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f525,f458])).
% 10.14/1.77  fof(f941,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(sK49_skl)|~ssList(nil)|~memberP(sK49_skl,X0)|memberP(sK49_skl,X0)|memberP(nil,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f270])).
% 10.14/1.77  fof(f943,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f270])).
% 10.14/1.77  fof(f944,definition,(
% 10.14/1.77    ![X0]: (sQ45_spl <=> (~ssItem(X0)|~memberP(sK49_skl,X0)|memberP(sK49_skl,X0)|memberP(nil,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f947,plain,(
% 10.14/1.77    sQ45_spl|~sQ16_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f941,f944,f609,f573])).
% 10.14/1.77  fof(f949,definition,(
% 10.14/1.77    ![X0]: (sQ46_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f952,plain,(
% 10.14/1.77    sQ46_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f943,f949,f573])).
% 10.14/1.77  fof(f1034,definition,(
% 10.14/1.77    ![X0,X1]: (sQ50_spl <=> (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),nil),X1)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1046,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK50_skl)|~memberP(sK50_skl,X0)|memberP(nil,X0)|memberP(sK50_skl,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f821,f270])).
% 10.14/1.77  fof(f1047,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(sK50_skl,X0))|~ssList(sK50_skl)|segmentP(app(app(nil,sK50_skl),X0),sK50_skl)|~ssList(nil)|~ssList(X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f821,f488])).
% 10.14/1.77  fof(f1048,definition,(
% 10.14/1.77    ![X0]: (sQ51_spl <=> (~ssItem(X0)|~memberP(sK50_skl,X0)|memberP(nil,X0)|memberP(sK50_skl,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1051,definition,(
% 10.14/1.77    sQ52_spl <=> (ssList(sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1053,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|sQ52_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f1051])).
% 10.14/1.77  fof(f1054,plain,(
% 10.14/1.77    sQ51_spl|~sQ13_spl|~sQ52_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1046,f1048,f573,f1051])).
% 10.14/1.77  fof(f1055,definition,(
% 10.14/1.77    ![X0]: (sQ53_spl <=> (~ssList(app(sK50_skl,X0))|segmentP(app(app(nil,sK50_skl),X0),sK50_skl)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1058,plain,(
% 10.14/1.77    sQ53_spl|~sQ52_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1047,f1055,f1051,f573])).
% 10.14/1.77  fof(f1059,plain,(
% 10.14/1.77    $false|sQ52_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1053,f424])).
% 10.14/1.77  fof(f1060,plain,(
% 10.14/1.77    sQ52_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f1059])).
% 10.14/1.77  fof(f1063,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(sK50_skl,X0))|~ssList(nil)|segmentP(app(app(sK50_skl,nil),X0),nil)|~ssList(sK50_skl)|~ssList(X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f820,f488])).
% 10.14/1.77  fof(f1065,definition,(
% 10.14/1.77    ![X0]: (sQ54_spl <=> (~ssList(app(sK50_skl,X0))|segmentP(app(app(sK50_skl,nil),X0),nil)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1068,plain,(
% 10.14/1.77    sQ54_spl|~sQ13_spl|~sQ52_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1063,f1065,f573,f1051])).
% 10.14/1.77  fof(f1070,plain,(
% 10.14/1.77    app(app(sK52_skl(sK51_skl,sK50_skl,sK49_skl),sK49_skl),sK53_skl(sK51_skl,sK50_skl,sK49_skl))=sK50_skl|~sQ0_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f458,f440])).
% 10.14/1.77  fof(f1071,plain,(
% 10.14/1.77    cons(sK51_skl,nil)=sK49_skl|~sQ0_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f458,f439])).
% 10.14/1.77  fof(f1072,plain,(
% 10.14/1.77    ssItem(sK51_skl)|~sQ0_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f458,f436])).
% 10.14/1.77  fof(f1077,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~cons(sK51_skl,X0)=X0|~sQ0_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f1072,f225])).
% 10.14/1.77  fof(f1151,plain,(
% 10.14/1.77    ![X0,X1,X2]: (sP0_prd(X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|~ssList(X2)|ssItem(sK55_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil)))|memberP(X1,sK54_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))))),
% 10.14/1.77    inference(resolution,[status(thm)],[f512,f455])).
% 10.14/1.77  fof(f1160,plain,(
% 10.14/1.77    neq(nil,nil)|~sQ1_spl|~sQ4_spl),
% 10.14/1.77    inference(backward_demodulation,[status(thm)],[f461,f839])).
% 10.14/1.77  fof(f1197,plain,(
% 10.14/1.77    ~ssList(nil)|~sQ1_spl|~sQ4_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f1160,f498])).
% 10.14/1.77  fof(f1198,plain,(
% 10.14/1.77    ~sQ13_spl|~sQ1_spl|~sQ4_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1197,f573,f460,f471])).
% 10.14/1.77  fof(f1234,plain,(
% 10.14/1.77    ![X0,X1,X2]: (sP0_prd(X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(X2,sK55_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil)))|ssItem(sK54_skl(X2,X1,X0,app(app(X1,cons(X0,nil)),X2),cons(X0,nil))))),
% 10.14/1.77    inference(resolution,[status(thm)],[f513,f454])).
% 10.14/1.77  fof(f1251,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1))),
% 10.14/1.77    inference(resolution,[status(thm)],[f315,f323])).
% 10.14/1.77  fof(f1253,definition,(
% 10.14/1.77    ![X0,X1]: (sQ67_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|segmentP(X0,nil)|~ssList(X1)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1256,plain,(
% 10.14/1.77    sQ67_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1251,f1253,f573])).
% 10.14/1.77  fof(f1258,plain,(
% 10.14/1.77    app(app(sK52_skl(sK51_skl,sK50_skl,sK49_skl),sK49_skl),sK53_skl(sK51_skl,sK50_skl,sK49_skl))=sK50_skl|~sQ0_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f458,f440])).
% 10.14/1.77  fof(f1424,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f317,f323])).
% 10.14/1.77  fof(f1426,definition,(
% 10.14/1.77    ![X0]: (sQ81_spl <=> (~ssList(X0)|~segmentP(nil,X0)|nil=X0|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1429,plain,(
% 10.14/1.77    ~sQ13_spl|sQ81_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1424,f573,f1426])).
% 10.14/1.77  fof(f1431,plain,(
% 10.14/1.77    ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X0),X2),nil)|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f321,f323])).
% 10.14/1.77  fof(f1433,definition,(
% 10.14/1.77    ![X0,X1,X2]: (sQ82_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X0),X2),nil)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1436,plain,(
% 10.14/1.77    sQ82_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1431,f1433,f573])).
% 10.14/1.77  fof(f1541,plain,(
% 10.14/1.77    ~cons(sK51_skl,nil)=nil|~sQ0_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f1077,f223])).
% 10.14/1.77  fof(f1542,plain,(
% 10.14/1.77    ~sK49_skl=nil|~sQ0_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f1071,f1541])).
% 10.14/1.77  fof(f1580,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK49_skl),X1)|~ssList(X0)|~ssList(sK49_skl))),
% 10.14/1.77    inference(resolution,[status(thm)],[f834,f488])).
% 10.14/1.77  fof(f1590,definition,(
% 10.14/1.77    ![X0,X1]: (sQ98_spl <=> (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK49_skl),X1)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1593,plain,(
% 10.14/1.77    sQ98_spl|~sQ16_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1580,f1590,f609])).
% 10.14/1.77  fof(f1596,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK50_skl),X1)|~ssList(X0)|~ssList(sK50_skl))),
% 10.14/1.77    inference(resolution,[status(thm)],[f826,f488])).
% 10.14/1.77  fof(f1606,definition,(
% 10.14/1.77    ![X0,X1]: (sQ99_spl <=> (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),sK50_skl),X1)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f1609,plain,(
% 10.14/1.77    sQ99_spl|~sQ52_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1596,f1606,f1051])).
% 10.14/1.77  fof(f1627,plain,(
% 10.14/1.77    ~nil=cons(sK1_skl,sK50_skl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f822,f424])).
% 10.14/1.77  fof(f1908,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|segmentP(app(app(X0,X1),nil),X1)|~ssList(X0)|~ssList(nil))),
% 10.14/1.77    inference(resolution,[status(thm)],[f833,f488])).
% 10.14/1.77  fof(f1931,plain,(
% 10.14/1.77    sQ50_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f1908,f1034,f573])).
% 10.14/1.77  fof(f2227,plain,(
% 10.14/1.77    ~ssItem(sK0_skl)|sK0_skl=sK0_skl),
% 10.14/1.77    inference(resolution,[status(thm)],[f521,f522])).
% 10.14/1.77  fof(f2229,definition,(
% 10.14/1.77    sQ116_spl <=> (ssItem(sK0_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2231,plain,(
% 10.14/1.77    ~ssItem(sK0_skl)|sQ116_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f2229])).
% 10.14/1.77  fof(f2232,plain,(
% 10.14/1.77    ~sQ116_spl|sQ10_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2227,f2229,f543])).
% 10.14/1.77  fof(f2234,plain,(
% 10.14/1.77    ~ssItem(sK1_skl)|sK1_skl=sK1_skl),
% 10.14/1.77    inference(resolution,[status(thm)],[f523,f524])).
% 10.14/1.77  fof(f2236,definition,(
% 10.14/1.77    sQ117_spl <=> (ssItem(sK1_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2238,plain,(
% 10.14/1.77    ~ssItem(sK1_skl)|sQ117_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f2236])).
% 10.14/1.77  fof(f2239,plain,(
% 10.14/1.77    ~sQ117_spl|sQ8_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2234,f2236,f536])).
% 10.14/1.77  fof(f2557,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|sK49_skl=nil|sQ5_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f220,f840])).
% 10.14/1.77  fof(f2569,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ2_spl|sQ5_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2557,f609,f573,f464,f475])).
% 10.14/1.77  fof(f2576,plain,(
% 10.14/1.77    ~segmentP(sK50_skl,sK47_skl)|sQ6_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f425,f480])).
% 10.14/1.77  fof(f2577,plain,(
% 10.14/1.77    ~segmentP(sK50_skl,sK49_skl)|sQ6_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f426,f2576])).
% 10.14/1.77  fof(f2578,plain,(
% 10.14/1.77    $false|~sQ0_spl|~sQ2_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f465,f1542])).
% 10.14/1.77  fof(f2579,plain,(
% 10.14/1.77    ~sQ0_spl|~sQ2_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f2578])).
% 10.14/1.77  fof(f2580,plain,(
% 10.14/1.77    sQ1_spl|~sQ3_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f525,f460,f468])).
% 10.14/1.77  fof(f2594,plain,(
% 10.14/1.77    ~ssList(nil)|rearsegP(sK49_skl,nil)|~ssList(sK49_skl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f824])).
% 10.14/1.77  fof(f2595,plain,(
% 10.14/1.77    ~ssList(nil)|rearsegP(sK50_skl,nil)|~ssList(sK50_skl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f820,f824])).
% 10.14/1.77  fof(f2596,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|rearsegP(sK49_skl,sK49_skl)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f597,f824])).
% 10.14/1.77  fof(f2597,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|rearsegP(sK50_skl,sK50_skl)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f821,f824])).
% 10.14/1.77  fof(f2598,plain,(
% 10.14/1.77    ~ssList(nil)|rearsegP(nil,nil)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f824])).
% 10.14/1.77  fof(f2603,definition,(
% 10.14/1.77    sQ144_spl <=> (rearsegP(sK49_skl,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2606,plain,(
% 10.14/1.77    ~sQ13_spl|sQ144_spl|~sQ16_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2594,f573,f2603,f609])).
% 10.14/1.77  fof(f2607,definition,(
% 10.14/1.77    sQ145_spl <=> (rearsegP(sK50_skl,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2608,plain,(
% 10.14/1.77    rearsegP(sK50_skl,nil)|~sQ145_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f2607])).
% 10.14/1.77  fof(f2610,plain,(
% 10.14/1.77    ~sQ13_spl|sQ145_spl|~sQ52_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2595,f573,f2607,f1051])).
% 10.14/1.77  fof(f2611,definition,(
% 10.14/1.77    sQ146_spl <=> (rearsegP(sK49_skl,sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2614,plain,(
% 10.14/1.77    ~sQ16_spl|sQ146_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2596,f609,f2611,f573])).
% 10.14/1.77  fof(f2615,definition,(
% 10.14/1.77    sQ147_spl <=> (rearsegP(sK50_skl,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2616,plain,(
% 10.14/1.77    rearsegP(sK50_skl,sK50_skl)|~sQ147_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f2615])).
% 10.14/1.77  fof(f2618,plain,(
% 10.14/1.77    ~sQ52_spl|sQ147_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2597,f1051,f2615,f573])).
% 10.14/1.77  fof(f2619,definition,(
% 10.14/1.77    sQ148_spl <=> (rearsegP(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2622,plain,(
% 10.14/1.77    ~sQ13_spl|sQ148_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2598,f573,f2619])).
% 10.14/1.77  fof(f2623,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(nil)|app(sK6_skl(nil,sK50_skl),nil)=sK50_skl|~sQ145_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2608,f129])).
% 10.14/1.77  fof(f2624,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK50_skl))|~sQ145_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2608,f128])).
% 10.14/1.77  fof(f2625,definition,(
% 10.14/1.77    sQ149_spl <=> (app(sK6_skl(nil,sK50_skl),nil)=sK50_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2628,plain,(
% 10.14/1.77    ~sQ52_spl|~sQ13_spl|sQ149_spl|~sQ145_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2623,f1051,f573,f2625,f2607])).
% 10.14/1.77  fof(f2629,definition,(
% 10.14/1.77    sQ150_spl <=> (ssList(sK6_skl(nil,sK50_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2632,plain,(
% 10.14/1.77    ~sQ52_spl|~sQ13_spl|sQ150_spl|~sQ145_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2624,f1051,f573,f2629,f2607])).
% 10.14/1.77  fof(f2633,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(sK50_skl)|app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)=sK50_skl|~sQ147_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2616,f129])).
% 10.14/1.77  fof(f2634,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK6_skl(sK50_skl,sK50_skl))|~sQ147_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2616,f128])).
% 10.14/1.77  fof(f2635,definition,(
% 10.14/1.77    sQ151_spl <=> (app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)=sK50_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2638,plain,(
% 10.14/1.77    ~sQ52_spl|sQ151_spl|~sQ147_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2633,f1051,f2635,f2615])).
% 10.14/1.77  fof(f2639,definition,(
% 10.14/1.77    sQ152_spl <=> (ssList(sK6_skl(sK50_skl,sK50_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2642,plain,(
% 10.14/1.77    ~sQ52_spl|sQ152_spl|~sQ147_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2634,f1051,f2639,f2615])).
% 10.14/1.77  fof(f2799,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|frontsegP(sK49_skl,sK49_skl)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f825])).
% 10.14/1.77  fof(f2800,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|frontsegP(sK50_skl,sK50_skl)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f820,f825])).
% 10.14/1.77  fof(f2801,plain,(
% 10.14/1.77    ~ssList(nil)|frontsegP(sK49_skl,nil)|~ssList(sK49_skl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f597,f825])).
% 10.14/1.77  fof(f2802,plain,(
% 10.14/1.77    ~ssList(nil)|frontsegP(sK50_skl,nil)|~ssList(sK50_skl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f821,f825])).
% 10.14/1.77  fof(f2803,plain,(
% 10.14/1.77    ~ssList(nil)|frontsegP(nil,nil)|~ssList(nil)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f825])).
% 10.14/1.77  fof(f2806,definition,(
% 10.14/1.77    sQ175_spl <=> (frontsegP(sK49_skl,sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2809,plain,(
% 10.14/1.77    ~sQ16_spl|sQ175_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2799,f609,f2806,f573])).
% 10.14/1.77  fof(f2810,definition,(
% 10.14/1.77    sQ176_spl <=> (frontsegP(sK50_skl,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2811,plain,(
% 10.14/1.77    frontsegP(sK50_skl,sK50_skl)|~sQ176_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f2810])).
% 10.14/1.77  fof(f2813,plain,(
% 10.14/1.77    ~sQ52_spl|sQ176_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2800,f1051,f2810,f573])).
% 10.14/1.77  fof(f2814,definition,(
% 10.14/1.77    sQ177_spl <=> (frontsegP(sK49_skl,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2817,plain,(
% 10.14/1.77    ~sQ13_spl|sQ177_spl|~sQ16_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2801,f573,f2814,f609])).
% 10.14/1.77  fof(f2818,definition,(
% 10.14/1.77    sQ178_spl <=> (frontsegP(sK50_skl,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2819,plain,(
% 10.14/1.77    frontsegP(sK50_skl,nil)|~sQ178_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f2818])).
% 10.14/1.77  fof(f2821,plain,(
% 10.14/1.77    ~sQ13_spl|sQ178_spl|~sQ52_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2802,f573,f2818,f1051])).
% 10.14/1.77  fof(f2822,definition,(
% 10.14/1.77    sQ179_spl <=> (frontsegP(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2825,plain,(
% 10.14/1.77    ~sQ13_spl|sQ179_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2803,f573,f2822])).
% 10.14/1.77  fof(f2840,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(sK50_skl)|app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))=sK50_skl|~sQ176_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2811,f123])).
% 10.14/1.77  fof(f2841,definition,(
% 10.14/1.77    sQ180_spl <=> (app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))=sK50_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2844,plain,(
% 10.14/1.77    ~sQ52_spl|sQ180_spl|~sQ176_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2840,f1051,f2841,f2810])).
% 10.14/1.77  fof(f2845,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK50_skl))=sK50_skl|~sQ178_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2819,f123])).
% 10.14/1.77  fof(f2846,definition,(
% 10.14/1.77    sQ181_spl <=> (app(nil,sK5_skl(nil,sK50_skl))=sK50_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f2849,plain,(
% 10.14/1.77    ~sQ52_spl|~sQ13_spl|sQ181_spl|~sQ178_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f2845,f1051,f573,f2846,f2818])).
% 10.14/1.77  fof(f3128,plain,(
% 10.14/1.77    ~ssList(sK5_skl(nil,sK49_skl))|rearsegP(sK49_skl,sK5_skl(nil,sK49_skl))|~ssList(nil)|~sQ19_spl),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f626,f824])).
% 10.14/1.77  fof(f3129,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK5_skl(nil,sK49_skl))|~memberP(sK49_skl,X0)|memberP(nil,X0)|memberP(sK5_skl(nil,sK49_skl),X0)|~sQ19_spl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f626,f270])).
% 10.14/1.77  fof(f3130,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(sK5_skl(nil,sK49_skl))|segmentP(app(app(nil,sK5_skl(nil,sK49_skl)),X0),sK5_skl(nil,sK49_skl))|~ssList(nil)|~ssList(X0)|~sQ19_spl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f626,f488])).
% 10.14/1.77  fof(f3131,definition,(
% 10.14/1.77    sQ199_spl <=> (ssList(sK5_skl(nil,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3133,plain,(
% 10.14/1.77    ~ssList(sK5_skl(nil,sK49_skl))|sQ199_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f3131])).
% 10.14/1.77  fof(f3135,definition,(
% 10.14/1.77    sQ200_spl <=> (rearsegP(sK49_skl,sK5_skl(nil,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3138,plain,(
% 10.14/1.77    ~sQ199_spl|sQ200_spl|~sQ13_spl|~sQ19_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3128,f3131,f3135,f573,f625])).
% 10.14/1.77  fof(f3139,definition,(
% 10.14/1.77    ![X0]: (sQ201_spl <=> (~ssItem(X0)|~memberP(sK49_skl,X0)|memberP(nil,X0)|memberP(sK5_skl(nil,sK49_skl),X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3142,plain,(
% 10.14/1.77    sQ201_spl|~sQ13_spl|~sQ199_spl|~sQ19_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3129,f3139,f573,f3131,f625])).
% 10.14/1.77  fof(f3143,definition,(
% 10.14/1.77    ![X0]: (sQ202_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(nil,sK5_skl(nil,sK49_skl)),X0),sK5_skl(nil,sK49_skl))|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3146,plain,(
% 10.14/1.77    sQ202_spl|~sQ199_spl|~sQ13_spl|~sQ19_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3130,f3143,f3131,f573,f625])).
% 10.14/1.77  fof(f3147,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|~frontsegP(sK49_skl,nil)|sQ199_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3133,f122])).
% 10.14/1.77  fof(f3148,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|~sQ177_spl|sQ199_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3147,f609,f573,f2814,f3131])).
% 10.14/1.77  fof(f3487,plain,(
% 10.14/1.77    ~ssList(sK5_skl(nil,nil))|rearsegP(nil,sK5_skl(nil,nil))|~ssList(nil)|~sQ22_spl),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f644,f824])).
% 10.14/1.77  fof(f3488,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK5_skl(nil,nil))|~memberP(nil,X0)|memberP(nil,X0)|memberP(sK5_skl(nil,nil),X0)|~sQ22_spl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f644,f270])).
% 10.14/1.77  fof(f3489,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(nil,X0))|~ssList(sK5_skl(nil,nil))|segmentP(app(app(nil,sK5_skl(nil,nil)),X0),sK5_skl(nil,nil))|~ssList(nil)|~ssList(X0)|~sQ22_spl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f644,f488])).
% 10.14/1.77  fof(f3490,definition,(
% 10.14/1.77    sQ241_spl <=> (ssList(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3491,plain,(
% 10.14/1.77    ssList(sK5_skl(nil,nil))|~sQ241_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f3490])).
% 10.14/1.77  fof(f3492,plain,(
% 10.14/1.77    ~ssList(sK5_skl(nil,nil))|sQ241_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f3490])).
% 10.14/1.77  fof(f3494,definition,(
% 10.14/1.77    sQ242_spl <=> (rearsegP(nil,sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3497,plain,(
% 10.14/1.77    ~sQ241_spl|sQ242_spl|~sQ13_spl|~sQ22_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3487,f3490,f3494,f573,f643])).
% 10.14/1.77  fof(f3498,definition,(
% 10.14/1.77    ![X0]: (sQ243_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(sK5_skl(nil,nil),X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3501,plain,(
% 10.14/1.77    sQ243_spl|~sQ13_spl|~sQ241_spl|~sQ22_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3488,f3498,f573,f3490,f643])).
% 10.14/1.77  fof(f3502,definition,(
% 10.14/1.77    ![X0]: (sQ244_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,sK5_skl(nil,nil)),X0),sK5_skl(nil,nil))|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3505,plain,(
% 10.14/1.77    sQ244_spl|~sQ241_spl|~sQ13_spl|~sQ22_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3489,f3502,f3490,f573,f643])).
% 10.14/1.77  fof(f3506,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|~frontsegP(nil,nil)|sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3492,f122])).
% 10.14/1.77  fof(f3507,plain,(
% 10.14/1.77    ~sQ13_spl|~sQ179_spl|sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3506,f573,f2822,f3490])).
% 10.14/1.77  fof(f3509,plain,(
% 10.14/1.77    duplicatefreeP(sK5_skl(nil,nil))|sK34_skl(sK5_skl(nil,nil))=sK35_skl(sK5_skl(nil,nil))|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f206])).
% 10.14/1.77  fof(f3510,plain,(
% 10.14/1.77    duplicatefreeP(sK5_skl(nil,nil))|app(app(sK36_skl(sK5_skl(nil,nil)),cons(sK34_skl(sK5_skl(nil,nil)),sK37_skl(sK5_skl(nil,nil)))),cons(sK35_skl(sK5_skl(nil,nil)),sK38_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil)|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f205])).
% 10.14/1.77  fof(f3511,plain,(
% 10.14/1.77    strictorderedP(sK5_skl(nil,nil))|app(app(sK31_skl(sK5_skl(nil,nil)),cons(sK29_skl(sK5_skl(nil,nil)),sK32_skl(sK5_skl(nil,nil)))),cons(sK30_skl(sK5_skl(nil,nil)),sK33_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil)|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f194])).
% 10.14/1.77  fof(f3513,plain,(
% 10.14/1.77    totalorderedP(sK5_skl(nil,nil))|app(app(sK26_skl(sK5_skl(nil,nil)),cons(sK24_skl(sK5_skl(nil,nil)),sK27_skl(sK5_skl(nil,nil)))),cons(sK25_skl(sK5_skl(nil,nil)),sK28_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil)|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f183])).
% 10.14/1.77  fof(f3516,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~nil=app(X0,sK5_skl(nil,nil))|nil=sK5_skl(nil,nil)|~sQ241_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f385])).
% 10.14/1.77  fof(f3518,plain,(
% 10.14/1.77    strictorderP(sK5_skl(nil,nil))|app(app(sK21_skl(sK5_skl(nil,nil)),cons(sK19_skl(sK5_skl(nil,nil)),sK22_skl(sK5_skl(nil,nil)))),cons(sK20_skl(sK5_skl(nil,nil)),sK23_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil)|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f171])).
% 10.14/1.77  fof(f3535,plain,(
% 10.14/1.77    totalorderP(sK5_skl(nil,nil))|app(app(sK16_skl(sK5_skl(nil,nil)),cons(sK14_skl(sK5_skl(nil,nil)),sK17_skl(sK5_skl(nil,nil)))),cons(sK15_skl(sK5_skl(nil,nil)),sK18_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil)|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f159])).
% 10.14/1.77  fof(f3536,plain,(
% 10.14/1.77    cyclefreeP(sK5_skl(nil,nil))|app(app(sK11_skl(sK5_skl(nil,nil)),cons(sK9_skl(sK5_skl(nil,nil)),sK12_skl(sK5_skl(nil,nil)))),cons(sK10_skl(sK5_skl(nil,nil)),sK13_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil)|~sQ241_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3491,f147])).
% 10.14/1.77  fof(f3542,definition,(
% 10.14/1.77    sQ245_spl <=> (duplicatefreeP(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3545,definition,(
% 10.14/1.77    sQ246_spl <=> (sK34_skl(sK5_skl(nil,nil))=sK35_skl(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3548,plain,(
% 10.14/1.77    sQ245_spl|sQ246_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3509,f3542,f3545,f3490])).
% 10.14/1.77  fof(f3549,definition,(
% 10.14/1.77    sQ247_spl <=> (app(app(sK36_skl(sK5_skl(nil,nil)),cons(sK34_skl(sK5_skl(nil,nil)),sK37_skl(sK5_skl(nil,nil)))),cons(sK35_skl(sK5_skl(nil,nil)),sK38_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3552,plain,(
% 10.14/1.77    sQ245_spl|sQ247_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3510,f3542,f3549,f3490])).
% 10.14/1.77  fof(f3553,definition,(
% 10.14/1.77    sQ248_spl <=> (strictorderedP(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3556,definition,(
% 10.14/1.77    sQ249_spl <=> (app(app(sK31_skl(sK5_skl(nil,nil)),cons(sK29_skl(sK5_skl(nil,nil)),sK32_skl(sK5_skl(nil,nil)))),cons(sK30_skl(sK5_skl(nil,nil)),sK33_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3559,plain,(
% 10.14/1.77    sQ248_spl|sQ249_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3511,f3553,f3556,f3490])).
% 10.14/1.77  fof(f3560,definition,(
% 10.14/1.77    sQ250_spl <=> (totalorderedP(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3563,definition,(
% 10.14/1.77    sQ251_spl <=> (app(app(sK26_skl(sK5_skl(nil,nil)),cons(sK24_skl(sK5_skl(nil,nil)),sK27_skl(sK5_skl(nil,nil)))),cons(sK25_skl(sK5_skl(nil,nil)),sK28_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3566,plain,(
% 10.14/1.77    sQ250_spl|sQ251_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3513,f3560,f3563,f3490])).
% 10.14/1.77  fof(f3567,definition,(
% 10.14/1.77    ![X0]: (sQ252_spl <=> (~ssList(X0)|~nil=app(X0,sK5_skl(nil,nil))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3570,definition,(
% 10.14/1.77    sQ253_spl <=> (nil=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3573,plain,(
% 10.14/1.77    sQ252_spl|sQ253_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3516,f3567,f3570,f3490])).
% 10.14/1.77  fof(f3574,definition,(
% 10.14/1.77    sQ254_spl <=> (strictorderP(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3577,definition,(
% 10.14/1.77    sQ255_spl <=> (app(app(sK21_skl(sK5_skl(nil,nil)),cons(sK19_skl(sK5_skl(nil,nil)),sK22_skl(sK5_skl(nil,nil)))),cons(sK20_skl(sK5_skl(nil,nil)),sK23_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3580,plain,(
% 10.14/1.77    sQ254_spl|sQ255_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3518,f3574,f3577,f3490])).
% 10.14/1.77  fof(f3581,definition,(
% 10.14/1.77    sQ256_spl <=> (totalorderP(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3584,definition,(
% 10.14/1.77    sQ257_spl <=> (app(app(sK16_skl(sK5_skl(nil,nil)),cons(sK14_skl(sK5_skl(nil,nil)),sK17_skl(sK5_skl(nil,nil)))),cons(sK15_skl(sK5_skl(nil,nil)),sK18_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3587,plain,(
% 10.14/1.77    sQ256_spl|sQ257_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3535,f3581,f3584,f3490])).
% 10.14/1.77  fof(f3588,definition,(
% 10.14/1.77    sQ258_spl <=> (cyclefreeP(sK5_skl(nil,nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3591,definition,(
% 10.14/1.77    sQ259_spl <=> (app(app(sK11_skl(sK5_skl(nil,nil)),cons(sK9_skl(sK5_skl(nil,nil)),sK12_skl(sK5_skl(nil,nil)))),cons(sK10_skl(sK5_skl(nil,nil)),sK13_skl(sK5_skl(nil,nil))))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3594,plain,(
% 10.14/1.77    sQ258_spl|sQ259_spl|~sQ241_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3536,f3588,f3591,f3490])).
% 10.14/1.77  fof(f3596,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK50_skl))=sK5_skl(nil,sK50_skl)|~sQ178_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f598,f2819])).
% 10.14/1.77  fof(f3597,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(sK50_skl)|app(nil,sK5_skl(sK50_skl,sK50_skl))=sK5_skl(sK50_skl,sK50_skl)|~sQ176_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f598,f2811])).
% 10.14/1.77  fof(f3599,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|app(nil,sK5_skl(sK49_skl,sK49_skl))=sK5_skl(sK49_skl,sK49_skl)|~sQ23_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f598,f665])).
% 10.14/1.77  fof(f3600,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK49_skl))=sK5_skl(nil,sK49_skl)|~sQ17_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f598,f622])).
% 10.14/1.77  fof(f3601,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=sK5_skl(nil,nil)|~sQ20_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f598,f640])).
% 10.14/1.77  fof(f3602,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=sK5_skl(nil,X0)|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f598,f295])).
% 10.14/1.77  fof(f3604,definition,(
% 10.14/1.77    sQ260_spl <=> (app(nil,sK5_skl(nil,sK50_skl))=sK5_skl(nil,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3607,plain,(
% 10.14/1.77    ~sQ52_spl|~sQ13_spl|sQ260_spl|~sQ178_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3596,f1051,f573,f3604,f2818])).
% 10.14/1.77  fof(f3608,definition,(
% 10.14/1.77    sQ261_spl <=> (app(nil,sK5_skl(sK50_skl,sK50_skl))=sK5_skl(sK50_skl,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3611,plain,(
% 10.14/1.77    ~sQ52_spl|sQ261_spl|~sQ176_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3597,f1051,f3608,f2810])).
% 10.14/1.77  fof(f3614,definition,(
% 10.14/1.77    sQ262_spl <=> (app(nil,sK5_skl(sK49_skl,sK49_skl))=sK5_skl(sK49_skl,sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3617,plain,(
% 10.14/1.77    ~sQ16_spl|sQ262_spl|~sQ23_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3599,f609,f3614,f657])).
% 10.14/1.77  fof(f3618,definition,(
% 10.14/1.77    sQ263_spl <=> (app(nil,sK5_skl(nil,sK49_skl))=sK5_skl(nil,sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3621,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ263_spl|~sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3600,f609,f573,f3618,f612])).
% 10.14/1.77  fof(f3622,definition,(
% 10.14/1.77    sQ264_spl <=> (app(nil,sK5_skl(nil,nil))=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3625,plain,(
% 10.14/1.77    ~sQ13_spl|sQ264_spl|~sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3601,f573,f3622,f632])).
% 10.14/1.77  fof(f3626,definition,(
% 10.14/1.77    ![X0]: (sQ265_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=sK5_skl(nil,X0)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3629,plain,(
% 10.14/1.77    sQ265_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3602,f3626,f573])).
% 10.14/1.77  fof(f3635,plain,(
% 10.14/1.77    app(sK5_skl(nil,sK50_skl),nil)=sK5_skl(nil,sK50_skl)|~ssList(sK50_skl)|~ssList(nil)|~sQ178_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f648,f2819])).
% 10.14/1.77  fof(f3636,plain,(
% 10.14/1.77    app(sK5_skl(sK50_skl,sK50_skl),nil)=sK5_skl(sK50_skl,sK50_skl)|~ssList(sK50_skl)|~ssList(sK50_skl)|~sQ176_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f648,f2811])).
% 10.14/1.77  fof(f3638,plain,(
% 10.14/1.77    app(sK5_skl(sK49_skl,sK49_skl),nil)=sK5_skl(sK49_skl,sK49_skl)|~ssList(sK49_skl)|~ssList(sK49_skl)|~sQ23_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f648,f665])).
% 10.14/1.77  fof(f3639,plain,(
% 10.14/1.77    app(sK5_skl(nil,sK49_skl),nil)=sK5_skl(nil,sK49_skl)|~ssList(sK49_skl)|~ssList(nil)|~sQ17_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f648,f622])).
% 10.14/1.77  fof(f3640,plain,(
% 10.14/1.77    app(sK5_skl(nil,nil),nil)=sK5_skl(nil,nil)|~ssList(nil)|~ssList(nil)|~sQ20_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f648,f640])).
% 10.14/1.77  fof(f3641,plain,(
% 10.14/1.77    ![X0]: (app(sK5_skl(nil,X0),nil)=sK5_skl(nil,X0)|~ssList(X0)|~ssList(nil)|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f648,f295])).
% 10.14/1.77  fof(f3643,definition,(
% 10.14/1.77    sQ266_spl <=> (app(sK5_skl(nil,sK50_skl),nil)=sK5_skl(nil,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3646,plain,(
% 10.14/1.77    sQ266_spl|~sQ52_spl|~sQ13_spl|~sQ178_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3635,f3643,f1051,f573,f2818])).
% 10.14/1.77  fof(f3647,definition,(
% 10.14/1.77    sQ267_spl <=> (app(sK5_skl(sK50_skl,sK50_skl),nil)=sK5_skl(sK50_skl,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3650,plain,(
% 10.14/1.77    sQ267_spl|~sQ52_spl|~sQ176_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3636,f3647,f1051,f2810])).
% 10.14/1.77  fof(f3653,definition,(
% 10.14/1.77    sQ268_spl <=> (app(sK5_skl(sK49_skl,sK49_skl),nil)=sK5_skl(sK49_skl,sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3656,plain,(
% 10.14/1.77    sQ268_spl|~sQ16_spl|~sQ23_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3638,f3653,f609,f657])).
% 10.14/1.77  fof(f3657,definition,(
% 10.14/1.77    sQ269_spl <=> (app(sK5_skl(nil,sK49_skl),nil)=sK5_skl(nil,sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3660,plain,(
% 10.14/1.77    sQ269_spl|~sQ16_spl|~sQ13_spl|~sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3639,f3657,f609,f573,f612])).
% 10.14/1.77  fof(f3661,definition,(
% 10.14/1.77    sQ270_spl <=> (app(sK5_skl(nil,nil),nil)=sK5_skl(nil,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3664,plain,(
% 10.14/1.77    sQ270_spl|~sQ13_spl|~sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3640,f3661,f573,f632])).
% 10.14/1.77  fof(f3665,definition,(
% 10.14/1.77    ![X0]: (sQ271_spl <=> (app(sK5_skl(nil,X0),nil)=sK5_skl(nil,X0)|~ssList(X0)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3668,plain,(
% 10.14/1.77    sQ271_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3641,f3665,f573])).
% 10.14/1.77  fof(f3734,plain,(
% 10.14/1.77    ~ssList(sK5_skl(sK49_skl,sK49_skl))|rearsegP(sK49_skl,sK5_skl(sK49_skl,sK49_skl))|~ssList(sK49_skl)|~sQ25_spl),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f669,f824])).
% 10.14/1.77  fof(f3735,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(sK49_skl)|~ssList(sK5_skl(sK49_skl,sK49_skl))|~memberP(sK49_skl,X0)|memberP(sK49_skl,X0)|memberP(sK5_skl(sK49_skl,sK49_skl),X0)|~sQ25_spl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f669,f270])).
% 10.14/1.77  fof(f3736,plain,(
% 10.14/1.77    ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(sK5_skl(sK49_skl,sK49_skl))|segmentP(app(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),X0),sK5_skl(sK49_skl,sK49_skl))|~ssList(sK49_skl)|~ssList(X0)|~sQ25_spl)),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f669,f488])).
% 10.14/1.77  fof(f3737,definition,(
% 10.14/1.77    sQ272_spl <=> (ssList(sK5_skl(sK49_skl,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3739,plain,(
% 10.14/1.77    ~ssList(sK5_skl(sK49_skl,sK49_skl))|sQ272_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f3737])).
% 10.14/1.77  fof(f3741,definition,(
% 10.14/1.77    sQ273_spl <=> (rearsegP(sK49_skl,sK5_skl(sK49_skl,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3742,plain,(
% 10.14/1.77    rearsegP(sK49_skl,sK5_skl(sK49_skl,sK49_skl))|~sQ273_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f3741])).
% 10.14/1.77  fof(f3744,plain,(
% 10.14/1.77    ~sQ272_spl|sQ273_spl|~sQ16_spl|~sQ25_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3734,f3737,f3741,f609,f668])).
% 10.14/1.77  fof(f3745,definition,(
% 10.14/1.77    ![X0]: (sQ274_spl <=> (~ssItem(X0)|~memberP(sK49_skl,X0)|memberP(sK49_skl,X0)|memberP(sK5_skl(sK49_skl,sK49_skl),X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3748,plain,(
% 10.14/1.77    sQ274_spl|~sQ16_spl|~sQ272_spl|~sQ25_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3735,f3745,f609,f3737,f668])).
% 10.14/1.77  fof(f3749,definition,(
% 10.14/1.77    ![X0]: (sQ275_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),X0),sK5_skl(sK49_skl,sK49_skl))|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3752,plain,(
% 10.14/1.77    sQ275_spl|~sQ272_spl|~sQ16_spl|~sQ25_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3736,f3749,f3737,f609,f668])).
% 10.14/1.77  fof(f3753,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|~frontsegP(sK49_skl,sK49_skl)|sQ272_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3739,f122])).
% 10.14/1.77  fof(f3754,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ175_spl|sQ272_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3753,f609,f2806,f3737])).
% 10.14/1.77  fof(f3868,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK5_skl(sK49_skl,sK49_skl))|app(sK6_skl(sK5_skl(sK49_skl,sK49_skl),sK49_skl),sK5_skl(sK49_skl,sK49_skl))=sK49_skl|~sQ273_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3742,f129])).
% 10.14/1.77  fof(f3869,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK5_skl(sK49_skl,sK49_skl))|ssList(sK6_skl(sK5_skl(sK49_skl,sK49_skl),sK49_skl))|~sQ273_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f3742,f128])).
% 10.14/1.77  fof(f3870,definition,(
% 10.14/1.77    sQ292_spl <=> (app(sK6_skl(sK5_skl(sK49_skl,sK49_skl),sK49_skl),sK5_skl(sK49_skl,sK49_skl))=sK49_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3873,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ272_spl|sQ292_spl|~sQ273_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3868,f609,f3737,f3870,f3741])).
% 10.14/1.77  fof(f3874,definition,(
% 10.14/1.77    sQ293_spl <=> (ssList(sK6_skl(sK5_skl(sK49_skl,sK49_skl),sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f3877,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ272_spl|sQ293_spl|~sQ273_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f3869,f609,f3737,f3874,f3741])).
% 10.14/1.77  fof(f4714,plain,(
% 10.14/1.77    ![X0,X1]: (sP0_prd(X0,app(app(nil,cons(X0,nil)),X1),cons(X0,nil))|~ssItem(X0)|~ssList(nil)|~ssList(X1)|ssItem(sK55_skl(X1,nil,X0,app(app(nil,cons(X0,nil)),X1),cons(X0,nil)))|~ssItem(sK54_skl(X1,nil,X0,app(app(nil,cons(X0,nil)),X1),cons(X0,nil))))),
% 10.14/1.77    inference(resolution,[status(thm)],[f1151,f279])).
% 10.14/1.77  fof(f4731,definition,(
% 10.14/1.77    ![X0,X1]: (sQ336_spl <=> (sP0_prd(X0,app(app(nil,cons(X0,nil)),X1),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|ssItem(sK55_skl(X1,nil,X0,app(app(nil,cons(X0,nil)),X1),cons(X0,nil)))|~ssItem(sK54_skl(X1,nil,X0,app(app(nil,cons(X0,nil)),X1),cons(X0,nil)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4734,plain,(
% 10.14/1.77    sQ336_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4714,f4731,f573])).
% 10.14/1.77  fof(f4874,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK5_skl(nil,sK50_skl)))|~ssList(sK50_skl)|~ssList(nil)|~sQ178_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f828,f2819])).
% 10.14/1.77  fof(f4875,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK5_skl(sK50_skl,sK50_skl)))|~ssList(sK50_skl)|~ssList(sK50_skl)|~sQ176_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f828,f2811])).
% 10.14/1.77  fof(f4877,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK5_skl(sK49_skl,sK49_skl)))|~ssList(sK49_skl)|~ssList(sK49_skl)|~sQ23_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f828,f665])).
% 10.14/1.77  fof(f4878,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK5_skl(nil,sK49_skl)))|~ssList(sK49_skl)|~ssList(nil)|~sQ17_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f828,f622])).
% 10.14/1.77  fof(f4879,plain,(
% 10.14/1.77    ![X0]: (~ssList(X0)|ssList(app(X0,sK5_skl(nil,nil)))|~ssList(nil)|~ssList(nil)|~sQ20_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f828,f640])).
% 10.14/1.77  fof(f4880,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(X0)|ssList(app(X0,sK5_skl(nil,X1)))|~ssList(X1)|~ssList(nil)|~ssList(X1))),
% 10.14/1.77    inference(resolution,[status(thm)],[f828,f295])).
% 10.14/1.77  fof(f4882,definition,(
% 10.14/1.77    ![X0]: (sQ339_spl <=> (~ssList(X0)|ssList(app(X0,sK5_skl(nil,sK50_skl)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4885,plain,(
% 10.14/1.77    sQ339_spl|~sQ52_spl|~sQ13_spl|~sQ178_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4874,f4882,f1051,f573,f2818])).
% 10.14/1.77  fof(f4886,definition,(
% 10.14/1.77    ![X0]: (sQ340_spl <=> (~ssList(X0)|ssList(app(X0,sK5_skl(sK50_skl,sK50_skl)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4889,plain,(
% 10.14/1.77    sQ340_spl|~sQ52_spl|~sQ176_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4875,f4886,f1051,f2810])).
% 10.14/1.77  fof(f4892,definition,(
% 10.14/1.77    ![X0]: (sQ341_spl <=> (~ssList(X0)|ssList(app(X0,sK5_skl(sK49_skl,sK49_skl)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4895,plain,(
% 10.14/1.77    sQ341_spl|~sQ16_spl|~sQ23_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4877,f4892,f609,f657])).
% 10.14/1.77  fof(f4896,definition,(
% 10.14/1.77    ![X0]: (sQ342_spl <=> (~ssList(X0)|ssList(app(X0,sK5_skl(nil,sK49_skl)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4899,plain,(
% 10.14/1.77    sQ342_spl|~sQ16_spl|~sQ13_spl|~sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4878,f4896,f609,f573,f612])).
% 10.14/1.77  fof(f4900,definition,(
% 10.14/1.77    ![X0]: (sQ343_spl <=> (~ssList(X0)|ssList(app(X0,sK5_skl(nil,nil)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4903,plain,(
% 10.14/1.77    sQ343_spl|~sQ13_spl|~sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4879,f4900,f573,f632])).
% 10.14/1.77  fof(f4904,definition,(
% 10.14/1.77    ![X0,X1]: (sQ344_spl <=> (~ssList(X0)|ssList(app(X0,sK5_skl(nil,X1)))|~ssList(X1)|~ssList(X1)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f4907,plain,(
% 10.14/1.77    sQ344_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f4880,f4904,f573])).
% 10.14/1.77  fof(f5008,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(nil)|~ssList(X0)|~ssList(X1)|~frontsegP(nil,X0)|~frontsegP(X0,X1)|~ssList(X1)|nil=X1)),
% 10.14/1.77    inference(resolution,[status(thm)],[f282,f298])).
% 10.14/1.77  fof(f5013,definition,(
% 10.14/1.77    ![X0,X1]: (sQ345_spl <=> (~ssList(X0)|~ssList(X1)|~frontsegP(nil,X0)|~frontsegP(X0,X1)|~ssList(X1)|nil=X1))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5016,plain,(
% 10.14/1.77    ~sQ13_spl|sQ345_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5008,f573,f5013])).
% 10.14/1.77  fof(f5400,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f284,f295])).
% 10.14/1.77  fof(f5407,definition,(
% 10.14/1.77    sQ353_spl <=> (sK50_skl=sK50_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5413,definition,(
% 10.14/1.77    sQ354_spl <=> (sK49_skl=sK49_skl)),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5422,definition,(
% 10.14/1.77    ![X0]: (sQ356_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|nil=X0|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5425,plain,(
% 10.14/1.77    ~sQ13_spl|sQ356_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5400,f573,f5422])).
% 10.14/1.77  fof(f5432,plain,(
% 10.14/1.77    ![X0]: (~ssList(sK50_skl)|~ssList(nil)|~ssList(X0)|frontsegP(app(sK50_skl,X0),nil)|~sQ178_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f288,f2819])).
% 10.14/1.77  fof(f5433,plain,(
% 10.14/1.77    ![X0]: (~ssList(sK50_skl)|~ssList(sK50_skl)|~ssList(X0)|frontsegP(app(sK50_skl,X0),sK50_skl)|~sQ176_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f288,f2811])).
% 10.14/1.77  fof(f5435,plain,(
% 10.14/1.77    ![X0]: (~ssList(sK49_skl)|~ssList(sK49_skl)|~ssList(X0)|frontsegP(app(sK49_skl,X0),sK49_skl)|~sQ23_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f288,f665])).
% 10.14/1.77  fof(f5436,plain,(
% 10.14/1.77    ![X0]: (~ssList(sK49_skl)|~ssList(nil)|~ssList(X0)|frontsegP(app(sK49_skl,X0),nil)|~sQ17_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f288,f622])).
% 10.14/1.77  fof(f5437,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(nil)|~ssList(X0)|frontsegP(app(nil,X0),nil)|~sQ20_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f288,f640])).
% 10.14/1.77  fof(f5438,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|frontsegP(app(X0,X1),nil)|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f288,f295])).
% 10.14/1.77  fof(f5441,definition,(
% 10.14/1.77    ![X0]: (sQ357_spl <=> (~ssList(X0)|frontsegP(app(sK50_skl,X0),nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5444,plain,(
% 10.14/1.77    ~sQ52_spl|~sQ13_spl|sQ357_spl|~sQ178_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5432,f1051,f573,f5441,f2818])).
% 10.14/1.77  fof(f5445,definition,(
% 10.14/1.77    ![X0]: (sQ358_spl <=> (~ssList(X0)|frontsegP(app(sK50_skl,X0),sK50_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5448,plain,(
% 10.14/1.77    ~sQ52_spl|sQ358_spl|~sQ176_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5433,f1051,f5445,f2810])).
% 10.14/1.77  fof(f5451,definition,(
% 10.14/1.77    ![X0]: (sQ359_spl <=> (~ssList(X0)|frontsegP(app(sK49_skl,X0),sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5454,plain,(
% 10.14/1.77    ~sQ16_spl|sQ359_spl|~sQ23_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5435,f609,f5451,f657])).
% 10.14/1.77  fof(f5455,definition,(
% 10.14/1.77    ![X0]: (sQ360_spl <=> (~ssList(X0)|frontsegP(app(sK49_skl,X0),nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5458,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ13_spl|sQ360_spl|~sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5436,f609,f573,f5455,f612])).
% 10.14/1.77  fof(f5459,definition,(
% 10.14/1.77    ![X0]: (sQ361_spl <=> (~ssList(X0)|frontsegP(app(nil,X0),nil)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5462,plain,(
% 10.14/1.77    ~sQ13_spl|sQ361_spl|~sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5437,f573,f5459,f632])).
% 10.14/1.77  fof(f5463,definition,(
% 10.14/1.77    ![X0,X1]: (sQ362_spl <=> (~ssList(X0)|~ssList(X1)|frontsegP(app(X0,X1),nil)|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5466,plain,(
% 10.14/1.77    sQ362_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5438,f5463,f573])).
% 10.14/1.77  fof(f5658,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(sK49_skl)|~ssList(sK49_skl)|frontsegP(cons(X0,sK49_skl),cons(X0,sK49_skl))|~sQ23_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f502,f665])).
% 10.14/1.77  fof(f5659,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(sK49_skl)|~ssList(nil)|frontsegP(cons(X0,sK49_skl),cons(X0,nil))|~sQ17_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f502,f622])).
% 10.14/1.77  fof(f5660,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|frontsegP(cons(X0,nil),cons(X0,nil))|~sQ20_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f502,f640])).
% 10.14/1.77  fof(f5661,plain,(
% 10.14/1.77    ![X0,X1]: (~ssItem(X0)|~ssList(X1)|~ssList(nil)|frontsegP(cons(X0,X1),cons(X0,nil))|~ssList(X1))),
% 10.14/1.77    inference(resolution,[status(thm)],[f502,f295])).
% 10.14/1.77  fof(f5666,definition,(
% 10.14/1.77    ![X0]: (sQ370_spl <=> (~ssItem(X0)|frontsegP(cons(X0,sK49_skl),cons(X0,sK49_skl))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5669,plain,(
% 10.14/1.77    sQ370_spl|~sQ16_spl|~sQ23_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5658,f5666,f609,f657])).
% 10.14/1.77  fof(f5670,definition,(
% 10.14/1.77    ![X0]: (sQ371_spl <=> (~ssItem(X0)|frontsegP(cons(X0,sK49_skl),cons(X0,nil))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5673,plain,(
% 10.14/1.77    sQ371_spl|~sQ16_spl|~sQ13_spl|~sQ17_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5659,f5670,f609,f573,f612])).
% 10.14/1.77  fof(f5674,definition,(
% 10.14/1.77    ![X0]: (sQ372_spl <=> (~ssItem(X0)|frontsegP(cons(X0,nil),cons(X0,nil))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5677,plain,(
% 10.14/1.77    sQ372_spl|~sQ13_spl|~sQ20_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5660,f5674,f573,f632])).
% 10.14/1.77  fof(f5678,definition,(
% 10.14/1.77    ![X0,X1]: (sQ373_spl <=> (~ssItem(X0)|~ssList(X1)|frontsegP(cons(X0,X1),cons(X0,nil))|~ssList(X1)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5681,plain,(
% 10.14/1.77    sQ373_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5661,f5678,f573])).
% 10.14/1.77  fof(f5685,plain,(
% 10.14/1.77    ![X0,X1]: (~ssList(nil)|~ssList(X0)|~ssList(X1)|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~ssList(X1)|nil=X1)),
% 10.14/1.77    inference(resolution,[status(thm)],[f301,f312])).
% 10.14/1.77  fof(f5688,definition,(
% 10.14/1.77    ![X0,X1]: (sQ374_spl <=> (~ssList(X0)|~ssList(X1)|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~ssList(X1)|nil=X1))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5691,plain,(
% 10.14/1.77    ~sQ13_spl|sQ374_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5685,f573,f5688])).
% 10.14/1.77  fof(f5695,plain,(
% 10.14/1.77    app(app(sK52_skl(sK51_skl,nil,sK49_skl),sK49_skl),sK53_skl(sK51_skl,sK50_skl,sK49_skl))=sK50_skl|~sQ1_spl|~sQ0_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f461,f1070])).
% 10.14/1.77  fof(f5696,plain,(
% 10.14/1.77    app(app(sK52_skl(sK51_skl,nil,sK49_skl),sK49_skl),sK53_skl(sK51_skl,nil,sK49_skl))=sK50_skl|~sQ1_spl|~sQ0_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f461,f5695])).
% 10.14/1.77  fof(f5697,plain,(
% 10.14/1.77    app(app(sK52_skl(sK51_skl,nil,sK49_skl),sK49_skl),sK53_skl(sK51_skl,nil,sK49_skl))=nil|~sQ1_spl|~sQ0_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f461,f5696])).
% 10.14/1.77  fof(f5698,plain,(
% 10.14/1.77    ~ssList(nil)|~ssList(sK49_skl)|segmentP(app(app(sK52_skl(sK51_skl,nil,sK49_skl),sK49_skl),sK53_skl(sK51_skl,nil,sK49_skl)),sK49_skl)|~ssList(sK52_skl(sK51_skl,nil,sK49_skl))|~ssList(sK53_skl(sK51_skl,nil,sK49_skl))|~sQ1_spl|~sQ0_spl),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f5697,f488])).
% 10.14/1.77  fof(f5703,definition,(
% 10.14/1.77    sQ375_spl <=> (segmentP(app(app(sK52_skl(sK51_skl,nil,sK49_skl),sK49_skl),sK53_skl(sK51_skl,nil,sK49_skl)),sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5704,plain,(
% 10.14/1.77    segmentP(app(app(sK52_skl(sK51_skl,nil,sK49_skl),sK49_skl),sK53_skl(sK51_skl,nil,sK49_skl)),sK49_skl)|~sQ375_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f5703])).
% 10.14/1.77  fof(f5706,definition,(
% 10.14/1.77    sQ376_spl <=> (ssList(sK52_skl(sK51_skl,nil,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5708,plain,(
% 10.14/1.77    ~ssList(sK52_skl(sK51_skl,nil,sK49_skl))|sQ376_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f5706])).
% 10.14/1.77  fof(f5709,definition,(
% 10.14/1.77    sQ377_spl <=> (ssList(sK53_skl(sK51_skl,nil,sK49_skl)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5711,plain,(
% 10.14/1.77    ~ssList(sK53_skl(sK51_skl,nil,sK49_skl))|sQ377_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f5709])).
% 10.14/1.77  fof(f5712,plain,(
% 10.14/1.77    ~sQ13_spl|~sQ16_spl|sQ375_spl|~sQ376_spl|~sQ377_spl|~sQ1_spl|~sQ0_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5698,f573,f609,f5703,f5706,f5709,f460,f457])).
% 10.14/1.77  fof(f5809,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|~ssList(sK49_skl)|~rearsegP(sK49_skl,sK49_skl)|sK49_skl=sK49_skl|~sQ30_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f303,f735])).
% 10.14/1.77  fof(f5812,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(X0)|~rearsegP(nil,X0)|nil=X0|~ssList(X0))),
% 10.14/1.77    inference(resolution,[status(thm)],[f303,f309])).
% 10.14/1.77  fof(f5824,plain,(
% 10.14/1.77    ~sQ16_spl|~sQ146_spl|sQ354_spl|~sQ30_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5809,f609,f2611,f5413,f729])).
% 10.14/1.77  fof(f5830,definition,(
% 10.14/1.77    ![X0]: (sQ387_spl <=> (~ssList(X0)|~rearsegP(nil,X0)|nil=X0|~ssList(X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5833,plain,(
% 10.14/1.77    ~sQ13_spl|sQ387_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5812,f573,f5830])).
% 10.14/1.77  fof(f5840,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(sK49_skl)|~rearsegP(nil,X0)|rearsegP(sK49_skl,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f654,f307])).
% 10.14/1.77  fof(f5841,plain,(
% 10.14/1.77    ![X0]: (~ssList(sK49_skl)|~ssList(X0)|~ssList(nil)|~rearsegP(sK49_skl,X0)|rearsegP(sK49_skl,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f597,f307])).
% 10.14/1.77  fof(f5842,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(nil)|~rearsegP(nil,X0)|rearsegP(nil,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f596,f307])).
% 10.14/1.77  fof(f5853,definition,(
% 10.14/1.77    ![X0]: (sQ389_spl <=> (~ssList(X0)|~rearsegP(nil,X0)|rearsegP(sK49_skl,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5856,plain,(
% 10.14/1.77    ~sQ13_spl|sQ389_spl|~sQ16_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5840,f573,f5853,f609])).
% 10.14/1.77  fof(f5857,definition,(
% 10.14/1.77    ![X0]: (sQ390_spl <=> (~ssList(X0)|~rearsegP(sK49_skl,X0)|rearsegP(sK49_skl,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5860,plain,(
% 10.14/1.77    ~sQ16_spl|sQ390_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5841,f609,f5857,f573])).
% 10.14/1.77  fof(f5861,definition,(
% 10.14/1.77    ![X0]: (sQ391_spl <=> (~ssList(X0)|~rearsegP(nil,X0)|rearsegP(nil,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5864,plain,(
% 10.14/1.77    ~sQ13_spl|sQ391_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5842,f573,f5861])).
% 10.14/1.77  fof(f5897,definition,(
% 10.14/1.77    sQ397_spl <=> (nil=cons(sK1_skl,nil))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f5898,plain,(
% 10.14/1.77    nil=cons(sK1_skl,nil)|~sQ397_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f5897])).
% 10.14/1.77  fof(f5901,plain,(
% 10.14/1.77    ~sP0_prd(sK51_skl,nil,sK49_skl)|sQ377_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f5711,f438])).
% 10.14/1.77  fof(f5902,plain,(
% 10.14/1.77    $false|~sQ3_spl|~sQ0_spl|sQ377_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f5901,f895])).
% 10.14/1.77  fof(f5903,plain,(
% 10.14/1.77    ~sQ3_spl|~sQ0_spl|sQ377_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f5902])).
% 10.14/1.77  fof(f5904,plain,(
% 10.14/1.77    segmentP(nil,sK49_skl)|~sQ1_spl|~sQ0_spl|~sQ375_spl),
% 10.14/1.77    inference(forward_demodulation,[status(thm)],[f5697,f5704])).
% 10.14/1.77  fof(f5905,plain,(
% 10.14/1.77    ~ssList(sK49_skl)|nil=sK49_skl|~sQ1_spl|~sQ0_spl|~sQ375_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f5904,f326])).
% 10.14/1.77  fof(f5912,plain,(
% 10.14/1.77    ~sQ16_spl|sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ375_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f5905,f609,f464,f460,f457,f5703])).
% 10.14/1.77  fof(f6146,plain,(
% 10.14/1.77    ~sP0_prd(sK51_skl,nil,sK49_skl)|sQ376_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f5708,f437])).
% 10.14/1.77  fof(f6147,plain,(
% 10.14/1.77    $false|~sQ3_spl|~sQ0_spl|sQ376_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f6146,f895])).
% 10.14/1.77  fof(f6148,plain,(
% 10.14/1.77    ~sQ3_spl|~sQ0_spl|sQ376_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f6147])).
% 10.14/1.77  fof(f6223,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(sK50_skl)|~ssList(nil)|frontsegP(cons(X0,sK50_skl),cons(X0,nil))|~sQ178_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f2819,f502])).
% 10.14/1.77  fof(f6230,definition,(
% 10.14/1.77    ![X0]: (sQ426_spl <=> (~ssItem(X0)|frontsegP(cons(X0,sK50_skl),cons(X0,nil))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f6233,plain,(
% 10.14/1.77    sQ426_spl|~sQ52_spl|~sQ13_spl|~sQ178_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f6223,f6230,f1051,f573,f2818])).
% 10.14/1.77  fof(f6240,plain,(
% 10.14/1.77    ![X0]: (~ssItem(X0)|~ssList(sK50_skl)|~ssList(sK50_skl)|frontsegP(cons(X0,sK50_skl),cons(X0,sK50_skl))|~sQ176_spl)),
% 10.14/1.77    inference(resolution,[status(thm)],[f2811,f502])).
% 10.14/1.77  fof(f6247,definition,(
% 10.14/1.77    ![X0]: (sQ427_spl <=> (~ssItem(X0)|frontsegP(cons(X0,sK50_skl),cons(X0,sK50_skl))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f6250,plain,(
% 10.14/1.77    sQ427_spl|~sQ52_spl|~sQ176_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f6240,f6247,f1051,f2810])).
% 10.14/1.77  fof(f6257,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(sK50_skl)|~rearsegP(sK50_skl,sK50_skl)|sK50_skl=sK50_skl|~sQ147_spl),
% 10.14/1.77    inference(resolution,[status(thm)],[f2616,f303])).
% 10.14/1.77  fof(f6260,plain,(
% 10.14/1.77    ~sQ52_spl|~sQ147_spl|sQ353_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f6257,f1051,f2615,f5407])).
% 10.14/1.77  fof(f6991,plain,(
% 10.14/1.77    ![X0]: (~ssList(sK50_skl)|~ssList(X0)|~ssList(nil)|~rearsegP(sK50_skl,X0)|rearsegP(sK50_skl,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f821,f307])).
% 10.14/1.77  fof(f6995,definition,(
% 10.14/1.77    ![X0]: (sQ456_spl <=> (~ssList(X0)|~rearsegP(sK50_skl,X0)|rearsegP(sK50_skl,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f6998,plain,(
% 10.14/1.77    ~sQ52_spl|sQ456_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f6991,f1051,f6995,f573])).
% 10.14/1.77  fof(f7003,plain,(
% 10.14/1.77    ![X0]: (~ssList(nil)|~ssList(X0)|~ssList(sK50_skl)|~rearsegP(nil,X0)|rearsegP(sK50_skl,X0))),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f820,f307])).
% 10.14/1.77  fof(f7008,definition,(
% 10.14/1.77    ![X0]: (sQ457_spl <=> (~ssList(X0)|~rearsegP(nil,X0)|rearsegP(sK50_skl,X0)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ457_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f7011,plain,(
% 10.14/1.77    ~sQ13_spl|sQ457_spl|~sQ52_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f7003,f573,f7008,f1051])).
% 10.14/1.77  fof(f7125,plain,(
% 10.14/1.77    ![X0,X1]: (~ssItem(sK55_skl(nil,X0,X1,app(app(X0,cons(X1,nil)),nil),cons(X1,nil)))|sP0_prd(X1,app(app(X0,cons(X1,nil)),nil),cons(X1,nil))|~ssItem(X1)|~ssList(X0)|~ssList(nil)|~sP2_prd(sK54_skl(nil,X0,X1,app(app(X0,cons(X1,nil)),nil),cons(X1,nil)),X0,X1))),
% 10.14/1.77    inference(resolution,[status(thm)],[f279,f513])).
% 10.14/1.77  fof(f7126,definition,(
% 10.14/1.77    ![X0,X1]: (sQ464_spl <=> (~ssItem(sK55_skl(nil,X0,X1,app(app(X0,cons(X1,nil)),nil),cons(X1,nil)))|sP0_prd(X1,app(app(X0,cons(X1,nil)),nil),cons(X1,nil))|~ssItem(X1)|~ssList(X0)|~sP2_prd(sK54_skl(nil,X0,X1,app(app(X0,cons(X1,nil)),nil),cons(X1,nil)),X0,X1)))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f7129,plain,(
% 10.14/1.77    sQ464_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f7125,f7126,f573])).
% 10.14/1.77  fof(f7388,definition,(
% 10.14/1.77    sQ490_spl <=> (nil=cons(sK1_skl,sK50_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f7389,plain,(
% 10.14/1.77    nil=cons(sK1_skl,sK50_skl)|~sQ490_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f7388])).
% 10.14/1.77  fof(f7392,plain,(
% 10.14/1.77    $false|~sQ490_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f7389,f1627])).
% 10.14/1.77  fof(f7393,plain,(
% 10.14/1.77    ~sQ490_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f7392])).
% 10.14/1.77  fof(f7408,plain,(
% 10.14/1.77    $false|~sQ397_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f5898,f684])).
% 10.14/1.77  fof(f7409,plain,(
% 10.14/1.77    ~sQ397_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f7408])).
% 10.14/1.77  fof(f7725,plain,(
% 10.14/1.77    ![X0,X1]: (sP0_prd(X0,app(app(X1,cons(X0,nil)),nil),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|~ssList(nil)|ssItem(sK54_skl(nil,X1,X0,app(app(X1,cons(X0,nil)),nil),cons(X0,nil)))|~ssItem(sK55_skl(nil,X1,X0,app(app(X1,cons(X0,nil)),nil),cons(X0,nil))))),
% 10.14/1.77    inference(resolution,[status(thm)],[f1234,f279])).
% 10.14/1.77  fof(f7728,definition,(
% 10.14/1.77    ![X0,X1]: (sQ534_spl <=> (sP0_prd(X0,app(app(X1,cons(X0,nil)),nil),cons(X0,nil))|~ssItem(X0)|~ssList(X1)|ssItem(sK54_skl(nil,X1,X0,app(app(X1,cons(X0,nil)),nil),cons(X0,nil)))|~ssItem(sK55_skl(nil,X1,X0,app(app(X1,cons(X0,nil)),nil),cons(X0,nil)))))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ534_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f7731,plain,(
% 10.14/1.77    sQ534_spl|~sQ13_spl),
% 10.14/1.77    inference(split_clause,[status(thm)],[f7725,f7728,f573])).
% 10.14/1.77  fof(f7793,plain,(
% 10.14/1.77    $false|sQ116_spl),
% 10.14/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2231,f103])).
% 10.14/1.77  fof(f7794,plain,(
% 10.14/1.77    sQ116_spl),
% 10.14/1.77    inference(contradiction_clause,[status(thm)],[f7793])).
% 10.14/1.77  fof(f7886,plain,(
% 10.14/1.77    ~ssList(sK50_skl)|~ssList(sK49_skl)|segmentP(app(app(sK52_skl(sK51_skl,sK50_skl,sK49_skl),sK49_skl),sK53_skl(sK51_skl,sK50_skl,sK49_skl)),sK49_skl)|~ssList(sK52_skl(sK51_skl,sK50_skl,sK49_skl))|~ssList(sK53_skl(sK51_skl,sK50_skl,sK49_skl))|~sQ0_spl),
% 10.14/1.77    inference(paramodulation,[status(thm)],[f1258,f488])).
% 10.14/1.77  fof(f7891,definition,(
% 10.14/1.77    sQ553_spl <=> (segmentP(app(app(sK52_skl(sK51_skl,sK50_skl,sK49_skl),sK49_skl),sK53_skl(sK51_skl,sK50_skl,sK49_skl)),sK49_skl))),
% 10.14/1.77    introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition])).
% 10.14/1.77  fof(f7892,plain,(
% 10.14/1.77    segmentP(app(app(sK52_skl(sK51_skl,sK50_skl,sK49_skl),sK49_skl),sK53_skl(sK51_skl,sK50_skl,sK49_skl)),sK49_skl)|~sQ553_spl),
% 10.14/1.77    inference(component_clause,[status(thm)],[f7891])).
% 10.14/1.78  fof(f7894,definition,(
% 10.14/1.78    sQ554_spl <=> (ssList(sK52_skl(sK51_skl,sK50_skl,sK49_skl)))),
% 10.14/1.78    introduced(definition,[new_symbols(definition,[sQ554_spl])],[split_symbol_definition])).
% 10.14/1.78  fof(f7896,plain,(
% 10.14/1.78    ~ssList(sK52_skl(sK51_skl,sK50_skl,sK49_skl))|sQ554_spl),
% 10.14/1.78    inference(component_clause,[status(thm)],[f7894])).
% 10.14/1.78  fof(f7897,definition,(
% 10.14/1.78    sQ555_spl <=> (ssList(sK53_skl(sK51_skl,sK50_skl,sK49_skl)))),
% 10.14/1.78    introduced(definition,[new_symbols(definition,[sQ555_spl])],[split_symbol_definition])).
% 10.14/1.78  fof(f7899,plain,(
% 10.14/1.78    ~ssList(sK53_skl(sK51_skl,sK50_skl,sK49_skl))|sQ555_spl),
% 10.14/1.78    inference(component_clause,[status(thm)],[f7897])).
% 10.14/1.78  fof(f7900,plain,(
% 10.14/1.78    ~sQ52_spl|~sQ16_spl|sQ553_spl|~sQ554_spl|~sQ555_spl|~sQ0_spl),
% 10.14/1.78    inference(split_clause,[status(thm)],[f7886,f1051,f609,f7891,f7894,f7897,f457])).
% 10.14/1.78  fof(f7921,plain,(
% 10.14/1.78    segmentP(sK50_skl,sK49_skl)|~sQ0_spl|~sQ553_spl),
% 10.14/1.78    inference(forward_demodulation,[status(thm)],[f1258,f7892])).
% 10.14/1.78  fof(f7922,plain,(
% 10.14/1.78    $false|sQ6_spl|~sQ0_spl|~sQ553_spl),
% 10.14/1.78    inference(forward_subsumption_resolution,[status(thm)],[f7921,f2577])).
% 10.14/1.78  fof(f7923,plain,(
% 10.14/1.78    sQ6_spl|~sQ0_spl|~sQ553_spl),
% 10.14/1.78    inference(contradiction_clause,[status(thm)],[f7922])).
% 10.14/1.78  fof(f8031,plain,(
% 10.14/1.78    $false|sQ117_spl),
% 10.14/1.78    inference(forward_subsumption_resolution,[status(thm)],[f2238,f104])).
% 10.14/1.78  fof(f8032,plain,(
% 10.14/1.78    sQ117_spl),
% 10.14/1.78    inference(contradiction_clause,[status(thm)],[f8031])).
% 10.14/1.78  fof(f8118,plain,(
% 10.14/1.78    ~sP0_prd(sK51_skl,sK50_skl,sK49_skl)|sQ555_spl),
% 10.14/1.78    inference(resolution,[status(thm)],[f7899,f438])).
% 10.14/1.78  fof(f8119,plain,(
% 10.14/1.78    ~sQ0_spl|sQ555_spl),
% 10.14/1.78    inference(split_clause,[status(thm)],[f8118,f457,f7897])).
% 10.14/1.78  fof(f8120,plain,(
% 10.14/1.78    ~sP0_prd(sK51_skl,sK50_skl,sK49_skl)|sQ554_spl),
% 10.14/1.78    inference(resolution,[status(thm)],[f7896,f437])).
% 10.14/1.78  fof(f8121,plain,(
% 10.14/1.78    ~sQ0_spl|sQ554_spl),
% 10.14/1.78    inference(split_clause,[status(thm)],[f8120,f457,f7894])).
% 10.14/1.78  fof(f8122,plain,(
% 10.14/1.78    $false),
% 10.14/1.78    inference(sat_refutation,[status(thm)],[f463,f467,f474,f481,f555,f570,f579,f581,f604,f615,f619,f621,f628,f635,f639,f646,f660,f664,f671,f707,f715,f724,f728,f732,f741,f745,f751,f755,f767,f771,f817,f859,f867,f875,f947,f952,f1054,f1058,f1060,f1068,f1198,f1256,f1429,f1436,f1593,f1609,f1931,f2232,f2239,f2569,f2579,f2580,f2606,f2610,f2614,f2618,f2622,f2628,f2632,f2638,f2642,f2809,f2813,f2817,f2821,f2825,f2844,f2849,f3138,f3142,f3146,f3148,f3497,f3501,f3505,f3507,f3548,f3552,f3559,f3566,f3573,f3580,f3587,f3594,f3607,f3611,f3617,f3621,f3625,f3629,f3646,f3650,f3656,f3660,f3664,f3668,f3744,f3748,f3752,f3754,f3873,f3877,f4734,f4885,f4889,f4895,f4899,f4903,f4907,f5016,f5425,f5444,f5448,f5454,f5458,f5462,f5466,f5669,f5673,f5677,f5681,f5691,f5712,f5824,f5833,f5856,f5860,f5864,f5903,f5912,f6148,f6233,f6250,f6260,f6998,f7011,f7129,f7393,f7409,f7731,f7794,f7900,f7923,f8032,f8119,f8121])).
% 10.14/1.78  % SZS output end CNFRefutation for theBenchmark.p
% 10.14/1.79  % Elapsed time: 1.406054 seconds
% 10.14/1.79  % CPU time: 10.675717 seconds
% 10.14/1.79  % Total memory used: 225.171 MB
% 10.14/1.79  % Net memory used: 216.236 MB
%------------------------------------------------------------------------------