%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC410-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:41:08 PM UTC 2026
% Result : Unsatisfiable 136.14s 18.72s
% Output : CNFRefutation 136.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 256
% Syntax : Number of formulae : 913 ( 93 unt; 169 def)
% Number of atoms : 3042 ( 394 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 4029 (1900 ~;1960 |; 0 &)
% ( 169 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 184 ( 182 usr; 170 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 6 con; 0-2 aty)
% Number of variables : 746 ( 746 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] : ssList(skaf80(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] : ssList(skaf73(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [U] : ssList(skaf72(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U] : ssList(skaf71(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] : ssItem(skaf70(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [U] : ssItem(skaf69(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [U] : ssList(skaf68(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] : ssList(skaf67(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [U] : ssList(skaf66(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U] : ssItem(skaf65(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [U] : ssItem(skaf64(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [U] : ssList(skaf63(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] : ssList(skaf58(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] : ssList(skaf53(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U] : ssItem(skaf44(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U,V] : ssList(skaf46(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [U,V] : ssList(skaf42(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [U] :
( rearsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [U] :
( strictorderedP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [U,V] :
( ssItem(V)
| duplicatefreeP(U)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ segmentP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ rearsegP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ frontsegP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = V
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [U,V] :
( hd(cons(U,V)) = U
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [U] :
( cons(skaf44(U),nil) = U
| ~ ssList(U)
| ~ singletonP(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [U,V] :
( singletonP(V)
| ~ ssList(V)
| ~ ssItem(U)
| cons(U,nil) != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ segmentP(V,U)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ rearsegP(V,U)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,axiom,
! [U,V] :
( app(skaf46(U,V),V) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [U,V] :
( app(V,skaf45(U,V)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [U,V,W] :
( segmentP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,axiom,
! [U,V,W] :
( rearsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [U] :
( app(app(skaf71(U),cons(skaf69(U),skaf72(U))),cons(skaf70(U),skaf73(U))) = U
| strictorderedP(U)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,axiom,
! [U] :
( app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U))) = U
| totalorderedP(U)
| ~ ssList(U) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [U,V] :
( app(skaf42(U,V),cons(V,skaf43(V,U))) = U
| ~ ssList(U)
| ~ ssItem(V)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [U,V,W,X] :
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f176,axiom,
! [U,V,W,X] :
( U = W
| ~ ssItem(U)
| ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,axiom,
! [U,V,W,X] :
( frontsegP(cons(W,U),cons(X,V))
| ~ ssItem(W)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(V)
| W != X
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [U,V,W,X,Y] :
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
memberP(sk2,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
~ memberP(sk1,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/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/sandbox/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(f212,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f219,plain,
! [X0] : ssList(skaf73(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f220,plain,
! [X0] : ssList(skaf72(X0)),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f221,plain,
! [X0] : ssList(skaf71(X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f222,plain,
! [X0] : ssItem(skaf70(X0)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f223,plain,
! [X0] : ssItem(skaf69(X0)),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f224,plain,
! [X0] : ssList(skaf68(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f225,plain,
! [X0] : ssList(skaf67(X0)),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f226,plain,
! [X0] : ssList(skaf66(X0)),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f227,plain,
! [X0] : ssItem(skaf65(X0)),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f228,plain,
! [X0] : ssItem(skaf64(X0)),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f229,plain,
! [X0] : ssList(skaf63(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f234,plain,
! [X0] : ssList(skaf58(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f239,plain,
! [X0] : ssList(skaf53(X0)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f244,plain,
! [X0] : ssItem(skaf44(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f247,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f248,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f250,plain,
! [X0,X1] : ssList(skaf42(X0,X1)),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f253,plain,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,nil) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f255,plain,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,nil) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f257,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f263,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f268,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f269,plain,
( ! [V] : ssItem(V)
| ! [U] :
( duplicatefreeP(U)
| ~ ssList(U) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f270,plain,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f271,plain,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f272,plain,
! [X0] :
( ~ ssList(X0)
| X0 = app(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f275,plain,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f276,plain,
! [X0] :
( ssItem(hd(X0))
| ~ ssList(X0)
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f278,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f280,plain,
! [X0] :
( X0 = nil
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f282,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f283,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f284,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f294,plain,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f295,plain,
! [X0,X1] :
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssList(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] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) != nil ),
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] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f301,plain,
! [X0] :
( ~ singletonP(X0)
| cons(skaf44(X0),nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f304,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| X0 = cons(hd(X0),tl(X0)) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f309,plain,
! [X0] :
( cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0)
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f109]) ).
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)
| X0 = nil
| ~ ssList(X0)
| nil != app(X0,X1) ),
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] :
( nil = X1
| ~ ssList(X1)
| nil != app(X0,X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f337,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f338,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f339,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f341,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = app(skaf46(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f342,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ frontsegP(X0,X1)
| app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
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(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(X1)
| ~ memberP(X1,X2)
| ~ ssItem(X2)
| memberP(cons(X0,X1),X2)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f353,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X2,X0),X1)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
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] :
( ~ ssList(X2)
| X1 = X2
| app(X0,X2) != app(X0,X1)
| ~ 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)
| ~ ssList(X0)
| app(X0,X2) != app(X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f371,plain,
! [U,W] :
( segmentP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ) ),
inference(miniscoping,[status(thm)],[f152]) ).
fof(f372,plain,
! [X0,X1,X2] :
( ~ segmentP(X2,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| segmentP(X2,X1)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f373,plain,
! [U,W] :
( rearsegP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V) ) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f374,plain,
! [X0,X1,X2] :
( ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ rearsegP(X2,X0)
| rearsegP(X2,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f373]) ).
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] :
( ~ ssList(X2)
| ~ frontsegP(X2,X0)
| frontsegP(X2,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f381,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ ssItem(X0)
| ~ 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(X0,X2)
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ memberP(app(X0,X1),X2) ),
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] :
( ~ memberP(cons(X2,X0),X1)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssItem(X2)
| X1 = X2
| memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f391,plain,
! [X0] :
( ~ ssList(X0)
| app(app(skaf71(X0),cons(skaf69(X0),skaf72(X0))),cons(skaf70(X0),skaf73(X0))) = X0
| strictorderedP(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f392,plain,
! [X0] :
( totalorderedP(X0)
| ~ ssList(X0)
| app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0))) = X0 ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f396,plain,
! [X0,X1] :
( app(app(skaf47(X1,X0),X0),skaf48(X0,X1)) = X1
| ~ segmentP(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f397,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ memberP(X1,X0)
| app(skaf42(X1,X0),cons(X0,skaf43(X0,X1))) = X1
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
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] :
( ~ ssItem(X1)
| ~ ssList(X3)
| cons(X1,X2) != cons(X0,X3)
| ~ ssList(X2)
| X0 = X1
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f400,plain,
! [V,X] :
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ! [U] :
( ~ ssItem(U)
| ! [W] :
( ~ ssItem(W)
| cons(U,V) != cons(W,X) ) ) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f401,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X0)
| cons(X3,X1) != cons(X2,X0)
| ~ ssList(X1)
| ~ ssItem(X3)
| ~ ssItem(X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f400]) ).
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(f409,plain,
! [U,W] :
( U = W
| ~ ssItem(U)
| ~ ssItem(W)
| ! [V] :
( ~ ssList(V)
| ! [X] :
( ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f410,plain,
! [X0,X1,X2,X3] :
( ~ ssItem(X1)
| ~ frontsegP(cons(X1,X0),cons(X2,X3))
| ~ ssList(X3)
| ~ ssItem(X2)
| X1 = X2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f413,plain,
! [X0,X1,X2,X3] :
( frontsegP(cons(X2,X0),cons(X3,X1))
| ~ ssItem(X2)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| X2 != X3
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f414,plain,
! [Y] :
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [X] :
( ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ) ) ) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f415,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(X4)
| ~ duplicatefreeP(X4)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3)
| app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4 ),
inference(cnf_transformation,[status(thm)],[f414]) ).
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(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(sk2,sk5),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f436,plain,
~ memberP(sk1,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(f441,definition,
! [X0] :
( sQ0_spl
<=> ( duplicatefreeP(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f442,plain,
! [X0] :
( ~ sQ0_spl
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(component_clause,[status(thm)],[f441]) ).
fof(f444,definition,
! [X1] :
( sQ1_spl
<=> ssItem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f445,plain,
! [X0] :
( ~ sQ1_spl
| ssItem(X0) ),
inference(component_clause,[status(thm)],[f444]) ).
fof(f447,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f270,f441,f444]) ).
fof(f448,definition,
( sQ2_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ2_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f450,plain,
( sQ2_spl
| sk3 != nil ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
( sQ3_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ3_spl
| sk4 = nil ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f437,f448,f451]) ).
fof(f455,definition,
( sQ4_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ4_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,definition,
( sQ5_spl
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f459,plain,
( ~ sQ5_spl
| neq(sk3,nil) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f438,f455,f458]) ).
fof(f462,definition,
! [X0,X1,X2,X3] :
( sQ6_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,[sQ6_spl])],[split_symbol_definition]) ).
fof(f463,plain,
! [X0,X1,X2,X3] :
( ~ sQ6_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)],[f462]) ).
fof(f465,definition,
( sQ7_spl
<=> neq(nil,sk3) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( sQ7_spl
| ~ neq(nil,sk3) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,plain,
( ~ sQ7_spl
| sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f440,f455,f462,f465]) ).
fof(f471,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f472,plain,
! [X0] :
( ~ neq(X0,X0)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f471]) ).
fof(f476,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f321]) ).
fof(f478,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f350]) ).
fof(f479,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| memberP(cons(X0,X1),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f478]) ).
fof(f488,plain,
! [X0,X1,X2] :
( ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| ~ ssList(X2)
| ~ ssList(X0)
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(destructive_equality_resolution,[status(thm)],[f408]) ).
fof(f489,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(destructive_equality_resolution,[status(thm)],[f415]) ).
fof(f490,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssItem(X1)
| ~ ssList(app(app(X3,cons(X0,X2)),cons(X1,X4)))
| ~ ssList(X4)
| ~ ssList(X3)
| ~ cyclefreeP(app(app(X3,cons(X0,X2)),cons(X1,X4)))
| ~ ssList(X2)
| ~ leq(X1,X0)
| ~ leq(X0,X1)
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f427]) ).
fof(f491,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssItem(X3)
| ~ ssList(app(app(X2,cons(X0,X1)),cons(X3,X4)))
| leq(X0,X3)
| ~ ssList(X2)
| ~ ssList(X4)
| ~ totalorderedP(app(app(X2,cons(X0,X1)),cons(X3,X4)))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f421]) ).
fof(f492,plain,
! [X0,X1,X3] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssItem(X3)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f413]) ).
fof(f493,plain,
! [X0,X1,X2] :
( ~ ssItem(X1)
| ~ frontsegP(X0,X2)
| ~ ssList(X2)
| frontsegP(cons(X1,X0),cons(X1,X2))
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f492]) ).
fof(f503,plain,
memberP(sk4,sk5),
inference(forward_demodulation,[status(thm)],[f432,f435]) ).
fof(f505,plain,
( ~ sQ2_spl
| sk3 = nil ),
inference(backward_demodulation,[status(thm)],[f508,f433]) ).
fof(f506,plain,
( ~ sQ2_spl
| ~ memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f508,f436]) ).
fof(f508,plain,
( ~ sQ2_spl
| sk1 = nil ),
inference(forward_demodulation,[status(thm)],[f433,f449]) ).
fof(f509,plain,
( ~ ssList(nil)
| ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f271,f327]) ).
fof(f510,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f512,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,definition,
( sQ9_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f509,f510,f513]) ).
fof(f517,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f512,f205]) ).
fof(f518,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f517]) ).
fof(f519,plain,
( sQ4_spl
| ~ ssList(nil)
| ~ ssList(sk4)
| nil = sk4 ),
inference(resolution,[status(thm)],[f300,f457]) ).
fof(f522,definition,
( sQ10_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f524,plain,
( sQ10_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f522]) ).
fof(f525,plain,
( sQ4_spl
| ~ sQ8_spl
| ~ sQ10_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f519,f451,f522,f510,f455]) ).
fof(f526,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f431]) ).
fof(f527,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f528,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| neq(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f505,f459]) ).
fof(f534,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f528,f472]) ).
fof(f535,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f534,f510,f448,f458]) ).
fof(f536,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil))) ),
inference(destructive_equality_resolution,[status(thm)],[f463]) ).
fof(f537,plain,
( ~ sQ6_spl
| ~ ssList(tl(sk3))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f536,f283]) ).
fof(f546,definition,
( sQ13_spl
<=> ssList(cons(skaf60(nil),skaf63(nil))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( sQ13_spl
| ~ ssList(cons(skaf60(nil),skaf63(nil))) ),
inference(component_clause,[status(thm)],[f546]) ).
fof(f555,plain,
( sQ2_spl
| nil != sk1 ),
inference(forward_demodulation,[status(thm)],[f433,f450]) ).
fof(f557,plain,
( ~ sQ6_spl
| ~ ssList(tl(sk3))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f537]) ).
fof(f558,plain,
( ~ sQ6_spl
| ~ ssList(tl(sk3))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssItem(hd(sk1))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f557]) ).
fof(f559,plain,
( ~ sQ6_spl
| ~ ssList(tl(sk3))
| sk4 = app(tl(sk1),cons(hd(sk3),nil))
| ~ ssItem(hd(sk1))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f558]) ).
fof(f560,plain,
( ~ sQ6_spl
| ~ ssList(tl(sk3))
| sk4 = app(tl(sk1),cons(hd(sk1),nil))
| ~ ssItem(hd(sk1))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f559]) ).
fof(f561,plain,
( ~ sQ6_spl
| ~ ssList(tl(sk1))
| ~ ssItem(hd(sk1))
| sk4 = app(tl(sk1),cons(hd(sk1),nil))
| ~ ssList(cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f560]) ).
fof(f578,definition,
( sQ16_spl
<=> ssList(tl(nil)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f580,plain,
( sQ16_spl
| ~ ssList(tl(nil)) ),
inference(component_clause,[status(thm)],[f578]) ).
fof(f581,definition,
( sQ17_spl
<=> ssItem(hd(nil)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( sQ17_spl
| ~ ssItem(hd(nil)) ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f585,plain,
! [X0] :
( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f370,f271]) ).
fof(f588,definition,
! [X0] :
( sQ18_spl
<=> ( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f591,plain,
( ~ sQ8_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f585,f588,f510]) ).
fof(f592,definition,
! [X0] :
( sQ19_spl
<=> ( X0 = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f595,definition,
! [X1] :
( sQ20_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f596,plain,
! [X0] :
( ~ sQ20_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f595]) ).
fof(f601,plain,
! [X0] :
( ~ ssList(app(nil,X0))
| ~ ssList(X0)
| ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f368,f272]) ).
fof(f604,definition,
! [X0] :
( sQ21_spl
<=> ( ~ ssList(app(nil,X0))
| ~ ssList(X0)
| ~ ssList(app(nil,X0))
| app(nil,X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f607,plain,
( sQ21_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f601,f510,f604]) ).
fof(f613,plain,
( ~ ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil))))
| app(skaf71(nil),cons(skaf69(nil),skaf72(nil))) = nil
| ~ ssList(cons(skaf70(nil),skaf73(nil)))
| strictorderedP(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f391,f325]) ).
fof(f614,plain,
( ~ ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil))))
| ~ ssList(cons(skaf70(nil),skaf73(nil)))
| cons(skaf70(nil),skaf73(nil)) = nil
| strictorderedP(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f391,f327]) ).
fof(f615,definition,
( sQ22_spl
<=> strictorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f618,definition,
( sQ23_spl
<=> cons(skaf70(nil),skaf73(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f621,definition,
( sQ24_spl
<=> ssList(cons(skaf70(nil),skaf73(nil))) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ24_spl
| ~ ssList(cons(skaf70(nil),skaf73(nil))) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f624,definition,
( sQ25_spl
<=> ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil)))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( sQ25_spl
| ~ ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil)))) ),
inference(component_clause,[status(thm)],[f624]) ).
fof(f627,plain,
( ~ sQ25_spl
| ~ sQ24_spl
| sQ23_spl
| sQ22_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f614,f510,f615,f618,f621,f624]) ).
fof(f628,definition,
( sQ26_spl
<=> app(skaf71(nil),cons(skaf69(nil),skaf72(nil))) = nil ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( ~ sQ25_spl
| sQ26_spl
| ~ sQ24_spl
| sQ22_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f613,f510,f615,f621,f628,f624]) ).
fof(f632,plain,
( sQ24_spl
| ~ ssItem(skaf70(nil))
| ~ ssList(skaf73(nil)) ),
inference(resolution,[status(thm)],[f623,f284]) ).
fof(f633,definition,
( sQ27_spl
<=> ssList(skaf73(nil)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f635,plain,
( sQ27_spl
| ~ ssList(skaf73(nil)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,definition,
( sQ28_spl
<=> ssItem(skaf70(nil)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( sQ28_spl
| ~ ssItem(skaf70(nil)) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f639,plain,
( sQ24_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f632,f633,f636,f621]) ).
fof(f640,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f638,f222]) ).
fof(f641,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f640]) ).
fof(f642,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f635,f219]) ).
fof(f643,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f642]) ).
fof(f644,plain,
( sQ25_spl
| ~ ssList(skaf71(nil))
| ~ ssList(cons(skaf69(nil),skaf72(nil))) ),
inference(resolution,[status(thm)],[f626,f283]) ).
fof(f645,definition,
( sQ29_spl
<=> ssList(cons(skaf69(nil),skaf72(nil))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( sQ29_spl
| ~ ssList(cons(skaf69(nil),skaf72(nil))) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
( sQ30_spl
<=> ssList(skaf71(nil)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( sQ30_spl
| ~ ssList(skaf71(nil)) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,plain,
( sQ25_spl
| ~ sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f644,f645,f648,f624]) ).
fof(f652,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f221]) ).
fof(f653,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f652]) ).
fof(f665,plain,
( sQ29_spl
| ~ ssItem(skaf69(nil))
| ~ ssList(skaf72(nil)) ),
inference(resolution,[status(thm)],[f647,f284]) ).
fof(f666,definition,
( sQ31_spl
<=> ssList(skaf72(nil)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( sQ31_spl
| ~ ssList(skaf72(nil)) ),
inference(component_clause,[status(thm)],[f666]) ).
fof(f669,definition,
( sQ32_spl
<=> ssItem(skaf69(nil)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f671,plain,
( sQ32_spl
| ~ ssItem(skaf69(nil)) ),
inference(component_clause,[status(thm)],[f669]) ).
fof(f672,plain,
( sQ29_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f665,f666,f669,f645]) ).
fof(f673,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f223]) ).
fof(f674,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f673]) ).
fof(f675,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f668,f220]) ).
fof(f676,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f675]) ).
fof(f679,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| X0 = X0
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f401]) ).
fof(f680,definition,
! [X1] :
( sQ33_spl
<=> ( ~ ssItem(X1)
| ~ ssItem(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f681,plain,
! [X0] :
( ~ sQ33_spl
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,plain,
( sQ33_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f679,f592,f680]) ).
fof(f686,plain,
! [X0,X1] :
( ~ ssList(X1)
| X0 = X0
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(equality_resolution,[status(thm)],[f399]) ).
fof(f687,definition,
! [X0] :
( sQ34_spl
<=> ( X0 = X0
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f690,definition,
! [X1] :
( sQ35_spl
<=> ( ~ ssList(X1)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f691,plain,
! [X0] :
( ~ sQ35_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,plain,
( sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f686,f687,f690]) ).
fof(f715,plain,
! [X0,X1] :
( ~ ssList(X1)
| skaf83(cons(X0,X1)) = X0
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1))
| cons(X0,X1) = nil ),
inference(resolution,[status(thm)],[f309,f399]) ).
fof(f718,plain,
! [X0,X1] :
( ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(X1)
| X1 = skaf82(cons(X0,X1))
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(cons(X0,X1))
| cons(X0,X1) = nil ),
inference(resolution,[status(thm)],[f309,f401]) ).
fof(f720,plain,
! [X0,X1] :
( skaf82(cons(X0,X1)) = X1
| ~ ssItem(X0)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssList(cons(X0,X1))
| ~ ssList(skaf82(cons(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f718,f297]) ).
fof(f721,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssList(cons(X0,X1))
| X0 = skaf83(cons(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f715,f297]) ).
fof(f722,definition,
( sQ36_spl
<=> ssList(skaf82(nil)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( sQ36_spl
| ~ ssList(skaf82(nil)) ),
inference(component_clause,[status(thm)],[f722]) ).
fof(f725,definition,
( sQ37_spl
<=> ssItem(skaf83(nil)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( sQ37_spl
| ~ ssItem(skaf83(nil)) ),
inference(component_clause,[status(thm)],[f725]) ).
fof(f731,plain,
! [X0,X1] :
( ~ ssList(X1)
| X1 = skaf82(cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1))
| ~ ssItem(skaf83(cons(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f210]) ).
fof(f732,plain,
! [X0,X1] :
( ~ ssList(X1)
| X1 = skaf82(cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f731,f209]) ).
fof(f733,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| skaf82(cons(X0,X1)) = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f284]) ).
fof(f735,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X0) ),
inference(resolution,[status(thm)],[f339,f257]) ).
fof(f739,definition,
! [X0] :
( sQ38_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f742,plain,
( ~ sQ8_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f735,f739,f510]) ).
fof(f744,plain,
! [X0,X1] :
( ~ ssItem(X0)
| X0 = skaf83(cons(X0,X1))
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssList(skaf82(cons(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f721,f284]) ).
fof(f745,plain,
! [X0,X1] :
( ~ ssItem(X0)
| X0 = skaf83(cons(X0,X1))
| ~ ssList(X1)
| ~ ssList(skaf82(cons(X0,X1))) ),
inference(resolution,[status(thm)],[f744,f209]) ).
fof(f746,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| skaf83(cons(X0,X1)) = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f745,f210]) ).
fof(f750,plain,
! [X0] :
( ~ ssList(app(skaf47(nil,X0),X0))
| app(skaf47(nil,X0),X0) = nil
| ~ ssList(skaf48(X0,nil))
| ~ segmentP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f396,f325]) ).
fof(f751,plain,
! [X0] :
( ~ ssList(app(skaf47(nil,X0),X0))
| ~ ssList(skaf48(X0,nil))
| skaf48(X0,nil) = nil
| ~ segmentP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f396,f327]) ).
fof(f752,definition,
! [X0] :
( sQ39_spl
<=> ( ~ ssList(app(skaf47(nil,X0),X0))
| app(skaf47(nil,X0),X0) = nil
| ~ ssList(skaf48(X0,nil))
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f755,plain,
( ~ sQ8_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f750,f752,f510]) ).
fof(f756,definition,
! [X0] :
( sQ40_spl
<=> ( ~ ssList(app(skaf47(nil,X0),X0))
| ~ ssList(skaf48(X0,nil))
| skaf48(X0,nil) = nil
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f759,plain,
( ~ sQ8_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f751,f756,f510]) ).
fof(f798,plain,
( ~ ssList(app(skaf66(nil),cons(skaf64(nil),skaf67(nil))))
| app(skaf66(nil),cons(skaf64(nil),skaf67(nil))) = nil
| ~ ssList(cons(skaf65(nil),skaf68(nil)))
| totalorderedP(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f392,f325]) ).
fof(f799,plain,
( ~ ssList(app(skaf66(nil),cons(skaf64(nil),skaf67(nil))))
| ~ ssList(cons(skaf65(nil),skaf68(nil)))
| cons(skaf65(nil),skaf68(nil)) = nil
| totalorderedP(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f392,f327]) ).
fof(f800,definition,
( sQ41_spl
<=> totalorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f803,definition,
( sQ42_spl
<=> ssList(cons(skaf65(nil),skaf68(nil))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f805,plain,
( sQ42_spl
| ~ ssList(cons(skaf65(nil),skaf68(nil))) ),
inference(component_clause,[status(thm)],[f803]) ).
fof(f806,definition,
( sQ43_spl
<=> app(skaf66(nil),cons(skaf64(nil),skaf67(nil))) = nil ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f809,definition,
( sQ44_spl
<=> ssList(app(skaf66(nil),cons(skaf64(nil),skaf67(nil)))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f811,plain,
( sQ44_spl
| ~ ssList(app(skaf66(nil),cons(skaf64(nil),skaf67(nil)))) ),
inference(component_clause,[status(thm)],[f809]) ).
fof(f812,plain,
( ~ sQ44_spl
| sQ43_spl
| ~ sQ42_spl
| sQ41_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f798,f510,f800,f803,f806,f809]) ).
fof(f813,definition,
( sQ45_spl
<=> cons(skaf65(nil),skaf68(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f816,plain,
( ~ sQ44_spl
| ~ sQ42_spl
| sQ45_spl
| sQ41_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f799,f510,f800,f813,f803,f809]) ).
fof(f817,plain,
( sQ42_spl
| ~ ssItem(skaf65(nil))
| ~ ssList(skaf68(nil)) ),
inference(resolution,[status(thm)],[f805,f284]) ).
fof(f818,definition,
( sQ46_spl
<=> ssList(skaf68(nil)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f820,plain,
( sQ46_spl
| ~ ssList(skaf68(nil)) ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f821,definition,
( sQ47_spl
<=> ssItem(skaf65(nil)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f823,plain,
( sQ47_spl
| ~ ssItem(skaf65(nil)) ),
inference(component_clause,[status(thm)],[f821]) ).
fof(f824,plain,
( sQ42_spl
| ~ sQ47_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f817,f818,f821,f803]) ).
fof(f825,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f823,f227]) ).
fof(f826,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f825]) ).
fof(f827,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f820,f224]) ).
fof(f828,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f827]) ).
fof(f829,plain,
( sQ44_spl
| ~ ssList(skaf66(nil))
| ~ ssList(cons(skaf64(nil),skaf67(nil))) ),
inference(resolution,[status(thm)],[f811,f283]) ).
fof(f830,definition,
( sQ48_spl
<=> ssList(cons(skaf64(nil),skaf67(nil))) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f832,plain,
( sQ48_spl
| ~ ssList(cons(skaf64(nil),skaf67(nil))) ),
inference(component_clause,[status(thm)],[f830]) ).
fof(f833,definition,
( sQ49_spl
<=> ssList(skaf66(nil)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f835,plain,
( sQ49_spl
| ~ ssList(skaf66(nil)) ),
inference(component_clause,[status(thm)],[f833]) ).
fof(f836,plain,
( sQ44_spl
| ~ sQ49_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f829,f830,f833,f809]) ).
fof(f837,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f835,f226]) ).
fof(f838,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f837]) ).
fof(f839,plain,
( sQ48_spl
| ~ ssItem(skaf64(nil))
| ~ ssList(skaf67(nil)) ),
inference(resolution,[status(thm)],[f832,f284]) ).
fof(f840,definition,
( sQ50_spl
<=> ssList(skaf67(nil)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f842,plain,
( sQ50_spl
| ~ ssList(skaf67(nil)) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f843,definition,
( sQ51_spl
<=> ssItem(skaf64(nil)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( sQ51_spl
| ~ ssItem(skaf64(nil)) ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,plain,
( sQ48_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f839,f840,f843,f830]) ).
fof(f847,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f845,f228]) ).
fof(f848,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f847]) ).
fof(f849,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f842,f225]) ).
fof(f850,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f849]) ).
fof(f871,plain,
! [X0,X1] :
( ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(X1)
| X1 = nil
| ~ ssList(nil)
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f301,f401]) ).
fof(f873,plain,
( ~ ssItem(skaf44(nil))
| ~ ssList(nil)
| ~ ssList(nil)
| ~ singletonP(nil) ),
inference(resolution,[status(thm)],[f301,f299]) ).
fof(f874,plain,
! [X0,X1] :
( ~ ssList(X1)
| skaf44(cons(X0,X1)) = X0
| ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f301,f399]) ).
fof(f876,definition,
! [X0,X1] :
( sQ52_spl
<=> ( ~ ssList(X1)
| skaf44(cons(X0,X1)) = X0
| ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f879,plain,
( ~ sQ8_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f874,f876,f510]) ).
fof(f880,definition,
( sQ53_spl
<=> singletonP(nil) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f883,definition,
( sQ54_spl
<=> ssItem(skaf44(nil)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( sQ54_spl
| ~ ssItem(skaf44(nil)) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f886,plain,
( ~ sQ54_spl
| ~ sQ8_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f873,f880,f510,f883]) ).
fof(f888,definition,
! [X0,X1] :
( sQ55_spl
<=> ( ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(X1)
| X1 = nil
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f891,plain,
( ~ sQ8_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f871,f888,f510]) ).
fof(f932,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
inference(resolution,[status(thm)],[f338,f255]) ).
fof(f936,definition,
! [X0] :
( sQ56_spl
<=> ( ~ ssList(X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| nil = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f939,plain,
( ~ sQ8_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f932,f936,f510]) ).
fof(f942,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ segmentP(nil,X0)
| nil = X0 ),
inference(resolution,[status(thm)],[f337,f253]) ).
fof(f945,definition,
! [X0] :
( sQ57_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0)
| ~ segmentP(nil,X0)
| nil = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f948,plain,
( ~ sQ8_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f942,f945,f510]) ).
fof(f1009,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssItem(X0)
| singletonP(cons(X0,nil)) ),
inference(resolution,[status(thm)],[f476,f284]) ).
fof(f1010,definition,
! [X0] :
( sQ58_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0)
| singletonP(cons(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1013,plain,
( ~ sQ8_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1009,f1010,f510]) ).
fof(f1017,plain,
! [X0] :
( ~ sQ33_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f681]) ).
fof(f1021,plain,
( ~ sQ33_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f227,f1017]) ).
fof(f1037,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1021]) ).
fof(f1038,definition,
( sQ59_spl
<=> ssList(cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( sQ59_spl
| ~ ssList(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f1038]) ).
fof(f1041,definition,
( sQ60_spl
<=> sk4 = app(tl(sk1),cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( ~ sQ60_spl
| app(tl(sk1),cons(hd(sk1),nil)) = sk4 ),
inference(component_clause,[status(thm)],[f1041]) ).
fof(f1044,definition,
( sQ61_spl
<=> ssItem(hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1046,plain,
( sQ61_spl
| ~ ssItem(hd(sk1)) ),
inference(component_clause,[status(thm)],[f1044]) ).
fof(f1047,definition,
( sQ62_spl
<=> ssList(tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( sQ62_spl
| ~ ssList(tl(sk1)) ),
inference(component_clause,[status(thm)],[f1047]) ).
fof(f1050,plain,
( ~ sQ6_spl
| ~ sQ62_spl
| ~ sQ61_spl
| sQ60_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f561,f1038,f1041,f1044,f1047,f462]) ).
fof(f1051,plain,
( sQ7_spl
| ~ neq(nil,sk1) ),
inference(forward_demodulation,[status(thm)],[f433,f467]) ).
fof(f1052,plain,
( sQ62_spl
| sk1 = nil
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f1049,f275]) ).
fof(f1053,definition,
( sQ63_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
( sQ63_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f1053]) ).
fof(f1056,definition,
( sQ64_spl
<=> sk1 = nil ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1057,plain,
( ~ sQ64_spl
| sk1 = nil ),
inference(component_clause,[status(thm)],[f1056]) ).
fof(f1059,plain,
( sQ62_spl
| sQ64_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f1052,f1053,f1056,f1047]) ).
fof(f1060,plain,
( ~ sQ64_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1057,f555]) ).
fof(f1061,plain,
( ~ sQ64_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1060]) ).
fof(f1062,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1055,f428]) ).
fof(f1063,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f1062]) ).
fof(f1064,plain,
( sQ7_spl
| ~ ssList(sk1)
| ~ ssList(nil)
| sk1 = nil ),
inference(resolution,[status(thm)],[f1051,f300]) ).
fof(f1065,plain,
( sQ7_spl
| ~ sQ63_spl
| ~ sQ8_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1064,f1056,f510,f1053,f465]) ).
fof(f1067,plain,
( sQ61_spl
| nil = sk1
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f276,f1046]) ).
fof(f1068,plain,
( sQ61_spl
| sQ64_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f1067,f1053,f1056,f1044]) ).
fof(f1072,plain,
( sQ59_spl
| ~ ssList(nil)
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f284,f1040]) ).
fof(f1073,plain,
( sQ59_spl
| ~ sQ8_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f1072,f1044,f510,f1038]) ).
fof(f1094,plain,
( ~ sQ60_spl
| sk4 = tl(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk1)
| sk1 = nil ),
inference(paramodulation,[status(thm)],[f1042,f343]) ).
fof(f1184,definition,
( sQ79_spl
<=> sk4 = tl(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1185,plain,
( ~ sQ79_spl
| sk4 = tl(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1184]) ).
fof(f1187,plain,
( ~ sQ60_spl
| sQ79_spl
| ~ sQ59_spl
| ~ sQ63_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1094,f1056,f1053,f1038,f1184,f1041]) ).
fof(f1247,definition,
( sQ95_spl
<=> cons(hd(sk1),nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
( ~ sQ95_spl
| cons(hd(sk1),nil) = nil ),
inference(component_clause,[status(thm)],[f1247]) ).
fof(f1271,plain,
! [X0] :
( ~ sQ35_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f691]) ).
fof(f1272,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f210]) ).
fof(f1273,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1272]) ).
fof(f1274,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f885,f244]) ).
fof(f1275,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f1274]) ).
fof(f1277,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f727,f209]) ).
fof(f1278,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f1277]) ).
fof(f1283,plain,
( ~ sQ35_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f250,f1271]) ).
fof(f1317,plain,
~ sQ35_spl,
inference(contradiction_clause,[status(thm)],[f1283]) ).
fof(f1318,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f205,f596]) ).
fof(f1319,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1318]) ).
fof(f1321,definition,
( sQ100_spl
<=> ssItem(nil) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1323,plain,
( sQ100_spl
| ~ ssItem(nil) ),
inference(component_clause,[status(thm)],[f1321]) ).
fof(f1324,definition,
( sQ101_spl
<=> ssItem(sk4) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1326,plain,
( sQ101_spl
| ~ ssItem(sk4) ),
inference(component_clause,[status(thm)],[f1324]) ).
fof(f1331,plain,
! [X0] :
( ~ sQ1_spl
| ~ memberP(nil,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f268,f445]) ).
fof(f1335,plain,
( sQ100_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1323,f445]) ).
fof(f1336,plain,
( sQ100_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1335]) ).
fof(f1367,definition,
( sQ103_spl
<=> ssItem(sk1) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1369,plain,
( sQ103_spl
| ~ ssItem(sk1) ),
inference(component_clause,[status(thm)],[f1367]) ).
fof(f1374,plain,
( ~ sQ3_spl
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f452,f503]) ).
fof(f1376,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1374,f506]) ).
fof(f1377,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1376]) ).
fof(f1392,definition,
( sQ105_spl
<=> ssList(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( ~ sQ105_spl
| ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1392]) ).
fof(f1394,plain,
( sQ105_spl
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1392]) ).
fof(f1395,definition,
( sQ106_spl
<=> nil = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1396,plain,
( ~ sQ106_spl
| app(sk1,cons(hd(sk1),nil)) = nil ),
inference(component_clause,[status(thm)],[f1395]) ).
fof(f1397,plain,
( sQ106_spl
| nil != app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f1395]) ).
fof(f1421,definition,
( sQ110_spl
<=> sk4 = sk4 ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1423,plain,
( sQ110_spl
| sk4 != sk4 ),
inference(component_clause,[status(thm)],[f1421]) ).
fof(f1437,definition,
( sQ112_spl
<=> ssList(app(nil,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1439,plain,
( sQ112_spl
| ~ ssList(app(nil,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1437]) ).
fof(f1447,definition,
( sQ113_spl
<=> sk4 = cons(hd(sk1),nil) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1448,plain,
( ~ sQ113_spl
| cons(hd(sk1),nil) = sk4 ),
inference(component_clause,[status(thm)],[f1447]) ).
fof(f1468,plain,
( ~ sQ113_spl
| sk4 != nil
| ~ ssItem(hd(sk1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1448,f299]) ).
fof(f1471,plain,
( ~ sQ113_spl
| ~ sQ3_spl
| ~ sQ61_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1468,f510,f1044,f451,f1447]) ).
fof(f1555,plain,
( sQ110_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1423]) ).
fof(f1556,plain,
sQ110_spl,
inference(contradiction_clause,[status(thm)],[f1555]) ).
fof(f1636,definition,
( sQ138_spl
<=> ssList(app(sk4,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1637,plain,
( ~ sQ138_spl
| ssList(app(sk4,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1636]) ).
fof(f1638,plain,
( sQ138_spl
| ~ ssList(app(sk4,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f1636]) ).
fof(f1737,definition,
( sQ148_spl
<=> ssItem(skaf83(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1739,plain,
( sQ148_spl
| ~ ssItem(skaf83(sk4)) ),
inference(component_clause,[status(thm)],[f1737]) ).
fof(f1785,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(X0)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f442]) ).
fof(f1786,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(cons(X0,X3))
| ~ ssList(app(X2,cons(X0,X1)))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1785,f283]) ).
fof(f1787,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssList(app(X0,cons(X2,X1)))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1786,f284]) ).
fof(f1813,definition,
( sQ163_spl
<=> sk4 = cons(skaf83(sk4),nil) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1814,plain,
( ~ sQ163_spl
| cons(skaf83(sk4),nil) = sk4 ),
inference(component_clause,[status(thm)],[f1813]) ).
fof(f1841,definition,
( sQ168_spl
<=> ssList(app(sk1,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1843,plain,
( sQ168_spl
| ~ ssList(app(sk1,sk4)) ),
inference(component_clause,[status(thm)],[f1841]) ).
fof(f1844,definition,
( sQ169_spl
<=> nil = app(sk1,sk4) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1845,plain,
( ~ sQ169_spl
| app(sk1,sk4) = nil ),
inference(component_clause,[status(thm)],[f1844]) ).
fof(f1926,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ ssList(X3)
| cons(X2,X3) != cons(X1,X0)
| X2 = X1
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f399,f445]) ).
fof(f1929,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ ssList(X3)
| X0 = X3
| cons(X2,X0) != cons(X1,X3)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f401,f445]) ).
fof(f1932,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ ssList(X2)
| cons(X1,app(X0,X2)) = app(cons(X1,X0),X2)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f381,f445]) ).
fof(f1937,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ ssList(app(X1,cons(X2,X0)))
| memberP(app(X1,cons(X2,X0)),X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f488,f445]) ).
fof(f1941,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ ssList(X0)
| ~ ssList(X2)
| memberP(X2,X1)
| ~ memberP(app(X2,X0),X1)
| memberP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f383,f445]) ).
fof(f1943,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(backward_subsumption_resolution,[status(thm)],[f294,f445]) ).
fof(f1944,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X0)
| X0 = skaf82(cons(X1,X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f733,f445]) ).
fof(f1945,plain,
! [X0,X1] :
( ~ sQ1_spl
| memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f479,f445]) ).
fof(f1948,plain,
! [X0,X1] :
( ~ sQ1_spl
| hd(cons(X1,X0)) = X1
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f295,f445]) ).
fof(f1949,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| X0 = skaf83(cons(X0,X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f746,f445]) ).
fof(f1951,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| nil != cons(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f297,f445]) ).
fof(f1953,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f284,f445]) ).
fof(f1954,plain,
! [X0,X1] :
( ~ sQ1_spl
| cons(X1,X0) != X0
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f299,f445]) ).
fof(f1959,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ ssList(X0)
| ~ ssList(X1)
| cons(X2,X1) != cons(X3,X0)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1929,f445]) ).
fof(f1966,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ ssList(X3)
| cons(X2,X0) != cons(X1,X3)
| X1 = X2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1926,f445]) ).
fof(f2022,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ memberP(X0,X1)
| X0 = app(skaf42(X0,X1),cons(X1,skaf43(X1,X0)))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f397,f445]) ).
fof(f2023,plain,
! [X0] :
( ~ sQ1_spl
| ~ ssList(nil)
| ~ memberP(nil,X0)
| ~ ssList(skaf42(nil,X0))
| ~ ssList(cons(X0,skaf43(X0,nil)))
| nil = cons(X0,skaf43(X0,nil)) ),
inference(resolution,[status(thm)],[f327,f2022]) ).
fof(f2029,plain,
! [X0] :
( ~ frontsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0))
| nil = skaf45(nil,X0) ),
inference(resolution,[status(thm)],[f327,f342]) ).
fof(f2051,definition,
( sQ189_spl
<=> ssList(skaf80(nil)) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2053,plain,
( sQ189_spl
| ~ ssList(skaf80(nil)) ),
inference(component_clause,[status(thm)],[f2051]) ).
fof(f2060,definition,
! [X0] :
( sQ191_spl
<=> ( ~ memberP(nil,X0)
| ~ ssList(skaf42(nil,X0))
| ~ ssList(cons(X0,skaf43(X0,nil)))
| nil = cons(X0,skaf43(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f2063,plain,
( ~ sQ1_spl
| ~ sQ8_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f2023,f2060,f510,f444]) ).
fof(f2067,definition,
( sQ193_spl
<=> ssList(cons(skaf55(nil),skaf58(nil))) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( sQ193_spl
| ~ ssList(cons(skaf55(nil),skaf58(nil))) ),
inference(component_clause,[status(thm)],[f2067]) ).
fof(f2077,definition,
! [X0] :
( sQ196_spl
<=> ( ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0))
| nil = skaf45(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2080,plain,
( ~ sQ8_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f2029,f2077,f510]) ).
fof(f2081,plain,
( sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2053,f212]) ).
fof(f2082,plain,
sQ189_spl,
inference(contradiction_clause,[status(thm)],[f2081]) ).
fof(f2108,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ1_spl
| ~ ssList(X0)
| leq(X1,X3)
| ~ ssList(X4)
| ~ ssList(X2)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssItem(X1)
| ~ totalorderedP(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(forward_subsumption_resolution,[status(thm)],[f491,f445]) ).
fof(f2143,definition,
( sQ203_spl
<=> ssList(skaf45(sk4,nil)) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2145,plain,
( sQ203_spl
| ~ ssList(skaf45(sk4,nil)) ),
inference(component_clause,[status(thm)],[f2143]) ).
fof(f2153,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2145,f248]) ).
fof(f2154,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f2153]) ).
fof(f2205,plain,
! [X0,X1] :
( ~ ssList(X0)
| rearsegP(X0,X1)
| ~ rearsegP(nil,X1)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f255,f374]) ).
fof(f2206,definition,
! [X0,X1] :
( sQ211_spl
<=> ( ~ ssList(X0)
| rearsegP(X0,X1)
| ~ rearsegP(nil,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2209,plain,
( ~ sQ8_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f2205,f2206,f510]) ).
fof(f2211,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| frontsegP(X0,X1)
| ~ ssList(nil)
| ~ frontsegP(nil,X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f257,f376]) ).
fof(f2212,definition,
! [X0,X1] :
( sQ212_spl
<=> ( ~ ssList(X0)
| ~ ssList(X1)
| frontsegP(X0,X1)
| ~ frontsegP(nil,X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f2215,plain,
( ~ sQ8_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f2211,f2212,f510]) ).
fof(f2234,plain,
! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(X1)
| segmentP(X0,X1)
| ~ ssList(X0)
| ~ segmentP(nil,X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f253,f372]) ).
fof(f2235,definition,
! [X0,X1] :
( sQ215_spl
<=> ( ~ ssList(X1)
| segmentP(X0,X1)
| ~ ssList(X0)
| ~ segmentP(nil,X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2238,plain,
( ~ sQ8_spl
| sQ215_spl ),
inference(split_clause,[status(thm)],[f2234,f2235,f510]) ).
fof(f2254,plain,
( ~ sQ1_spl
| sQ13_spl
| ~ ssList(skaf63(nil)) ),
inference(resolution,[status(thm)],[f548,f1953]) ).
fof(f2255,plain,
( ~ sQ1_spl
| sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2254,f229]) ).
fof(f2256,plain,
( ~ sQ1_spl
| sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f2255]) ).
fof(f2261,plain,
( ~ sQ1_spl
| sQ193_spl
| ~ ssList(skaf58(nil)) ),
inference(resolution,[status(thm)],[f2069,f1953]) ).
fof(f2262,plain,
( ~ sQ1_spl
| sQ193_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2261,f234]) ).
fof(f2263,plain,
( ~ sQ1_spl
| sQ193_spl ),
inference(contradiction_clause,[status(thm)],[f2262]) ).
fof(f2264,plain,
! [X0] :
( ~ ssList(skaf46(nil,X0))
| ~ ssList(X0)
| nil = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ),
inference(resolution,[status(thm)],[f341,f327]) ).
fof(f2266,definition,
! [X0] :
( sQ216_spl
<=> ( ~ ssList(skaf46(nil,X0))
| ~ ssList(X0)
| nil = X0
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f2269,plain,
( ~ sQ8_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f2264,f2266,f510]) ).
fof(f2270,definition,
( sQ217_spl
<=> ssList(skaf46(sk4,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f2272,plain,
( sQ217_spl
| ~ ssList(skaf46(sk4,sk4)) ),
inference(component_clause,[status(thm)],[f2270]) ).
fof(f2277,plain,
( sQ217_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2272,f247]) ).
fof(f2278,plain,
sQ217_spl,
inference(contradiction_clause,[status(thm)],[f2277]) ).
fof(f2297,definition,
( sQ221_spl
<=> ssList(app(sk4,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2299,plain,
( sQ221_spl
| ~ ssList(app(sk4,sk4)) ),
inference(component_clause,[status(thm)],[f2297]) ).
fof(f2309,plain,
( sQ221_spl
| ~ ssList(sk4)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f2299,f283]) ).
fof(f2310,plain,
( sQ221_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f2309,f522,f2297]) ).
fof(f2338,definition,
! [X0] :
( sQ227_spl
<=> ( segmentP(app(sk4,X0),sk4)
| ~ ssList(app(app(nil,sk4),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f2339,plain,
! [X0] :
( ~ sQ227_spl
| ~ ssList(X0)
| segmentP(app(sk4,X0),sk4)
| ~ ssList(app(app(nil,sk4),X0)) ),
inference(component_clause,[status(thm)],[f2338]) ).
fof(f2365,definition,
( sQ231_spl
<=> ssList(tl(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f2367,plain,
( sQ231_spl
| ~ ssList(tl(sk4)) ),
inference(component_clause,[status(thm)],[f2365]) ).
fof(f2387,plain,
( sQ168_spl
| ~ ssList(sk4)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f1843,f283]) ).
fof(f2388,plain,
( sQ168_spl
| ~ sQ10_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f2387,f1053,f522,f1841]) ).
fof(f2444,definition,
! [X0,X1,X2] :
( sQ237_spl
<=> ( ~ ssItem(X2)
| ~ ssList(app(X0,cons(X2,X1)))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f2447,plain,
( ~ sQ0_spl
| sQ20_spl
| sQ237_spl ),
inference(split_clause,[status(thm)],[f1787,f2444,f595,f441]) ).
fof(f2561,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| skaf46(nil,X0) = nil
| ~ ssList(skaf46(nil,X0)) ),
inference(resolution,[status(thm)],[f325,f341]) ).
fof(f2567,plain,
! [X0] :
( ~ frontsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0))
| X0 = nil
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f325,f342]) ).
fof(f2572,definition,
! [X0] :
( sQ249_spl
<=> ( ~ ssList(X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| skaf46(nil,X0) = nil
| ~ ssList(skaf46(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f2575,plain,
( ~ sQ8_spl
| sQ249_spl ),
inference(split_clause,[status(thm)],[f2561,f2572,f510]) ).
fof(f2580,definition,
! [X0] :
( sQ251_spl
<=> ( ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0))
| X0 = nil
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f2583,plain,
( ~ sQ8_spl
| sQ251_spl ),
inference(split_clause,[status(thm)],[f2567,f2580,f510]) ).
fof(f2612,plain,
! [X0] :
( ~ sQ79_spl
| app(sk1,cons(hd(sk1),nil)) = nil
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(X0)
| tl(app(app(sk1,cons(hd(sk1),nil)),X0)) = app(sk4,X0) ),
inference(paramodulation,[status(thm)],[f1185,f343]) ).
fof(f2613,plain,
( ~ sQ79_spl
| nil = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil)))
| cons(hd(app(sk1,cons(hd(sk1),nil))),sk4) = app(sk1,cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f1185,f304]) ).
fof(f2615,definition,
! [X0] :
( sQ254_spl
<=> ( ~ ssList(X0)
| tl(app(app(sk1,cons(hd(sk1),nil)),X0)) = app(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f2618,plain,
( ~ sQ79_spl
| sQ106_spl
| ~ sQ105_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f2612,f2615,f1392,f1395,f1184]) ).
fof(f2619,definition,
( sQ255_spl
<=> cons(hd(app(sk1,cons(hd(sk1),nil))),sk4) = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f2620,plain,
( ~ sQ255_spl
| cons(hd(app(sk1,cons(hd(sk1),nil))),sk4) = app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f2619]) ).
fof(f2622,plain,
( ~ sQ79_spl
| sQ106_spl
| ~ sQ105_spl
| sQ255_spl ),
inference(split_clause,[status(thm)],[f2613,f2619,f1392,f1395,f1184]) ).
fof(f2656,plain,
( sQ105_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f1394,f283]) ).
fof(f2657,plain,
( sQ105_spl
| ~ sQ59_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f2656,f1053,f1038,f1392]) ).
fof(f2666,plain,
( ~ sQ106_spl
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil))
| nil = cons(hd(sk1),nil) ),
inference(resolution,[status(thm)],[f1396,f327]) ).
fof(f2702,plain,
( ~ sQ106_spl
| ~ sQ63_spl
| ~ sQ59_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2666,f1247,f1038,f1053,f1395]) ).
fof(f2732,plain,
( sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1739,f209]) ).
fof(f2733,plain,
sQ148_spl,
inference(contradiction_clause,[status(thm)],[f2732]) ).
fof(f2750,plain,
( sQ231_spl
| nil = sk4
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f2367,f275]) ).
fof(f2751,plain,
( sQ231_spl
| sQ3_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f2750,f522,f451,f2365]) ).
fof(f2799,plain,
( ~ sQ95_spl
| ~ ssItem(hd(sk1))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1248,f297]) ).
fof(f2806,plain,
( ~ sQ95_spl
| ~ ssItem(hd(sk1))
| ~ ssList(nil)
| skaf83(nil) = hd(sk1) ),
inference(paramodulation,[status(thm)],[f1248,f746]) ).
fof(f2818,plain,
( ~ sQ95_spl
| ~ sQ61_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2799,f510,f1044,f1247]) ).
fof(f2835,definition,
( sQ275_spl
<=> skaf83(nil) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition]) ).
fof(f2836,plain,
( ~ sQ275_spl
| hd(sk1) = skaf83(nil) ),
inference(component_clause,[status(thm)],[f2835]) ).
fof(f2838,plain,
( ~ sQ95_spl
| ~ sQ61_spl
| ~ sQ8_spl
| sQ275_spl ),
inference(split_clause,[status(thm)],[f2806,f2835,f510,f1044,f1247]) ).
fof(f2852,plain,
( ~ sQ275_spl
| nil = sk1
| ~ ssList(sk1)
| cons(skaf83(nil),tl(sk1)) = sk1 ),
inference(paramodulation,[status(thm)],[f2836,f304]) ).
fof(f2854,definition,
( sQ278_spl
<=> cons(skaf83(nil),tl(sk1)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f2855,plain,
( ~ sQ278_spl
| cons(skaf83(nil),tl(sk1)) = sk1 ),
inference(component_clause,[status(thm)],[f2854]) ).
fof(f2857,plain,
( ~ sQ275_spl
| sQ64_spl
| ~ sQ63_spl
| sQ278_spl ),
inference(split_clause,[status(thm)],[f2852,f2854,f1053,f1056,f2835]) ).
fof(f2929,definition,
( sQ289_spl
<=> ssItem(skaf83(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition]) ).
fof(f2931,plain,
( sQ289_spl
| ~ ssItem(skaf83(sk1)) ),
inference(component_clause,[status(thm)],[f2929]) ).
fof(f2993,definition,
( sQ296_spl
<=> cons(skaf83(sk1),tl(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f2994,plain,
( ~ sQ296_spl
| nil = cons(skaf83(sk1),tl(nil)) ),
inference(component_clause,[status(thm)],[f2993]) ).
fof(f3031,plain,
( ~ sQ296_spl
| ~ ssItem(skaf83(sk1))
| ~ ssList(tl(nil)) ),
inference(resolution,[status(thm)],[f2994,f297]) ).
fof(f3064,definition,
( sQ305_spl
<=> tl(nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f3065,plain,
( ~ sQ305_spl
| nil = tl(nil) ),
inference(component_clause,[status(thm)],[f3064]) ).
fof(f3073,plain,
( ~ sQ296_spl
| ~ sQ289_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f3031,f578,f2929,f2993]) ).
fof(f3077,definition,
( sQ307_spl
<=> memberP(nil,skaf83(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f3078,plain,
( ~ sQ307_spl
| memberP(nil,skaf83(sk1)) ),
inference(component_clause,[status(thm)],[f3077]) ).
fof(f3093,plain,
( ~ sQ307_spl
| ~ ssItem(skaf83(sk1)) ),
inference(resolution,[status(thm)],[f3078,f268]) ).
fof(f3094,plain,
( ~ sQ307_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3093,f209]) ).
fof(f3095,plain,
~ sQ307_spl,
inference(contradiction_clause,[status(thm)],[f3094]) ).
fof(f3127,plain,
( ~ sQ105_spl
| ~ sQ275_spl
| ssList(app(sk1,cons(skaf83(nil),nil))) ),
inference(forward_demodulation,[status(thm)],[f2836,f1393]) ).
fof(f3128,plain,
( sQ106_spl
| ~ sQ275_spl
| nil != app(sk1,cons(skaf83(nil),nil)) ),
inference(forward_demodulation,[status(thm)],[f2836,f1397]) ).
fof(f3197,plain,
( ~ sQ79_spl
| ~ sQ275_spl
| tl(app(sk1,cons(skaf83(nil),nil))) = sk4 ),
inference(forward_demodulation,[status(thm)],[f2836,f1185]) ).
fof(f3198,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ275_spl
| app(sk1,cons(skaf83(nil),nil)) = nil
| ~ ssList(app(sk1,cons(skaf83(nil),nil)))
| ~ ssList(X0)
| tl(app(app(sk1,cons(skaf83(nil),nil)),X0)) = app(sk4,X0) ),
inference(paramodulation,[status(thm)],[f3197,f343]) ).
fof(f3199,plain,
( ~ sQ79_spl
| ~ sQ275_spl
| nil = app(sk1,cons(skaf83(nil),nil))
| ~ ssList(app(sk1,cons(skaf83(nil),nil)))
| cons(hd(app(sk1,cons(skaf83(nil),nil))),sk4) = app(sk1,cons(skaf83(nil),nil)) ),
inference(paramodulation,[status(thm)],[f3197,f304]) ).
fof(f3201,definition,
! [X0] :
( sQ320_spl
<=> ( ~ ssList(X0)
| tl(app(app(sk1,cons(skaf83(nil),nil)),X0)) = app(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f3204,definition,
( sQ321_spl
<=> ssList(app(sk1,cons(skaf83(nil),nil))) ),
introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition]) ).
fof(f3206,plain,
( sQ321_spl
| ~ ssList(app(sk1,cons(skaf83(nil),nil))) ),
inference(component_clause,[status(thm)],[f3204]) ).
fof(f3207,definition,
( sQ322_spl
<=> app(sk1,cons(skaf83(nil),nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f3208,plain,
( ~ sQ322_spl
| app(sk1,cons(skaf83(nil),nil)) = nil ),
inference(component_clause,[status(thm)],[f3207]) ).
fof(f3210,plain,
( ~ sQ79_spl
| ~ sQ275_spl
| sQ322_spl
| ~ sQ321_spl
| sQ320_spl ),
inference(split_clause,[status(thm)],[f3198,f3201,f3204,f3207,f2835,f1184]) ).
fof(f3211,definition,
( sQ323_spl
<=> cons(hd(app(sk1,cons(skaf83(nil),nil))),sk4) = app(sk1,cons(skaf83(nil),nil)) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f3214,plain,
( ~ sQ79_spl
| ~ sQ275_spl
| sQ322_spl
| ~ sQ321_spl
| sQ323_spl ),
inference(split_clause,[status(thm)],[f3199,f3211,f3204,f3207,f2835,f1184]) ).
fof(f3216,plain,
( sQ321_spl
| ~ sQ105_spl
| ~ sQ275_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3206,f3127]) ).
fof(f3217,plain,
( sQ321_spl
| ~ sQ105_spl
| ~ sQ275_spl ),
inference(contradiction_clause,[status(thm)],[f3216]) ).
fof(f3218,plain,
( ~ sQ322_spl
| sQ106_spl
| ~ sQ275_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3208,f3128]) ).
fof(f3219,plain,
( ~ sQ322_spl
| sQ106_spl
| ~ sQ275_spl ),
inference(contradiction_clause,[status(thm)],[f3218]) ).
fof(f3242,definition,
( sQ326_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition]) ).
fof(f3244,plain,
( sQ326_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f3242]) ).
fof(f3250,plain,
( sQ326_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3244,f434]) ).
fof(f3251,plain,
sQ326_spl,
inference(contradiction_clause,[status(thm)],[f3250]) ).
fof(f3270,definition,
( sQ328_spl
<=> cons(sk5,tl(sk1)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f3271,plain,
( ~ sQ328_spl
| cons(sk5,tl(sk1)) = sk1 ),
inference(component_clause,[status(thm)],[f3270]) ).
fof(f3293,definition,
( sQ330_spl
<=> sk5 = sk5 ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f3311,definition,
( sQ332_spl
<=> ssList(skaf46(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f3313,plain,
( sQ332_spl
| ~ ssList(skaf46(nil,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f3311]) ).
fof(f3320,definition,
( sQ335_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f3322,plain,
( sQ335_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f3320]) ).
fof(f3326,plain,
( sQ332_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3313,f247]) ).
fof(f3327,plain,
sQ332_spl,
inference(contradiction_clause,[status(thm)],[f3326]) ).
fof(f3333,definition,
( sQ337_spl
<=> ssList(skaf46(sk4,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f3335,plain,
( sQ337_spl
| ~ ssList(skaf46(sk4,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f3333]) ).
fof(f3340,plain,
( sQ337_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3335,f247]) ).
fof(f3341,plain,
sQ337_spl,
inference(contradiction_clause,[status(thm)],[f3340]) ).
fof(f3362,definition,
! [X0] :
( sQ340_spl
<=> ( ~ ssItem(X0)
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition]) ).
fof(f3363,plain,
! [X0] :
( ~ sQ340_spl
| ~ ssItem(X0)
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f3362]) ).
fof(f3366,plain,
! [X0] :
( ~ sQ340_spl
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3363]) ).
fof(f3392,definition,
( sQ342_spl
<=> ssItem(hd(app(sk1,cons(sk5,nil)))) ),
introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition]) ).
fof(f3394,plain,
( sQ342_spl
| ~ ssItem(hd(app(sk1,cons(sk5,nil)))) ),
inference(component_clause,[status(thm)],[f3392]) ).
fof(f3444,definition,
! [X0] :
( sQ355_spl
<=> ( ~ memberP(sk4,X0)
| ~ ssItem(X0)
| memberP(app(sk1,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition]) ).
fof(f3445,plain,
! [X0] :
( ~ sQ355_spl
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| memberP(app(sk1,cons(sk5,nil)),X0) ),
inference(component_clause,[status(thm)],[f3444]) ).
fof(f3466,plain,
! [X0] :
( ~ sQ355_spl
| memberP(sk1,X0)
| memberP(cons(sk5,nil),X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk1)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(resolution,[status(thm)],[f3445,f383]) ).
fof(f3467,definition,
! [X0] :
( sQ359_spl
<=> ( memberP(sk1,X0)
| memberP(cons(sk5,nil),X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f3468,plain,
! [X0] :
( ~ sQ359_spl
| memberP(sk1,X0)
| memberP(cons(sk5,nil),X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(component_clause,[status(thm)],[f3467]) ).
fof(f3470,plain,
( ~ sQ355_spl
| ~ sQ335_spl
| ~ sQ63_spl
| sQ359_spl ),
inference(split_clause,[status(thm)],[f3466,f3467,f1053,f3320,f3444]) ).
fof(f3471,plain,
! [X0] :
( ~ sQ359_spl
| ~ memberP(sk4,X0)
| ~ ssItem(X0)
| memberP(cons(sk5,nil),X0)
| memberP(sk1,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3468]) ).
fof(f3473,plain,
! [X0] :
( ~ sQ359_spl
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk5)
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f3471,f389]) ).
fof(f3474,definition,
! [X0] :
( sQ360_spl
<=> ( ~ ssItem(X0)
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f3475,plain,
! [X0] :
( ~ sQ360_spl
| ~ ssItem(X0)
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f3474]) ).
fof(f3477,plain,
( ~ sQ359_spl
| ~ sQ8_spl
| ~ sQ326_spl
| sQ360_spl ),
inference(split_clause,[status(thm)],[f3473,f3474,f3242,f510,f3467]) ).
fof(f3478,plain,
! [X0] :
( ~ sQ360_spl
| X0 = sk5
| memberP(nil,X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3475]) ).
fof(f3626,plain,
! [X0] :
( ~ sQ169_spl
| ~ ssList(sk1)
| ~ ssList(sk4)
| ~ ssItem(X0)
| memberP(nil,X0)
| ~ memberP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f1845,f353]) ).
fof(f3665,definition,
! [X0] :
( sQ384_spl
<=> ( ~ ssItem(X0)
| memberP(nil,X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f3666,plain,
! [X0] :
( ~ sQ384_spl
| ~ ssItem(X0)
| memberP(nil,X0)
| ~ memberP(sk4,X0) ),
inference(component_clause,[status(thm)],[f3665]) ).
fof(f3668,plain,
( ~ sQ169_spl
| ~ sQ63_spl
| ~ sQ10_spl
| sQ384_spl ),
inference(split_clause,[status(thm)],[f3626,f3665,f522,f1053,f1844]) ).
fof(f3688,plain,
! [X0] :
( ~ sQ384_spl
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3666,f268]) ).
fof(f3702,plain,
( ~ sQ384_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f3688,f503]) ).
fof(f3704,plain,
( ~ sQ384_spl
| ~ sQ326_spl ),
inference(split_clause,[status(thm)],[f3702,f3242,f3665]) ).
fof(f3707,plain,
! [X0] :
( ~ sQ340_spl
| ~ memberP(sk4,X0)
| ~ ssItem(X0)
| sk5 = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f3366,f268]) ).
fof(f3709,plain,
( sQ289_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2931,f209]) ).
fof(f3710,plain,
sQ289_spl,
inference(contradiction_clause,[status(thm)],[f3709]) ).
fof(f3772,plain,
( sQ335_spl
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f3322,f284]) ).
fof(f3773,plain,
( sQ335_spl
| ~ sQ326_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3772,f510,f3242,f3320]) ).
fof(f3882,definition,
( sQ405_spl
<=> ssItem(skaf44(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f3884,plain,
( sQ405_spl
| ~ ssItem(skaf44(sk4)) ),
inference(component_clause,[status(thm)],[f3882]) ).
fof(f3902,plain,
( ~ sQ328_spl
| ~ ssItem(sk5)
| ~ ssList(tl(sk1))
| memberP(sk1,sk5) ),
inference(paramodulation,[status(thm)],[f3271,f479]) ).
fof(f3915,definition,
( sQ407_spl
<=> memberP(sk1,sk5) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f3916,plain,
( ~ sQ407_spl
| memberP(sk1,sk5) ),
inference(component_clause,[status(thm)],[f3915]) ).
fof(f3918,plain,
( ~ sQ328_spl
| ~ sQ326_spl
| ~ sQ62_spl
| sQ407_spl ),
inference(split_clause,[status(thm)],[f3902,f3915,f1047,f3242,f3270]) ).
fof(f3960,definition,
! [X0] :
( sQ418_spl
<=> ( ~ memberP(tl(sk1),X0)
| ~ ssItem(X0)
| memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f3961,plain,
! [X0] :
( ~ sQ418_spl
| ~ memberP(tl(sk1),X0)
| ~ ssItem(X0)
| memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f3960]) ).
fof(f3977,definition,
( sQ422_spl
<=> hd(sk1) = sk5 ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f3978,plain,
( ~ sQ422_spl
| sk5 = hd(sk1) ),
inference(component_clause,[status(thm)],[f3977]) ).
fof(f3992,plain,
( ~ sQ407_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3916,f436]) ).
fof(f3993,plain,
~ sQ407_spl,
inference(contradiction_clause,[status(thm)],[f3992]) ).
fof(f4011,plain,
( ~ sQ422_spl
| nil = sk1
| ~ ssList(sk1)
| cons(sk5,tl(sk1)) = sk1 ),
inference(paramodulation,[status(thm)],[f3978,f304]) ).
fof(f4012,plain,
( ~ sQ422_spl
| sQ64_spl
| ~ sQ63_spl
| sQ328_spl ),
inference(split_clause,[status(thm)],[f4011,f3270,f1053,f1056,f3977]) ).
fof(f4023,plain,
! [X0,X1] :
( ~ ssList(nil)
| ~ rearsegP(nil,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f280,f374]) ).
fof(f4026,definition,
! [X0,X1] :
( sQ426_spl
<=> ( ~ rearsegP(nil,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition]) ).
fof(f4029,plain,
( ~ sQ8_spl
| sQ426_spl ),
inference(split_clause,[status(thm)],[f4023,f4026,f510]) ).
fof(f4042,definition,
( sQ428_spl
<=> ssList(skaf82(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f4044,plain,
( sQ428_spl
| ~ ssList(skaf82(sk1)) ),
inference(component_clause,[status(thm)],[f4042]) ).
fof(f4104,plain,
( ~ sQ340_spl
| ~ ssItem(sk5)
| sk5 = sk5 ),
inference(resolution,[status(thm)],[f3707,f503]) ).
fof(f4106,plain,
( ~ sQ340_spl
| ~ sQ326_spl
| sQ330_spl ),
inference(split_clause,[status(thm)],[f4104,f3293,f3242,f3362]) ).
fof(f4107,definition,
( sQ430_spl
<=> sk5 = skaf83(sk4) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f4108,plain,
( ~ sQ430_spl
| sk5 = skaf83(sk4) ),
inference(component_clause,[status(thm)],[f4107]) ).
fof(f4128,plain,
! [X0] :
( ~ sQ278_spl
| ~ ssList(tl(sk1))
| ~ memberP(tl(sk1),X0)
| ~ ssItem(X0)
| memberP(sk1,X0)
| ~ ssItem(skaf83(nil)) ),
inference(paramodulation,[status(thm)],[f2855,f351]) ).
fof(f4132,plain,
( ~ sQ278_spl
| hd(sk1) = skaf83(nil)
| ~ ssItem(skaf83(nil))
| ~ ssList(tl(sk1)) ),
inference(paramodulation,[status(thm)],[f2855,f295]) ).
fof(f4169,plain,
( ~ sQ278_spl
| ~ sQ62_spl
| sQ418_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f4128,f725,f3960,f1047,f2854]) ).
fof(f4180,plain,
( ~ sQ278_spl
| sQ275_spl
| ~ sQ37_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f4132,f1047,f725,f2835,f2854]) ).
fof(f4222,plain,
! [X0,X1] :
( ~ frontsegP(nil,X1)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| X0 = nil
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f282,f376]) ).
fof(f4225,definition,
! [X0,X1] :
( sQ444_spl
<=> ( ~ frontsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| X0 = nil
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).
fof(f4228,plain,
( ~ sQ8_spl
| sQ444_spl ),
inference(split_clause,[status(thm)],[f4222,f4225,f510]) ).
fof(f4239,plain,
! [X0] :
( ~ sQ360_spl
| X0 = sk5
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3478,f268]) ).
fof(f4361,plain,
( sQ405_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3884,f244]) ).
fof(f4362,plain,
sQ405_spl,
inference(contradiction_clause,[status(thm)],[f4361]) ).
fof(f4516,plain,
( sQ428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4044,f210]) ).
fof(f4517,plain,
sQ428_spl,
inference(contradiction_clause,[status(thm)],[f4516]) ).
fof(f4553,definition,
( sQ493_spl
<=> ssItem(skaf44(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition]) ).
fof(f4555,plain,
( sQ493_spl
| ~ ssItem(skaf44(sk1)) ),
inference(component_clause,[status(thm)],[f4553]) ).
fof(f4752,plain,
( sQ493_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4555,f244]) ).
fof(f4753,plain,
sQ493_spl,
inference(contradiction_clause,[status(thm)],[f4752]) ).
fof(f4763,definition,
( sQ514_spl
<=> ssList(skaf46(nil,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition]) ).
fof(f4765,plain,
( sQ514_spl
| ~ ssList(skaf46(nil,sk4)) ),
inference(component_clause,[status(thm)],[f4763]) ).
fof(f4770,plain,
( sQ514_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4765,f247]) ).
fof(f4771,plain,
sQ514_spl,
inference(contradiction_clause,[status(thm)],[f4770]) ).
fof(f4787,definition,
( sQ517_spl
<=> cons(sk5,tl(sk4)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ517_spl])],[split_symbol_definition]) ).
fof(f4788,plain,
( ~ sQ517_spl
| sk4 = cons(sk5,tl(sk4)) ),
inference(component_clause,[status(thm)],[f4787]) ).
fof(f4829,plain,
( ~ sQ517_spl
| ~ ssItem(sk5)
| ~ ssList(tl(sk4))
| skaf83(sk4) = sk5 ),
inference(paramodulation,[status(thm)],[f4788,f746]) ).
fof(f4909,plain,
( ~ sQ517_spl
| ~ sQ326_spl
| ~ sQ231_spl
| sQ430_spl ),
inference(split_clause,[status(thm)],[f4829,f4107,f2365,f3242,f4787]) ).
fof(f4931,definition,
( sQ536_spl
<=> ssList(skaf82(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f4933,plain,
( sQ536_spl
| ~ ssList(skaf82(sk4)) ),
inference(component_clause,[status(thm)],[f4931]) ).
fof(f5100,plain,
( sQ536_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4933,f210]) ).
fof(f5101,plain,
sQ536_spl,
inference(contradiction_clause,[status(thm)],[f5100]) ).
fof(f5111,plain,
( sQ112_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1439,f283]) ).
fof(f5112,plain,
( sQ112_spl
| ~ sQ59_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f5111,f510,f1038,f1437]) ).
fof(f5113,plain,
( sQ138_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f1638,f283]) ).
fof(f5114,plain,
( sQ138_spl
| ~ sQ59_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f5113,f522,f1038,f1636]) ).
fof(f5120,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(nil,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| nil = X0 ),
inference(resolution,[status(thm)],[f278,f372]) ).
fof(f5123,definition,
! [X0,X1] :
( sQ562_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(nil,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| nil = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ562_spl])],[split_symbol_definition]) ).
fof(f5126,plain,
( ~ sQ8_spl
| sQ562_spl ),
inference(split_clause,[status(thm)],[f5120,f5123,f510]) ).
fof(f5136,plain,
! [X0] :
( ~ sQ227_spl
| ~ ssList(X0)
| ~ ssList(app(nil,sk4))
| ~ ssList(X0)
| segmentP(app(sk4,X0),sk4) ),
inference(resolution,[status(thm)],[f2339,f283]) ).
fof(f5137,definition,
! [X0] :
( sQ563_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0)
| segmentP(app(sk4,X0),sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ563_spl])],[split_symbol_definition]) ).
fof(f5140,definition,
( sQ564_spl
<=> ssList(app(nil,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition]) ).
fof(f5142,plain,
( sQ564_spl
| ~ ssList(app(nil,sk4)) ),
inference(component_clause,[status(thm)],[f5140]) ).
fof(f5143,plain,
( ~ sQ227_spl
| ~ sQ564_spl
| sQ563_spl ),
inference(split_clause,[status(thm)],[f5136,f5137,f5140,f2338]) ).
fof(f5145,plain,
( sQ564_spl
| ~ ssList(sk4)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f5142,f283]) ).
fof(f5146,plain,
( sQ564_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f5145,f510,f522,f5140]) ).
fof(f5147,plain,
( ~ sQ360_spl
| ~ ssItem(sk5)
| memberP(sk1,sk5)
| sk5 = sk5 ),
inference(resolution,[status(thm)],[f4239,f503]) ).
fof(f5149,plain,
( ~ sQ360_spl
| ~ sQ326_spl
| sQ407_spl
| sQ330_spl ),
inference(split_clause,[status(thm)],[f5147,f3293,f3915,f3242,f3474]) ).
fof(f5156,plain,
( ~ sQ163_spl
| ~ sQ430_spl
| sk4 = cons(sk5,nil) ),
inference(forward_demodulation,[status(thm)],[f4108,f1814]) ).
fof(f5182,plain,
! [X0] :
( ~ sQ163_spl
| ~ sQ430_spl
| ~ memberP(sk4,X0)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk5)
| X0 = sk5
| memberP(nil,X0) ),
inference(paramodulation,[status(thm)],[f5156,f389]) ).
fof(f5234,definition,
! [X0] :
( sQ574_spl
<=> ( ~ memberP(sk4,X0)
| ~ ssItem(X0)
| X0 = sk5
| memberP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition]) ).
fof(f5235,plain,
! [X0] :
( ~ sQ574_spl
| ~ memberP(sk4,X0)
| ~ ssItem(X0)
| X0 = sk5
| memberP(nil,X0) ),
inference(component_clause,[status(thm)],[f5234]) ).
fof(f5237,plain,
( ~ sQ163_spl
| ~ sQ430_spl
| ~ sQ8_spl
| ~ sQ326_spl
| sQ574_spl ),
inference(split_clause,[status(thm)],[f5182,f5234,f3242,f510,f4107,f1813]) ).
fof(f5264,plain,
! [X0] :
( ~ sQ574_spl
| sk5 = X0
| ~ memberP(sk4,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5235,f268]) ).
fof(f5277,plain,
( ~ sQ574_spl
| sk5 = sk5
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f5264,f503]) ).
fof(f5279,plain,
( ~ sQ574_spl
| sQ330_spl
| ~ sQ326_spl ),
inference(split_clause,[status(thm)],[f5277,f3242,f3293,f5234]) ).
fof(f5353,definition,
( sQ579_spl
<=> hd(nil) = skaf83(sk4) ),
introduced(definition,[new_symbols(definition,[sQ579_spl])],[split_symbol_definition]) ).
fof(f5354,plain,
( ~ sQ579_spl
| hd(nil) = skaf83(sk4) ),
inference(component_clause,[status(thm)],[f5353]) ).
fof(f5361,plain,
( sQ17_spl
| ~ sQ579_spl
| ~ ssItem(skaf83(sk4)) ),
inference(backward_demodulation,[status(thm)],[f5354,f583]) ).
fof(f5367,definition,
( sQ581_spl
<=> cons(skaf83(sk4),tl(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ581_spl])],[split_symbol_definition]) ).
fof(f5368,plain,
( ~ sQ581_spl
| nil = cons(skaf83(sk4),tl(nil)) ),
inference(component_clause,[status(thm)],[f5367]) ).
fof(f5375,plain,
( sQ17_spl
| ~ sQ579_spl
| ~ sQ148_spl ),
inference(split_clause,[status(thm)],[f5361,f1737,f5353,f581]) ).
fof(f5396,plain,
( ~ sQ581_spl
| ~ ssItem(skaf83(sk4))
| ~ ssList(tl(nil)) ),
inference(resolution,[status(thm)],[f5368,f297]) ).
fof(f5463,plain,
( ~ sQ581_spl
| ~ sQ148_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f5396,f578,f1737,f5367]) ).
fof(f5481,definition,
( sQ596_spl
<=> skaf82(nil) = tl(nil) ),
introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition]) ).
fof(f5482,plain,
( ~ sQ596_spl
| tl(nil) = skaf82(nil) ),
inference(component_clause,[status(thm)],[f5481]) ).
fof(f5555,plain,
( sQ16_spl
| ~ sQ596_spl
| ~ ssList(skaf82(nil)) ),
inference(backward_demodulation,[status(thm)],[f5482,f580]) ).
fof(f5563,definition,
( sQ609_spl
<=> cons(hd(nil),skaf82(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition]) ).
fof(f5564,plain,
( ~ sQ609_spl
| nil = cons(hd(nil),skaf82(nil)) ),
inference(component_clause,[status(thm)],[f5563]) ).
fof(f5567,plain,
( sQ16_spl
| ~ sQ596_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f5555,f722,f5481,f578]) ).
fof(f5571,plain,
( ~ sQ609_spl
| ~ ssItem(hd(nil))
| ~ ssList(skaf82(nil)) ),
inference(resolution,[status(thm)],[f5564,f297]) ).
fof(f5609,plain,
( ~ sQ609_spl
| ~ sQ17_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f5571,f722,f581,f5563]) ).
fof(f5679,definition,
( sQ628_spl
<=> skaf83(nil) = hd(nil) ),
introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition]) ).
fof(f5680,plain,
( ~ sQ628_spl
| skaf83(nil) = hd(nil) ),
inference(component_clause,[status(thm)],[f5679]) ).
fof(f5728,definition,
( sQ638_spl
<=> cons(skaf44(nil),tl(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f5729,plain,
( ~ sQ638_spl
| nil = cons(skaf44(nil),tl(nil)) ),
inference(component_clause,[status(thm)],[f5728]) ).
fof(f5741,plain,
( sQ17_spl
| ~ sQ628_spl
| ~ ssItem(skaf83(nil)) ),
inference(backward_demodulation,[status(thm)],[f5680,f583]) ).
fof(f5751,definition,
( sQ641_spl
<=> cons(skaf83(nil),tl(nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition]) ).
fof(f5752,plain,
( ~ sQ641_spl
| cons(skaf83(nil),tl(nil)) = nil ),
inference(component_clause,[status(thm)],[f5751]) ).
fof(f5759,plain,
( sQ17_spl
| ~ sQ628_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f5741,f725,f5679,f581]) ).
fof(f5769,plain,
( ~ sQ638_spl
| ~ ssItem(skaf44(nil))
| ~ ssList(tl(nil)) ),
inference(resolution,[status(thm)],[f5729,f297]) ).
fof(f5864,plain,
( ~ sQ638_spl
| ~ sQ54_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f5769,f578,f883,f5728]) ).
fof(f5873,definition,
( sQ658_spl
<=> memberP(nil,skaf44(nil)) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f5874,plain,
( ~ sQ658_spl
| memberP(nil,skaf44(nil)) ),
inference(component_clause,[status(thm)],[f5873]) ).
fof(f5890,plain,
( sQ16_spl
| ~ sQ305_spl
| ~ ssList(nil) ),
inference(backward_demodulation,[status(thm)],[f3065,f580]) ).
fof(f5894,definition,
( sQ661_spl
<=> cons(hd(nil),nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition]) ).
fof(f5895,plain,
( ~ sQ661_spl
| cons(hd(nil),nil) = nil ),
inference(component_clause,[status(thm)],[f5894]) ).
fof(f5898,plain,
( sQ16_spl
| ~ sQ305_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f5890,f510,f3064,f578]) ).
fof(f5906,plain,
( ~ sQ658_spl
| ~ ssItem(skaf44(nil)) ),
inference(resolution,[status(thm)],[f5874,f268]) ).
fof(f5907,plain,
( ~ sQ658_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f5906,f883,f5873]) ).
fof(f5921,plain,
( ~ sQ661_spl
| ~ ssItem(hd(nil))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f5895,f297]) ).
fof(f5925,plain,
( ~ sQ661_spl
| strictorderedP(nil)
| ~ ssItem(hd(nil)) ),
inference(paramodulation,[status(thm)],[f5895,f263]) ).
fof(f5977,plain,
( ~ sQ661_spl
| sQ22_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f5925,f581,f615,f5894]) ).
fof(f5984,plain,
( ~ sQ661_spl
| ~ sQ17_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f5921,f510,f581,f5894]) ).
fof(f6048,plain,
( ~ sQ641_spl
| ~ ssItem(skaf83(nil))
| ~ ssList(tl(nil)) ),
inference(resolution,[status(thm)],[f5752,f297]) ).
fof(f6109,plain,
( ~ sQ641_spl
| ~ sQ37_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f6048,f578,f725,f5751]) ).
fof(f6133,definition,
( sQ692_spl
<=> memberP(nil,skaf83(nil)) ),
introduced(definition,[new_symbols(definition,[sQ692_spl])],[split_symbol_definition]) ).
fof(f6134,plain,
( ~ sQ692_spl
| memberP(nil,skaf83(nil)) ),
inference(component_clause,[status(thm)],[f6133]) ).
fof(f6163,plain,
( ~ sQ692_spl
| ~ ssItem(skaf83(nil)) ),
inference(resolution,[status(thm)],[f6134,f268]) ).
fof(f6164,plain,
( ~ sQ692_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f6163,f725,f6133]) ).
fof(f6271,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(app(X2,cons(X3,X0)),cons(X3,X1)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f442]) ).
fof(f6273,plain,
! [X0] :
( ~ sQ60_spl
| ~ sQ0_spl
| ~ ssList(app(sk4,cons(hd(sk1),X0)))
| ~ ssItem(hd(sk1))
| ~ ssList(tl(sk1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1042,f6271]) ).
fof(f6275,definition,
! [X0] :
( sQ701_spl
<=> ( ~ ssList(app(sk4,cons(hd(sk1),X0)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ701_spl])],[split_symbol_definition]) ).
fof(f6276,plain,
! [X0] :
( ~ sQ701_spl
| ~ ssList(app(sk4,cons(hd(sk1),X0)))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f6275]) ).
fof(f6278,plain,
( ~ sQ60_spl
| ~ sQ0_spl
| ~ sQ61_spl
| ~ sQ62_spl
| sQ701_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f6273,f510,f6275,f1047,f1044,f441,f1041]) ).
fof(f6282,plain,
( ~ sQ138_spl
| ~ sQ701_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f6276,f1637]) ).
fof(f6283,plain,
! [X0] :
( ~ sQ701_spl
| ~ ssList(cons(hd(sk1),X0))
| ~ ssList(sk4)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f6276,f283]) ).
fof(f6284,plain,
( ~ sQ138_spl
| ~ sQ701_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f6282,f510,f6275,f1636]) ).
fof(f6285,definition,
! [X0] :
( sQ702_spl
<=> ( ~ ssList(cons(hd(sk1),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition]) ).
fof(f6286,plain,
! [X0] :
( ~ sQ702_spl
| ~ ssList(X0)
| ~ ssList(cons(hd(sk1),X0)) ),
inference(component_clause,[status(thm)],[f6285]) ).
fof(f6288,plain,
( ~ sQ701_spl
| ~ sQ10_spl
| sQ702_spl ),
inference(split_clause,[status(thm)],[f6283,f6285,f522,f6275]) ).
fof(f6290,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1))
| ~ ssList(nil)
| ~ ssList(X1)
| X0 = skaf44(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f1966,f301]) ).
fof(f6295,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| ~ ssList(X1)
| X0 = X0 ),
inference(equality_resolution,[status(thm)],[f1966]) ).
fof(f6297,definition,
! [X0,X1] :
( sQ703_spl
<=> ( ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1))
| ~ ssList(X1)
| X0 = skaf44(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ703_spl])],[split_symbol_definition]) ).
fof(f6300,plain,
( ~ sQ1_spl
| ~ sQ8_spl
| sQ703_spl ),
inference(split_clause,[status(thm)],[f6290,f6297,f510,f444]) ).
fof(f6304,definition,
! [X0] :
( sQ704_spl
<=> X0 = X0 ),
introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition]) ).
fof(f6307,plain,
( ~ sQ1_spl
| sQ35_spl
| sQ704_spl ),
inference(split_clause,[status(thm)],[f6295,f6304,f690,f444]) ).
fof(f6316,plain,
! [X0] :
( ~ sQ418_spl
| ~ sQ1_spl
| memberP(sk1,X0)
| ~ memberP(tl(sk1),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3961,f445]) ).
fof(f6333,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ ssList(X1)
| ~ memberP(X1,X2)
| memberP(cons(X0,X1),X2)
| ~ ssItem(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f351,f445]) ).
fof(f6347,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ ssList(X0)
| cons(X3,X1) != cons(X2,X0)
| ~ ssList(X1)
| ~ ssItem(X2)
| X0 = X1 ),
inference(backward_subsumption_resolution,[status(thm)],[f401,f445]) ).
fof(f6351,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ memberP(cons(X2,X0),X1)
| ~ ssList(X0)
| ~ ssItem(X2)
| X1 = X2
| memberP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f389,f445]) ).
fof(f6368,plain,
( sQ17_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f583,f445]) ).
fof(f6369,plain,
( sQ342_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3394,f445]) ).
fof(f6370,plain,
( sQ103_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1369,f445]) ).
fof(f6371,plain,
( sQ101_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1326,f445]) ).
fof(f6377,plain,
( sQ103_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f6370]) ).
fof(f6382,plain,
( sQ17_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f6368]) ).
fof(f6386,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| memberP(cons(X2,X0),X1)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6333,f445]) ).
fof(f6389,plain,
( sQ101_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f6371]) ).
fof(f6390,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ ssList(X3)
| ~ ssList(X1)
| X1 = X3
| cons(X0,X1) != cons(X2,X3) ),
inference(forward_subsumption_resolution,[status(thm)],[f6347,f445]) ).
fof(f6400,plain,
( sQ342_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f6369]) ).
fof(f6401,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ ssList(X2)
| ~ memberP(cons(X1,X2),X0)
| memberP(X2,X0)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f6351,f445]) ).
fof(f6476,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ frontsegP(X0,X1)
| frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f445]) ).
fof(f6533,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(cons(X1,X0))
| ~ singletonP(cons(X1,X0))
| nil = X0
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1959,f301]) ).
fof(f6537,definition,
! [X0,X1] :
( sQ713_spl
<=> ( ~ ssList(cons(X1,X0))
| ~ singletonP(cons(X1,X0))
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition]) ).
fof(f6540,plain,
( ~ sQ1_spl
| sQ713_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f6533,f510,f6537,f444]) ).
fof(f6556,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ frontsegP(cons(X0,X3),cons(X1,X2))
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ ssList(X2)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f445]) ).
fof(f6557,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ ssList(X1)
| ~ frontsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| X0 = X0 ),
inference(resolution,[status(thm)],[f6556,f6476]) ).
fof(f6560,definition,
! [X0] :
( sQ714_spl
<=> ( ~ ssItem(X0)
| X0 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition]) ).
fof(f6563,definition,
! [X1,X2] :
( sQ715_spl
<=> ( ~ ssList(X1)
| ~ frontsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X2)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition]) ).
fof(f6564,plain,
! [X0,X1] :
( ~ sQ715_spl
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ ssList(X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f6563]) ).
fof(f6566,plain,
( ~ sQ1_spl
| sQ715_spl
| sQ714_spl ),
inference(split_clause,[status(thm)],[f6557,f6560,f6563,f444]) ).
fof(f6568,plain,
! [X0,X1] :
( ~ sQ715_spl
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f6564]) ).
fof(f6649,plain,
! [X0] :
( ~ sQ715_spl
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f6568,f257]) ).
fof(f6654,plain,
( ~ sQ715_spl
| ~ sQ8_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f6649,f690,f510,f6563]) ).
fof(f6812,plain,
( ~ sQ702_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f239,f6852]) ).
fof(f6852,plain,
! [X0] :
( ~ sQ702_spl
| ~ sQ1_spl
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6286,f1953]) ).
fof(f6853,plain,
( ~ sQ702_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f6812]) ).
fof(f6888,plain,
! [X0] :
( ~ sQ60_spl
| ~ sQ1_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1))
| memberP(tl(sk1),X0)
| ~ memberP(sk4,X0)
| memberP(cons(hd(sk1),nil),X0) ),
inference(paramodulation,[status(thm)],[f1042,f1941]) ).
fof(f6890,definition,
! [X0] :
( sQ749_spl
<=> ( memberP(tl(sk1),X0)
| ~ memberP(sk4,X0)
| memberP(cons(hd(sk1),nil),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition]) ).
fof(f6891,plain,
! [X0] :
( ~ sQ749_spl
| memberP(cons(hd(sk1),nil),X0)
| ~ memberP(sk4,X0)
| memberP(tl(sk1),X0) ),
inference(component_clause,[status(thm)],[f6890]) ).
fof(f6893,plain,
( ~ sQ60_spl
| ~ sQ1_spl
| ~ sQ59_spl
| ~ sQ62_spl
| sQ749_spl ),
inference(split_clause,[status(thm)],[f6888,f6890,f1047,f1038,f444,f1041]) ).
fof(f6902,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ1_spl
| leq(X1,X3)
| ~ ssList(X2)
| ~ totalorderedP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X4)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(forward_subsumption_resolution,[status(thm)],[f491,f445]) ).
fof(f7037,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ1_spl
| ~ leq(X4,X2)
| ~ leq(X2,X4)
| ~ cyclefreeP(app(app(X1,cons(X4,X0)),cons(X2,X3)))
| ~ ssList(app(app(X1,cons(X4,X0)),cons(X2,X3)))
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f490,f445]) ).
fof(f7074,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ749_spl
| ~ ssList(nil)
| memberP(nil,X0)
| X0 = hd(sk1)
| ~ memberP(sk4,X0)
| memberP(tl(sk1),X0) ),
inference(resolution,[status(thm)],[f6891,f6401]) ).
fof(f7075,definition,
! [X0] :
( sQ763_spl
<=> ( memberP(nil,X0)
| X0 = hd(sk1)
| ~ memberP(sk4,X0)
| memberP(tl(sk1),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ763_spl])],[split_symbol_definition]) ).
fof(f7076,plain,
! [X0] :
( ~ sQ763_spl
| memberP(nil,X0)
| X0 = hd(sk1)
| ~ memberP(sk4,X0)
| memberP(tl(sk1),X0) ),
inference(component_clause,[status(thm)],[f7075]) ).
fof(f7078,plain,
( ~ sQ1_spl
| ~ sQ749_spl
| ~ sQ8_spl
| sQ763_spl ),
inference(split_clause,[status(thm)],[f7074,f7075,f510,f6890,f444]) ).
fof(f7079,plain,
! [X0] :
( ~ sQ763_spl
| ~ sQ1_spl
| X0 = hd(sk1)
| memberP(tl(sk1),X0)
| ~ memberP(sk4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7076,f1331]) ).
fof(f7081,plain,
! [X0] :
( ~ sQ418_spl
| ~ sQ1_spl
| ~ sQ763_spl
| hd(sk1) = X0
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ),
inference(resolution,[status(thm)],[f7079,f6316]) ).
fof(f7083,plain,
( ~ sQ418_spl
| ~ sQ1_spl
| ~ sQ763_spl
| hd(sk1) = sk5
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f7081,f503]) ).
fof(f7087,plain,
( ~ sQ418_spl
| ~ sQ1_spl
| ~ sQ763_spl
| sQ422_spl
| sQ407_spl ),
inference(split_clause,[status(thm)],[f7083,f3915,f3977,f7075,f444,f3960]) ).
fof(f7105,plain,
! [X0,X1] :
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(X1)
| ~ ssList(sk4)
| sk4 = X1
| app(sk1,cons(hd(sk1),nil)) != cons(X0,X1) ),
inference(paramodulation,[status(thm)],[f2620,f6390]) ).
fof(f7106,plain,
! [X0,X1,X2] :
( ~ sQ255_spl
| ~ sQ1_spl
| ~ leq(X2,hd(app(sk1,cons(hd(sk1),nil))))
| ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X2)
| ~ cyclefreeP(app(app(X1,cons(X2,X0)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(app(app(X1,cons(X2,X0)),app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f2620,f7037]) ).
fof(f7107,plain,
! [X0,X1,X2] :
( ~ sQ255_spl
| ~ sQ1_spl
| ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ cyclefreeP(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssList(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2)))
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f7037]) ).
fof(f7108,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(sk4)
| ~ memberP(app(sk1,cons(hd(sk1),nil)),X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f2620,f6401]) ).
fof(f7110,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ1_spl
| memberP(app(sk1,cons(hd(sk1),nil)),X0)
| ~ ssList(sk4)
| ~ memberP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f2620,f6386]) ).
fof(f7114,plain,
! [X0,X1,X2] :
( ~ sQ255_spl
| ~ sQ1_spl
| leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(sk4)
| ~ totalorderedP(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2))) ),
inference(paramodulation,[status(thm)],[f2620,f6902]) ).
fof(f7115,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| memberP(app(sk1,cons(hd(sk1),nil)),hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f1945]) ).
fof(f7116,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| hd(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f1948]) ).
fof(f7117,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(sk4)
| tl(app(sk1,cons(hd(sk1),nil))) = sk4 ),
inference(paramodulation,[status(thm)],[f2620,f1943]) ).
fof(f7118,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(sk4)
| hd(app(sk1,cons(hd(sk1),nil))) = skaf83(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f2620,f1949]) ).
fof(f7119,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(sk4)
| sk4 = skaf82(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f2620,f1944]) ).
fof(f7120,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(sk4)
| ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f2620,f1953]) ).
fof(f7121,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(sk4)
| nil != app(sk1,cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f2620,f1951]) ).
fof(f7122,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| app(sk1,cons(hd(sk1),nil)) != sk4
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f1954]) ).
fof(f7123,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ1_spl
| ~ ssList(X0)
| cons(hd(app(sk1,cons(hd(sk1),nil))),app(sk4,X0)) = app(app(sk1,cons(hd(sk1),nil)),X0)
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f1932]) ).
fof(f7124,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ1_spl
| ~ 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))))
| ~ ssList(X0)
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f1937]) ).
fof(f7125,definition,
! [X0] :
( sQ765_spl
<=> ( ~ memberP(app(sk1,cons(hd(sk1),nil)),X0)
| memberP(sk4,X0)
| X0 = hd(app(sk1,cons(hd(sk1),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition]) ).
fof(f7128,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ765_spl ),
inference(split_clause,[status(thm)],[f7108,f7125,f522,f444,f2619]) ).
fof(f7129,definition,
( sQ766_spl
<=> sk4 = skaf82(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ766_spl])],[split_symbol_definition]) ).
fof(f7132,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ766_spl ),
inference(split_clause,[status(thm)],[f7119,f7129,f522,f444,f2619]) ).
fof(f7133,definition,
! [X0] :
( sQ767_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,[sQ767_spl])],[split_symbol_definition]) ).
fof(f7136,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| sQ767_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7123,f522,f7133,f444,f2619]) ).
fof(f7137,definition,
( sQ768_spl
<=> hd(app(sk1,cons(hd(sk1),nil))) = skaf83(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ768_spl])],[split_symbol_definition]) ).
fof(f7140,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ768_spl ),
inference(split_clause,[status(thm)],[f7118,f7137,f522,f444,f2619]) ).
fof(f7141,definition,
! [X0,X1,X2] :
( sQ769_spl
<=> ( leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ totalorderedP(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ769_spl])],[split_symbol_definition]) ).
fof(f7144,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ769_spl ),
inference(split_clause,[status(thm)],[f7114,f7141,f522,f444,f2619]) ).
fof(f7145,definition,
! [X0] :
( sQ770_spl
<=> ( ~ 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))))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ770_spl])],[split_symbol_definition]) ).
fof(f7148,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| sQ770_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7124,f522,f7145,f444,f2619]) ).
fof(f7149,definition,
! [X0] :
( sQ771_spl
<=> ( memberP(app(sk1,cons(hd(sk1),nil)),X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ771_spl])],[split_symbol_definition]) ).
fof(f7150,plain,
! [X0] :
( ~ sQ771_spl
| ~ memberP(sk4,X0)
| memberP(app(sk1,cons(hd(sk1),nil)),X0) ),
inference(component_clause,[status(thm)],[f7149]) ).
fof(f7152,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ771_spl ),
inference(split_clause,[status(thm)],[f7110,f7149,f522,f444,f2619]) ).
fof(f7153,definition,
! [X0,X1,X2] :
( sQ772_spl
<=> ( ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ cyclefreeP(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssList(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2)))
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ772_spl])],[split_symbol_definition]) ).
fof(f7156,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| sQ772_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7107,f522,f7153,f444,f2619]) ).
fof(f7157,definition,
! [X0,X1,X2] :
( sQ773_spl
<=> ( ~ leq(X2,hd(app(sk1,cons(hd(sk1),nil))))
| ~ leq(hd(app(sk1,cons(hd(sk1),nil))),X2)
| ~ cyclefreeP(app(app(X1,cons(X2,X0)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(app(app(X1,cons(X2,X0)),app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ773_spl])],[split_symbol_definition]) ).
fof(f7160,definition,
( sQ774_spl
<=> ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ774_spl])],[split_symbol_definition]) ).
fof(f7162,plain,
( sQ774_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f7160]) ).
fof(f7163,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ774_spl
| sQ773_spl ),
inference(split_clause,[status(thm)],[f7106,f7157,f7160,f522,f444,f2619]) ).
fof(f7164,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ106_spl ),
inference(split_clause,[status(thm)],[f7121,f1395,f522,f444,f2619]) ).
fof(f7169,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f7117,f1184,f522,f444,f2619]) ).
fof(f7173,definition,
( sQ777_spl
<=> sk4 = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ777_spl])],[split_symbol_definition]) ).
fof(f7177,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f7120,f1392,f522,f444,f2619]) ).
fof(f7178,definition,
( sQ778_spl
<=> hd(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ778_spl])],[split_symbol_definition]) ).
fof(f7181,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| sQ778_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7116,f522,f7178,f444,f2619]) ).
fof(f7182,definition,
! [X0,X1] :
( sQ779_spl
<=> ( ~ ssList(X1)
| sk4 = X1
| app(sk1,cons(hd(sk1),nil)) != cons(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ779_spl])],[split_symbol_definition]) ).
fof(f7185,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ779_spl ),
inference(split_clause,[status(thm)],[f7105,f7182,f522,f444,f2619]) ).
fof(f7186,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ777_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7122,f522,f7173,f444,f2619]) ).
fof(f7187,definition,
( sQ780_spl
<=> memberP(app(sk1,cons(hd(sk1),nil)),hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ780_spl])],[split_symbol_definition]) ).
fof(f7190,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| sQ780_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7115,f522,f7187,f444,f2619]) ).
fof(f7191,definition,
! [X0,X1,X2] :
( sQ781_spl
<=> ( leq(X1,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X2)
| ~ totalorderedP(app(app(X0,cons(X1,X2)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(X0)
| ~ ssList(app(app(X0,cons(X1,X2)),app(sk1,cons(hd(sk1),nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ781_spl])],[split_symbol_definition]) ).
fof(f7204,plain,
( sQ774_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7162,f445]) ).
fof(f7205,plain,
( sQ774_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f7204]) ).
fof(f7219,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ1_spl
| leq(X2,X3)
| ~ ssList(X4)
| ~ totalorderedP(app(app(X1,cons(X2,X0)),cons(X3,X4)))
| ~ ssList(X1)
| ~ ssList(app(app(X1,cons(X2,X0)),cons(X3,X4)))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2108,f445]) ).
fof(f7222,plain,
! [X0,X1,X2] :
( ~ sQ255_spl
| ~ sQ1_spl
| leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(X2)
| ~ totalorderedP(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssList(X0)
| ~ ssList(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2)))
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f2620,f7219]) ).
fof(f7223,plain,
! [X0,X1,X2] :
( ~ sQ255_spl
| ~ sQ1_spl
| leq(X2,hd(app(sk1,cons(hd(sk1),nil))))
| ~ ssList(sk4)
| ~ totalorderedP(app(app(X1,cons(X2,X0)),cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)))
| ~ ssList(X1)
| ~ ssList(app(app(X1,cons(X2,X0)),app(sk1,cons(hd(sk1),nil))))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f2620,f7219]) ).
fof(f7224,definition,
! [X0,X1,X2] :
( sQ782_spl
<=> ( leq(hd(app(sk1,cons(hd(sk1),nil))),X1)
| ~ ssList(X2)
| ~ totalorderedP(app(app(X0,cons(hd(app(sk1,cons(hd(sk1),nil))),sk4)),cons(X1,X2)))
| ~ ssList(X0)
| ~ ssList(app(app(X0,app(sk1,cons(hd(sk1),nil))),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ782_spl])],[split_symbol_definition]) ).
fof(f7227,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| sQ782_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7222,f522,f7224,f444,f2619]) ).
fof(f7228,plain,
( ~ sQ255_spl
| ~ sQ1_spl
| ~ sQ10_spl
| sQ781_spl ),
inference(split_clause,[status(thm)],[f7223,f7191,f522,f444,f2619]) ).
fof(f7357,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ771_spl
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(sk1)
| memberP(sk1,X0)
| memberP(cons(hd(sk1),nil),X0)
| ~ memberP(sk4,X0) ),
inference(resolution,[status(thm)],[f7150,f1941]) ).
fof(f7358,definition,
! [X0] :
( sQ790_spl
<=> ( memberP(sk1,X0)
| memberP(cons(hd(sk1),nil),X0)
| ~ memberP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ790_spl])],[split_symbol_definition]) ).
fof(f7359,plain,
! [X0] :
( ~ sQ790_spl
| memberP(cons(hd(sk1),nil),X0)
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f7358]) ).
fof(f7361,plain,
( ~ sQ1_spl
| ~ sQ771_spl
| ~ sQ59_spl
| ~ sQ63_spl
| sQ790_spl ),
inference(split_clause,[status(thm)],[f7357,f7358,f1053,f1038,f7149,f444]) ).
fof(f7369,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ790_spl
| ~ ssList(nil)
| memberP(nil,X0)
| X0 = hd(sk1)
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ),
inference(resolution,[status(thm)],[f7359,f6401]) ).
fof(f7370,definition,
! [X0] :
( sQ791_spl
<=> ( memberP(nil,X0)
| X0 = hd(sk1)
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ791_spl])],[split_symbol_definition]) ).
fof(f7371,plain,
! [X0] :
( ~ sQ791_spl
| memberP(nil,X0)
| X0 = hd(sk1)
| ~ memberP(sk4,X0)
| memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f7370]) ).
fof(f7373,plain,
( ~ sQ1_spl
| ~ sQ790_spl
| ~ sQ8_spl
| sQ791_spl ),
inference(split_clause,[status(thm)],[f7369,f7370,f510,f7358,f444]) ).
fof(f7374,plain,
! [X0] :
( ~ sQ791_spl
| ~ sQ1_spl
| X0 = hd(sk1)
| memberP(sk1,X0)
| ~ memberP(sk4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7371,f1331]) ).
fof(f7376,plain,
( ~ sQ791_spl
| ~ sQ1_spl
| sk5 = hd(sk1)
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f7374,f503]) ).
fof(f7379,plain,
( ~ sQ791_spl
| ~ sQ1_spl
| sQ422_spl
| sQ407_spl ),
inference(split_clause,[status(thm)],[f7376,f3915,f3977,f444,f7370]) ).
fof(f7381,plain,
$false,
inference(sat_refutation,[status(thm)],[f447,f454,f461,f468,f516,f518,f525,f527,f535,f591,f607,f627,f631,f639,f641,f643,f651,f653,f672,f674,f676,f683,f693,f742,f755,f759,f812,f816,f824,f826,f828,f836,f838,f846,f848,f850,f879,f886,f891,f939,f948,f1013,f1037,f1050,f1059,f1061,f1063,f1065,f1068,f1073,f1187,f1273,f1275,f1278,f1317,f1319,f1336,f1377,f1471,f1556,f2063,f2080,f2082,f2154,f2209,f2215,f2238,f2256,f2263,f2269,f2278,f2310,f2388,f2447,f2575,f2583,f2618,f2622,f2657,f2702,f2733,f2751,f2818,f2838,f2857,f3073,f3095,f3210,f3214,f3217,f3219,f3251,f3327,f3341,f3470,f3477,f3668,f3704,f3710,f3773,f3918,f3993,f4012,f4029,f4106,f4169,f4180,f4228,f4362,f4517,f4753,f4771,f4909,f5101,f5112,f5114,f5126,f5143,f5146,f5149,f5237,f5279,f5375,f5463,f5567,f5609,f5759,f5864,f5898,f5907,f5977,f5984,f6109,f6164,f6278,f6284,f6288,f6300,f6307,f6377,f6382,f6389,f6400,f6540,f6566,f6654,f6853,f6893,f7078,f7087,f7128,f7132,f7136,f7140,f7144,f7148,f7152,f7156,f7163,f7164,f7169,f7177,f7181,f7185,f7186,f7190,f7205,f7227,f7228,f7361,f7373,f7379]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC410-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 08:22:19 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.39 % Drodi V4.1.1
% 136.14/18.72 % Refutation found
% 136.14/18.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 136.14/18.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 68.46/18.80 % Elapsed time: 18.405531 seconds
% 68.46/18.80 % CPU time: 145.531396 seconds
% 68.46/18.80 % Total memory used: 588.636 MB
% 68.46/18.80 % Net memory used: 540.952 MB
%------------------------------------------------------------------------------