%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC376-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:40:59 PM UTC 2026
% Result : Unsatisfiable 149.36s 19.31s
% Output : CNFRefutation 140.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 263
% Syntax : Number of formulae : 886 ( 35 unt; 186 def)
% Number of atoms : 3675 ( 447 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 5248 (2459 ~;2603 |; 0 &)
% ( 186 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 203 ( 201 usr; 187 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-2 aty)
% Number of variables : 793 ( 793 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] : ssList(skaf73(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] : ssItem(skaf70(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [U] : ssItem(skaf59(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [U] :
( frontsegP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [U] :
( leq(U,U)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ rearsegP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [U] :
( frontsegP(nil,U)
| ~ ssList(U)
| nil != U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ frontsegP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = V
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [U,V] :
( hd(cons(U,V)) = U
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [U,V] :
( ~ ssItem(V)
| ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [U,V] :
( singletonP(V)
| ~ ssList(V)
| ~ ssItem(U)
| cons(U,nil) != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [U,V] :
( U = V
| lt(U,V)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ leq(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [U,V] :
( hd(app(V,U)) = hd(V)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [U,V] :
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [U,V] :
( nil = V
| lt(U,hd(V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ strictorderedP(cons(U,V)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,axiom,
! [U,V] :
( nil = V
| leq(U,hd(V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ totalorderedP(cons(U,V)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,axiom,
! [U,V,W] :
( rearsegP(app(W,U),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [U,V,W] :
( memberP(cons(W,U),V)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [U,V,W] :
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W] :
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [U,V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != W ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [U,V] :
( app(U,V) = nil
| ~ ssList(U)
| ~ ssList(V)
| nil != V
| nil != U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [U,V,W] :
( lt(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ lt(V,W)
| ~ leq(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [U,V,W] :
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,axiom,
! [U,V,W] :
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,axiom,
! [U,V,W] :
( frontsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,axiom,
! [U,V,W] :
( leq(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ leq(V,W)
| ~ leq(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f157,axiom,
! [U,V,W] :
( cons(U,app(V,W)) = app(cons(U,V),W)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [U,V,W] :
( memberP(U,W)
| memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [U,V,W] :
( W = U
| memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
! [U,V] :
( app(app(skaf47(U,V),V),skaf48(V,U)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
! [U,V,W,X] :
( U = W
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [U,V,W,X] :
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [U,V,W,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f177,axiom,
! [U,V] :
( nil = U
| U = V
| nil = V
| ~ ssList(V)
| ~ ssList(U)
| hd(U) != hd(V)
| tl(U) != tl(V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,axiom,
! [U,V,W,X,Y,Z] :
( lt(V,X)
| ~ ssList(Z)
| ~ strictorderedP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
! [U,V,W,X,Y,Z] :
( leq(V,X)
| ~ ssList(Z)
| ~ totalorderedP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,axiom,
! [U,V,W,X,Y,Z] :
( lt(X,V)
| lt(V,X)
| ~ ssList(Z)
| ~ strictorderP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f184,axiom,
! [U,V,W,X,Y,Z] :
( leq(X,V)
| leq(V,X)
| ~ ssList(Z)
| ~ totalorderP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,axiom,
! [U,V,W,X,Y,Z] :
( ~ ssList(Z)
| ~ cyclefreeP(Z)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(X)
| ~ ssList(Y)
| app(app(W,cons(U,X)),cons(V,Y)) != Z
| ~ leq(V,U)
| ~ leq(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
( memberP(sk1,sk5)
| memberP(sk2,sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
( ~ memberP(sk1,sk5)
| ~ memberP(sk2,sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
! [A,B,C,D] :
( ~ neq(nil,sk3)
| ~ neq(nil,sk3)
| hd(sk3) != D
| cons(D,nil) != C
| ~ ssItem(D)
| app(B,C) != A
| tl(sk3) != B
| ~ ssList(C)
| ~ ssList(B)
| sk4 = A
| ~ ssList(A)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f209,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f210,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f219,plain,
! [X0] : ssList(skaf73(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f222,plain,
! [X0] : ssItem(skaf70(X0)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f233,plain,
! [X0] : ssItem(skaf59(X0)),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f253,plain,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,nil) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f254,plain,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f257,plain,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f258,plain,
! [X0] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f259,plain,
! [X0] :
( ~ ssItem(X0)
| leq(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f268,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f271,plain,
! [X0] :
( X0 = app(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f272,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f275,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ssList(tl(X0)) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f276,plain,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f280,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ rearsegP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f281,plain,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f282,plain,
! [X0] :
( ~ ssList(X0)
| ~ frontsegP(nil,X0)
| nil = X0 ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f283,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f284,plain,
! [X0,X1] :
( ~ ssList(X1)
| ssList(cons(X0,X1))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f294,plain,
! [X0,X1] :
( ~ ssItem(X1)
| X0 = tl(cons(X1,X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f295,plain,
! [X0,X1] :
( X0 = hd(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f296,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f297,plain,
! [X0,X1] :
( ~ ssList(X1)
| cons(X0,X1) != nil
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f298,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f299,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| X0 != cons(X1,X0) ),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
! [X0,X1] :
( X0 = X1
| ~ ssList(X1)
| neq(X1,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f304,plain,
! [X0] :
( X0 = cons(hd(X0),tl(X0))
| ~ ssList(X0)
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f309,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0 ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f316,plain,
! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ) ),
inference(miniscoping,[status(thm)],[f114]) ).
fof(f317,plain,
! [X0,X1] :
( ~ lt(X1,X0)
| ~ ssItem(X1)
| ~ lt(X0,X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
! [U] :
( ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ neq(U,V)
| U != V ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f319,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ neq(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f320,plain,
! [V] :
( singletonP(V)
| ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,nil) != V ) ),
inference(miniscoping,[status(thm)],[f116]) ).
fof(f321,plain,
! [X0,X1] :
( singletonP(X1)
| ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,nil) != X1 ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f324,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f325,plain,
! [X0,X1] :
( ~ ssList(X1)
| app(X0,X1) != nil
| ~ ssList(X0)
| nil = X0 ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f327,plain,
! [X0,X1] :
( ~ ssList(X1)
| X1 = nil
| ~ ssList(X0)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f330,plain,
! [X0,X1] :
( lt(X0,X1)
| X0 = X1
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f331,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| hd(app(X0,X1)) = hd(X0)
| nil = X0 ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f339,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| X1 = X0
| ~ frontsegP(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f343,plain,
! [X0,X1] :
( tl(app(X0,X1)) = app(tl(X0),X1)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f344,plain,
! [V] :
( nil = V
| ! [U] :
( lt(U,hd(V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ strictorderedP(cons(U,V)) ) ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(f345,plain,
! [X0,X1] :
( X1 = nil
| lt(X0,hd(X1))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ strictorderedP(cons(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f346,plain,
! [V] :
( nil = V
| ! [U] :
( leq(U,hd(V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ totalorderedP(cons(U,V)) ) ),
inference(miniscoping,[status(thm)],[f135]) ).
fof(f347,plain,
! [X0,X1] :
( nil = X1
| leq(X0,hd(X1))
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ totalorderedP(cons(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f348,plain,
! [X0,X1,X2] :
( rearsegP(app(X1,X0),X2)
| ~ rearsegP(X0,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f349,plain,
! [X0,X1,X2] :
( ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X2)
| frontsegP(app(X0,X1),X2)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f350,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f351,plain,
! [X0,X1,X2] :
( ~ ssList(X0)
| ~ ssItem(X2)
| memberP(cons(X2,X0),X1)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f352,plain,
! [X0,X1,X2] :
( ~ ssList(X1)
| ~ ssItem(X2)
| memberP(app(X1,X0),X2)
| ~ memberP(X1,X2)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f353,plain,
! [X0,X1,X2] :
( ~ ssItem(X2)
| ~ ssList(X1)
| ~ memberP(X1,X2)
| memberP(app(X0,X1),X2)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f355,plain,
! [V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f356,plain,
! [X0,X1,X2] :
( rearsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f359,plain,
! [X0,X1] :
( app(X0,X1) = nil
| ~ ssList(X0)
| ~ ssList(X1)
| nil != X1
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f362,plain,
! [U,W] :
( lt(U,W)
| ~ ssItem(U)
| ! [V] :
( ~ ssItem(V)
| ~ ssItem(W)
| ~ lt(V,W)
| ~ leq(U,V) ) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f363,plain,
! [X0,X1,X2] :
( ~ ssItem(X2)
| ~ ssItem(X0)
| lt(X0,X2)
| ~ lt(X1,X2)
| ~ ssItem(X1)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f366,plain,
! [X0,X1,X2] :
( ~ ssList(X1)
| ~ ssList(X2)
| app(X1,app(X0,X2)) = app(app(X1,X0),X2)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f367,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f368,plain,
! [X0,X1,X2] :
( X2 = X0
| ~ ssList(X2)
| app(X1,X0) != app(X1,X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f369,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f370,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ ssList(X1)
| X1 = X0
| app(X1,X2) != app(X0,X2)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f375,plain,
! [U,W] :
( frontsegP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V) ) ),
inference(miniscoping,[status(thm)],[f154]) ).
fof(f376,plain,
! [X0,X1,X2] :
( ~ frontsegP(X2,X1)
| frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f379,plain,
! [U,W] :
( leq(U,W)
| ~ ssItem(U)
| ! [V] :
( ~ ssItem(V)
| ~ ssItem(W)
| ~ leq(V,W)
| ~ leq(U,V) ) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f380,plain,
! [X0,X1,X2] :
( ~ ssItem(X2)
| ~ ssItem(X1)
| ~ leq(X2,X0)
| ~ leq(X1,X2)
| leq(X1,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f381,plain,
! [X0,X1,X2] :
( ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| cons(X0,app(X1,X2)) = app(cons(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f382,plain,
! [U,W] :
( memberP(U,W)
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f158]) ).
fof(f383,plain,
! [X0,X1,X2] :
( memberP(X2,X0)
| memberP(X1,X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ memberP(app(X1,X2),X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f388,plain,
! [U,W] :
( W = U
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f389,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssItem(X2)
| memberP(X1,X2)
| ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f396,plain,
! [X0,X1] :
( ~ ssList(X1)
| X1 = app(app(skaf47(X1,X0),X0),skaf48(X0,X1))
| ~ segmentP(X1,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f398,plain,
! [U,W] :
( U = W
| ! [V] :
( ~ ssList(V)
| ! [X] :
( ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f399,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ ssItem(X3)
| cons(X2,X1) != cons(X3,X0)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f402,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X2)
| ~ ssList(X3)
| segmentP(app(app(X3,X2),X0),X1)
| ~ segmentP(X2,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f403,plain,
! [V,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(app(U,V),W) != X ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f404,plain,
! [X0,X1,X2,X3] :
( segmentP(X3,X1)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(app(X0,X1),X2) != X3 ),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f407,plain,
! [V,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(U,cons(V,W)) != X ) ) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f408,plain,
! [X0,X1,X2,X3] :
( memberP(X3,X1)
| ~ ssList(X3)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(X0,cons(X1,X2)) != X3 ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f411,plain,
! [U] :
( nil = U
| ! [V] :
( U = V
| nil = V
| ~ ssList(V)
| ~ ssList(U)
| hd(U) != hd(V)
| tl(U) != tl(V) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f412,plain,
! [X0,X1] :
( ~ ssList(X1)
| tl(X1) != tl(X0)
| X1 = X0
| X0 = nil
| nil = X1
| hd(X0) != hd(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f411]) ).
fof(f418,plain,
! [V,X] :
( lt(V,X)
| ! [Z] :
( ~ ssList(Z)
| ~ strictorderedP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [Y] :
( ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ) ) ) ) ),
inference(miniscoping,[status(thm)],[f181]) ).
fof(f419,plain,
! [X0,X1,X2,X3,X4,X5] :
( lt(X1,X3)
| ~ ssList(X5)
| ~ strictorderedP(X5)
| ~ ssItem(X1)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X4)
| app(app(X0,cons(X1,X2)),cons(X3,X4)) != X5 ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f420,plain,
! [V,X] :
( leq(V,X)
| ! [Z] :
( ~ ssList(Z)
| ~ totalorderedP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [Y] :
( ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ) ) ) ) ),
inference(miniscoping,[status(thm)],[f182]) ).
fof(f421,plain,
! [X0,X1,X2,X3,X4,X5] :
( leq(X1,X3)
| ~ ssList(X5)
| ~ totalorderedP(X5)
| ~ ssItem(X1)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X4)
| app(app(X0,cons(X1,X2)),cons(X3,X4)) != X5 ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f422,plain,
! [V,X] :
( lt(X,V)
| lt(V,X)
| ! [Z] :
( ~ ssList(Z)
| ~ strictorderP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [Y] :
( ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ) ) ) ) ),
inference(miniscoping,[status(thm)],[f183]) ).
fof(f423,plain,
! [X0,X1,X2,X3,X4,X5] :
( lt(X3,X1)
| lt(X1,X3)
| ~ ssList(X5)
| ~ strictorderP(X5)
| ~ ssItem(X1)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X4)
| app(app(X0,cons(X1,X2)),cons(X3,X4)) != X5 ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f424,plain,
! [V,X] :
( leq(X,V)
| leq(V,X)
| ! [Z] :
( ~ ssList(Z)
| ~ totalorderP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [Y] :
( ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ) ) ) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f425,plain,
! [X0,X1,X2,X3,X4,X5] :
( leq(X3,X1)
| leq(X1,X3)
| ~ ssList(X5)
| ~ totalorderP(X5)
| ~ ssItem(X1)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X4)
| app(app(X0,cons(X1,X2)),cons(X3,X4)) != X5 ),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f426,plain,
! [Z] :
( ~ ssList(Z)
| ~ cyclefreeP(Z)
| ! [U] :
( ~ ssItem(U)
| ! [V] :
( ~ ssItem(V)
| ! [W] :
( ~ ssList(W)
| ! [X] :
( ~ ssList(X)
| ! [Y] :
( ~ ssList(Y)
| app(app(W,cons(U,X)),cons(V,Y)) != Z
| ~ leq(V,U)
| ~ leq(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f185]) ).
fof(f427,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ ssList(X5)
| ~ cyclefreeP(X5)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| app(app(X2,cons(X0,X3)),cons(X1,X4)) != X5
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f426]) ).
fof(f428,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f431,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f432,plain,
sk4 = sk2,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f433,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f434,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f435,plain,
( memberP(sk1,sk5)
| memberP(sk2,sk5) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f436,plain,
( ~ memberP(sk1,sk5)
| ~ memberP(sk2,sk5) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f437,plain,
( nil != sk4
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f438,plain,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f439,plain,
( ~ neq(nil,sk3)
| ~ neq(nil,sk3)
| ! [D] :
( hd(sk3) != D
| ! [C] :
( cons(D,nil) != C
| ~ ssItem(D)
| ! [A,B] :
( app(B,C) != A
| tl(sk3) != B
| ~ ssList(C)
| ~ ssList(B)
| sk4 = A
| ~ ssList(A)
| ~ neq(sk4,nil) ) ) ) ),
inference(miniscoping,[status(thm)],[f197]) ).
fof(f440,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,sk3)
| ~ neq(nil,sk3)
| hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f448,definition,
( sQ2_spl
<=> memberP(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ2_spl
| memberP(sk2,sk5) ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f450,plain,
( sQ2_spl
| ~ memberP(sk2,sk5) ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
( sQ3_spl
<=> memberP(sk1,sk5) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ3_spl
| memberP(sk1,sk5) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f453,plain,
( sQ3_spl
| ~ memberP(sk1,sk5) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f435,f448,f451]) ).
fof(f455,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f436,f448,f451]) ).
fof(f456,definition,
( sQ4_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( ~ sQ4_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
( sQ5_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( ~ sQ5_spl
| sk4 = nil ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,plain,
( ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f437,f456,f459]) ).
fof(f463,definition,
( sQ6_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( sQ6_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,definition,
( sQ7_spl
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ7_spl
| neq(sk3,nil) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f438,f463,f466]) ).
fof(f470,definition,
! [X0,X1,X2,X3] :
( sQ8_spl
<=> ( hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f471,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,definition,
( sQ9_spl
<=> neq(nil,sk3) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ9_spl
| ~ neq(nil,sk3) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,plain,
( ~ sQ9_spl
| sQ8_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f440,f463,f470,f473]) ).
fof(f477,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(X4)
| ~ ssList(app(app(X4,cons(X2,X3)),cons(X1,X0)))
| ~ strictorderP(app(app(X4,cons(X2,X3)),cons(X1,X0)))
| ~ ssItem(X1)
| ~ ssList(X3)
| lt(X2,X1)
| ~ ssItem(X2)
| lt(X1,X2)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f423]) ).
fof(f478,plain,
! [X0,X1] :
( ~ ssList(X1)
| rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f356]) ).
fof(f481,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f281]) ).
fof(f482,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X3)
| lt(X1,X3)
| ~ ssList(X0)
| ~ ssList(X4)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(destructive_equality_resolution,[status(thm)],[f419]) ).
fof(f483,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(X1)
| leq(X2,X0)
| ~ ssList(X4)
| leq(X0,X2)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssList(app(app(X1,cons(X2,X3)),cons(X0,X4)))
| ~ totalorderP(app(app(X1,cons(X2,X3)),cons(X0,X4)))
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f425]) ).
fof(f484,plain,
! [X0] :
( ~ ssList(cons(X0,nil))
| ~ ssItem(X0)
| singletonP(cons(X0,nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f321]) ).
fof(f486,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f350]) ).
fof(f487,plain,
! [X0,X1] :
( ~ ssItem(X1)
| memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f486]) ).
fof(f488,plain,
( app(nil,nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f359]) ).
fof(f489,plain,
( nil = app(nil,nil)
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f488]) ).
fof(f490,plain,
! [X0,X1,X2] :
( segmentP(app(app(X0,X1),X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f404]) ).
fof(f491,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssItem(X1)
| ~ leq(X1,X0)
| ~ cyclefreeP(app(app(X2,cons(X1,X3)),cons(X0,X4)))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X4)
| ~ ssList(app(app(X2,cons(X1,X3)),cons(X0,X4)))
| ~ leq(X0,X1)
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f427]) ).
fof(f493,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssItem(X2)
| ~ ssList(X3)
| ~ totalorderedP(app(app(X1,cons(X2,X3)),cons(X0,X4)))
| leq(X2,X0)
| ~ ssList(X1)
| ~ ssList(X4)
| ~ ssList(app(app(X1,cons(X2,X3)),cons(X0,X4)))
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f421]) ).
fof(f497,plain,
! [X0,X1,X2] :
( ~ ssList(X1)
| ~ ssList(app(X1,cons(X0,X2)))
| ~ ssList(X2)
| memberP(app(X1,cons(X0,X2)),X0)
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f408]) ).
fof(f499,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f500,plain,
! [X0] :
( ~ neq(X0,X0)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f499]) ).
fof(f511,plain,
( sQ2_spl
| ~ memberP(sk4,sk5) ),
inference(forward_demodulation,[status(thm)],[f432,f450]) ).
fof(f514,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f516,f452]) ).
fof(f516,plain,
( ~ sQ4_spl
| nil = sk1 ),
inference(forward_demodulation,[status(thm)],[f433,f457]) ).
fof(f517,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f268,f514]) ).
fof(f518,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f517,f434]) ).
fof(f519,plain,
( ~ sQ3_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f518]) ).
fof(f520,plain,
( ~ sQ2_spl
| memberP(sk4,sk5) ),
inference(forward_demodulation,[status(thm)],[f432,f449]) ).
fof(f525,definition,
( sQ11_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f527,plain,
( sQ11_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f550,plain,
( sQ6_spl
| ~ ssList(nil)
| ~ ssList(sk4)
| sk4 = nil ),
inference(resolution,[status(thm)],[f300,f465]) ).
fof(f553,definition,
( sQ17_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ17_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,plain,
( sQ6_spl
| ~ sQ11_spl
| ~ sQ17_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f550,f459,f553,f525,f463]) ).
fof(f557,plain,
( sQ9_spl
| ~ neq(nil,sk1) ),
inference(forward_demodulation,[status(thm)],[f433,f475]) ).
fof(f558,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f431]) ).
fof(f559,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f558]) ).
fof(f560,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f527,f205]) ).
fof(f561,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f560]) ).
fof(f563,plain,
( ~ sQ7_spl
| neq(sk1,nil) ),
inference(forward_demodulation,[status(thm)],[f433,f467]) ).
fof(f564,plain,
( sQ9_spl
| ~ ssList(sk1)
| ~ ssList(nil)
| nil = sk1 ),
inference(resolution,[status(thm)],[f557,f300]) ).
fof(f566,definition,
( sQ18_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( ~ sQ18_spl
| sk1 = nil ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f573,definition,
( sQ20_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f575,plain,
( sQ20_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f573]) ).
fof(f576,plain,
( sQ9_spl
| ~ sQ20_spl
| ~ sQ11_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f564,f566,f525,f573,f473]) ).
fof(f577,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f575,f428]) ).
fof(f578,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f577]) ).
fof(f579,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk1) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f433,f471]) ).
fof(f580,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| hd(sk1) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk1) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f433,f579]) ).
fof(f581,plain,
( ~ sQ8_spl
| ~ ssItem(hd(sk1))
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1))
| sk4 = app(tl(sk1),cons(hd(sk1),nil))
| ~ ssList(app(tl(sk1),cons(hd(sk1),nil))) ),
inference(destructive_equality_resolution,[status(thm)],[f580]) ).
fof(f582,plain,
( ~ sQ8_spl
| app(tl(sk1),cons(hd(sk1),nil)) = sk4
| ~ ssItem(hd(sk1))
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f581,f283]) ).
fof(f585,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f516,f563]) ).
fof(f586,plain,
( sQ3_spl
| ~ sQ4_spl
| ~ memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f516,f453]) ).
fof(f591,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f585,f500]) ).
fof(f592,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f591,f525,f456,f466]) ).
fof(f599,definition,
( sQ22_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f601,plain,
( sQ22_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f608,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f460,f520]) ).
fof(f612,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sQ3_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f608,f586]) ).
fof(f613,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sQ3_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f612]) ).
fof(f614,definition,
( sQ23_spl
<=> ssList(tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f615,plain,
( ~ sQ23_spl
| ssList(tl(sk1)) ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f616,plain,
( sQ23_spl
| ~ ssList(tl(sk1)) ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f617,definition,
( sQ24_spl
<=> ssList(cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f618,plain,
( ~ sQ24_spl
| ssList(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f619,plain,
( sQ24_spl
| ~ ssList(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f620,definition,
( sQ25_spl
<=> ssItem(hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( sQ25_spl
| ~ ssItem(hd(sk1)) ),
inference(component_clause,[status(thm)],[f620]) ).
fof(f623,definition,
( sQ26_spl
<=> app(tl(sk1),cons(hd(sk1),nil)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f624,plain,
( ~ sQ26_spl
| app(tl(sk1),cons(hd(sk1),nil)) = sk4 ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f626,plain,
( ~ sQ8_spl
| sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f582,f614,f617,f620,f623,f470]) ).
fof(f627,plain,
( sQ25_spl
| ~ ssList(sk1)
| nil = sk1 ),
inference(resolution,[status(thm)],[f622,f276]) ).
fof(f628,plain,
( sQ25_spl
| ~ sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f627,f566,f573,f620]) ).
fof(f633,definition,
( sQ28_spl
<=> cons(skaf70(nil),skaf73(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( ~ sQ28_spl
| cons(skaf70(nil),skaf73(nil)) = nil ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f647,plain,
( sQ23_spl
| nil = sk1
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f616,f275]) ).
fof(f648,plain,
( sQ23_spl
| sQ18_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f647,f573,f566,f614]) ).
fof(f649,plain,
( sQ24_spl
| ~ ssItem(hd(sk1))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f619,f284]) ).
fof(f650,plain,
( sQ24_spl
| ~ sQ25_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f649,f525,f620,f617]) ).
fof(f653,plain,
( ~ ssList(nil)
| ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f271,f327]) ).
fof(f654,definition,
( sQ31_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ31_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f653,f525,f654]) ).
fof(f658,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ ssList(X1)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| ~ ssList(app(sk4,cons(X0,X1)))
| lt(hd(sk1),X0)
| ~ strictorderP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(tl(sk1))
| ~ ssList(nil)
| lt(X0,hd(sk1)) ),
inference(paramodulation,[status(thm)],[f624,f477]) ).
fof(f659,plain,
! [X0] :
( ~ sQ26_spl
| ~ ssItem(X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(tl(sk1),X0)
| ~ ssList(tl(sk1))
| memberP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f624,f352]) ).
fof(f660,plain,
! [X0] :
( ~ sQ26_spl
| ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1))
| memberP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f624,f353]) ).
fof(f662,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ ssList(X1)
| ~ segmentP(cons(hd(sk1),nil),X1)
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(X0)
| ~ ssList(tl(sk1))
| segmentP(app(sk4,X0),X1) ),
inference(paramodulation,[status(thm)],[f624,f402]) ).
fof(f663,plain,
( ~ sQ26_spl
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil))
| cons(hd(sk1),nil) = nil
| sk4 != nil ),
inference(paramodulation,[status(thm)],[f624,f327]) ).
fof(f664,definition,
( sQ32_spl
<=> cons(hd(sk1),nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f665,plain,
( ~ sQ32_spl
| cons(hd(sk1),nil) = nil ),
inference(component_clause,[status(thm)],[f664]) ).
fof(f667,plain,
( ~ sQ26_spl
| ~ sQ23_spl
| ~ sQ24_spl
| sQ32_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f663,f459,f664,f617,f614,f623]) ).
fof(f669,definition,
! [X0] :
( sQ33_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0)
| memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f670,plain,
! [X0] :
( ~ sQ33_spl
| ~ memberP(cons(hd(sk1),nil),X0)
| memberP(sk4,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f669]) ).
fof(f672,plain,
( ~ sQ26_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f660,f669,f614,f617,f623]) ).
fof(f673,definition,
! [X0,X1] :
( sQ34_spl
<=> ( ~ ssList(X1)
| ~ segmentP(cons(hd(sk1),nil),X1)
| ~ ssList(X0)
| segmentP(app(sk4,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f674,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ ssList(X0)
| segmentP(app(sk4,X1),X0)
| ~ ssList(X1)
| ~ segmentP(cons(hd(sk1),nil),X0) ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f676,plain,
( ~ sQ26_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f662,f673,f614,f617,f623]) ).
fof(f677,definition,
! [X0,X1] :
( sQ35_spl
<=> ( ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(app(sk4,cons(X0,X1)))
| lt(hd(sk1),X0)
| ~ strictorderP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| lt(X0,hd(sk1)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f678,plain,
! [X0,X1] :
( ~ sQ35_spl
| ~ strictorderP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| lt(hd(sk1),X0)
| lt(X0,hd(sk1))
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f677]) ).
fof(f680,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ23_spl
| ~ sQ11_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f658,f677,f525,f614,f620,f623]) ).
fof(f681,definition,
! [X0] :
( sQ36_spl
<=> ( ~ ssItem(X0)
| ~ memberP(tl(sk1),X0)
| memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( ~ sQ26_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f659,f681,f614,f617,f623]) ).
fof(f712,plain,
( ~ sQ32_spl
| ~ ssItem(hd(sk1))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f299,f665]) ).
fof(f715,plain,
( ~ sQ32_spl
| ~ sQ25_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f712,f525,f620,f664]) ).
fof(f718,plain,
! [X0,X1] :
( ~ ssList(X1)
| rearsegP(app(X1,X0),X0)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f283]) ).
fof(f724,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f567,f563]) ).
fof(f730,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f724,f500]) ).
fof(f731,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f730,f525,f566,f466]) ).
fof(f736,plain,
( ~ sQ26_spl
| ~ ssList(sk1)
| sk4 = tl(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(cons(hd(sk1),nil))
| nil = sk1 ),
inference(paramodulation,[status(thm)],[f624,f343]) ).
fof(f737,plain,
( ~ sQ26_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1))
| rearsegP(sk4,cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f624,f718]) ).
fof(f738,plain,
! [X0] :
( ~ sQ26_spl
| ~ frontsegP(tl(sk1),X0)
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil))
| frontsegP(sk4,X0)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f624,f349]) ).
fof(f742,definition,
( sQ37_spl
<=> rearsegP(sk4,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( ~ sQ26_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f737,f742,f614,f617,f623]) ).
fof(f746,definition,
( sQ38_spl
<=> sk4 = tl(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( ~ sQ38_spl
| sk4 = tl(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f746]) ).
fof(f749,plain,
( ~ sQ26_spl
| ~ sQ20_spl
| sQ38_spl
| ~ sQ24_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f736,f566,f617,f746,f573,f623]) ).
fof(f753,definition,
! [X0] :
( sQ39_spl
<=> ( ~ frontsegP(tl(sk1),X0)
| frontsegP(sk4,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f754,plain,
! [X0] :
( ~ sQ39_spl
| frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ frontsegP(tl(sk1),X0) ),
inference(component_clause,[status(thm)],[f753]) ).
fof(f756,plain,
( ~ sQ26_spl
| ~ sQ23_spl
| ~ sQ24_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f738,f753,f617,f614,f623]) ).
fof(f757,plain,
! [X0] :
( ~ sQ38_spl
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| app(sk4,X0) = tl(app(app(sk1,cons(hd(sk1),nil)),X0))
| ~ ssList(X0)
| nil = app(sk1,cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f747,f343]) ).
fof(f759,definition,
( sQ40_spl
<=> ssList(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( sQ40_spl
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,definition,
( sQ41_spl
<=> nil = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ41_spl
| app(sk1,cons(hd(sk1),nil)) = nil ),
inference(component_clause,[status(thm)],[f762]) ).
fof(f766,definition,
! [X0] :
( sQ42_spl
<=> ( app(sk4,X0) = tl(app(app(sk1,cons(hd(sk1),nil)),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ38_spl
| ~ sQ40_spl
| sQ42_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f757,f762,f766,f759,f746]) ).
fof(f771,plain,
( ~ sQ41_spl
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil))
| cons(hd(sk1),nil) = nil ),
inference(resolution,[status(thm)],[f763,f327]) ).
fof(f778,definition,
( sQ43_spl
<=> rearsegP(nil,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f779,plain,
( ~ sQ43_spl
| rearsegP(nil,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f778]) ).
fof(f782,plain,
( ~ sQ41_spl
| ~ sQ20_spl
| ~ sQ24_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f771,f664,f617,f573,f762]) ).
fof(f788,definition,
! [X0] :
( sQ45_spl
<=> ( ~ frontsegP(sk1,X0)
| frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f789,plain,
! [X0] :
( ~ sQ45_spl
| frontsegP(nil,X0)
| ~ ssList(X0)
| ~ frontsegP(sk1,X0) ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f793,plain,
( sQ40_spl
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f761,f283]) ).
fof(f794,plain,
( sQ40_spl
| ~ sQ20_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f793,f617,f573,f759]) ).
fof(f799,plain,
( ~ sQ33_spl
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| memberP(sk4,hd(sk1))
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f670,f487]) ).
fof(f800,definition,
( sQ46_spl
<=> memberP(sk4,hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f803,plain,
( ~ sQ33_spl
| ~ sQ11_spl
| sQ46_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f799,f620,f800,f525,f669]) ).
fof(f804,plain,
! [X0] :
( ~ sQ33_spl
| memberP(sk4,X0)
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ memberP(nil,X0)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f351,f670]) ).
fof(f806,definition,
! [X0] :
( sQ47_spl
<=> ( memberP(sk4,X0)
| ~ ssItem(X0)
| ~ memberP(nil,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f809,plain,
( ~ sQ33_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f804,f806,f620,f525,f669]) ).
fof(f817,plain,
! [X0] :
( ~ sQ26_spl
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(sk4,X0)
| ~ ssItem(X0)
| memberP(tl(sk1),X0)
| memberP(cons(hd(sk1),nil),X0) ),
inference(paramodulation,[status(thm)],[f624,f383]) ).
fof(f818,definition,
! [X0] :
( sQ48_spl
<=> ( ~ memberP(sk4,X0)
| ~ ssItem(X0)
| memberP(tl(sk1),X0)
| memberP(cons(hd(sk1),nil),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f819,plain,
! [X0] :
( ~ sQ48_spl
| ~ ssItem(X0)
| memberP(cons(hd(sk1),nil),X0)
| memberP(tl(sk1),X0)
| ~ memberP(sk4,X0) ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f821,plain,
( ~ sQ26_spl
| ~ sQ23_spl
| ~ sQ24_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f817,f818,f617,f614,f623]) ).
fof(f824,plain,
( sQ22_spl
| ~ ssList(sk1) ),
inference(backward_demodulation,[status(thm)],[f433,f601]) ).
fof(f825,plain,
( sQ22_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f824,f573,f599]) ).
fof(f828,plain,
! [X0] :
( ~ ssList(app(X0,nil))
| ~ ssList(X0)
| X0 = app(X0,nil)
| ~ ssList(nil)
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f370,f271]) ).
fof(f830,plain,
! [X0] :
( ~ sQ26_spl
| ~ ssList(X0)
| app(X0,cons(hd(sk1),nil)) != sk4
| X0 = tl(sk1)
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1)) ),
inference(paramodulation,[status(thm)],[f624,f370]) ).
fof(f831,plain,
! [X0,X1] :
( ~ ssList(X0)
| X0 = X0
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f370]) ).
fof(f832,definition,
! [X0] :
( sQ49_spl
<=> ( ~ ssList(app(X0,nil))
| ~ ssList(X0)
| X0 = app(X0,nil)
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f835,plain,
( ~ sQ11_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f828,f832,f525]) ).
fof(f836,definition,
! [X0] :
( sQ50_spl
<=> ( ~ ssList(X0)
| app(X0,cons(hd(sk1),nil)) != sk4
| X0 = tl(sk1) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f837,plain,
! [X0] :
( ~ sQ50_spl
| app(X0,cons(hd(sk1),nil)) != sk4
| X0 = tl(sk1)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f836]) ).
fof(f839,plain,
( ~ sQ26_spl
| sQ50_spl
| ~ sQ24_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f830,f614,f617,f836,f623]) ).
fof(f840,definition,
! [X0] :
( sQ51_spl
<=> ( ~ ssList(X0)
| X0 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f843,definition,
! [X1] :
( sQ52_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f844,plain,
! [X0] :
( ~ sQ52_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,plain,
( sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f831,f840,f843]) ).
fof(f877,plain,
( ~ sQ52_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f219,f844]) ).
fof(f883,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f877]) ).
fof(f885,definition,
( sQ53_spl
<=> ssList(app(tl(sk1),cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f887,plain,
( sQ53_spl
| ~ ssList(app(tl(sk1),cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f885]) ).
fof(f888,definition,
( sQ54_spl
<=> frontsegP(sk4,tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f889,plain,
( ~ sQ54_spl
| frontsegP(sk4,tl(sk1)) ),
inference(component_clause,[status(thm)],[f888]) ).
fof(f892,plain,
( sQ53_spl
| ~ sQ26_spl
| ~ ssList(sk4) ),
inference(forward_demodulation,[status(thm)],[f624,f887]) ).
fof(f893,plain,
( sQ53_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f892,f431]) ).
fof(f894,plain,
( sQ53_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f893]) ).
fof(f896,plain,
app(nil,nil) = nil,
inference(backward_subsumption_resolution,[status(thm)],[f489,f205]) ).
fof(f897,plain,
! [X0,X1] :
( X1 = X1
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f399]) ).
fof(f898,definition,
! [X0] :
( sQ55_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f899,plain,
! [X0] :
( ~ sQ55_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f898]) ).
fof(f901,definition,
! [X1] :
( sQ56_spl
<=> ( X1 = X1
| ~ ssItem(X1)
| ~ ssItem(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f904,plain,
( sQ56_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f897,f898,f901]) ).
fof(f905,plain,
! [X0] :
( ~ sQ55_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f899]) ).
fof(f906,plain,
! [X0] :
( ~ sQ26_spl
| app(sk4,X0) = app(tl(sk1),app(cons(hd(sk1),nil),X0))
| ~ ssList(X0)
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f624,f366]) ).
fof(f907,definition,
! [X0] :
( sQ57_spl
<=> ( app(sk4,X0) = app(tl(sk1),app(cons(hd(sk1),nil),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f910,plain,
( ~ sQ26_spl
| sQ57_spl
| ~ sQ23_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f906,f617,f614,f907,f623]) ).
fof(f912,plain,
( ~ sQ23_spl
| ~ sQ55_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f615,f905]) ).
fof(f920,plain,
( ~ sQ23_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f912]) ).
fof(f931,plain,
frontsegP(nil,nil),
inference(forward_subsumption_resolution,[status(thm)],[f481,f205]) ).
fof(f954,plain,
( ~ sQ38_spl
| app(sk1,cons(hd(sk1),nil)) = cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| app(sk1,cons(hd(sk1),nil)) = nil ),
inference(paramodulation,[status(thm)],[f747,f304]) ).
fof(f955,definition,
( sQ60_spl
<=> app(sk1,cons(hd(sk1),nil)) = cons(hd(app(sk1,cons(hd(sk1),nil))),sk4) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( ~ sQ60_spl
| app(sk1,cons(hd(sk1),nil)) = cons(hd(app(sk1,cons(hd(sk1),nil))),sk4) ),
inference(component_clause,[status(thm)],[f955]) ).
fof(f958,plain,
( ~ sQ38_spl
| sQ60_spl
| ~ sQ40_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f954,f762,f759,f955,f746]) ).
fof(f966,plain,
( ~ sQ26_spl
| ~ sQ50_spl
| tl(sk1) = tl(sk1)
| ~ ssList(tl(sk1)) ),
inference(resolution,[status(thm)],[f837,f624]) ).
fof(f968,definition,
( sQ63_spl
<=> tl(sk1) = tl(sk1) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f971,plain,
( ~ sQ26_spl
| ~ sQ50_spl
| sQ63_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f966,f614,f968,f836,f623]) ).
fof(f972,definition,
( sQ64_spl
<=> sk4 = sk4 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f991,plain,
! [X0] :
( ~ sQ60_spl
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0)
| ~ ssList(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| memberP(app(X0,app(sk1,cons(hd(sk1),nil))),hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f497]) ).
fof(f992,plain,
! [X0] :
( ~ sQ60_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| memberP(app(sk1,cons(hd(sk1),nil)),X0)
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f956,f351]) ).
fof(f993,plain,
( ~ sQ60_spl
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| hd(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f956,f295]) ).
fof(f995,plain,
( ~ sQ60_spl
| ~ ssList(sk4)
| memberP(app(sk1,cons(hd(sk1),nil)),hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f487]) ).
fof(f998,plain,
( ~ sQ60_spl
| app(sk1,cons(hd(sk1),nil)) != sk4
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f299]) ).
fof(f999,definition,
! [X0] :
( sQ65_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk4,X0)
| memberP(app(sk1,cons(hd(sk1),nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1000,plain,
! [X0] :
( ~ sQ65_spl
| ~ memberP(sk4,X0)
| ~ ssItem(X0)
| memberP(app(sk1,cons(hd(sk1),nil)),X0) ),
inference(component_clause,[status(thm)],[f999]) ).
fof(f1002,definition,
( sQ66_spl
<=> ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1004,plain,
( sQ66_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f1002]) ).
fof(f1005,plain,
( ~ sQ60_spl
| ~ sQ66_spl
| sQ65_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f992,f553,f999,f1002,f955]) ).
fof(f1006,definition,
! [X0] :
( sQ67_spl
<=> ( ~ ssList(X0)
| ~ ssList(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| memberP(app(X0,app(sk1,cons(hd(sk1),nil))),hd(app(sk1,cons(hd(sk1),nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| ~ sQ66_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f991,f1006,f1002,f553,f955]) ).
fof(f1010,definition,
( sQ68_spl
<=> memberP(app(sk1,cons(hd(sk1),nil)),hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
( ~ sQ68_spl
| memberP(app(sk1,cons(hd(sk1),nil)),hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| sQ68_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f995,f1002,f1010,f553,f955]) ).
fof(f1015,definition,
( sQ69_spl
<=> hd(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1018,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| ~ sQ66_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f993,f1015,f1002,f553,f955]) ).
fof(f1021,definition,
( sQ70_spl
<=> app(sk1,cons(hd(sk1),nil)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1024,plain,
( ~ sQ60_spl
| ~ sQ70_spl
| ~ sQ17_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f998,f1002,f553,f1021,f955]) ).
fof(f1026,plain,
( sQ66_spl
| nil = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f1004,f276]) ).
fof(f1027,plain,
( sQ66_spl
| sQ41_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1026,f759,f762,f1002]) ).
fof(f1028,plain,
! [X0] :
( ~ sQ65_spl
| memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssList(sk1)
| ~ ssItem(X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1000,f383]) ).
fof(f1029,definition,
! [X0] :
( sQ71_spl
<=> ( memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
! [X0] :
( ~ sQ71_spl
| memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1029]) ).
fof(f1032,plain,
( ~ sQ65_spl
| ~ sQ20_spl
| ~ sQ24_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1028,f1029,f617,f573,f999]) ).
fof(f1033,plain,
! [X0] :
( ~ sQ71_spl
| ~ memberP(sk4,X0)
| memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1030]) ).
fof(f1035,plain,
( ~ sQ68_spl
| memberP(cons(hd(sk1),nil),hd(app(sk1,cons(hd(sk1),nil))))
| memberP(sk1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk1)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f1011,f383]) ).
fof(f1036,definition,
( sQ72_spl
<=> memberP(sk1,hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1039,definition,
( sQ73_spl
<=> memberP(cons(hd(sk1),nil),hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( ~ sQ73_spl
| memberP(cons(hd(sk1),nil),hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f1039]) ).
fof(f1042,plain,
( ~ sQ68_spl
| sQ73_spl
| sQ72_spl
| ~ sQ20_spl
| ~ sQ66_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1035,f617,f1002,f573,f1036,f1039,f1010]) ).
fof(f1043,plain,
! [X0] :
( ~ ssList(skaf48(X0,nil))
| ~ ssList(app(skaf47(nil,X0),X0))
| nil = app(skaf47(nil,X0),X0)
| ~ ssList(nil)
| ~ segmentP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f396,f325]) ).
fof(f1044,definition,
! [X0] :
( sQ74_spl
<=> ( ~ ssList(skaf48(X0,nil))
| ~ ssList(app(skaf47(nil,X0),X0))
| nil = app(skaf47(nil,X0),X0)
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1047,plain,
( ~ sQ11_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f1043,f1044,f525]) ).
fof(f1048,plain,
( ~ sQ33_spl
| ~ sQ73_spl
| memberP(sk4,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(resolution,[status(thm)],[f1040,f670]) ).
fof(f1049,definition,
( sQ75_spl
<=> memberP(sk4,hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1050,plain,
( ~ sQ75_spl
| memberP(sk4,hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f1049]) ).
fof(f1052,plain,
( ~ sQ33_spl
| ~ sQ73_spl
| sQ75_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f1048,f1002,f1049,f1039,f669]) ).
fof(f1110,definition,
( sQ80_spl
<=> hd(sk1) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1119,definition,
( sQ82_spl
<=> memberP(sk1,hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1180,definition,
! [X1] :
( sQ87_spl
<=> ( ~ ssItem(X1)
| ~ ssItem(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1181,plain,
! [X0] :
( ~ sQ87_spl
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1180]) ).
fof(f1185,plain,
! [X0] :
( ~ sQ87_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1181]) ).
fof(f1188,plain,
( ~ sQ87_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f233,f1185]) ).
fof(f1204,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1188]) ).
fof(f1257,definition,
! [X0] :
( sQ94_spl
<=> ( X0 = sk1
| ~ ssList(X0)
| sk4 != app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1258,plain,
! [X0] :
( ~ sQ94_spl
| ~ ssList(X0)
| sk1 = X0
| sk4 != app(nil,X0) ),
inference(component_clause,[status(thm)],[f1257]) ).
fof(f1268,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ ssList(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(tl(sk1))
| ~ ssList(X1)
| ~ strictorderedP(app(sk4,cons(X0,X1))) ),
inference(paramodulation,[status(thm)],[f624,f482]) ).
fof(f1269,plain,
! [X0] :
( ~ sQ26_spl
| cons(hd(sk1),nil) = X0
| ~ ssList(cons(hd(sk1),nil))
| app(tl(sk1),X0) != sk4
| ~ ssList(tl(sk1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f624,f368]) ).
fof(f1276,definition,
! [X0,X1] :
( sQ96_spl
<=> ( ~ ssList(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(X1)
| ~ strictorderedP(app(sk4,cons(X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1279,plain,
( ~ sQ26_spl
| ~ sQ11_spl
| ~ sQ25_spl
| ~ sQ23_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1268,f1276,f614,f620,f525,f623]) ).
fof(f1280,definition,
! [X0] :
( sQ97_spl
<=> ( cons(hd(sk1),nil) = X0
| app(tl(sk1),X0) != sk4
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1283,plain,
( ~ sQ26_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1269,f1280,f614,f617,f623]) ).
fof(f1298,plain,
! [X0,X1] :
( ~ sQ35_spl
| ~ sQ26_spl
| ~ ssList(app(sk4,cons(X1,X0)))
| lt(hd(sk1),X1)
| lt(X1,hd(sk1))
| ~ ssItem(X1)
| ~ strictorderP(app(sk4,cons(X1,X0)))
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f624,f678]) ).
fof(f1299,plain,
! [X0,X1] :
( ~ sQ35_spl
| ~ sQ26_spl
| ~ ssList(sk4)
| ~ ssList(cons(X0,X1))
| lt(X0,hd(sk1))
| ~ strictorderP(app(sk4,cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(X1)
| lt(hd(sk1),X0) ),
inference(resolution,[status(thm)],[f1298,f283]) ).
fof(f1300,definition,
! [X0,X1] :
( sQ98_spl
<=> ( ~ ssList(cons(X0,X1))
| lt(X0,hd(sk1))
| ~ strictorderP(app(sk4,cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(X1)
| lt(hd(sk1),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( ~ sQ35_spl
| ~ sQ26_spl
| ~ sQ17_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1299,f1300,f553,f623,f677]) ).
fof(f1326,plain,
( ~ sQ39_spl
| ~ ssList(tl(sk1))
| ~ ssList(tl(sk1))
| frontsegP(sk4,tl(sk1)) ),
inference(resolution,[status(thm)],[f754,f258]) ).
fof(f1327,plain,
( ~ sQ39_spl
| ~ sQ23_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1326,f888,f614,f753]) ).
fof(f1329,definition,
( sQ103_spl
<=> sk4 = tl(sk1) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1330,plain,
( ~ sQ103_spl
| sk4 = tl(sk1) ),
inference(component_clause,[status(thm)],[f1329]) ).
fof(f1336,plain,
( ~ sQ54_spl
| ~ sQ103_spl
| frontsegP(sk4,sk4) ),
inference(backward_demodulation,[status(thm)],[f1330,f889]) ).
fof(f1341,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| app(sk4,cons(hd(sk1),nil)) = sk4 ),
inference(backward_demodulation,[status(thm)],[f1330,f624]) ).
fof(f1342,plain,
! [X0] :
( ~ sQ103_spl
| tl(app(sk1,X0)) = app(sk4,X0)
| ~ ssList(X0)
| ~ ssList(sk1)
| sk1 = nil ),
inference(paramodulation,[status(thm)],[f1330,f343]) ).
fof(f1343,plain,
( ~ sQ103_spl
| sk1 = cons(hd(sk1),sk4)
| ~ ssList(sk1)
| sk1 = nil ),
inference(paramodulation,[status(thm)],[f1330,f304]) ).
fof(f1345,definition,
( sQ105_spl
<=> sk1 = cons(hd(sk1),sk4) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1346,plain,
( ~ sQ105_spl
| cons(hd(sk1),sk4) = sk1 ),
inference(component_clause,[status(thm)],[f1345]) ).
fof(f1348,plain,
( ~ sQ103_spl
| sQ105_spl
| ~ sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1343,f566,f573,f1345,f1329]) ).
fof(f1349,definition,
! [X0] :
( sQ106_spl
<=> ( tl(app(sk1,X0)) = app(sk4,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1352,plain,
( ~ sQ103_spl
| sQ106_spl
| ~ sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1342,f566,f573,f1349,f1329]) ).
fof(f1354,plain,
( ~ sQ54_spl
| ~ sQ103_spl
| ~ frontsegP(sk4,sk4)
| sk4 = sk4
| ~ ssList(sk4)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f1336,f339]) ).
fof(f1355,definition,
( sQ107_spl
<=> frontsegP(sk4,sk4) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1357,plain,
( sQ107_spl
| ~ frontsegP(sk4,sk4) ),
inference(component_clause,[status(thm)],[f1355]) ).
fof(f1358,plain,
( ~ sQ54_spl
| ~ sQ103_spl
| ~ sQ107_spl
| sQ64_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1354,f553,f972,f1355,f1329,f888]) ).
fof(f1359,plain,
( sQ107_spl
| ~ sQ54_spl
| ~ sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1357,f1336]) ).
fof(f1360,plain,
( sQ107_spl
| ~ sQ54_spl
| ~ sQ103_spl ),
inference(contradiction_clause,[status(thm)],[f1359]) ).
fof(f1361,plain,
! [X0] :
( ~ sQ105_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(sk1,X0)
| ~ ssList(sk4)
| ~ ssItem(hd(sk1)) ),
inference(paramodulation,[status(thm)],[f1346,f389]) ).
fof(f1362,plain,
( ~ sQ105_spl
| ~ ssItem(hd(sk1))
| memberP(sk1,hd(sk1))
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f1346,f487]) ).
fof(f1365,plain,
( ~ sQ105_spl
| ~ sQ35_spl
| ~ sQ26_spl
| lt(hd(sk1),hd(sk1))
| ~ strictorderP(app(sk4,cons(hd(sk1),sk4)))
| ~ ssItem(hd(sk1))
| ~ ssList(sk4)
| ~ ssList(app(sk4,sk1))
| lt(hd(sk1),hd(sk1)) ),
inference(paramodulation,[status(thm)],[f1346,f1298]) ).
fof(f1366,plain,
! [X0] :
( ~ sQ105_spl
| ~ ssItem(hd(sk1))
| ~ ssList(X0)
| ~ ssList(sk4)
| cons(hd(sk1),app(sk4,X0)) = app(sk1,X0) ),
inference(paramodulation,[status(thm)],[f1346,f381]) ).
fof(f1369,plain,
( ~ sQ105_spl
| ~ ssList(sk4)
| ~ ssItem(hd(sk1))
| sk4 != sk1 ),
inference(paramodulation,[status(thm)],[f1346,f299]) ).
fof(f1370,plain,
! [X0,X1,X2] :
( ~ sQ105_spl
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sk1),sk4)))
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(hd(sk1))
| lt(X1,hd(sk1))
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),sk1)) ),
inference(paramodulation,[status(thm)],[f1346,f482]) ).
fof(f1371,plain,
! [X0,X1,X2] :
( ~ sQ105_spl
| ~ ssList(app(app(X0,cons(hd(sk1),sk4)),cons(X1,X2)))
| ~ ssList(sk4)
| ~ ssItem(hd(sk1))
| ~ ssItem(X1)
| lt(hd(sk1),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X0,sk1),cons(X1,X2))) ),
inference(paramodulation,[status(thm)],[f1346,f482]) ).
fof(f1373,definition,
! [X0,X1,X2] :
( sQ108_spl
<=> ( ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sk1),sk4)))
| ~ ssList(X2)
| ~ ssItem(X1)
| lt(X1,hd(sk1))
| ~ ssList(X0)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),sk1)) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1376,plain,
( ~ sQ105_spl
| ~ sQ25_spl
| ~ sQ17_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f1370,f1373,f553,f620,f1345]) ).
fof(f1377,definition,
( sQ109_spl
<=> sk4 = sk1 ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1380,plain,
( ~ sQ105_spl
| ~ sQ17_spl
| ~ sQ25_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f1369,f1377,f620,f553,f1345]) ).
fof(f1381,definition,
! [X0] :
( sQ110_spl
<=> ( hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1382,plain,
! [X0] :
( ~ sQ110_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| ~ memberP(sk1,X0)
| memberP(sk4,X0) ),
inference(component_clause,[status(thm)],[f1381]) ).
fof(f1384,plain,
( ~ sQ105_spl
| sQ110_spl
| ~ sQ17_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1361,f620,f553,f1381,f1345]) ).
fof(f1388,plain,
( ~ sQ105_spl
| ~ sQ25_spl
| sQ82_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1362,f553,f1119,f620,f1345]) ).
fof(f1389,definition,
! [X0,X1,X2] :
( sQ111_spl
<=> ( ~ ssList(app(app(X0,cons(hd(sk1),sk4)),cons(X1,X2)))
| ~ ssItem(X1)
| lt(hd(sk1),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X0,sk1),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1392,plain,
( ~ sQ105_spl
| ~ sQ17_spl
| ~ sQ25_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f1371,f1389,f620,f553,f1345]) ).
fof(f1393,definition,
( sQ112_spl
<=> lt(hd(sk1),hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1394,plain,
( ~ sQ112_spl
| lt(hd(sk1),hd(sk1)) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1395,plain,
( sQ112_spl
| ~ lt(hd(sk1),hd(sk1)) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1396,definition,
( sQ113_spl
<=> ssList(app(sk4,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1398,plain,
( sQ113_spl
| ~ ssList(app(sk4,sk1)) ),
inference(component_clause,[status(thm)],[f1396]) ).
fof(f1399,definition,
( sQ114_spl
<=> strictorderP(app(sk4,cons(hd(sk1),sk4))) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( ~ sQ105_spl
| ~ sQ35_spl
| ~ sQ26_spl
| ~ sQ114_spl
| ~ sQ25_spl
| ~ sQ17_spl
| ~ sQ113_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1365,f1393,f1396,f553,f620,f1399,f623,f677,f1345]) ).
fof(f1403,definition,
! [X0] :
( sQ115_spl
<=> ( ~ ssList(X0)
| cons(hd(sk1),app(sk4,X0)) = app(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1406,plain,
( ~ sQ105_spl
| ~ sQ25_spl
| ~ sQ17_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f1366,f1403,f553,f620,f1345]) ).
fof(f1410,plain,
( sQ113_spl
| ~ ssList(sk4)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f1398,f283]) ).
fof(f1411,plain,
( sQ113_spl
| ~ sQ17_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1410,f573,f553,f1396]) ).
fof(f1412,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ sQ35_spl
| lt(hd(sk1),hd(sk1))
| ~ strictorderP(app(sk4,cons(hd(sk1),nil)))
| ~ ssItem(hd(sk1))
| ~ ssList(nil)
| ~ ssList(sk4)
| lt(hd(sk1),hd(sk1)) ),
inference(paramodulation,[status(thm)],[f1341,f1298]) ).
fof(f1413,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ sQ103_spl
| ~ ssList(app(app(sk4,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(sk4)
| ~ ssList(X1)
| ~ strictorderedP(app(sk4,cons(X0,X1))) ),
inference(paramodulation,[status(thm)],[f1341,f482]) ).
fof(f1414,plain,
! [X0] :
( ~ sQ26_spl
| ~ sQ103_spl
| cons(hd(sk1),nil) = X0
| ~ ssList(cons(hd(sk1),nil))
| app(sk4,X0) != sk4
| ~ ssList(sk4)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1341,f368]) ).
fof(f1416,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk4)
| hd(sk4) = hd(sk4)
| nil = sk4 ),
inference(paramodulation,[status(thm)],[f1341,f331]) ).
fof(f1419,definition,
! [X0,X1] :
( sQ116_spl
<=> ( ~ ssList(app(app(sk4,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(X1)
| ~ strictorderedP(app(sk4,cons(X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ sQ11_spl
| ~ sQ25_spl
| ~ sQ17_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f1413,f1419,f553,f620,f525,f1329,f623]) ).
fof(f1424,definition,
! [X0] :
( sQ117_spl
<=> ( cons(hd(sk1),nil) = X0
| app(sk4,X0) != sk4
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ sQ24_spl
| ~ sQ17_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1414,f1424,f553,f617,f1329,f623]) ).
fof(f1429,definition,
( sQ118_spl
<=> hd(sk4) = hd(sk4) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1432,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ sQ24_spl
| ~ sQ17_spl
| sQ118_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1416,f459,f1429,f553,f617,f1329,f623]) ).
fof(f1433,definition,
( sQ119_spl
<=> strictorderP(app(sk4,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ sQ35_spl
| ~ sQ119_spl
| ~ sQ25_spl
| ~ sQ11_spl
| ~ sQ17_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1412,f1393,f553,f525,f620,f1433,f677,f1329,f623]) ).
fof(f1454,plain,
! [X0] :
( ~ sQ26_spl
| ~ sQ103_spl
| ~ ssList(sk4)
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(sk4,X0)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f1341,f352]) ).
fof(f1455,definition,
! [X0] :
( sQ120_spl
<=> ( ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1458,plain,
( ~ sQ26_spl
| ~ sQ103_spl
| ~ sQ17_spl
| sQ120_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1454,f617,f1455,f553,f1329,f623]) ).
fof(f1461,plain,
! [X0] :
( ~ sQ105_spl
| ~ ssList(sk4)
| ~ ssItem(hd(sk1))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f1346,f351]) ).
fof(f1462,definition,
! [X0] :
( sQ121_spl
<=> ( memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1463,plain,
! [X0] :
( ~ sQ121_spl
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f1462]) ).
fof(f1465,plain,
( ~ sQ105_spl
| ~ sQ17_spl
| ~ sQ25_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f1461,f1462,f620,f553,f1345]) ).
fof(f1467,plain,
( ~ sQ75_spl
| ~ sQ121_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| memberP(sk1,hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(resolution,[status(thm)],[f1463,f1050]) ).
fof(f1468,plain,
( ~ sQ2_spl
| ~ sQ121_spl
| ~ ssItem(sk5)
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f1463,f520]) ).
fof(f1470,plain,
( ~ sQ75_spl
| ~ sQ121_spl
| ~ sQ66_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1467,f1036,f1002,f1462,f1049]) ).
fof(f1471,definition,
( sQ122_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1473,plain,
( sQ122_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f1471]) ).
fof(f1474,plain,
( ~ sQ2_spl
| ~ sQ121_spl
| ~ sQ122_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1468,f451,f1471,f1462,f448]) ).
fof(f1475,plain,
( sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1473,f434]) ).
fof(f1476,plain,
sQ122_spl,
inference(contradiction_clause,[status(thm)],[f1475]) ).
fof(f1479,plain,
( sQ2_spl
| ~ sQ110_spl
| hd(sk1) = sk5
| ~ ssItem(sk5)
| ~ memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f1382,f511]) ).
fof(f1481,definition,
( sQ123_spl
<=> hd(sk1) = sk5 ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1482,plain,
( ~ sQ123_spl
| hd(sk1) = sk5 ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1484,plain,
( sQ2_spl
| ~ sQ110_spl
| sQ123_spl
| ~ sQ122_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1479,f451,f1471,f1481,f1381,f448]) ).
fof(f1486,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ123_spl
| ~ memberP(cons(sk5,nil),X0)
| ~ ssItem(X0)
| memberP(sk4,X0) ),
inference(backward_demodulation,[status(thm)],[f1482,f670]) ).
fof(f1506,plain,
( ~ sQ123_spl
| sk1 = cons(sk5,tl(sk1))
| ~ ssList(sk1)
| sk1 = nil ),
inference(paramodulation,[status(thm)],[f1482,f304]) ).
fof(f1514,definition,
( sQ125_spl
<=> sk1 = cons(sk5,tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1515,plain,
( ~ sQ125_spl
| sk1 = cons(sk5,tl(sk1)) ),
inference(component_clause,[status(thm)],[f1514]) ).
fof(f1517,plain,
( ~ sQ123_spl
| sQ125_spl
| ~ sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1506,f566,f573,f1514,f1481]) ).
fof(f1539,plain,
( ~ sQ33_spl
| ~ sQ123_spl
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ ssItem(sk5)
| memberP(sk4,sk5) ),
inference(resolution,[status(thm)],[f1486,f487]) ).
fof(f1541,definition,
( sQ129_spl
<=> memberP(sk4,sk5) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1542,plain,
( ~ sQ129_spl
| memberP(sk4,sk5) ),
inference(component_clause,[status(thm)],[f1541]) ).
fof(f1544,plain,
( ~ sQ33_spl
| ~ sQ123_spl
| ~ sQ11_spl
| ~ sQ122_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f1539,f1541,f1471,f525,f1481,f669]) ).
fof(f1545,plain,
( ~ sQ129_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1542,f511]) ).
fof(f1546,plain,
( ~ sQ129_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1545]) ).
fof(f1551,plain,
( ~ sQ125_spl
| ~ ssItem(sk5)
| memberP(sk1,sk5)
| ~ ssList(tl(sk1)) ),
inference(paramodulation,[status(thm)],[f1515,f487]) ).
fof(f1552,plain,
( ~ sQ125_spl
| sk5 = hd(sk1)
| ~ ssList(tl(sk1))
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f1515,f295]) ).
fof(f1557,plain,
( ~ sQ125_spl
| ~ ssList(tl(sk1))
| ~ ssItem(sk5)
| tl(sk1) != sk1 ),
inference(paramodulation,[status(thm)],[f1515,f299]) ).
fof(f1568,plain,
( ~ sQ125_spl
| sQ123_spl
| ~ sQ23_spl
| ~ sQ122_spl ),
inference(split_clause,[status(thm)],[f1552,f1471,f614,f1481,f1514]) ).
fof(f1582,definition,
( sQ135_spl
<=> tl(sk1) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1585,plain,
( ~ sQ125_spl
| ~ sQ23_spl
| ~ sQ122_spl
| ~ sQ135_spl ),
inference(split_clause,[status(thm)],[f1557,f1582,f1471,f614,f1514]) ).
fof(f1591,plain,
( ~ sQ125_spl
| ~ sQ122_spl
| sQ3_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f1551,f614,f451,f1471,f1514]) ).
fof(f1611,plain,
( ~ sQ43_spl
| ~ ssList(cons(hd(sk1),nil))
| cons(hd(sk1),nil) = nil ),
inference(resolution,[status(thm)],[f280,f779]) ).
fof(f1613,plain,
( ~ sQ43_spl
| ~ sQ24_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1611,f664,f617,f778]) ).
fof(f1623,plain,
! [X0] :
( ~ ssList(nil)
| ~ segmentP(nil,X0)
| ~ ssList(X0)
| ~ ssList(skaf48(X0,nil))
| skaf48(X0,nil) = nil
| ~ ssList(app(skaf47(nil,X0),X0)) ),
inference(resolution,[status(thm)],[f327,f396]) ).
fof(f1628,definition,
! [X0] :
( sQ139_spl
<=> ( ~ segmentP(nil,X0)
| ~ ssList(X0)
| ~ ssList(skaf48(X0,nil))
| skaf48(X0,nil) = nil
| ~ ssList(app(skaf47(nil,X0),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1631,plain,
( ~ sQ11_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f1623,f1628,f525]) ).
fof(f1644,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ ssList(tl(sk1))
| leq(hd(sk1),X0)
| ~ ssList(X1)
| leq(X0,hd(sk1))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ totalorderP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f624,f483]) ).
fof(f1655,definition,
! [X0,X1] :
( sQ140_spl
<=> ( leq(hd(sk1),X0)
| ~ ssList(X1)
| leq(X0,hd(sk1))
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ totalorderP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1658,plain,
( ~ sQ26_spl
| ~ sQ23_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ140_spl ),
inference(split_clause,[status(thm)],[f1644,f1655,f620,f525,f614,f623]) ).
fof(f1693,plain,
! [X0] :
( ~ sQ71_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(nil,X0)
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1033,f389]) ).
fof(f1694,definition,
! [X0] :
( sQ141_spl
<=> ( hd(sk1) = X0
| ~ ssItem(X0)
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1695,plain,
! [X0] :
( ~ sQ141_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1694]) ).
fof(f1697,plain,
( ~ sQ71_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f1693,f1694,f620,f525,f1029]) ).
fof(f1698,plain,
! [X0] :
( ~ sQ141_spl
| hd(sk1) = X0
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1695]) ).
fof(f1699,plain,
! [X0] :
( ~ sQ141_spl
| ~ ssItem(X0)
| hd(sk1) = X0
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1698,f268]) ).
fof(f1701,plain,
( ~ sQ2_spl
| ~ sQ141_spl
| memberP(sk1,sk5)
| ~ ssItem(sk5)
| sk5 = hd(sk1) ),
inference(resolution,[status(thm)],[f1699,f520]) ).
fof(f1704,plain,
( ~ sQ2_spl
| ~ sQ141_spl
| sQ3_spl
| ~ sQ122_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f1701,f1481,f1471,f451,f1694,f448]) ).
fof(f1706,definition,
( sQ142_spl
<=> hd(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1707,plain,
( ~ sQ142_spl
| hd(sk1) = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1706]) ).
fof(f1712,plain,
( ~ sQ24_spl
| ~ ssItem(hd(sk1))
| singletonP(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f484,f618]) ).
fof(f1713,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(X0)
| singletonP(cons(X0,nil)) ),
inference(resolution,[status(thm)],[f484,f284]) ).
fof(f1714,definition,
! [X0] :
( sQ143_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0)
| singletonP(cons(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1717,plain,
( ~ sQ11_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f1713,f1714,f525]) ).
fof(f1718,definition,
( sQ144_spl
<=> singletonP(cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1721,plain,
( ~ sQ24_spl
| ~ sQ25_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f1712,f1718,f620,f617]) ).
fof(f1727,plain,
( ~ sQ142_spl
| ~ ssList(sk1)
| tl(sk1) != tl(app(sk1,cons(hd(sk1),nil)))
| sk1 = app(sk1,cons(hd(sk1),nil))
| app(sk1,cons(hd(sk1),nil)) = nil
| nil = sk1
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f1707,f412]) ).
fof(f1731,plain,
! [X0] :
( ~ sQ142_spl
| ~ ssList(X0)
| tl(X0) != tl(app(sk1,cons(hd(sk1),nil)))
| X0 = app(sk1,cons(hd(sk1),nil))
| app(sk1,cons(hd(sk1),nil)) = nil
| nil = X0
| hd(sk1) != hd(X0)
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f1707,f412]) ).
fof(f1732,plain,
( ~ sQ142_spl
| app(sk1,cons(hd(sk1),nil)) = cons(hd(sk1),tl(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| app(sk1,cons(hd(sk1),nil)) = nil ),
inference(paramodulation,[status(thm)],[f1707,f304]) ).
fof(f1733,definition,
( sQ145_spl
<=> sk1 = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1734,plain,
( ~ sQ145_spl
| sk1 = app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f1733]) ).
fof(f1736,definition,
( sQ146_spl
<=> tl(sk1) = tl(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1739,plain,
( ~ sQ142_spl
| ~ sQ20_spl
| ~ sQ146_spl
| sQ145_spl
| sQ41_spl
| sQ18_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1727,f759,f566,f762,f1733,f1736,f573,f1706]) ).
fof(f1740,definition,
( sQ147_spl
<=> app(sk1,cons(hd(sk1),nil)) = cons(hd(sk1),tl(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1741,plain,
( ~ sQ147_spl
| app(sk1,cons(hd(sk1),nil)) = cons(hd(sk1),tl(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f1740]) ).
fof(f1743,plain,
( ~ sQ142_spl
| sQ147_spl
| ~ sQ40_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1732,f762,f759,f1740,f1706]) ).
fof(f1745,definition,
! [X0] :
( sQ148_spl
<=> ( ~ ssList(X0)
| tl(X0) != tl(app(sk1,cons(hd(sk1),nil)))
| X0 = app(sk1,cons(hd(sk1),nil))
| nil = X0
| hd(sk1) != hd(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1748,plain,
( ~ sQ142_spl
| sQ41_spl
| sQ148_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1731,f759,f1745,f762,f1706]) ).
fof(f1753,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| app(sk1,cons(hd(sk1),nil)) = cons(hd(sk1),sk4) ),
inference(forward_demodulation,[status(thm)],[f747,f1741]) ).
fof(f1756,plain,
( ~ sQ38_spl
| ~ sQ145_spl
| sk4 = tl(sk1) ),
inference(backward_demodulation,[status(thm)],[f1734,f747]) ).
fof(f1761,plain,
! [X0,X1] :
( ~ sQ145_spl
| ~ ssList(sk1)
| leq(hd(sk1),X0)
| ~ ssList(X1)
| leq(X0,hd(sk1))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssList(app(sk1,cons(X0,X1)))
| ~ totalorderP(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f1734,f483]) ).
fof(f1762,plain,
! [X0,X1] :
( ~ sQ145_spl
| ~ ssList(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(sk1)
| ~ ssList(X1)
| ~ strictorderedP(app(sk1,cons(X0,X1))) ),
inference(paramodulation,[status(thm)],[f1734,f482]) ).
fof(f1763,plain,
! [X0] :
( ~ sQ145_spl
| memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f1734,f383]) ).
fof(f1765,plain,
! [X0] :
( ~ sQ145_spl
| ~ ssList(sk1)
| ~ ssItem(X0)
| memberP(sk1,X0)
| ~ memberP(sk1,X0)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f1734,f352]) ).
fof(f1766,plain,
! [X0] :
( ~ sQ145_spl
| ~ ssItem(X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssList(sk1) ),
inference(paramodulation,[status(thm)],[f1734,f353]) ).
fof(f1767,plain,
! [X0] :
( ~ sQ145_spl
| cons(hd(sk1),nil) = X0
| ~ ssList(cons(hd(sk1),nil))
| app(sk1,X0) != sk1
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1734,f368]) ).
fof(f1772,definition,
! [X0] :
( sQ149_spl
<=> ( cons(hd(sk1),nil) = X0
| app(sk1,X0) != sk1
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1775,plain,
( ~ sQ145_spl
| ~ sQ24_spl
| ~ sQ20_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1767,f1772,f573,f617,f1733]) ).
fof(f1777,plain,
( ~ sQ38_spl
| ~ sQ145_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1756,f1329,f1733,f746]) ).
fof(f1779,definition,
! [X0,X1] :
( sQ150_spl
<=> ( leq(hd(sk1),X0)
| ~ ssList(X1)
| leq(X0,hd(sk1))
| ~ ssList(app(sk1,cons(X0,X1)))
| ~ totalorderP(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1782,plain,
( ~ sQ145_spl
| ~ sQ20_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f1761,f1779,f620,f525,f573,f1733]) ).
fof(f1783,definition,
! [X0] :
( sQ151_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1784,plain,
! [X0] :
( ~ sQ151_spl
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0) ),
inference(component_clause,[status(thm)],[f1783]) ).
fof(f1786,plain,
( ~ sQ145_spl
| ~ sQ24_spl
| sQ151_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1766,f573,f1783,f617,f1733]) ).
fof(f1789,definition,
! [X0] :
( sQ152_spl
<=> ( ~ ssItem(X0)
| memberP(sk1,X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1792,plain,
( ~ sQ145_spl
| ~ sQ20_spl
| sQ152_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1765,f617,f1789,f573,f1733]) ).
fof(f1795,definition,
! [X0] :
( sQ153_spl
<=> ( memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ memberP(sk1,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1798,plain,
( ~ sQ145_spl
| ~ sQ20_spl
| ~ sQ24_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f1763,f1795,f617,f573,f1733]) ).
fof(f1799,definition,
! [X0,X1] :
( sQ154_spl
<=> ( ~ ssList(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(X1)
| ~ strictorderedP(app(sk1,cons(X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1802,plain,
( ~ sQ145_spl
| ~ sQ11_spl
| ~ sQ25_spl
| ~ sQ20_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f1762,f1799,f573,f620,f525,f1733]) ).
fof(f1816,plain,
! [X0] :
( ~ sQ151_spl
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| ~ memberP(nil,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1784,f351]) ).
fof(f1819,definition,
! [X0] :
( sQ155_spl
<=> ( ~ ssItem(X0)
| ~ memberP(nil,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1822,plain,
( ~ sQ151_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f1816,f1819,f620,f525,f1783]) ).
fof(f1832,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ50_spl
| cons(hd(sk1),sk4) != sk4
| ~ ssList(sk1)
| sk1 = tl(sk1) ),
inference(paramodulation,[status(thm)],[f1753,f837]) ).
fof(f1833,plain,
! [X0,X1] :
( ~ sQ147_spl
| ~ sQ38_spl
| ~ ssList(sk1)
| leq(hd(sk1),X0)
| ~ ssList(X1)
| leq(X0,hd(sk1))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssList(app(cons(hd(sk1),sk4),cons(X0,X1)))
| ~ totalorderP(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f1753,f483]) ).
fof(f1834,plain,
! [X0,X1] :
( ~ sQ147_spl
| ~ sQ38_spl
| ~ ssList(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(sk1)
| ~ ssList(X1)
| ~ strictorderedP(app(cons(hd(sk1),sk4),cons(X0,X1))) ),
inference(paramodulation,[status(thm)],[f1753,f482]) ).
fof(f1835,plain,
! [X0] :
( ~ sQ147_spl
| ~ sQ38_spl
| memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(cons(hd(sk1),sk4),X0)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f1753,f383]) ).
fof(f1837,plain,
! [X0] :
( ~ sQ147_spl
| ~ sQ38_spl
| ~ ssList(sk1)
| ~ ssItem(X0)
| memberP(cons(hd(sk1),sk4),X0)
| ~ memberP(sk1,X0)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f1753,f352]) ).
fof(f1838,plain,
! [X0] :
( ~ sQ147_spl
| ~ sQ38_spl
| ~ ssItem(X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(cons(hd(sk1),nil),X0)
| memberP(cons(hd(sk1),sk4),X0)
| ~ ssList(sk1) ),
inference(paramodulation,[status(thm)],[f1753,f353]) ).
fof(f1839,plain,
! [X0] :
( ~ sQ147_spl
| ~ sQ38_spl
| cons(hd(sk1),nil) = X0
| ~ ssList(cons(hd(sk1),nil))
| app(sk1,X0) != cons(hd(sk1),sk4)
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1753,f368]) ).
fof(f1841,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk1)
| hd(cons(hd(sk1),sk4)) = hd(sk1)
| nil = sk1 ),
inference(paramodulation,[status(thm)],[f1753,f331]) ).
fof(f1843,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ ssList(cons(hd(sk1),nil))
| cons(hd(sk1),sk4) != nil
| ~ ssList(sk1)
| nil = sk1 ),
inference(paramodulation,[status(thm)],[f1753,f325]) ).
fof(f1844,definition,
! [X0] :
( sQ156_spl
<=> ( cons(hd(sk1),nil) = X0
| app(sk1,X0) != cons(hd(sk1),sk4)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1847,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ20_spl
| sQ156_spl ),
inference(split_clause,[status(thm)],[f1839,f1844,f573,f617,f746,f1740]) ).
fof(f1848,definition,
! [X0] :
( sQ157_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0)
| memberP(cons(hd(sk1),sk4),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1849,plain,
! [X0] :
( ~ sQ157_spl
| ~ memberP(cons(hd(sk1),nil),X0)
| ~ ssItem(X0)
| memberP(cons(hd(sk1),sk4),X0) ),
inference(component_clause,[status(thm)],[f1848]) ).
fof(f1851,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ24_spl
| sQ157_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1838,f573,f1848,f617,f746,f1740]) ).
fof(f1852,definition,
! [X0] :
( sQ158_spl
<=> ( ~ ssItem(X0)
| memberP(cons(hd(sk1),sk4),X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f1853,plain,
! [X0] :
( ~ sQ158_spl
| ~ ssItem(X0)
| ~ memberP(sk1,X0)
| memberP(cons(hd(sk1),sk4),X0) ),
inference(component_clause,[status(thm)],[f1852]) ).
fof(f1855,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ20_spl
| sQ158_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1837,f617,f1852,f573,f746,f1740]) ).
fof(f1856,definition,
( sQ159_spl
<=> cons(hd(sk1),sk4) = nil ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1859,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ159_spl
| ~ sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1843,f566,f573,f1856,f617,f746,f1740]) ).
fof(f1860,definition,
( sQ160_spl
<=> cons(hd(sk1),sk4) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1863,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ50_spl
| ~ sQ160_spl
| ~ sQ20_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f1832,f1582,f573,f1860,f836,f746,f1740]) ).
fof(f1864,definition,
! [X0] :
( sQ161_spl
<=> ( memberP(cons(hd(sk1),nil),X0)
| memberP(sk1,X0)
| ~ memberP(cons(hd(sk1),sk4),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f1867,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ20_spl
| ~ sQ24_spl
| sQ161_spl ),
inference(split_clause,[status(thm)],[f1835,f1864,f617,f573,f746,f1740]) ).
fof(f1868,definition,
! [X0,X1] :
( sQ162_spl
<=> ( ~ ssList(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0)
| lt(hd(sk1),X0)
| ~ ssList(X1)
| ~ strictorderedP(app(cons(hd(sk1),sk4),cons(X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1871,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ11_spl
| ~ sQ25_spl
| ~ sQ20_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f1834,f1868,f573,f620,f525,f746,f1740]) ).
fof(f1874,definition,
( sQ163_spl
<=> hd(cons(hd(sk1),sk4)) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1875,plain,
( ~ sQ163_spl
| hd(sk1) = hd(cons(hd(sk1),sk4)) ),
inference(component_clause,[status(thm)],[f1874]) ).
fof(f1877,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ20_spl
| sQ163_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1841,f566,f1874,f573,f617,f746,f1740]) ).
fof(f1878,definition,
( sQ164_spl
<=> ssList(cons(hd(sk1),sk4)) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1880,plain,
( sQ164_spl
| ~ ssList(cons(hd(sk1),sk4)) ),
inference(component_clause,[status(thm)],[f1878]) ).
fof(f1882,definition,
! [X0,X1] :
( sQ165_spl
<=> ( leq(hd(sk1),X0)
| ~ ssList(X1)
| leq(X0,hd(sk1))
| ~ ssList(app(cons(hd(sk1),sk4),cons(X0,X1)))
| ~ totalorderP(app(app(sk1,cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1885,plain,
( ~ sQ147_spl
| ~ sQ38_spl
| ~ sQ20_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f1833,f1882,f620,f525,f573,f746,f1740]) ).
fof(f1914,plain,
! [X0] :
( ~ sQ163_spl
| ~ ssList(cons(hd(sk1),sk4))
| tl(cons(hd(sk1),sk4)) != tl(X0)
| cons(hd(sk1),sk4) = X0
| X0 = nil
| nil = cons(hd(sk1),sk4)
| hd(X0) != hd(sk1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1875,f412]) ).
fof(f1916,plain,
( ~ sQ163_spl
| cons(hd(sk1),sk4) = cons(hd(sk1),tl(cons(hd(sk1),sk4)))
| ~ ssList(cons(hd(sk1),sk4))
| cons(hd(sk1),sk4) = nil ),
inference(paramodulation,[status(thm)],[f1875,f304]) ).
fof(f1918,definition,
! [X0] :
( sQ170_spl
<=> ( tl(cons(hd(sk1),sk4)) != tl(X0)
| cons(hd(sk1),sk4) = X0
| X0 = nil
| hd(X0) != hd(sk1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1921,plain,
( ~ sQ163_spl
| ~ sQ164_spl
| sQ159_spl
| sQ170_spl ),
inference(split_clause,[status(thm)],[f1914,f1918,f1856,f1878,f1874]) ).
fof(f1928,definition,
( sQ172_spl
<=> cons(hd(sk1),sk4) = cons(hd(sk1),tl(cons(hd(sk1),sk4))) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1929,plain,
( ~ sQ172_spl
| cons(hd(sk1),tl(cons(hd(sk1),sk4))) = cons(hd(sk1),sk4) ),
inference(component_clause,[status(thm)],[f1928]) ).
fof(f1931,plain,
( ~ sQ163_spl
| sQ172_spl
| ~ sQ164_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f1916,f1856,f1878,f1928,f1874]) ).
fof(f1939,plain,
! [X0] :
( ~ sQ26_spl
| rearsegP(sk4,X0)
| ~ rearsegP(cons(hd(sk1),nil),X0)
| ~ ssList(X0)
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f624,f348]) ).
fof(f1940,definition,
! [X0] :
( sQ173_spl
<=> ( rearsegP(sk4,X0)
| ~ rearsegP(cons(hd(sk1),nil),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1943,plain,
( ~ sQ26_spl
| sQ173_spl
| ~ sQ23_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1939,f617,f614,f1940,f623]) ).
fof(f1946,plain,
! [X0] :
( ~ sQ158_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ ssList(sk4)
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(resolution,[status(thm)],[f1853,f389]) ).
fof(f1947,definition,
! [X0] :
( sQ174_spl
<=> ( hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1948,plain,
! [X0] :
( ~ sQ174_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f1947]) ).
fof(f1950,plain,
( ~ sQ158_spl
| ~ sQ17_spl
| ~ sQ25_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f1946,f1947,f620,f553,f1852]) ).
fof(f1951,plain,
! [X0] :
( ~ sQ174_spl
| ~ memberP(sk1,X0)
| X0 = hd(sk1)
| ~ ssItem(X0)
| memberP(sk4,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1948]) ).
fof(f1952,plain,
( sQ2_spl
| ~ sQ174_spl
| ~ memberP(sk1,sk5)
| sk5 = hd(sk1)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1951,f511]) ).
fof(f1954,plain,
( sQ2_spl
| ~ sQ174_spl
| ~ sQ3_spl
| sQ123_spl
| ~ sQ122_spl ),
inference(split_clause,[status(thm)],[f1952,f1471,f1481,f451,f1947,f448]) ).
fof(f1960,plain,
! [X0,X1,X2] :
( ~ sQ172_spl
| ~ ssList(X0)
| leq(X1,hd(sk1))
| ~ ssList(tl(cons(hd(sk1),sk4)))
| leq(hd(sk1),X1)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sk1),sk4)))
| ~ totalorderP(app(app(X0,cons(X1,X2)),cons(hd(sk1),tl(cons(hd(sk1),sk4)))))
| ~ ssItem(hd(sk1)) ),
inference(paramodulation,[status(thm)],[f1929,f483]) ).
fof(f1961,plain,
! [X0,X1,X2] :
( ~ sQ172_spl
| ~ ssList(X1)
| leq(hd(sk1),X0)
| ~ ssList(X2)
| leq(X0,hd(sk1))
| ~ ssList(tl(cons(hd(sk1),sk4)))
| ~ ssItem(hd(sk1))
| ~ ssList(app(app(X1,cons(hd(sk1),sk4)),cons(X0,X2)))
| ~ totalorderP(app(app(X1,cons(hd(sk1),tl(cons(hd(sk1),sk4)))),cons(X0,X2)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f1929,f483]) ).
fof(f1962,plain,
! [X0] :
( ~ sQ172_spl
| ~ ssList(tl(cons(hd(sk1),sk4)))
| ~ ssItem(hd(sk1))
| memberP(cons(hd(sk1),sk4),X0)
| ~ ssItem(X0)
| ~ memberP(tl(cons(hd(sk1),sk4)),X0) ),
inference(paramodulation,[status(thm)],[f1929,f351]) ).
fof(f1963,plain,
! [X0] :
( ~ sQ172_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(tl(cons(hd(sk1),sk4)),X0)
| ~ memberP(cons(hd(sk1),sk4),X0)
| ~ ssList(tl(cons(hd(sk1),sk4)))
| ~ ssItem(hd(sk1)) ),
inference(paramodulation,[status(thm)],[f1929,f389]) ).
fof(f1964,plain,
( ~ sQ172_spl
| ~ ssItem(hd(sk1))
| memberP(cons(hd(sk1),sk4),hd(sk1))
| ~ ssList(tl(cons(hd(sk1),sk4))) ),
inference(paramodulation,[status(thm)],[f1929,f487]) ).
fof(f1966,plain,
( ~ sQ172_spl
| ~ ssItem(hd(sk1))
| tl(cons(hd(sk1),sk4)) = tl(cons(hd(sk1),sk4))
| ~ ssList(tl(cons(hd(sk1),sk4))) ),
inference(paramodulation,[status(thm)],[f1929,f294]) ).
fof(f1967,plain,
! [X0] :
( ~ sQ172_spl
| ~ ssItem(hd(sk1))
| ~ ssList(X0)
| ~ ssList(tl(cons(hd(sk1),sk4)))
| cons(hd(sk1),app(tl(cons(hd(sk1),sk4)),X0)) = app(cons(hd(sk1),sk4),X0) ),
inference(paramodulation,[status(thm)],[f1929,f381]) ).
fof(f1970,plain,
( ~ sQ172_spl
| ~ ssList(tl(cons(hd(sk1),sk4)))
| ~ ssItem(hd(sk1))
| tl(cons(hd(sk1),sk4)) != cons(hd(sk1),sk4) ),
inference(paramodulation,[status(thm)],[f1929,f299]) ).
fof(f1971,plain,
! [X0,X1,X2] :
( ~ sQ172_spl
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sk1),tl(cons(hd(sk1),sk4)))))
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(hd(sk1))
| lt(X1,hd(sk1))
| ~ ssList(X0)
| ~ ssList(tl(cons(hd(sk1),sk4)))
| ~ strictorderedP(app(app(X0,cons(X1,X2)),cons(hd(sk1),sk4))) ),
inference(paramodulation,[status(thm)],[f1929,f482]) ).
fof(f1972,plain,
! [X0,X1,X2] :
( ~ sQ172_spl
| ~ ssList(app(app(X0,cons(hd(sk1),tl(cons(hd(sk1),sk4)))),cons(X1,X2)))
| ~ ssList(tl(cons(hd(sk1),sk4)))
| ~ ssItem(hd(sk1))
| ~ ssItem(X1)
| lt(hd(sk1),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X0,cons(hd(sk1),sk4)),cons(X1,X2))) ),
inference(paramodulation,[status(thm)],[f1929,f482]) ).
fof(f1973,definition,
( sQ175_spl
<=> ssList(tl(cons(hd(sk1),sk4))) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f1975,plain,
( sQ175_spl
| ~ ssList(tl(cons(hd(sk1),sk4))) ),
inference(component_clause,[status(thm)],[f1973]) ).
fof(f1976,definition,
! [X0] :
( sQ176_spl
<=> ( hd(sk1) = X0
| ~ ssItem(X0)
| memberP(tl(cons(hd(sk1),sk4)),X0)
| ~ memberP(cons(hd(sk1),sk4),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1979,plain,
( ~ sQ172_spl
| sQ176_spl
| ~ sQ175_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1963,f620,f1973,f1976,f1928]) ).
fof(f1980,definition,
! [X0,X1,X2] :
( sQ177_spl
<=> ( ~ ssList(app(app(X0,cons(hd(sk1),tl(cons(hd(sk1),sk4)))),cons(X1,X2)))
| ~ ssItem(X1)
| lt(hd(sk1),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X0,cons(hd(sk1),sk4)),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1983,plain,
( ~ sQ172_spl
| ~ sQ175_spl
| ~ sQ25_spl
| sQ177_spl ),
inference(split_clause,[status(thm)],[f1972,f1980,f620,f1973,f1928]) ).
fof(f1984,definition,
! [X0,X1,X2] :
( sQ178_spl
<=> ( ~ ssList(X0)
| leq(X1,hd(sk1))
| leq(hd(sk1),X1)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sk1),sk4)))
| ~ totalorderP(app(app(X0,cons(X1,X2)),cons(hd(sk1),tl(cons(hd(sk1),sk4))))) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1987,plain,
( ~ sQ172_spl
| ~ sQ175_spl
| sQ178_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1960,f620,f1984,f1973,f1928]) ).
fof(f1988,definition,
( sQ179_spl
<=> memberP(cons(hd(sk1),sk4),hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1991,plain,
( ~ sQ172_spl
| ~ sQ25_spl
| sQ179_spl
| ~ sQ175_spl ),
inference(split_clause,[status(thm)],[f1964,f1973,f1988,f620,f1928]) ).
fof(f1992,definition,
! [X0,X1,X2] :
( sQ180_spl
<=> ( ~ ssList(X1)
| leq(hd(sk1),X0)
| ~ ssList(X2)
| leq(X0,hd(sk1))
| ~ ssList(app(app(X1,cons(hd(sk1),sk4)),cons(X0,X2)))
| ~ totalorderP(app(app(X1,cons(hd(sk1),tl(cons(hd(sk1),sk4)))),cons(X0,X2)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1995,plain,
( ~ sQ172_spl
| ~ sQ175_spl
| ~ sQ25_spl
| sQ180_spl ),
inference(split_clause,[status(thm)],[f1961,f1992,f620,f1973,f1928]) ).
fof(f1996,definition,
( sQ181_spl
<=> tl(cons(hd(sk1),sk4)) = tl(cons(hd(sk1),sk4)) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f1999,plain,
( ~ sQ172_spl
| ~ sQ25_spl
| sQ181_spl
| ~ sQ175_spl ),
inference(split_clause,[status(thm)],[f1966,f1973,f1996,f620,f1928]) ).
fof(f2000,definition,
! [X0,X1,X2] :
( sQ182_spl
<=> ( ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sk1),tl(cons(hd(sk1),sk4)))))
| ~ ssList(X2)
| ~ ssItem(X1)
| lt(X1,hd(sk1))
| ~ ssList(X0)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),cons(hd(sk1),sk4))) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2003,plain,
( ~ sQ172_spl
| ~ sQ25_spl
| ~ sQ175_spl
| sQ182_spl ),
inference(split_clause,[status(thm)],[f1971,f2000,f1973,f620,f1928]) ).
fof(f2004,definition,
! [X0] :
( sQ183_spl
<=> ( memberP(cons(hd(sk1),sk4),X0)
| ~ ssItem(X0)
| ~ memberP(tl(cons(hd(sk1),sk4)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f2007,plain,
( ~ sQ172_spl
| ~ sQ175_spl
| ~ sQ25_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f1962,f2004,f620,f1973,f1928]) ).
fof(f2009,definition,
( sQ184_spl
<=> tl(cons(hd(sk1),sk4)) = cons(hd(sk1),sk4) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f2012,plain,
( ~ sQ172_spl
| ~ sQ175_spl
| ~ sQ25_spl
| ~ sQ184_spl ),
inference(split_clause,[status(thm)],[f1970,f2009,f620,f1973,f1928]) ).
fof(f2014,definition,
! [X0] :
( sQ185_spl
<=> ( ~ ssList(X0)
| cons(hd(sk1),app(tl(cons(hd(sk1),sk4)),X0)) = app(cons(hd(sk1),sk4),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2017,plain,
( ~ sQ172_spl
| ~ sQ25_spl
| ~ sQ175_spl
| sQ185_spl ),
inference(split_clause,[status(thm)],[f1967,f2014,f1973,f620,f1928]) ).
fof(f2019,plain,
( sQ175_spl
| cons(hd(sk1),sk4) = nil
| ~ ssList(cons(hd(sk1),sk4)) ),
inference(resolution,[status(thm)],[f1975,f275]) ).
fof(f2020,plain,
( sQ175_spl
| sQ159_spl
| ~ sQ164_spl ),
inference(split_clause,[status(thm)],[f2019,f1878,f1856,f1973]) ).
fof(f2021,plain,
( sQ164_spl
| ~ ssList(sk4)
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f1880,f284]) ).
fof(f2022,plain,
( sQ164_spl
| ~ sQ17_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2021,f620,f553,f1878]) ).
fof(f2040,plain,
! [X0] :
( ~ sQ157_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ ssList(sk4)
| ~ ssItem(hd(sk1))
| ~ memberP(cons(hd(sk1),nil),X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1849,f389]) ).
fof(f2041,definition,
! [X0] :
( sQ187_spl
<=> ( hd(sk1) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(cons(hd(sk1),nil),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f2044,plain,
( ~ sQ157_spl
| ~ sQ17_spl
| ~ sQ25_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f2040,f2041,f620,f553,f1848]) ).
fof(f2047,plain,
! [X0] :
( ~ sQ48_spl
| hd(sk1) = X0
| ~ ssItem(X0)
| memberP(nil,X0)
| ~ ssList(nil)
| ~ ssItem(hd(sk1))
| memberP(tl(sk1),X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(resolution,[status(thm)],[f819,f389]) ).
fof(f2048,definition,
! [X0] :
( sQ188_spl
<=> ( hd(sk1) = X0
| ~ ssItem(X0)
| memberP(nil,X0)
| memberP(tl(sk1),X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2051,plain,
( ~ sQ48_spl
| ~ sQ11_spl
| ~ sQ25_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f2047,f2048,f620,f525,f818]) ).
fof(f2057,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssList(X0)
| leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4)
| leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil))))
| ~ totalorderP(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f483]) ).
fof(f2058,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssList(X1)
| leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ ssList(X2)
| leq(X0,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(app(app(X1,app(sk1,cons(hd(sk1),nil))),cons(X0,X2)))
| ~ totalorderP(app(app(X1,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X0,X2)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f956,f483]) ).
fof(f2060,plain,
! [X0] :
( ~ sQ60_spl
| hd(app(sk1,cons(hd(sk1),nil))) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(app(sk1,cons(hd(sk1),nil)),X0)
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f389]) ).
fof(f2064,plain,
! [X0] :
( ~ sQ60_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0)
| ~ ssList(sk4)
| cons(hd(app(sk1,cons(hd(sk1),nil))),app(sk4,X0)) = app(app(sk1,cons(hd(sk1),nil)),X0) ),
inference(paramodulation,[status(thm)],[f956,f381]) ).
fof(f2068,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| lt(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f482]) ).
fof(f2069,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssList(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X1)
| lt(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2))) ),
inference(paramodulation,[status(thm)],[f956,f482]) ).
fof(f2074,definition,
! [X0,X1,X2] :
( sQ189_spl
<=> ( ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(X2)
| ~ ssItem(X1)
| lt(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2077,plain,
( ~ sQ60_spl
| ~ sQ66_spl
| ~ sQ17_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f2068,f2074,f553,f1002,f955]) ).
fof(f2078,definition,
! [X0] :
( sQ190_spl
<=> ( hd(app(sk1,cons(hd(sk1),nil))) = X0
| ~ ssItem(X0)
| memberP(sk4,X0)
| ~ memberP(app(sk1,cons(hd(sk1),nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2079,plain,
! [X0] :
( ~ sQ190_spl
| ~ memberP(app(sk1,cons(hd(sk1),nil)),X0)
| ~ ssItem(X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f2078]) ).
fof(f2081,plain,
( ~ sQ60_spl
| sQ190_spl
| ~ sQ17_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f2060,f1002,f553,f2078,f955]) ).
fof(f2082,definition,
! [X0,X1,X2] :
( sQ191_spl
<=> ( ~ ssList(X0)
| leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil))))
| ~ totalorderP(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4))) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f2085,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| sQ191_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f2057,f1002,f2082,f553,f955]) ).
fof(f2086,definition,
! [X0,X1,X2] :
( sQ192_spl
<=> ( ~ ssList(X1)
| leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ ssList(X2)
| leq(X0,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(app(app(X1,app(sk1,cons(hd(sk1),nil))),cons(X0,X2)))
| ~ totalorderP(app(app(X1,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X0,X2)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2089,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| ~ sQ66_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f2058,f2086,f1002,f553,f955]) ).
fof(f2090,definition,
! [X0] :
( sQ193_spl
<=> ( ~ ssList(X0)
| cons(hd(app(sk1,cons(hd(sk1),nil))),app(sk4,X0)) = app(app(sk1,cons(hd(sk1),nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f2093,plain,
( ~ sQ60_spl
| ~ sQ66_spl
| ~ sQ17_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f2064,f2090,f553,f1002,f955]) ).
fof(f2096,definition,
! [X0,X1,X2] :
( sQ194_spl
<=> ( ~ ssList(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssItem(X1)
| lt(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2099,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| ~ sQ66_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f2069,f2096,f1002,f553,f955]) ).
fof(f2115,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(app(nil,X0))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f272,f368]) ).
fof(f2117,definition,
! [X0] :
( sQ196_spl
<=> ( app(nil,X0) = X0
| ~ ssList(app(nil,X0))
| ~ ssList(X0)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( ~ sQ11_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f2115,f2117,f525]) ).
fof(f2127,definition,
( sQ197_spl
<=> memberP(nil,hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f2128,plain,
( ~ sQ197_spl
| memberP(nil,hd(sk1)) ),
inference(component_clause,[status(thm)],[f2127]) ).
fof(f2133,plain,
! [X0] :
( ~ sQ26_spl
| segmentP(app(sk4,X0),cons(hd(sk1),nil))
| ~ ssList(X0)
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(app(app(tl(sk1),cons(hd(sk1),nil)),X0)) ),
inference(paramodulation,[status(thm)],[f624,f490]) ).
fof(f2134,definition,
! [X0] :
( sQ198_spl
<=> ( segmentP(app(sk4,X0),cons(hd(sk1),nil))
| ~ ssList(X0)
| ~ ssList(app(app(tl(sk1),cons(hd(sk1),nil)),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f2137,plain,
( ~ sQ26_spl
| ~ sQ23_spl
| ~ sQ24_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f2133,f2134,f617,f614,f623]) ).
fof(f2140,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ ssItem(hd(sk1))
| ~ leq(hd(sk1),X0)
| ~ cyclefreeP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(nil)
| ~ ssList(tl(sk1))
| ~ ssList(X1)
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ leq(X0,hd(sk1))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f624,f491]) ).
fof(f2141,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ cyclefreeP(app(app(X1,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X0,X2)))
| ~ ssList(sk4)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(app(app(X1,app(sk1,cons(hd(sk1),nil))),cons(X0,X2)))
| ~ leq(X0,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f956,f491]) ).
fof(f2142,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssItem(X0)
| ~ leq(X0,hd(app(sk1,cons(hd(sk1),nil))))
| ~ cyclefreeP(app(app(X1,cons(X0,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(sk4)
| ~ ssList(app(app(X1,cons(X0,X2)),app(sk1,cons(hd(sk1),nil))))
| ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f491]) ).
fof(f2143,definition,
! [X0,X1,X2] :
( sQ199_spl
<=> ( ~ ssItem(X0)
| ~ leq(X0,hd(app(sk1,cons(hd(sk1),nil))))
| ~ cyclefreeP(app(app(X1,cons(X0,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(app(app(X1,cons(X0,X2)),app(sk1,cons(hd(sk1),nil))))
| ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f2146,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| sQ199_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f2142,f1002,f2143,f553,f955]) ).
fof(f2148,definition,
! [X0,X1,X2] :
( sQ200_spl
<=> ( ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ cyclefreeP(app(app(X1,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X0,X2)))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(app(app(X1,app(sk1,cons(hd(sk1),nil))),cons(X0,X2)))
| ~ leq(X0,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f2151,plain,
( ~ sQ60_spl
| ~ sQ66_spl
| ~ sQ17_spl
| sQ200_spl ),
inference(split_clause,[status(thm)],[f2141,f2148,f553,f1002,f955]) ).
fof(f2152,definition,
! [X0,X1] :
( sQ201_spl
<=> ( ~ leq(hd(sk1),X0)
| ~ cyclefreeP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| ~ ssList(X1)
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ leq(X0,hd(sk1))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f2155,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ11_spl
| ~ sQ23_spl
| sQ201_spl ),
inference(split_clause,[status(thm)],[f2140,f2152,f614,f525,f620,f623]) ).
fof(f2162,plain,
! [X0] :
( ~ sQ190_spl
| ~ ssList(sk1)
| ~ ssItem(X0)
| ~ memberP(sk1,X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ ssItem(X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f2079,f352]) ).
fof(f2163,plain,
! [X0] :
( ~ sQ190_spl
| ~ ssItem(X0)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(cons(hd(sk1),nil),X0)
| ~ ssList(sk1)
| ~ ssItem(X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f2079,f353]) ).
fof(f2165,definition,
! [X0] :
( sQ202_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0)
| ~ ssItem(X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f2168,plain,
( ~ sQ190_spl
| ~ sQ24_spl
| ~ sQ20_spl
| sQ202_spl ),
inference(split_clause,[status(thm)],[f2163,f2165,f573,f617,f2078]) ).
fof(f2169,definition,
! [X0] :
( sQ203_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk1,X0)
| ~ ssItem(X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2170,plain,
! [X0] :
( ~ sQ203_spl
| ~ ssItem(X0)
| ~ memberP(sk1,X0)
| ~ ssItem(X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f2169]) ).
fof(f2172,plain,
( ~ sQ190_spl
| ~ sQ20_spl
| ~ sQ24_spl
| sQ203_spl ),
inference(split_clause,[status(thm)],[f2162,f2169,f617,f573,f2078]) ).
fof(f2174,plain,
! [X0] :
( ~ sQ203_spl
| memberP(sk4,X0)
| ~ memberP(sk1,X0)
| hd(app(sk1,cons(hd(sk1),nil))) = X0
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2170]) ).
fof(f2175,plain,
! [X0] :
( ~ sQ203_spl
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| tl(app(sk1,cons(hd(sk1),nil))) != tl(X0)
| app(sk1,cons(hd(sk1),nil)) = X0
| X0 = nil
| nil = app(sk1,cons(hd(sk1),nil))
| ~ ssList(X0)
| ~ ssItem(hd(X0))
| memberP(sk4,hd(X0))
| ~ memberP(sk1,hd(X0)) ),
inference(resolution,[status(thm)],[f2174,f412]) ).
fof(f2178,definition,
! [X0] :
( sQ204_spl
<=> ( tl(app(sk1,cons(hd(sk1),nil))) != tl(X0)
| app(sk1,cons(hd(sk1),nil)) = X0
| X0 = nil
| ~ ssList(X0)
| ~ ssItem(hd(X0))
| memberP(sk4,hd(X0))
| ~ memberP(sk1,hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f2181,plain,
( ~ sQ203_spl
| ~ sQ40_spl
| sQ41_spl
| sQ204_spl ),
inference(split_clause,[status(thm)],[f2175,f2178,f762,f759,f2169]) ).
fof(f2197,plain,
! [X0] :
( ~ frontsegP(nil,X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f257,f339]) ).
fof(f2199,definition,
! [X0] :
( sQ207_spl
<=> ( ~ frontsegP(nil,X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f2202,plain,
( ~ sQ11_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f2197,f2199,f525]) ).
fof(f2219,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ ssItem(hd(sk1))
| ~ ssList(nil)
| ~ totalorderedP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| leq(hd(sk1),X0)
| ~ ssList(tl(sk1))
| ~ ssList(X1)
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f624,f493]) ).
fof(f2220,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4)
| ~ totalorderedP(app(app(X1,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X0,X2)))
| leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(app(app(X1,app(sk1,cons(hd(sk1),nil))),cons(X0,X2)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f956,f493]) ).
fof(f2221,plain,
! [X0,X1,X2] :
( ~ sQ60_spl
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ totalorderedP(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f956,f493]) ).
fof(f2222,definition,
! [X0,X1,X2] :
( sQ210_spl
<=> ( ~ ssItem(X1)
| ~ ssList(X2)
| ~ totalorderedP(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0)
| ~ ssList(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f2225,plain,
( ~ sQ60_spl
| ~ sQ17_spl
| sQ210_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f2221,f1002,f2222,f553,f955]) ).
fof(f2227,definition,
! [X0,X1] :
( sQ211_spl
<=> ( ~ totalorderedP(app(app(tl(sk1),cons(hd(sk1),nil)),cons(X0,X1)))
| leq(hd(sk1),X0)
| ~ ssList(X1)
| ~ ssList(app(sk4,cons(X0,X1)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2230,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ11_spl
| ~ sQ23_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f2219,f2227,f614,f525,f620,f623]) ).
fof(f2231,definition,
! [X0,X1,X2] :
( sQ212_spl
<=> ( ~ totalorderedP(app(app(X1,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X0,X2)))
| leq(hd(app(sk1,cons(hd(sk1),nil))),X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(app(app(X1,app(sk1,cons(hd(sk1),nil))),cons(X0,X2)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f2234,plain,
( ~ sQ60_spl
| ~ sQ66_spl
| ~ sQ17_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f2220,f2231,f553,f1002,f955]) ).
fof(f2242,plain,
! [X0] :
( segmentP(app(nil,X0),nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(app(app(nil,nil),X0)) ),
inference(paramodulation,[status(thm)],[f896,f490]) ).
fof(f2243,plain,
! [X0] :
( rearsegP(nil,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f896,f348]) ).
fof(f2244,plain,
! [X0] :
( memberP(nil,X0)
| memberP(nil,X0)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f896,f383]) ).
fof(f2247,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(nil)
| ~ memberP(nil,X0)
| memberP(nil,X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f896,f353]) ).
fof(f2249,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| nil != app(nil,X0)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f896,f368]) ).
fof(f2253,definition,
! [X0] :
( sQ213_spl
<=> ( rearsegP(nil,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2256,plain,
( sQ213_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2243,f525,f2253]) ).
fof(f2259,definition,
! [X0] :
( sQ214_spl
<=> ( ~ ssItem(X0)
| ~ memberP(nil,X0)
| memberP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f2262,plain,
( sQ214_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2247,f525,f2259]) ).
fof(f2264,definition,
! [X0] :
( sQ215_spl
<=> ( segmentP(app(nil,X0),nil)
| ~ ssList(X0)
| ~ ssList(app(app(nil,nil),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2267,plain,
( ~ sQ11_spl
| sQ215_spl ),
inference(split_clause,[status(thm)],[f2242,f2264,f525]) ).
fof(f2276,definition,
! [X0] :
( sQ217_spl
<=> ( memberP(nil,X0)
| memberP(nil,X0)
| ~ memberP(nil,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f2279,plain,
( ~ sQ11_spl
| sQ217_spl ),
inference(split_clause,[status(thm)],[f2244,f2276,f525]) ).
fof(f2281,definition,
! [X0] :
( sQ218_spl
<=> ( X0 = nil
| ~ ssList(X0)
| nil != app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f2284,plain,
( sQ218_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2249,f525,f2281]) ).
fof(f2289,plain,
( ~ sQ197_spl
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f2128,f268]) ).
fof(f2290,plain,
( ~ sQ197_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2289,f620,f2127]) ).
fof(f2294,plain,
( ~ sQ112_spl
| ~ ssItem(hd(sk1))
| ~ lt(hd(sk1),hd(sk1))
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f1394,f317]) ).
fof(f2296,plain,
( ~ sQ112_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2294,f620,f1393]) ).
fof(f2297,definition,
( sQ219_spl
<=> leq(hd(sk1),hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f2298,plain,
( ~ sQ219_spl
| leq(hd(sk1),hd(sk1)) ),
inference(component_clause,[status(thm)],[f2297]) ).
fof(f2299,plain,
( sQ219_spl
| ~ leq(hd(sk1),hd(sk1)) ),
inference(component_clause,[status(thm)],[f2297]) ).
fof(f2306,definition,
( sQ221_spl
<=> strictorderedP(cons(hd(sk1),sk1)) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2312,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(nil)
| nil = X0
| nil != app(X0,nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f896,f370]) ).
fof(f2320,definition,
! [X0] :
( sQ222_spl
<=> ( nil = X0
| nil != app(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f2323,plain,
( ~ sQ11_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f2312,f2320,f525]) ).
fof(f2335,plain,
( sQ112_spl
| hd(sk1) = hd(sk1)
| ~ ssItem(hd(sk1))
| ~ ssItem(hd(sk1))
| ~ leq(hd(sk1),hd(sk1)) ),
inference(resolution,[status(thm)],[f1395,f330]) ).
fof(f2336,plain,
! [X0] :
( sQ112_spl
| ~ ssItem(hd(sk1))
| ~ ssItem(hd(sk1))
| ~ lt(X0,hd(sk1))
| ~ ssItem(X0)
| ~ leq(hd(sk1),X0) ),
inference(resolution,[status(thm)],[f1395,f363]) ).
fof(f2337,definition,
! [X0] :
( sQ223_spl
<=> ( ~ lt(X0,hd(sk1))
| ~ ssItem(X0)
| ~ leq(hd(sk1),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2340,plain,
( sQ112_spl
| ~ sQ25_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f2336,f2337,f620,f1393]) ).
fof(f2341,plain,
( sQ112_spl
| sQ80_spl
| ~ sQ25_spl
| ~ sQ219_spl ),
inference(split_clause,[status(thm)],[f2335,f2297,f620,f1110,f1393]) ).
fof(f2351,plain,
( sQ219_spl
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f2299,f259]) ).
fof(f2356,plain,
( sQ219_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2351,f620,f2297]) ).
fof(f2358,plain,
! [X0] :
( ~ sQ219_spl
| ~ ssItem(hd(sk1))
| ~ ssItem(X0)
| ~ leq(X0,hd(sk1))
| leq(X0,hd(sk1))
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f2298,f380]) ).
fof(f2360,plain,
! [X0] :
( ~ sQ219_spl
| ~ ssItem(hd(sk1))
| ~ ssItem(hd(sk1))
| ~ leq(hd(sk1),X0)
| leq(hd(sk1),X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f2298,f380]) ).
fof(f2361,definition,
! [X0] :
( sQ227_spl
<=> ( ~ ssItem(X0)
| ~ leq(X0,hd(sk1))
| leq(X0,hd(sk1)) ) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f2364,plain,
( ~ sQ219_spl
| sQ227_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2358,f620,f2361,f2297]) ).
fof(f2366,definition,
! [X0] :
( sQ228_spl
<=> ( ~ leq(hd(sk1),X0)
| leq(hd(sk1),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f2369,plain,
( ~ sQ219_spl
| ~ sQ25_spl
| sQ228_spl ),
inference(split_clause,[status(thm)],[f2360,f2366,f620,f2297]) ).
fof(f2377,plain,
( ~ sQ28_spl
| ~ ssList(skaf73(nil))
| ~ ssItem(skaf70(nil)) ),
inference(resolution,[status(thm)],[f634,f297]) ).
fof(f2395,definition,
( sQ229_spl
<=> ssItem(skaf70(nil)) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f2397,plain,
( sQ229_spl
| ~ ssItem(skaf70(nil)) ),
inference(component_clause,[status(thm)],[f2395]) ).
fof(f2398,definition,
( sQ230_spl
<=> ssList(skaf73(nil)) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2400,plain,
( sQ230_spl
| ~ ssList(skaf73(nil)) ),
inference(component_clause,[status(thm)],[f2398]) ).
fof(f2445,plain,
( ~ sQ28_spl
| ~ sQ230_spl
| ~ sQ229_spl ),
inference(split_clause,[status(thm)],[f2377,f2395,f2398,f633]) ).
fof(f2464,plain,
( sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2400,f219]) ).
fof(f2465,plain,
sQ230_spl,
inference(contradiction_clause,[status(thm)],[f2464]) ).
fof(f2466,plain,
( sQ229_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2397,f222]) ).
fof(f2467,plain,
sQ229_spl,
inference(contradiction_clause,[status(thm)],[f2466]) ).
fof(f2501,plain,
( ~ sQ45_spl
| ~ ssList(sk1)
| frontsegP(nil,sk1)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f789,f258]) ).
fof(f2503,definition,
( sQ250_spl
<=> frontsegP(nil,sk1) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f2504,plain,
( ~ sQ250_spl
| frontsegP(nil,sk1) ),
inference(component_clause,[status(thm)],[f2503]) ).
fof(f2505,plain,
( sQ250_spl
| ~ frontsegP(nil,sk1) ),
inference(component_clause,[status(thm)],[f2503]) ).
fof(f2506,plain,
( ~ sQ45_spl
| sQ250_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f2501,f573,f2503,f788]) ).
fof(f2507,plain,
( ~ sQ250_spl
| ~ ssList(sk1)
| nil = sk1 ),
inference(resolution,[status(thm)],[f2504,f282]) ).
fof(f2509,definition,
( sQ251_spl
<=> frontsegP(sk1,nil) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f2510,plain,
( ~ sQ251_spl
| frontsegP(sk1,nil) ),
inference(component_clause,[status(thm)],[f2509]) ).
fof(f2511,plain,
( sQ251_spl
| ~ frontsegP(sk1,nil) ),
inference(component_clause,[status(thm)],[f2509]) ).
fof(f2513,plain,
( ~ sQ250_spl
| ~ sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2507,f566,f573,f2503]) ).
fof(f2514,plain,
( sQ251_spl
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f2511,f257]) ).
fof(f2515,plain,
( sQ251_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f2514,f573,f2509]) ).
fof(f2518,plain,
( ~ sQ94_spl
| ~ ssList(sk4)
| ~ ssList(sk4)
| sk1 = sk4 ),
inference(resolution,[status(thm)],[f1258,f272]) ).
fof(f2520,plain,
( ~ sQ94_spl
| ~ sQ17_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f2518,f1377,f553,f1257]) ).
fof(f2573,plain,
( sQ112_spl
| sk1 = nil
| ~ ssItem(hd(sk1))
| ~ ssList(sk1)
| ~ strictorderedP(cons(hd(sk1),sk1)) ),
inference(resolution,[status(thm)],[f345,f1395]) ).
fof(f2581,plain,
( sQ112_spl
| sQ18_spl
| ~ sQ25_spl
| ~ sQ20_spl
| ~ sQ221_spl ),
inference(split_clause,[status(thm)],[f2573,f2306,f573,f620,f566,f1393]) ).
fof(f2588,plain,
! [X0] :
( sQ250_spl
| ~ frontsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(X0,sk1)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f376,f2505]) ).
fof(f2589,plain,
! [X0,X1] :
( ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f376,f282]) ).
fof(f2592,plain,
! [X0] :
( ~ sQ251_spl
| frontsegP(sk1,X0)
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f376,f2510]) ).
fof(f2593,plain,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f376,f931]) ).
fof(f2594,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(X1,X0)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f376,f257]) ).
fof(f2597,definition,
! [X0,X1] :
( sQ252_spl
<=> ( ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X1)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f2600,plain,
( ~ sQ11_spl
| sQ252_spl ),
inference(split_clause,[status(thm)],[f2589,f2597,f525]) ).
fof(f2603,definition,
! [X0] :
( sQ253_spl
<=> ( frontsegP(nil,X0)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f2606,plain,
( ~ sQ11_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f2593,f2603,f525]) ).
fof(f2607,definition,
! [X0] :
( sQ254_spl
<=> ( ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk1) ) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f2610,plain,
( sQ250_spl
| ~ sQ11_spl
| sQ254_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f2588,f573,f2607,f525,f2503]) ).
fof(f2611,definition,
! [X0,X1] :
( sQ255_spl
<=> ( ~ ssList(X1)
| frontsegP(X1,X0)
| ~ ssList(X1)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f2614,plain,
( ~ sQ11_spl
| sQ255_spl ),
inference(split_clause,[status(thm)],[f2594,f2611,f525]) ).
fof(f2616,definition,
! [X0] :
( sQ256_spl
<=> ( frontsegP(sk1,X0)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f2619,plain,
( ~ sQ251_spl
| ~ sQ20_spl
| ~ sQ11_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f2592,f2616,f525,f573,f2509]) ).
fof(f2622,plain,
( ~ ssList(nil)
| rearsegP(nil,nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f896,f718]) ).
fof(f2623,definition,
( sQ257_spl
<=> rearsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f2626,plain,
( sQ257_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2622,f525,f2623]) ).
fof(f2635,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(X0)
| app(nil,app(nil,X0)) = app(nil,X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f896,f366]) ).
fof(f2636,definition,
! [X0] :
( sQ258_spl
<=> ( ~ ssList(X0)
| app(nil,app(nil,X0)) = app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f2639,plain,
( sQ258_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2635,f525,f2636]) ).
fof(f2720,plain,
! [X0,X1] :
( ~ sQ60_spl
| X1 = hd(app(sk1,cons(hd(sk1),nil)))
| ~ ssItem(X1)
| app(sk1,cons(hd(sk1),nil)) != cons(X1,X0)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f956,f399]) ).
fof(f2743,definition,
! [X0,X1] :
( sQ259_spl
<=> ( X1 = hd(app(sk1,cons(hd(sk1),nil)))
| ~ ssItem(X1)
| app(sk1,cons(hd(sk1),nil)) != cons(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f2744,plain,
! [X0,X1] :
( ~ sQ259_spl
| ~ ssItem(X0)
| ~ ssList(X1)
| app(sk1,cons(hd(sk1),nil)) != cons(X0,X1)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f2743]) ).
fof(f2746,plain,
( ~ sQ60_spl
| ~ sQ66_spl
| ~ sQ17_spl
| sQ259_spl ),
inference(split_clause,[status(thm)],[f2720,f2743,f553,f1002,f955]) ).
fof(f2763,plain,
( ~ sQ259_spl
| nil = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| ~ ssItem(skaf83(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(skaf82(app(sk1,cons(hd(sk1),nil))))
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f2744,f309]) ).
fof(f2769,definition,
( sQ261_spl
<=> skaf83(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f2770,plain,
( ~ sQ261_spl
| hd(app(sk1,cons(hd(sk1),nil))) = skaf83(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f2769]) ).
fof(f2772,definition,
( sQ262_spl
<=> ssList(skaf82(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f2774,plain,
( sQ262_spl
| ~ ssList(skaf82(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f2772]) ).
fof(f2775,definition,
( sQ263_spl
<=> ssItem(skaf83(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f2777,plain,
( sQ263_spl
| ~ ssItem(skaf83(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f2775]) ).
fof(f2778,plain,
( ~ sQ259_spl
| sQ41_spl
| ~ sQ40_spl
| ~ sQ263_spl
| ~ sQ262_spl
| sQ261_spl ),
inference(split_clause,[status(thm)],[f2763,f2769,f2772,f2775,f759,f762,f2743]) ).
fof(f2780,definition,
( sQ264_spl
<=> ssList(tl(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f2782,plain,
( sQ264_spl
| ~ ssList(tl(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f2780]) ).
fof(f2784,plain,
( sQ263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2777,f209]) ).
fof(f2785,plain,
sQ263_spl,
inference(contradiction_clause,[status(thm)],[f2784]) ).
fof(f2786,plain,
( sQ264_spl
| ~ sQ38_spl
| ~ ssList(sk4) ),
inference(forward_demodulation,[status(thm)],[f747,f2782]) ).
fof(f2787,plain,
( sQ264_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2786,f431]) ).
fof(f2788,plain,
( sQ264_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f2787]) ).
fof(f2789,plain,
( sQ262_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2774,f210]) ).
fof(f2790,plain,
sQ262_spl,
inference(contradiction_clause,[status(thm)],[f2789]) ).
fof(f2800,plain,
( ~ sQ261_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk1)
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(sk1)
| nil = sk1 ),
inference(paramodulation,[status(thm)],[f2770,f331]) ).
fof(f2801,plain,
! [X0] :
( ~ sQ261_spl
| app(sk1,cons(hd(sk1),nil)) = nil
| lt(X0,skaf83(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X0)
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| ~ strictorderedP(cons(X0,app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f2770,f345]) ).
fof(f2803,plain,
! [X0] :
( ~ sQ261_spl
| nil = app(sk1,cons(hd(sk1),nil))
| leq(X0,skaf83(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| ~ ssItem(X0)
| ~ totalorderedP(cons(X0,app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f2770,f347]) ).
fof(f2805,plain,
! [X0] :
( ~ sQ261_spl
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| tl(app(sk1,cons(hd(sk1),nil))) != tl(X0)
| app(sk1,cons(hd(sk1),nil)) = X0
| X0 = nil
| nil = app(sk1,cons(hd(sk1),nil))
| hd(X0) != skaf83(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f2770,f412]) ).
fof(f2807,plain,
( ~ sQ261_spl
| app(sk1,cons(hd(sk1),nil)) = cons(skaf83(app(sk1,cons(hd(sk1),nil))),tl(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| app(sk1,cons(hd(sk1),nil)) = nil ),
inference(paramodulation,[status(thm)],[f2770,f304]) ).
fof(f2808,definition,
! [X0] :
( sQ265_spl
<=> ( lt(X0,skaf83(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X0)
| ~ strictorderedP(cons(X0,app(sk1,cons(hd(sk1),nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f2811,plain,
( ~ sQ261_spl
| sQ41_spl
| ~ sQ40_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f2801,f2808,f759,f762,f2769]) ).
fof(f2812,definition,
! [X0] :
( sQ266_spl
<=> ( tl(app(sk1,cons(hd(sk1),nil))) != tl(X0)
| app(sk1,cons(hd(sk1),nil)) = X0
| X0 = nil
| hd(X0) != skaf83(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f2815,plain,
( ~ sQ261_spl
| ~ sQ40_spl
| sQ41_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f2805,f2812,f762,f759,f2769]) ).
fof(f2817,definition,
! [X0] :
( sQ267_spl
<=> ( leq(X0,skaf83(app(sk1,cons(hd(sk1),nil))))
| ~ ssItem(X0)
| ~ totalorderedP(cons(X0,app(sk1,cons(hd(sk1),nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f2820,plain,
( ~ sQ261_spl
| sQ41_spl
| ~ sQ40_spl
| sQ267_spl ),
inference(split_clause,[status(thm)],[f2803,f2817,f759,f762,f2769]) ).
fof(f2821,definition,
( sQ268_spl
<=> app(sk1,cons(hd(sk1),nil)) = cons(skaf83(app(sk1,cons(hd(sk1),nil))),tl(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f2824,plain,
( ~ sQ261_spl
| sQ268_spl
| ~ sQ40_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f2807,f762,f759,f2821,f2769]) ).
fof(f2825,definition,
( sQ269_spl
<=> skaf83(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f2826,plain,
( ~ sQ269_spl
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
inference(component_clause,[status(thm)],[f2825]) ).
fof(f2828,plain,
( ~ sQ261_spl
| ~ sQ24_spl
| ~ sQ20_spl
| sQ269_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2800,f566,f2825,f573,f617,f2769]) ).
fof(f2844,plain,
! [X0] :
( ~ sQ34_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(nil)
| segmentP(app(sk4,X0),nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f674,f253]) ).
fof(f2845,plain,
! [X0] :
( ~ sQ34_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(cons(hd(sk1),nil))
| segmentP(app(sk4,X0),cons(hd(sk1),nil))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f674,f254]) ).
fof(f2846,definition,
! [X0] :
( sQ273_spl
<=> ( segmentP(app(sk4,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition]) ).
fof(f2849,plain,
( ~ sQ34_spl
| ~ sQ24_spl
| ~ sQ11_spl
| sQ273_spl ),
inference(split_clause,[status(thm)],[f2844,f2846,f525,f617,f673]) ).
fof(f2850,definition,
! [X0] :
( sQ274_spl
<=> ( segmentP(app(sk4,X0),cons(hd(sk1),nil))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f2853,plain,
( ~ sQ34_spl
| ~ sQ24_spl
| sQ274_spl ),
inference(split_clause,[status(thm)],[f2845,f2850,f617,f673]) ).
fof(f2857,plain,
( ~ sQ261_spl
| ~ sQ269_spl
| hd(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
inference(backward_demodulation,[status(thm)],[f2826,f2770]) ).
fof(f2858,plain,
( ~ sQ269_spl
| nil = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| cons(hd(sk1),skaf82(app(sk1,cons(hd(sk1),nil)))) = app(sk1,cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f2826,f309]) ).
fof(f2860,plain,
( ~ sQ261_spl
| ~ sQ269_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f2857,f1706,f2825,f2769]) ).
fof(f2861,definition,
( sQ275_spl
<=> cons(hd(sk1),skaf82(app(sk1,cons(hd(sk1),nil)))) = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition]) ).
fof(f2864,plain,
( ~ sQ269_spl
| sQ41_spl
| ~ sQ40_spl
| sQ275_spl ),
inference(split_clause,[status(thm)],[f2858,f2861,f759,f762,f2825]) ).
fof(f2865,plain,
$false,
inference(sat_refutation,[status(thm)],[f454,f455,f462,f469,f476,f519,f556,f559,f561,f576,f578,f592,f613,f626,f628,f648,f650,f657,f667,f672,f676,f680,f684,f715,f731,f745,f749,f756,f769,f782,f794,f803,f809,f821,f825,f835,f839,f846,f883,f894,f904,f910,f920,f958,f971,f1005,f1009,f1013,f1018,f1024,f1027,f1032,f1042,f1047,f1052,f1204,f1279,f1283,f1303,f1327,f1348,f1352,f1358,f1360,f1376,f1380,f1384,f1388,f1392,f1402,f1406,f1411,f1422,f1427,f1432,f1436,f1458,f1465,f1470,f1474,f1476,f1484,f1517,f1544,f1546,f1568,f1585,f1591,f1613,f1631,f1658,f1697,f1704,f1717,f1721,f1739,f1743,f1748,f1775,f1777,f1782,f1786,f1792,f1798,f1802,f1822,f1847,f1851,f1855,f1859,f1863,f1867,f1871,f1877,f1885,f1921,f1931,f1943,f1950,f1954,f1979,f1983,f1987,f1991,f1995,f1999,f2003,f2007,f2012,f2017,f2020,f2022,f2044,f2051,f2077,f2081,f2085,f2089,f2093,f2099,f2120,f2137,f2146,f2151,f2155,f2168,f2172,f2181,f2202,f2225,f2230,f2234,f2256,f2262,f2267,f2279,f2284,f2290,f2296,f2323,f2340,f2341,f2356,f2364,f2369,f2445,f2465,f2467,f2506,f2513,f2515,f2520,f2581,f2600,f2606,f2610,f2614,f2619,f2626,f2639,f2746,f2778,f2785,f2788,f2790,f2811,f2815,f2820,f2824,f2828,f2849,f2853,f2860,f2864]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC376-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:22:51 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 149.36/19.31 % Refutation found
% 149.36/19.31 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 149.36/19.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.18/20.09 % Elapsed time: 19.715197 seconds
% 10.18/20.09 % CPU time: 151.254533 seconds
% 10.18/20.09 % Total memory used: 625.861 MB
% 10.18/20.09 % Net memory used: 580.476 MB
%------------------------------------------------------------------------------