%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC085-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 : n008.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:39:54 PM UTC 2026
% Result : Unsatisfiable 1.27s 0.71s
% Output : CNFRefutation 1.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 353
% Syntax : Number of formulae : 1152 ( 119 unt; 298 def)
% Number of atoms : 4191 ( 242 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 5791 (2752 ~;2741 |; 0 &)
% ( 298 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 306 ( 304 usr; 299 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 5 con; 0-2 aty)
% Number of variables : 1195 (1195 !; 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(f14,axiom,
! [U] : ssList(skaf81(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] : ssList(skaf80(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [U] : ssList(skaf77(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [U] : ssList(skaf76(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [U] : ssList(skaf75(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(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(f32,axiom,
! [U] : ssList(skaf63(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [U] : ssList(skaf62(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [U] : ssList(skaf61(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] : ssList(skaf58(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [U] : ssList(skaf57(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [U] : ssList(skaf56(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] : ssList(skaf53(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [U] : ssList(skaf52(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [U] : ssList(skaf51(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(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(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ 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(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(f80,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ segmentP(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(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(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [U,V,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
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(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(f172,axiom,
! [U,V,W,X] :
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/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(f188,negated_conjecture,
ssList(sk3),
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,
neq(sk2,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
! [A] :
( ~ segmentP(sk1,A)
| ~ segmentP(sk2,A)
| ~ neq(A,nil)
| ~ ssList(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
( neq(sk3,nil)
| nil = sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( neq(sk3,nil)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
( frontsegP(sk4,sk3)
| nil = sk3 ),
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(f211,plain,
! [X0] : ssList(skaf81(X0)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f212,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f215,plain,
! [X0] : ssList(skaf77(X0)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f216,plain,
! [X0] : ssList(skaf76(X0)),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f217,plain,
! [X0] : ssList(skaf75(X0)),
inference(cnf_transformation,[status(thm)],[f20]) ).
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(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(f229,plain,
! [X0] : ssList(skaf63(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f230,plain,
! [X0] : ssList(skaf62(X0)),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f231,plain,
! [X0] : ssList(skaf61(X0)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f234,plain,
! [X0] : ssList(skaf58(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f235,plain,
! [X0] : ssList(skaf57(X0)),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f236,plain,
! [X0] : ssList(skaf56(X0)),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f239,plain,
! [X0] : ssList(skaf53(X0)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f240,plain,
! [X0] : ssList(skaf52(X0)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f241,plain,
! [X0] : ssList(skaf51(X0)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f248,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f253,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f254,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f255,plain,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f257,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f271,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f272,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f278,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f282,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f283,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f337,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f338,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f339,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f341,plain,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f342,plain,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f349,plain,
! [X0,X1,X2] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f357,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f358,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f357]) ).
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(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f375,plain,
! [U,W] :
( frontsegP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V) ) ),
inference(miniscoping,[status(thm)],[f154]) ).
fof(f376,plain,
! [X0,X1,X2] :
( frontsegP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f402,plain,
! [X0,X1,X2,X3] :
( segmentP(app(app(X3,X0),X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f403,plain,
! [V,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(app(U,V),W) != X ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f404,plain,
! [X0,X1,X2,X3] :
( segmentP(X3,X1)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(app(X0,X1),X2) != X3 ),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(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] :
( X0 = X2
| ~ ssItem(X0)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ frontsegP(cons(X0,X1),cons(X2,X3)) ),
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(f430,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f431,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f432,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f433,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f434,plain,
neq(sk2,nil),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f435,plain,
! [X0] :
( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f436,plain,
( neq(sk3,nil)
| nil = sk4 ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f438,plain,
( neq(sk3,nil)
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f439,plain,
( frontsegP(sk4,sk3)
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f447,definition,
( sQ2_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( ~ sQ2_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f450,definition,
( sQ3_spl
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f453,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f436,f447,f450]) ).
fof(f454,definition,
( sQ4_spl
<=> frontsegP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ4_spl
| frontsegP(sk4,sk3) ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f458,definition,
( sQ5_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f459,plain,
( ~ sQ5_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f438,f458,f450]) ).
fof(f462,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f439,f458,f454]) ).
fof(f478,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f358]) ).
fof(f481,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(app(app(X1,X2),X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f404]) ).
fof(f483,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(f484,plain,
! [X0,X1,X2] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f483]) ).
fof(f495,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| nil = sk4 ),
inference(backward_demodulation,[status(thm)],[f498,f459]) ).
fof(f496,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sk1 = sk4 ),
inference(backward_demodulation,[status(thm)],[f498,f433]) ).
fof(f498,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sk3 = sk4 ),
inference(forward_demodulation,[status(thm)],[f459,f448]) ).
fof(f499,plain,
neq(sk4,nil),
inference(forward_demodulation,[status(thm)],[f432,f434]) ).
fof(f500,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| neq(sk4,sk4) ),
inference(forward_demodulation,[status(thm)],[f495,f499]) ).
fof(f511,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,sk4)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f495,f435]) ).
fof(f512,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| ~ segmentP(sk1,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,sk4)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f511]) ).
fof(f513,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| ~ segmentP(sk4,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,sk4)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f496,f512]) ).
fof(f514,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| ~ segmentP(sk4,X0)
| ~ neq(X0,sk4)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f513]) ).
fof(f515,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ segmentP(sk4,sk4)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f514,f500]) ).
fof(f516,definition,
( sQ6_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ6_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,definition,
( sQ7_spl
<=> segmentP(sk4,sk4) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( ~ sQ7_spl
| segmentP(sk4,sk4) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f521,plain,
( sQ7_spl
| ~ segmentP(sk4,sk4) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f522,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f515,f516,f519,f447,f458]) ).
fof(f523,plain,
! [X0] :
( ~ segmentP(sk1,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f435]) ).
fof(f524,plain,
( sQ7_spl
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f521,f254]) ).
fof(f525,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f431]) ).
fof(f526,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f527,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f431]) ).
fof(f528,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f529,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f278,f254]) ).
fof(f530,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f532,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f530]) ).
fof(f533,definition,
( sQ9_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f536,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f529,f530,f533]) ).
fof(f537,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f532,f205]) ).
fof(f538,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f537]) ).
fof(f539,plain,
! [X0] :
( ~ segmentP(sk3,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f433,f523]) ).
fof(f540,plain,
( ~ ssList(sk3)
| ~ segmentP(sk4,sk3)
| ~ neq(sk3,nil)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f539,f254]) ).
fof(f541,definition,
( sQ10_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( sQ10_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f544,definition,
( sQ11_spl
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( sQ11_spl
| ~ segmentP(sk4,sk3) ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f547,plain,
( ~ sQ11_spl
| ~ sQ3_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f540,f541,f450,f544]) ).
fof(f548,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f430]) ).
fof(f549,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f548]) ).
fof(f550,plain,
( ~ segmentP(sk4,nil)
| ~ neq(nil,nil)
| ~ ssList(nil)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f253,f539]) ).
fof(f552,definition,
( sQ12_spl
<=> neq(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f555,definition,
( sQ13_spl
<=> segmentP(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f556,plain,
( ~ sQ13_spl
| segmentP(sk4,nil) ),
inference(component_clause,[status(thm)],[f555]) ).
fof(f557,plain,
( sQ13_spl
| ~ segmentP(sk4,nil) ),
inference(component_clause,[status(thm)],[f555]) ).
fof(f558,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f550,f541,f530,f552,f555]) ).
fof(f606,plain,
( sQ13_spl
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f557,f253]) ).
fof(f607,plain,
( sQ13_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f606,f516,f555]) ).
fof(f613,plain,
( ~ sQ7_spl
| sk4 = sk4
| ~ ssList(sk4)
| ~ ssList(sk4)
| ~ segmentP(sk4,sk4) ),
inference(resolution,[status(thm)],[f337,f520]) ).
fof(f614,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(nil,X0) ),
inference(resolution,[status(thm)],[f337,f253]) ).
fof(f620,definition,
( sQ16_spl
<=> sk4 = sk4 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ16_spl
| ~ sQ6_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f613,f519,f516,f620]) ).
fof(f624,definition,
! [X0] :
( sQ17_spl
<=> ( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( ~ sQ8_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f614,f624,f530]) ).
fof(f659,plain,
( ~ sQ4_spl
| sk4 = sk3
| ~ ssList(sk4)
| ~ ssList(sk3)
| ~ frontsegP(sk3,sk4) ),
inference(resolution,[status(thm)],[f339,f455]) ).
fof(f661,definition,
( sQ18_spl
<=> frontsegP(sk3,sk4) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f663,plain,
( sQ18_spl
| ~ frontsegP(sk3,sk4) ),
inference(component_clause,[status(thm)],[f661]) ).
fof(f664,definition,
( sQ19_spl
<=> sk4 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f665,plain,
( ~ sQ19_spl
| sk4 = sk3 ),
inference(component_clause,[status(thm)],[f664]) ).
fof(f667,plain,
( ~ sQ4_spl
| sQ19_spl
| ~ sQ6_spl
| ~ sQ10_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f659,f661,f541,f516,f664,f454]) ).
fof(f668,plain,
! [X0,X1,X2] :
( app(X0,X2) = X1
| ~ ssList(app(X0,X2))
| ~ ssList(X1)
| ~ frontsegP(X1,app(X0,X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(resolution,[status(thm)],[f349,f339]) ).
fof(f669,plain,
! [X0,X1,X2] :
( app(X0,X2) = X1
| ~ ssList(app(X0,X2))
| ~ frontsegP(X1,app(X0,X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f668]) ).
fof(f685,plain,
! [X0] :
( ~ sQ13_spl
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(nil)
| ~ segmentP(X0,sk4) ),
inference(resolution,[status(thm)],[f372,f556]) ).
fof(f686,plain,
! [X0] :
( ~ sQ7_spl
| segmentP(X0,sk4)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(sk4)
| ~ segmentP(X0,sk4) ),
inference(resolution,[status(thm)],[f372,f520]) ).
fof(f688,definition,
! [X0] :
( sQ21_spl
<=> ( segmentP(X0,nil)
| ~ ssList(X0)
| ~ segmentP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( ~ sQ13_spl
| ~ sQ6_spl
| ~ sQ8_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f685,f688,f530,f516,f555]) ).
fof(f692,definition,
! [X0] :
( sQ22_spl
<=> ( segmentP(X0,sk4)
| ~ ssList(X0)
| ~ segmentP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( ~ sQ7_spl
| ~ sQ6_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f686,f692,f516,f519]) ).
fof(f701,plain,
! [X0,X1] :
( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f253,f372]) ).
fof(f704,definition,
! [X0,X1] :
( sQ23_spl
<=> ( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( ~ sQ8_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f701,f704,f530]) ).
fof(f710,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f257,f339]) ).
fof(f711,definition,
! [X0] :
( sQ24_spl
<=> ( X0 = nil
| ~ ssList(X0)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( ~ sQ8_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f710,f711,f530]) ).
fof(f716,plain,
! [X0] :
( sQ18_spl
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(sk3,X0) ),
inference(resolution,[status(thm)],[f376,f663]) ).
fof(f717,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X0)
| ~ ssList(X2)
| ~ frontsegP(X2,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1) ),
inference(resolution,[status(thm)],[f376,f339]) ).
fof(f718,definition,
! [X0] :
( sQ25_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f719,plain,
! [X0] :
( ~ sQ25_spl
| ~ ssList(X0)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(sk3,X0) ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f721,plain,
( sQ18_spl
| ~ sQ10_spl
| ~ sQ6_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f716,f718,f516,f541,f661]) ).
fof(f722,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ frontsegP(X2,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f717]) ).
fof(f727,plain,
( sQ11_spl
| ~ sQ19_spl
| ~ segmentP(sk4,sk4) ),
inference(backward_demodulation,[status(thm)],[f665,f546]) ).
fof(f732,plain,
( sQ11_spl
| ~ sQ19_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f727,f519,f664,f544]) ).
fof(f735,plain,
! [X0,X1,X2,X3,X4] :
( segmentP(X4,X1)
| ~ ssList(X4)
| ~ ssList(app(app(X3,X0),X2))
| ~ ssList(X1)
| ~ segmentP(X4,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(resolution,[status(thm)],[f402,f372]) ).
fof(f736,plain,
! [X0,X1,X2,X3] :
( app(app(X3,X0),X2) = X1
| ~ ssList(app(app(X3,X0),X2))
| ~ ssList(X1)
| ~ segmentP(X1,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(resolution,[status(thm)],[f402,f337]) ).
fof(f737,plain,
! [X0,X1,X2,X3,X4] :
( segmentP(X4,X1)
| ~ ssList(X4)
| ~ ssList(app(app(X3,X0),X2))
| ~ segmentP(X4,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f735]) ).
fof(f738,plain,
! [X0,X1,X2,X3] :
( app(app(X3,X0),X2) = X1
| ~ ssList(app(app(X3,X0),X2))
| ~ segmentP(X1,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f736]) ).
fof(f741,plain,
app(sk3,nil) = sk3,
inference(resolution,[status(thm)],[f271,f430]) ).
fof(f745,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f271,f205]) ).
fof(f749,plain,
! [X0] : app(skaf51(X0),nil) = skaf51(X0),
inference(resolution,[status(thm)],[f271,f241]) ).
fof(f750,plain,
! [X0] : app(skaf52(X0),nil) = skaf52(X0),
inference(resolution,[status(thm)],[f271,f240]) ).
fof(f751,plain,
! [X0] : app(skaf53(X0),nil) = skaf53(X0),
inference(resolution,[status(thm)],[f271,f239]) ).
fof(f752,plain,
! [X0] : app(skaf56(X0),nil) = skaf56(X0),
inference(resolution,[status(thm)],[f271,f236]) ).
fof(f753,plain,
! [X0] : app(skaf57(X0),nil) = skaf57(X0),
inference(resolution,[status(thm)],[f271,f235]) ).
fof(f754,plain,
! [X0] : app(skaf58(X0),nil) = skaf58(X0),
inference(resolution,[status(thm)],[f271,f234]) ).
fof(f755,plain,
! [X0] : app(skaf61(X0),nil) = skaf61(X0),
inference(resolution,[status(thm)],[f271,f231]) ).
fof(f756,plain,
! [X0] : app(skaf62(X0),nil) = skaf62(X0),
inference(resolution,[status(thm)],[f271,f230]) ).
fof(f757,plain,
! [X0] : app(skaf63(X0),nil) = skaf63(X0),
inference(resolution,[status(thm)],[f271,f229]) ).
fof(f758,plain,
! [X0] : app(skaf66(X0),nil) = skaf66(X0),
inference(resolution,[status(thm)],[f271,f226]) ).
fof(f759,plain,
! [X0] : app(skaf67(X0),nil) = skaf67(X0),
inference(resolution,[status(thm)],[f271,f225]) ).
fof(f760,plain,
! [X0] : app(skaf68(X0),nil) = skaf68(X0),
inference(resolution,[status(thm)],[f271,f224]) ).
fof(f761,plain,
! [X0] : app(skaf71(X0),nil) = skaf71(X0),
inference(resolution,[status(thm)],[f271,f221]) ).
fof(f762,plain,
! [X0] : app(skaf72(X0),nil) = skaf72(X0),
inference(resolution,[status(thm)],[f271,f220]) ).
fof(f763,plain,
! [X0] : app(skaf73(X0),nil) = skaf73(X0),
inference(resolution,[status(thm)],[f271,f219]) ).
fof(f764,plain,
! [X0] : app(skaf75(X0),nil) = skaf75(X0),
inference(resolution,[status(thm)],[f271,f217]) ).
fof(f765,plain,
! [X0] : app(skaf76(X0),nil) = skaf76(X0),
inference(resolution,[status(thm)],[f271,f216]) ).
fof(f766,plain,
! [X0] : app(skaf77(X0),nil) = skaf77(X0),
inference(resolution,[status(thm)],[f271,f215]) ).
fof(f767,plain,
! [X0] : app(skaf80(X0),nil) = skaf80(X0),
inference(resolution,[status(thm)],[f271,f212]) ).
fof(f768,plain,
! [X0] : app(skaf81(X0),nil) = skaf81(X0),
inference(resolution,[status(thm)],[f271,f211]) ).
fof(f769,plain,
! [X0] : app(skaf82(X0),nil) = skaf82(X0),
inference(resolution,[status(thm)],[f271,f210]) ).
fof(f770,plain,
app(sk4,nil) = sk4,
inference(resolution,[status(thm)],[f271,f431]) ).
fof(f771,plain,
! [X0] :
( segmentP(app(app(sk3,nil),X0),nil)
| ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f741,f481]) ).
fof(f772,plain,
! [X0,X1] :
( segmentP(app(sk3,X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f741,f402]) ).
fof(f773,plain,
( frontsegP(app(sk3,nil),sk3)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f741,f478]) ).
fof(f774,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f741,f349]) ).
fof(f775,definition,
! [X0] :
( sQ26_spl
<=> ( segmentP(app(app(sk3,nil),X0),nil)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f771,f775,f541,f530]) ).
fof(f779,definition,
! [X0,X1] :
( sQ27_spl
<=> ( segmentP(app(sk3,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f780,plain,
! [X0,X1] :
( ~ sQ27_spl
| segmentP(app(sk3,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(component_clause,[status(thm)],[f779]) ).
fof(f782,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f772,f779,f541,f530]) ).
fof(f783,definition,
( sQ28_spl
<=> frontsegP(app(sk3,nil),sk3) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( ~ sQ28_spl
| frontsegP(app(sk3,nil),sk3) ),
inference(component_clause,[status(thm)],[f783]) ).
fof(f786,plain,
( sQ28_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f773,f530,f541,f783]) ).
fof(f787,definition,
! [X0] :
( sQ29_spl
<=> ( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f774,f787,f530,f541]) ).
fof(f792,plain,
( ~ sQ28_spl
| frontsegP(sk3,sk3) ),
inference(forward_demodulation,[status(thm)],[f741,f784]) ).
fof(f793,plain,
( ~ sQ28_spl
| sk3 = sk3
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ frontsegP(sk3,sk3) ),
inference(resolution,[status(thm)],[f792,f339]) ).
fof(f794,definition,
( sQ30_spl
<=> frontsegP(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f796,plain,
( sQ30_spl
| ~ frontsegP(sk3,sk3) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,definition,
( sQ31_spl
<=> sk3 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( ~ sQ28_spl
| sQ31_spl
| ~ sQ10_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f793,f794,f541,f797,f783]) ).
fof(f801,plain,
( sQ30_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f792]) ).
fof(f802,plain,
( sQ30_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f801]) ).
fof(f803,plain,
! [X0] :
( segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0))
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f745,f481]) ).
fof(f804,plain,
! [X0,X1] :
( segmentP(app(nil,X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f745,f402]) ).
fof(f805,plain,
( frontsegP(app(nil,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f745,f478]) ).
fof(f806,plain,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f745,f349]) ).
fof(f807,definition,
! [X0] :
( sQ32_spl
<=> ( segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f810,plain,
( ~ sQ8_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f803,f807,f530]) ).
fof(f811,definition,
! [X0,X1] :
( sQ33_spl
<=> ( segmentP(app(nil,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f814,plain,
( ~ sQ8_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f804,f811,f530]) ).
fof(f815,definition,
( sQ34_spl
<=> frontsegP(app(nil,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f816,plain,
( ~ sQ34_spl
| frontsegP(app(nil,nil),nil) ),
inference(component_clause,[status(thm)],[f815]) ).
fof(f818,plain,
( sQ34_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f805,f530,f815]) ).
fof(f819,definition,
! [X0] :
( sQ35_spl
<=> ( frontsegP(nil,X0)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f822,plain,
( ~ sQ8_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f806,f819,f530]) ).
fof(f824,plain,
( ~ sQ34_spl
| frontsegP(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f745,f816]) ).
fof(f826,definition,
( sQ36_spl
<=> frontsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f830,plain,
! [X0] :
( segmentP(app(app(sk4,nil),X0),nil)
| ~ ssList(app(sk4,X0))
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f770,f481]) ).
fof(f831,plain,
! [X0,X1] :
( segmentP(app(sk4,X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f770,f402]) ).
fof(f832,plain,
( frontsegP(app(sk4,nil),sk4)
| ~ ssList(sk4)
| ~ ssList(sk4)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f770,f478]) ).
fof(f833,plain,
! [X0] :
( frontsegP(sk4,X0)
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f770,f349]) ).
fof(f834,definition,
! [X0] :
( sQ37_spl
<=> ( segmentP(app(app(sk4,nil),X0),nil)
| ~ ssList(app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f837,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f830,f834,f516,f530]) ).
fof(f838,definition,
! [X0,X1] :
( sQ38_spl
<=> ( segmentP(app(sk4,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f839,plain,
! [X0,X1] :
( ~ sQ38_spl
| segmentP(app(sk4,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(component_clause,[status(thm)],[f838]) ).
fof(f841,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f831,f838,f516,f530]) ).
fof(f842,definition,
( sQ39_spl
<=> frontsegP(app(sk4,nil),sk4) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f843,plain,
( ~ sQ39_spl
| frontsegP(app(sk4,nil),sk4) ),
inference(component_clause,[status(thm)],[f842]) ).
fof(f845,plain,
( sQ39_spl
| ~ sQ6_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f832,f530,f516,f842]) ).
fof(f846,definition,
! [X0] :
( sQ40_spl
<=> ( frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ frontsegP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f849,plain,
( ~ sQ6_spl
| ~ sQ8_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f833,f846,f530,f516]) ).
fof(f851,plain,
( ~ sQ39_spl
| frontsegP(sk4,sk4) ),
inference(forward_demodulation,[status(thm)],[f770,f843]) ).
fof(f853,definition,
( sQ41_spl
<=> frontsegP(sk4,sk4) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f858,plain,
( ~ sQ25_spl
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ frontsegP(nil,sk4) ),
inference(resolution,[status(thm)],[f719,f257]) ).
fof(f862,definition,
( sQ42_spl
<=> frontsegP(nil,sk4) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ42_spl
| ~ frontsegP(nil,sk4) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f865,plain,
( ~ sQ25_spl
| ~ sQ10_spl
| ~ sQ8_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f858,f862,f530,f541,f718]) ).
fof(f872,plain,
! [X0] :
( sQ42_spl
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(nil,X0) ),
inference(resolution,[status(thm)],[f864,f376]) ).
fof(f873,definition,
! [X0] :
( sQ44_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f874,plain,
! [X0] :
( ~ sQ44_spl
| ~ ssList(X0)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(nil,X0) ),
inference(component_clause,[status(thm)],[f873]) ).
fof(f876,plain,
( sQ42_spl
| ~ sQ8_spl
| ~ sQ6_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f872,f873,f516,f530,f862]) ).
fof(f878,plain,
( ~ sQ44_spl
| ~ ssList(nil)
| ~ ssList(nil)
| ~ frontsegP(nil,sk4) ),
inference(resolution,[status(thm)],[f874,f257]) ).
fof(f879,plain,
! [X0,X1] :
( ~ sQ44_spl
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ),
inference(resolution,[status(thm)],[f874,f376]) ).
fof(f882,plain,
( ~ sQ44_spl
| ~ sQ8_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f878,f862,f530,f873]) ).
fof(f883,definition,
! [X0,X1] :
( sQ45_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f884,plain,
! [X0,X1] :
( ~ sQ45_spl
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f886,plain,
( ~ sQ44_spl
| ~ sQ8_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f879,f883,f530,f873]) ).
fof(f888,plain,
! [X0,X1] :
( ~ sQ45_spl
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ),
inference(duplicate_literals_removal,[status(thm)],[f884]) ).
fof(f898,plain,
app(nil,sk3) = sk3,
inference(resolution,[status(thm)],[f272,f430]) ).
fof(f906,plain,
! [X0] : app(nil,skaf51(X0)) = skaf51(X0),
inference(resolution,[status(thm)],[f272,f241]) ).
fof(f907,plain,
! [X0] : app(nil,skaf52(X0)) = skaf52(X0),
inference(resolution,[status(thm)],[f272,f240]) ).
fof(f908,plain,
! [X0] : app(nil,skaf53(X0)) = skaf53(X0),
inference(resolution,[status(thm)],[f272,f239]) ).
fof(f909,plain,
! [X0] : app(nil,skaf56(X0)) = skaf56(X0),
inference(resolution,[status(thm)],[f272,f236]) ).
fof(f910,plain,
! [X0] : app(nil,skaf57(X0)) = skaf57(X0),
inference(resolution,[status(thm)],[f272,f235]) ).
fof(f911,plain,
! [X0] : app(nil,skaf58(X0)) = skaf58(X0),
inference(resolution,[status(thm)],[f272,f234]) ).
fof(f912,plain,
! [X0] : app(nil,skaf61(X0)) = skaf61(X0),
inference(resolution,[status(thm)],[f272,f231]) ).
fof(f913,plain,
! [X0] : app(nil,skaf62(X0)) = skaf62(X0),
inference(resolution,[status(thm)],[f272,f230]) ).
fof(f914,plain,
! [X0] : app(nil,skaf63(X0)) = skaf63(X0),
inference(resolution,[status(thm)],[f272,f229]) ).
fof(f915,plain,
! [X0] : app(nil,skaf66(X0)) = skaf66(X0),
inference(resolution,[status(thm)],[f272,f226]) ).
fof(f916,plain,
! [X0] : app(nil,skaf67(X0)) = skaf67(X0),
inference(resolution,[status(thm)],[f272,f225]) ).
fof(f917,plain,
! [X0] : app(nil,skaf68(X0)) = skaf68(X0),
inference(resolution,[status(thm)],[f272,f224]) ).
fof(f918,plain,
! [X0] : app(nil,skaf71(X0)) = skaf71(X0),
inference(resolution,[status(thm)],[f272,f221]) ).
fof(f919,plain,
! [X0] : app(nil,skaf72(X0)) = skaf72(X0),
inference(resolution,[status(thm)],[f272,f220]) ).
fof(f920,plain,
! [X0] : app(nil,skaf73(X0)) = skaf73(X0),
inference(resolution,[status(thm)],[f272,f219]) ).
fof(f921,plain,
! [X0] : app(nil,skaf75(X0)) = skaf75(X0),
inference(resolution,[status(thm)],[f272,f217]) ).
fof(f922,plain,
! [X0] : app(nil,skaf76(X0)) = skaf76(X0),
inference(resolution,[status(thm)],[f272,f216]) ).
fof(f923,plain,
! [X0] : app(nil,skaf77(X0)) = skaf77(X0),
inference(resolution,[status(thm)],[f272,f215]) ).
fof(f924,plain,
! [X0] : app(nil,skaf80(X0)) = skaf80(X0),
inference(resolution,[status(thm)],[f272,f212]) ).
fof(f925,plain,
! [X0] : app(nil,skaf81(X0)) = skaf81(X0),
inference(resolution,[status(thm)],[f272,f211]) ).
fof(f926,plain,
! [X0] : app(nil,skaf82(X0)) = skaf82(X0),
inference(resolution,[status(thm)],[f272,f210]) ).
fof(f927,plain,
app(nil,sk4) = sk4,
inference(resolution,[status(thm)],[f272,f431]) ).
fof(f928,plain,
! [X0] :
( segmentP(app(app(nil,sk3),X0),sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f898,f481]) ).
fof(f929,plain,
! [X0,X1] :
( segmentP(app(sk3,X1),X0)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f898,f402]) ).
fof(f930,plain,
( frontsegP(app(nil,sk3),nil)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f898,f478]) ).
fof(f931,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f898,f349]) ).
fof(f932,definition,
! [X0] :
( sQ46_spl
<=> ( segmentP(app(app(nil,sk3),X0),sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f933,plain,
! [X0] :
( ~ sQ46_spl
| segmentP(app(app(nil,sk3),X0),sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f932]) ).
fof(f935,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f928,f932,f530,f541]) ).
fof(f936,definition,
! [X0,X1] :
( sQ47_spl
<=> ( segmentP(app(sk3,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f937,plain,
! [X0,X1] :
( ~ sQ47_spl
| segmentP(app(sk3,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk3,X0) ),
inference(component_clause,[status(thm)],[f936]) ).
fof(f939,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f929,f936,f530,f541]) ).
fof(f940,definition,
( sQ48_spl
<=> frontsegP(app(nil,sk3),nil) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f941,plain,
( ~ sQ48_spl
| frontsegP(app(nil,sk3),nil) ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f943,plain,
( sQ48_spl
| ~ sQ8_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f930,f541,f530,f940]) ).
fof(f944,definition,
! [X0] :
( sQ49_spl
<=> ( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f945,plain,
! [X0] :
( ~ sQ49_spl
| frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(component_clause,[status(thm)],[f944]) ).
fof(f947,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f931,f944,f541,f530]) ).
fof(f948,plain,
! [X0] :
( ~ sQ46_spl
| segmentP(app(sk3,X0),sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f898,f933]) ).
fof(f949,plain,
( ~ sQ48_spl
| frontsegP(sk3,nil) ),
inference(forward_demodulation,[status(thm)],[f898,f941]) ).
fof(f962,plain,
! [X0] :
( segmentP(app(app(nil,sk4),X0),sk4)
| ~ ssList(app(sk4,X0))
| ~ ssList(sk4)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f927,f481]) ).
fof(f963,plain,
! [X0,X1] :
( segmentP(app(sk4,X1),X0)
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f927,f402]) ).
fof(f964,plain,
( frontsegP(app(nil,sk4),nil)
| ~ ssList(sk4)
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(paramodulation,[status(thm)],[f927,f478]) ).
fof(f965,plain,
! [X0] :
( frontsegP(sk4,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f927,f349]) ).
fof(f966,definition,
! [X0] :
( sQ52_spl
<=> ( segmentP(app(app(nil,sk4),X0),sk4)
| ~ ssList(app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f967,plain,
! [X0] :
( ~ sQ52_spl
| segmentP(app(app(nil,sk4),X0),sk4)
| ~ ssList(app(sk4,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,plain,
( ~ sQ6_spl
| ~ sQ8_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f962,f966,f530,f516]) ).
fof(f970,definition,
! [X0,X1] :
( sQ53_spl
<=> ( segmentP(app(sk4,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f971,plain,
! [X0,X1] :
( ~ sQ53_spl
| segmentP(app(sk4,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk4,X0) ),
inference(component_clause,[status(thm)],[f970]) ).
fof(f973,plain,
( ~ sQ6_spl
| ~ sQ8_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f963,f970,f530,f516]) ).
fof(f974,definition,
( sQ54_spl
<=> frontsegP(app(nil,sk4),nil) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( ~ sQ54_spl
| frontsegP(app(nil,sk4),nil) ),
inference(component_clause,[status(thm)],[f974]) ).
fof(f977,plain,
( sQ54_spl
| ~ sQ8_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f964,f516,f530,f974]) ).
fof(f978,definition,
! [X0] :
( sQ55_spl
<=> ( frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f979,plain,
! [X0] :
( ~ sQ55_spl
| frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f981,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f965,f978,f516,f530]) ).
fof(f982,plain,
! [X0] :
( ~ sQ52_spl
| segmentP(app(sk4,X0),sk4)
| ~ ssList(app(sk4,X0))
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f927,f967]) ).
fof(f983,plain,
( ~ sQ54_spl
| frontsegP(sk4,nil) ),
inference(forward_demodulation,[status(thm)],[f927,f975]) ).
fof(f1028,plain,
( ~ sQ13_spl
| ~ sQ5_spl
| segmentP(sk4,sk3) ),
inference(backward_demodulation,[status(thm)],[f459,f556]) ).
fof(f1036,plain,
( ~ sQ13_spl
| ~ sQ5_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1028,f546]) ).
fof(f1037,plain,
( ~ sQ13_spl
| ~ sQ5_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1036]) ).
fof(f1060,plain,
! [X0,X1,X2] :
( X2 = X2
| ~ ssItem(X2)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(resolution,[status(thm)],[f484,f410]) ).
fof(f1063,definition,
! [X0,X1] :
( sQ56_spl
<=> ( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
! [X0,X1] :
( ~ sQ56_spl
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(component_clause,[status(thm)],[f1063]) ).
fof(f1066,definition,
! [X2] :
( sQ57_spl
<=> ( X2 = X2
| ~ ssItem(X2)
| ~ ssItem(X2)
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1069,plain,
( sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1060,f1063,f1066]) ).
fof(f1077,plain,
! [X0,X1] :
( ~ sQ56_spl
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1064]) ).
fof(f1148,plain,
! [X0] :
( ~ sQ49_spl
| sk3 = X0
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(resolution,[status(thm)],[f945,f339]) ).
fof(f1151,definition,
! [X0] :
( sQ60_spl
<=> ( sk3 = X0
| ~ ssList(X0)
| ~ frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1154,plain,
( ~ sQ49_spl
| ~ sQ10_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1148,f1151,f541,f944]) ).
fof(f1168,plain,
! [X0] :
( ~ sQ55_spl
| sk4 = X0
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(resolution,[status(thm)],[f979,f339]) ).
fof(f1169,definition,
! [X0] :
( sQ62_spl
<=> ( sk4 = X0
| ~ ssList(X0)
| ~ frontsegP(X0,sk4)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1172,plain,
( ~ sQ55_spl
| ~ sQ6_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1168,f1169,f516,f978]) ).
fof(f1174,plain,
! [X0] :
( ~ sQ27_spl
| ~ ssList(nil)
| segmentP(app(sk3,X0),nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f780,f253]) ).
fof(f1176,definition,
! [X0] :
( sQ63_spl
<=> ( segmentP(app(sk3,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
! [X0] :
( ~ sQ63_spl
| segmentP(app(sk3,X0),nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1176]) ).
fof(f1179,plain,
( ~ sQ27_spl
| ~ sQ8_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1174,f1176,f530,f779]) ).
fof(f1183,plain,
! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f282,f376]) ).
fof(f1187,definition,
! [X0,X1] :
( sQ64_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1190,plain,
( ~ sQ8_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1183,f1187,f530]) ).
fof(f1206,plain,
! [X0] : app(nil,skaf51(X0)) = skaf51(X0),
inference(resolution,[status(thm)],[f272,f241]) ).
fof(f1207,plain,
! [X0] : app(nil,skaf52(X0)) = skaf52(X0),
inference(resolution,[status(thm)],[f272,f240]) ).
fof(f1208,plain,
! [X0] : app(nil,skaf53(X0)) = skaf53(X0),
inference(resolution,[status(thm)],[f272,f239]) ).
fof(f1259,plain,
! [X0,X1] :
( ~ sQ63_spl
| segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ segmentP(X1,app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1177,f372]) ).
fof(f1260,plain,
! [X0] :
( ~ sQ63_spl
| app(sk3,X0) = nil
| ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ segmentP(nil,app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1177,f337]) ).
fof(f1261,plain,
( ~ sQ63_spl
| segmentP(sk3,nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f741,f1177]) ).
fof(f1262,definition,
! [X0,X1] :
( sQ65_spl
<=> ( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(app(sk3,X0))
| ~ segmentP(X1,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1265,plain,
( ~ sQ63_spl
| ~ sQ8_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1259,f1262,f530,f1176]) ).
fof(f1266,definition,
! [X0] :
( sQ66_spl
<=> ( app(sk3,X0) = nil
| ~ ssList(app(sk3,X0))
| ~ segmentP(nil,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1269,plain,
( ~ sQ63_spl
| ~ sQ8_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1260,f1266,f530,f1176]) ).
fof(f1270,definition,
( sQ67_spl
<=> segmentP(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
( ~ sQ67_spl
| segmentP(sk3,nil) ),
inference(component_clause,[status(thm)],[f1270]) ).
fof(f1273,plain,
( ~ sQ63_spl
| sQ67_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1261,f530,f1270,f1176]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ67_spl
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ segmentP(X0,sk3) ),
inference(resolution,[status(thm)],[f1271,f372]) ).
fof(f1278,definition,
! [X0] :
( sQ68_spl
<=> ( segmentP(X0,nil)
| ~ ssList(X0)
| ~ segmentP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1281,plain,
( ~ sQ67_spl
| ~ sQ10_spl
| ~ sQ8_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1275,f1278,f530,f541,f1270]) ).
fof(f1294,plain,
! [X0] :
( ~ sQ38_spl
| ~ ssList(nil)
| segmentP(app(sk4,X0),nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f839,f253]) ).
fof(f1296,definition,
! [X0] :
( sQ70_spl
<=> ( segmentP(app(sk4,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1297,plain,
! [X0] :
( ~ sQ70_spl
| segmentP(app(sk4,X0),nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1296]) ).
fof(f1299,plain,
( ~ sQ38_spl
| ~ sQ8_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1294,f1296,f530,f838]) ).
fof(f1398,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f478,f283]) ).
fof(f1422,plain,
! [X0] :
( ~ sQ46_spl
| ~ ssList(sk3)
| ~ ssList(X0)
| segmentP(app(sk3,X0),sk3)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f948,f283]) ).
fof(f1423,plain,
( ~ sQ46_spl
| segmentP(app(sk3,nil),sk3)
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f741,f948]) ).
fof(f1424,definition,
! [X0] :
( sQ71_spl
<=> ( ~ ssList(X0)
| segmentP(app(sk3,X0),sk3)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1425,plain,
! [X0] :
( ~ sQ71_spl
| ~ ssList(X0)
| segmentP(app(sk3,X0),sk3)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1424]) ).
fof(f1427,plain,
( ~ sQ46_spl
| ~ sQ10_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1422,f1424,f541,f932]) ).
fof(f1428,definition,
( sQ72_spl
<=> segmentP(app(sk3,nil),sk3) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
( ~ sQ72_spl
| segmentP(app(sk3,nil),sk3) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,plain,
( ~ sQ46_spl
| sQ72_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1423,f530,f541,f1428,f932]) ).
fof(f1432,plain,
! [X0] :
( ~ sQ71_spl
| segmentP(app(sk3,X0),sk3)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1425]) ).
fof(f1433,plain,
( ~ sQ72_spl
| segmentP(sk3,sk3) ),
inference(forward_demodulation,[status(thm)],[f741,f1429]) ).
fof(f1435,plain,
! [X0] :
( ~ sQ72_spl
| segmentP(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ segmentP(X0,sk3) ),
inference(resolution,[status(thm)],[f1433,f372]) ).
fof(f1438,definition,
! [X0] :
( sQ73_spl
<=> ( segmentP(X0,sk3)
| ~ ssList(X0)
| ~ segmentP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1441,plain,
( ~ sQ72_spl
| ~ sQ10_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1435,f1438,f541,f1428]) ).
fof(f1442,definition,
( sQ74_spl
<=> segmentP(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1449,plain,
( frontsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f745,f1398]) ).
fof(f1456,plain,
( sQ36_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1449,f530,f826]) ).
fof(f1457,definition,
( sQ75_spl
<=> frontsegP(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1461,definition,
( sQ76_spl
<=> frontsegP(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1531,plain,
! [X0] :
( frontsegP(skaf51(X0),skaf51(X0))
| ~ ssList(skaf51(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f749,f1398]) ).
fof(f1532,plain,
! [X0] :
( ssList(skaf51(X0))
| ~ ssList(skaf51(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f749,f283]) ).
fof(f1533,plain,
! [X0,X1] :
( segmentP(app(app(skaf51(X1),nil),X0),nil)
| ~ ssList(app(skaf51(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf51(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f749,f481]) ).
fof(f1534,plain,
! [X0,X1,X2] :
( segmentP(app(skaf51(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf51(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f749,f402]) ).
fof(f1535,plain,
! [X0,X1] :
( frontsegP(skaf51(X0),X1)
| ~ ssList(skaf51(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ frontsegP(skaf51(X0),X1) ),
inference(paramodulation,[status(thm)],[f749,f349]) ).
fof(f1536,definition,
! [X0] :
( sQ77_spl
<=> ( frontsegP(skaf51(X0),skaf51(X0))
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1539,plain,
( sQ77_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1531,f530,f1536]) ).
fof(f1540,definition,
! [X0] :
( sQ78_spl
<=> ( ssList(skaf51(X0))
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1543,plain,
( sQ78_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1532,f530,f1540]) ).
fof(f1544,definition,
! [X0,X1] :
( sQ79_spl
<=> ( segmentP(app(app(skaf51(X1),nil),X0),nil)
| ~ ssList(app(skaf51(X1),X0))
| ~ ssList(skaf51(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1547,plain,
( ~ sQ8_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1533,f1544,f530]) ).
fof(f1548,definition,
! [X0,X1,X2] :
( sQ80_spl
<=> ( segmentP(app(skaf51(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf51(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1551,plain,
( ~ sQ8_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1534,f1548,f530]) ).
fof(f1552,definition,
! [X0,X1] :
( sQ81_spl
<=> ( frontsegP(skaf51(X0),X1)
| ~ ssList(skaf51(X0))
| ~ ssList(X1)
| ~ frontsegP(skaf51(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1555,plain,
( ~ sQ8_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1535,f1552,f530]) ).
fof(f1558,plain,
! [X0] :
( frontsegP(skaf52(X0),skaf52(X0))
| ~ ssList(skaf52(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f750,f1398]) ).
fof(f1559,plain,
! [X0] :
( ssList(skaf52(X0))
| ~ ssList(skaf52(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f750,f283]) ).
fof(f1560,plain,
! [X0,X1] :
( segmentP(app(app(skaf52(X1),nil),X0),nil)
| ~ ssList(app(skaf52(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf52(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f750,f481]) ).
fof(f1561,plain,
! [X0,X1,X2] :
( segmentP(app(skaf52(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf52(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f750,f402]) ).
fof(f1562,plain,
! [X0,X1] :
( frontsegP(skaf52(X0),X1)
| ~ ssList(skaf52(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ frontsegP(skaf52(X0),X1) ),
inference(paramodulation,[status(thm)],[f750,f349]) ).
fof(f1563,definition,
! [X0] :
( sQ82_spl
<=> ( frontsegP(skaf52(X0),skaf52(X0))
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1566,plain,
( sQ82_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1558,f530,f1563]) ).
fof(f1567,definition,
! [X0] :
( sQ83_spl
<=> ( ssList(skaf52(X0))
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1570,plain,
( sQ83_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1559,f530,f1567]) ).
fof(f1571,definition,
! [X0,X1] :
( sQ84_spl
<=> ( segmentP(app(app(skaf52(X1),nil),X0),nil)
| ~ ssList(app(skaf52(X1),X0))
| ~ ssList(skaf52(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1574,plain,
( ~ sQ8_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1560,f1571,f530]) ).
fof(f1575,definition,
! [X0,X1,X2] :
( sQ85_spl
<=> ( segmentP(app(skaf52(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf52(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1578,plain,
( ~ sQ8_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1561,f1575,f530]) ).
fof(f1579,definition,
! [X0,X1] :
( sQ86_spl
<=> ( frontsegP(skaf52(X0),X1)
| ~ ssList(skaf52(X0))
| ~ ssList(X1)
| ~ frontsegP(skaf52(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1582,plain,
( ~ sQ8_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1562,f1579,f530]) ).
fof(f1585,plain,
! [X0] :
( frontsegP(skaf53(X0),skaf53(X0))
| ~ ssList(skaf53(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f751,f1398]) ).
fof(f1586,plain,
! [X0] :
( ssList(skaf53(X0))
| ~ ssList(skaf53(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f751,f283]) ).
fof(f1587,plain,
! [X0,X1] :
( segmentP(app(app(skaf53(X1),nil),X0),nil)
| ~ ssList(app(skaf53(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf53(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f751,f481]) ).
fof(f1588,plain,
! [X0,X1,X2] :
( segmentP(app(skaf53(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf53(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f751,f402]) ).
fof(f1589,plain,
! [X0,X1] :
( frontsegP(skaf53(X0),X1)
| ~ ssList(skaf53(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ frontsegP(skaf53(X0),X1) ),
inference(paramodulation,[status(thm)],[f751,f349]) ).
fof(f1590,definition,
! [X0] :
( sQ87_spl
<=> ( frontsegP(skaf53(X0),skaf53(X0))
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( sQ87_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1585,f530,f1590]) ).
fof(f1594,definition,
! [X0] :
( sQ88_spl
<=> ( ssList(skaf53(X0))
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1597,plain,
( sQ88_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1586,f530,f1594]) ).
fof(f1598,definition,
! [X0,X1] :
( sQ89_spl
<=> ( segmentP(app(app(skaf53(X1),nil),X0),nil)
| ~ ssList(app(skaf53(X1),X0))
| ~ ssList(skaf53(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1601,plain,
( ~ sQ8_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f1587,f1598,f530]) ).
fof(f1602,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> ( segmentP(app(skaf53(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf53(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1605,plain,
( ~ sQ8_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f1588,f1602,f530]) ).
fof(f1606,definition,
! [X0,X1] :
( sQ91_spl
<=> ( frontsegP(skaf53(X0),X1)
| ~ ssList(skaf53(X0))
| ~ ssList(X1)
| ~ frontsegP(skaf53(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1609,plain,
( ~ sQ8_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1589,f1606,f530]) ).
fof(f1612,plain,
! [X0,X1] :
( ~ sQ70_spl
| segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(app(sk4,X0))
| ~ ssList(nil)
| ~ segmentP(X1,app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1297,f372]) ).
fof(f1613,plain,
! [X0] :
( ~ sQ70_spl
| app(sk4,X0) = nil
| ~ ssList(app(sk4,X0))
| ~ ssList(nil)
| ~ segmentP(nil,app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1297,f337]) ).
fof(f1615,definition,
! [X0,X1] :
( sQ92_spl
<=> ( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(app(sk4,X0))
| ~ segmentP(X1,app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1618,plain,
( ~ sQ70_spl
| ~ sQ8_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f1612,f1615,f530,f1296]) ).
fof(f1619,definition,
! [X0] :
( sQ93_spl
<=> ( app(sk4,X0) = nil
| ~ ssList(app(sk4,X0))
| ~ segmentP(nil,app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1622,plain,
( ~ sQ70_spl
| ~ sQ8_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f1613,f1619,f530,f1296]) ).
fof(f1624,plain,
! [X0,X1] :
( ~ sQ71_spl
| segmentP(X1,sk3)
| ~ ssList(X1)
| ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ segmentP(X1,app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1432,f372]) ).
fof(f1625,plain,
! [X0] :
( ~ sQ71_spl
| app(sk3,X0) = sk3
| ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ segmentP(sk3,app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1432,f337]) ).
fof(f1626,plain,
( ~ sQ71_spl
| segmentP(sk3,sk3)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f741,f1432]) ).
fof(f1627,definition,
! [X0,X1] :
( sQ94_spl
<=> ( segmentP(X1,sk3)
| ~ ssList(X1)
| ~ ssList(app(sk3,X0))
| ~ segmentP(X1,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1630,plain,
( ~ sQ71_spl
| ~ sQ10_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1624,f1627,f541,f1424]) ).
fof(f1631,definition,
! [X0] :
( sQ95_spl
<=> ( app(sk3,X0) = sk3
| ~ ssList(app(sk3,X0))
| ~ segmentP(sk3,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1634,plain,
( ~ sQ71_spl
| ~ sQ10_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1625,f1631,f541,f1424]) ).
fof(f1635,plain,
( ~ sQ71_spl
| sQ74_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1626,f530,f1442,f1424]) ).
fof(f1638,plain,
! [X0] :
( ~ sQ47_spl
| segmentP(sk3,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f741,f937]) ).
fof(f1641,definition,
! [X0] :
( sQ96_spl
<=> ( segmentP(sk3,X0)
| ~ ssList(X0)
| ~ segmentP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1644,plain,
( ~ sQ47_spl
| ~ sQ8_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1638,f1641,f530,f936]) ).
fof(f1651,plain,
( ~ sQ39_spl
| ~ sQ56_spl
| ~ ssList(sk4)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f1077,f851]) ).
fof(f1665,plain,
( ~ sQ39_spl
| ~ sQ56_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1651,f516,f1063,f842]) ).
fof(f1693,plain,
! [X0] :
( frontsegP(skaf56(X0),skaf56(X0))
| ~ ssList(skaf56(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f752,f1398]) ).
fof(f1694,plain,
! [X0] :
( ssList(skaf56(X0))
| ~ ssList(skaf56(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f752,f283]) ).
fof(f1695,plain,
! [X0,X1] :
( segmentP(app(app(skaf56(X1),nil),X0),nil)
| ~ ssList(app(skaf56(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf56(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f752,f481]) ).
fof(f1696,plain,
! [X0,X1,X2] :
( segmentP(app(skaf56(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf56(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f752,f402]) ).
fof(f1697,definition,
! [X0] :
( sQ99_spl
<=> ( frontsegP(skaf56(X0),skaf56(X0))
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1700,plain,
( sQ99_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1693,f530,f1697]) ).
fof(f1701,definition,
! [X0] :
( sQ100_spl
<=> ( ssList(skaf56(X0))
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1704,plain,
( sQ100_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1694,f530,f1701]) ).
fof(f1705,definition,
! [X0,X1] :
( sQ101_spl
<=> ( segmentP(app(app(skaf56(X1),nil),X0),nil)
| ~ ssList(app(skaf56(X1),X0))
| ~ ssList(skaf56(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1708,plain,
( ~ sQ8_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1695,f1705,f530]) ).
fof(f1709,definition,
! [X0,X1,X2] :
( sQ102_spl
<=> ( segmentP(app(skaf56(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf56(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1712,plain,
( ~ sQ8_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f1696,f1709,f530]) ).
fof(f1715,plain,
! [X0] :
( frontsegP(skaf57(X0),skaf57(X0))
| ~ ssList(skaf57(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f753,f1398]) ).
fof(f1716,plain,
! [X0] :
( ssList(skaf57(X0))
| ~ ssList(skaf57(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f753,f283]) ).
fof(f1717,plain,
! [X0,X1] :
( segmentP(app(app(skaf57(X1),nil),X0),nil)
| ~ ssList(app(skaf57(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf57(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f753,f481]) ).
fof(f1718,plain,
! [X0,X1,X2] :
( segmentP(app(skaf57(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf57(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f753,f402]) ).
fof(f1719,definition,
! [X0] :
( sQ103_spl
<=> ( frontsegP(skaf57(X0),skaf57(X0))
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1722,plain,
( sQ103_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1715,f530,f1719]) ).
fof(f1723,definition,
! [X0] :
( sQ104_spl
<=> ( ssList(skaf57(X0))
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1726,plain,
( sQ104_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1716,f530,f1723]) ).
fof(f1727,definition,
! [X0,X1] :
( sQ105_spl
<=> ( segmentP(app(app(skaf57(X1),nil),X0),nil)
| ~ ssList(app(skaf57(X1),X0))
| ~ ssList(skaf57(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1730,plain,
( ~ sQ8_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1717,f1727,f530]) ).
fof(f1731,definition,
! [X0,X1,X2] :
( sQ106_spl
<=> ( segmentP(app(skaf57(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf57(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1734,plain,
( ~ sQ8_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f1718,f1731,f530]) ).
fof(f1737,plain,
! [X0] :
( frontsegP(skaf58(X0),skaf58(X0))
| ~ ssList(skaf58(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f754,f1398]) ).
fof(f1738,plain,
! [X0] :
( ssList(skaf58(X0))
| ~ ssList(skaf58(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f754,f283]) ).
fof(f1739,plain,
! [X0,X1] :
( segmentP(app(app(skaf58(X1),nil),X0),nil)
| ~ ssList(app(skaf58(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf58(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f754,f481]) ).
fof(f1740,plain,
! [X0,X1,X2] :
( segmentP(app(skaf58(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf58(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f754,f402]) ).
fof(f1741,definition,
! [X0] :
( sQ107_spl
<=> ( frontsegP(skaf58(X0),skaf58(X0))
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1744,plain,
( sQ107_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1737,f530,f1741]) ).
fof(f1745,definition,
! [X0] :
( sQ108_spl
<=> ( ssList(skaf58(X0))
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1748,plain,
( sQ108_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1738,f530,f1745]) ).
fof(f1749,definition,
! [X0,X1] :
( sQ109_spl
<=> ( segmentP(app(app(skaf58(X1),nil),X0),nil)
| ~ ssList(app(skaf58(X1),X0))
| ~ ssList(skaf58(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1752,plain,
( ~ sQ8_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f1739,f1749,f530]) ).
fof(f1753,definition,
! [X0,X1,X2] :
( sQ110_spl
<=> ( segmentP(app(skaf58(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf58(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1756,plain,
( ~ sQ8_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f1740,f1753,f530]) ).
fof(f1759,plain,
! [X0] :
( frontsegP(skaf61(X0),skaf61(X0))
| ~ ssList(skaf61(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f755,f1398]) ).
fof(f1760,plain,
! [X0] :
( ssList(skaf61(X0))
| ~ ssList(skaf61(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f755,f283]) ).
fof(f1761,plain,
! [X0,X1] :
( segmentP(app(app(skaf61(X1),nil),X0),nil)
| ~ ssList(app(skaf61(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf61(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f755,f481]) ).
fof(f1762,plain,
! [X0,X1,X2] :
( segmentP(app(skaf61(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf61(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f755,f402]) ).
fof(f1763,definition,
! [X0] :
( sQ111_spl
<=> ( frontsegP(skaf61(X0),skaf61(X0))
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1766,plain,
( sQ111_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1759,f530,f1763]) ).
fof(f1767,definition,
! [X0] :
( sQ112_spl
<=> ( ssList(skaf61(X0))
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1770,plain,
( sQ112_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1760,f530,f1767]) ).
fof(f1771,definition,
! [X0,X1] :
( sQ113_spl
<=> ( segmentP(app(app(skaf61(X1),nil),X0),nil)
| ~ ssList(app(skaf61(X1),X0))
| ~ ssList(skaf61(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1774,plain,
( ~ sQ8_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f1761,f1771,f530]) ).
fof(f1775,definition,
! [X0,X1,X2] :
( sQ114_spl
<=> ( segmentP(app(skaf61(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf61(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1778,plain,
( ~ sQ8_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f1762,f1775,f530]) ).
fof(f1781,plain,
! [X0] :
( frontsegP(skaf62(X0),skaf62(X0))
| ~ ssList(skaf62(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f756,f1398]) ).
fof(f1782,plain,
! [X0] :
( ssList(skaf62(X0))
| ~ ssList(skaf62(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f756,f283]) ).
fof(f1783,plain,
! [X0,X1] :
( segmentP(app(app(skaf62(X1),nil),X0),nil)
| ~ ssList(app(skaf62(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf62(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f756,f481]) ).
fof(f1784,plain,
! [X0,X1,X2] :
( segmentP(app(skaf62(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf62(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f756,f402]) ).
fof(f1785,definition,
! [X0] :
( sQ115_spl
<=> ( frontsegP(skaf62(X0),skaf62(X0))
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1788,plain,
( sQ115_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1781,f530,f1785]) ).
fof(f1789,definition,
! [X0] :
( sQ116_spl
<=> ( ssList(skaf62(X0))
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1792,plain,
( sQ116_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1782,f530,f1789]) ).
fof(f1793,definition,
! [X0,X1] :
( sQ117_spl
<=> ( segmentP(app(app(skaf62(X1),nil),X0),nil)
| ~ ssList(app(skaf62(X1),X0))
| ~ ssList(skaf62(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1796,plain,
( ~ sQ8_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1783,f1793,f530]) ).
fof(f1797,definition,
! [X0,X1,X2] :
( sQ118_spl
<=> ( segmentP(app(skaf62(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf62(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1800,plain,
( ~ sQ8_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1784,f1797,f530]) ).
fof(f1803,plain,
! [X0] :
( frontsegP(skaf63(X0),skaf63(X0))
| ~ ssList(skaf63(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f757,f1398]) ).
fof(f1804,plain,
! [X0] :
( ssList(skaf63(X0))
| ~ ssList(skaf63(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f757,f283]) ).
fof(f1805,plain,
! [X0,X1] :
( segmentP(app(app(skaf63(X1),nil),X0),nil)
| ~ ssList(app(skaf63(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf63(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f757,f481]) ).
fof(f1806,plain,
! [X0,X1,X2] :
( segmentP(app(skaf63(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf63(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f757,f402]) ).
fof(f1807,definition,
! [X0] :
( sQ119_spl
<=> ( frontsegP(skaf63(X0),skaf63(X0))
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1810,plain,
( sQ119_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1803,f530,f1807]) ).
fof(f1811,definition,
! [X0] :
( sQ120_spl
<=> ( ssList(skaf63(X0))
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1814,plain,
( sQ120_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1804,f530,f1811]) ).
fof(f1815,definition,
! [X0,X1] :
( sQ121_spl
<=> ( segmentP(app(app(skaf63(X1),nil),X0),nil)
| ~ ssList(app(skaf63(X1),X0))
| ~ ssList(skaf63(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1818,plain,
( ~ sQ8_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f1805,f1815,f530]) ).
fof(f1819,definition,
! [X0,X1,X2] :
( sQ122_spl
<=> ( segmentP(app(skaf63(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf63(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1822,plain,
( ~ sQ8_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1806,f1819,f530]) ).
fof(f1825,plain,
! [X0] :
( frontsegP(skaf66(X0),skaf66(X0))
| ~ ssList(skaf66(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f758,f1398]) ).
fof(f1826,plain,
! [X0] :
( ssList(skaf66(X0))
| ~ ssList(skaf66(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f758,f283]) ).
fof(f1827,plain,
! [X0,X1] :
( segmentP(app(app(skaf66(X1),nil),X0),nil)
| ~ ssList(app(skaf66(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf66(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f758,f481]) ).
fof(f1828,plain,
! [X0,X1,X2] :
( segmentP(app(skaf66(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf66(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f758,f402]) ).
fof(f1829,definition,
! [X0] :
( sQ123_spl
<=> ( frontsegP(skaf66(X0),skaf66(X0))
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1832,plain,
( sQ123_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1825,f530,f1829]) ).
fof(f1833,definition,
! [X0] :
( sQ124_spl
<=> ( ssList(skaf66(X0))
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1836,plain,
( sQ124_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1826,f530,f1833]) ).
fof(f1837,definition,
! [X0,X1] :
( sQ125_spl
<=> ( segmentP(app(app(skaf66(X1),nil),X0),nil)
| ~ ssList(app(skaf66(X1),X0))
| ~ ssList(skaf66(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1840,plain,
( ~ sQ8_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1827,f1837,f530]) ).
fof(f1841,definition,
! [X0,X1,X2] :
( sQ126_spl
<=> ( segmentP(app(skaf66(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf66(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1844,plain,
( ~ sQ8_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f1828,f1841,f530]) ).
fof(f1847,plain,
! [X0] :
( frontsegP(skaf67(X0),skaf67(X0))
| ~ ssList(skaf67(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f759,f1398]) ).
fof(f1848,plain,
! [X0] :
( ssList(skaf67(X0))
| ~ ssList(skaf67(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f759,f283]) ).
fof(f1849,plain,
! [X0,X1] :
( segmentP(app(app(skaf67(X1),nil),X0),nil)
| ~ ssList(app(skaf67(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf67(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f759,f481]) ).
fof(f1850,plain,
! [X0,X1,X2] :
( segmentP(app(skaf67(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf67(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f759,f402]) ).
fof(f1851,definition,
! [X0] :
( sQ127_spl
<=> ( frontsegP(skaf67(X0),skaf67(X0))
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1854,plain,
( sQ127_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1847,f530,f1851]) ).
fof(f1855,definition,
! [X0] :
( sQ128_spl
<=> ( ssList(skaf67(X0))
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1858,plain,
( sQ128_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1848,f530,f1855]) ).
fof(f1859,definition,
! [X0,X1] :
( sQ129_spl
<=> ( segmentP(app(app(skaf67(X1),nil),X0),nil)
| ~ ssList(app(skaf67(X1),X0))
| ~ ssList(skaf67(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1862,plain,
( ~ sQ8_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f1849,f1859,f530]) ).
fof(f1863,definition,
! [X0,X1,X2] :
( sQ130_spl
<=> ( segmentP(app(skaf67(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf67(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1866,plain,
( ~ sQ8_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f1850,f1863,f530]) ).
fof(f1869,plain,
! [X0] :
( frontsegP(skaf68(X0),skaf68(X0))
| ~ ssList(skaf68(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f760,f1398]) ).
fof(f1870,plain,
! [X0] :
( ssList(skaf68(X0))
| ~ ssList(skaf68(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f760,f283]) ).
fof(f1871,plain,
! [X0,X1] :
( segmentP(app(app(skaf68(X1),nil),X0),nil)
| ~ ssList(app(skaf68(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf68(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f760,f481]) ).
fof(f1872,plain,
! [X0,X1,X2] :
( segmentP(app(skaf68(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf68(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f760,f402]) ).
fof(f1873,definition,
! [X0] :
( sQ131_spl
<=> ( frontsegP(skaf68(X0),skaf68(X0))
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1876,plain,
( sQ131_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1869,f530,f1873]) ).
fof(f1877,definition,
! [X0] :
( sQ132_spl
<=> ( ssList(skaf68(X0))
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1880,plain,
( sQ132_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1870,f530,f1877]) ).
fof(f1881,definition,
! [X0,X1] :
( sQ133_spl
<=> ( segmentP(app(app(skaf68(X1),nil),X0),nil)
| ~ ssList(app(skaf68(X1),X0))
| ~ ssList(skaf68(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1884,plain,
( ~ sQ8_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f1871,f1881,f530]) ).
fof(f1885,definition,
! [X0,X1,X2] :
( sQ134_spl
<=> ( segmentP(app(skaf68(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf68(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1888,plain,
( ~ sQ8_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f1872,f1885,f530]) ).
fof(f1891,plain,
! [X0] :
( frontsegP(skaf71(X0),skaf71(X0))
| ~ ssList(skaf71(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f761,f1398]) ).
fof(f1892,plain,
! [X0] :
( ssList(skaf71(X0))
| ~ ssList(skaf71(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f761,f283]) ).
fof(f1893,plain,
! [X0,X1] :
( segmentP(app(app(skaf71(X1),nil),X0),nil)
| ~ ssList(app(skaf71(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf71(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f761,f481]) ).
fof(f1894,plain,
! [X0,X1,X2] :
( segmentP(app(skaf71(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf71(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f761,f402]) ).
fof(f1895,definition,
! [X0] :
( sQ135_spl
<=> ( frontsegP(skaf71(X0),skaf71(X0))
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1898,plain,
( sQ135_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1891,f530,f1895]) ).
fof(f1899,definition,
! [X0] :
( sQ136_spl
<=> ( ssList(skaf71(X0))
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1902,plain,
( sQ136_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1892,f530,f1899]) ).
fof(f1903,definition,
! [X0,X1] :
( sQ137_spl
<=> ( segmentP(app(app(skaf71(X1),nil),X0),nil)
| ~ ssList(app(skaf71(X1),X0))
| ~ ssList(skaf71(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1906,plain,
( ~ sQ8_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f1893,f1903,f530]) ).
fof(f1907,definition,
! [X0,X1,X2] :
( sQ138_spl
<=> ( segmentP(app(skaf71(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf71(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1910,plain,
( ~ sQ8_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f1894,f1907,f530]) ).
fof(f1913,plain,
! [X0] :
( frontsegP(skaf72(X0),skaf72(X0))
| ~ ssList(skaf72(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f762,f1398]) ).
fof(f1914,plain,
! [X0] :
( ssList(skaf72(X0))
| ~ ssList(skaf72(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f762,f283]) ).
fof(f1915,plain,
! [X0,X1] :
( segmentP(app(app(skaf72(X1),nil),X0),nil)
| ~ ssList(app(skaf72(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf72(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f762,f481]) ).
fof(f1916,plain,
! [X0,X1,X2] :
( segmentP(app(skaf72(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf72(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f762,f402]) ).
fof(f1917,definition,
! [X0] :
( sQ139_spl
<=> ( frontsegP(skaf72(X0),skaf72(X0))
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1920,plain,
( sQ139_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1913,f530,f1917]) ).
fof(f1921,definition,
! [X0] :
( sQ140_spl
<=> ( ssList(skaf72(X0))
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1924,plain,
( sQ140_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1914,f530,f1921]) ).
fof(f1925,definition,
! [X0,X1] :
( sQ141_spl
<=> ( segmentP(app(app(skaf72(X1),nil),X0),nil)
| ~ ssList(app(skaf72(X1),X0))
| ~ ssList(skaf72(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1928,plain,
( ~ sQ8_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f1915,f1925,f530]) ).
fof(f1929,definition,
! [X0,X1,X2] :
( sQ142_spl
<=> ( segmentP(app(skaf72(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf72(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1932,plain,
( ~ sQ8_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f1916,f1929,f530]) ).
fof(f1935,plain,
! [X0] :
( frontsegP(skaf73(X0),skaf73(X0))
| ~ ssList(skaf73(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f763,f1398]) ).
fof(f1936,plain,
! [X0] :
( ssList(skaf73(X0))
| ~ ssList(skaf73(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f763,f283]) ).
fof(f1937,plain,
! [X0,X1] :
( segmentP(app(app(skaf73(X1),nil),X0),nil)
| ~ ssList(app(skaf73(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf73(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f763,f481]) ).
fof(f1938,plain,
! [X0,X1,X2] :
( segmentP(app(skaf73(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf73(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f763,f402]) ).
fof(f1939,definition,
! [X0] :
( sQ143_spl
<=> ( frontsegP(skaf73(X0),skaf73(X0))
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1942,plain,
( sQ143_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1935,f530,f1939]) ).
fof(f1943,definition,
! [X0] :
( sQ144_spl
<=> ( ssList(skaf73(X0))
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1946,plain,
( sQ144_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1936,f530,f1943]) ).
fof(f1947,definition,
! [X0,X1] :
( sQ145_spl
<=> ( segmentP(app(app(skaf73(X1),nil),X0),nil)
| ~ ssList(app(skaf73(X1),X0))
| ~ ssList(skaf73(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1950,plain,
( ~ sQ8_spl
| sQ145_spl ),
inference(split_clause,[status(thm)],[f1937,f1947,f530]) ).
fof(f1951,definition,
! [X0,X1,X2] :
( sQ146_spl
<=> ( segmentP(app(skaf73(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf73(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1954,plain,
( ~ sQ8_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f1938,f1951,f530]) ).
fof(f1957,plain,
! [X0] :
( ~ sQ52_spl
| ~ ssList(sk4)
| ~ ssList(X0)
| segmentP(app(sk4,X0),sk4)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f982,f283]) ).
fof(f1958,plain,
( ~ sQ52_spl
| segmentP(app(sk4,nil),sk4)
| ~ ssList(sk4)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f770,f982]) ).
fof(f1959,definition,
! [X0] :
( sQ147_spl
<=> ( ~ ssList(X0)
| segmentP(app(sk4,X0),sk4)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1960,plain,
! [X0] :
( ~ sQ147_spl
| ~ ssList(X0)
| segmentP(app(sk4,X0),sk4)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1959]) ).
fof(f1962,plain,
( ~ sQ52_spl
| ~ sQ6_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f1957,f1959,f516,f966]) ).
fof(f1963,definition,
( sQ148_spl
<=> segmentP(app(sk4,nil),sk4) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1966,plain,
( ~ sQ52_spl
| sQ148_spl
| ~ sQ6_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1958,f530,f516,f1963,f966]) ).
fof(f1967,plain,
! [X0] :
( ~ sQ147_spl
| segmentP(app(sk4,X0),sk4)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1960]) ).
fof(f1969,plain,
! [X0,X1] :
( ~ sQ147_spl
| segmentP(X1,sk4)
| ~ ssList(X1)
| ~ ssList(app(sk4,X0))
| ~ ssList(sk4)
| ~ segmentP(X1,app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1967,f372]) ).
fof(f1970,plain,
! [X0] :
( ~ sQ147_spl
| app(sk4,X0) = sk4
| ~ ssList(app(sk4,X0))
| ~ ssList(sk4)
| ~ segmentP(sk4,app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1967,f337]) ).
fof(f1972,definition,
! [X0,X1] :
( sQ149_spl
<=> ( segmentP(X1,sk4)
| ~ ssList(X1)
| ~ ssList(app(sk4,X0))
| ~ segmentP(X1,app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1975,plain,
( ~ sQ147_spl
| ~ sQ6_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1969,f1972,f516,f1959]) ).
fof(f1976,definition,
! [X0] :
( sQ150_spl
<=> ( app(sk4,X0) = sk4
| ~ ssList(app(sk4,X0))
| ~ segmentP(sk4,app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1979,plain,
( ~ sQ147_spl
| ~ sQ6_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f1970,f1976,f516,f1959]) ).
fof(f1983,plain,
! [X0] :
( ~ sQ53_spl
| segmentP(sk4,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f770,f971]) ).
fof(f1986,definition,
! [X0] :
( sQ151_spl
<=> ( segmentP(sk4,X0)
| ~ ssList(X0)
| ~ segmentP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1989,plain,
( ~ sQ53_spl
| ~ sQ8_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f1983,f1986,f530,f970]) ).
fof(f2007,plain,
! [X0] :
( ~ sQ34_spl
| frontsegP(app(nil,X0),nil)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f824]) ).
fof(f2008,plain,
! [X0] :
( ~ sQ48_spl
| frontsegP(app(sk3,X0),nil)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f949]) ).
fof(f2009,plain,
! [X0] :
( ~ sQ28_spl
| frontsegP(app(sk3,X0),sk3)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f792]) ).
fof(f2010,plain,
! [X0,X1] :
( ~ sQ49_spl
| ~ ssList(X1)
| ~ frontsegP(nil,X1)
| frontsegP(app(sk3,X0),X1)
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f945]) ).
fof(f2011,plain,
! [X0] :
( ~ sQ54_spl
| frontsegP(app(sk4,X0),nil)
| ~ ssList(sk4)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f983]) ).
fof(f2012,plain,
! [X0] :
( ~ sQ39_spl
| frontsegP(app(sk4,X0),sk4)
| ~ ssList(sk4)
| ~ ssList(sk4)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f851]) ).
fof(f2014,plain,
! [X0,X1] :
( ~ sQ55_spl
| ~ ssList(X1)
| ~ frontsegP(nil,X1)
| frontsegP(app(sk4,X0),X1)
| ~ ssList(sk4)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f979]) ).
fof(f2016,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f349,f257]) ).
fof(f2020,definition,
! [X0] :
( sQ153_spl
<=> ( frontsegP(app(nil,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f2023,plain,
( ~ sQ34_spl
| ~ sQ8_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f2007,f2020,f530,f815]) ).
fof(f2024,definition,
! [X0] :
( sQ154_spl
<=> ( frontsegP(app(sk3,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f2025,plain,
! [X0] :
( ~ sQ154_spl
| frontsegP(app(sk3,X0),nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f2024]) ).
fof(f2027,plain,
( ~ sQ48_spl
| ~ sQ10_spl
| ~ sQ8_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f2008,f2024,f530,f541,f940]) ).
fof(f2028,definition,
! [X0] :
( sQ155_spl
<=> ( frontsegP(app(sk3,X0),sk3)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f2029,plain,
! [X0] :
( ~ sQ155_spl
| frontsegP(app(sk3,X0),sk3)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f2028]) ).
fof(f2031,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f2009,f2028,f541,f783]) ).
fof(f2032,definition,
! [X0,X1] :
( sQ156_spl
<=> ( ~ ssList(X1)
| ~ frontsegP(nil,X1)
| frontsegP(app(sk3,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f2035,plain,
( ~ sQ49_spl
| ~ sQ10_spl
| sQ156_spl ),
inference(split_clause,[status(thm)],[f2010,f2032,f541,f944]) ).
fof(f2036,definition,
! [X0] :
( sQ157_spl
<=> ( frontsegP(app(sk4,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f2037,plain,
! [X0] :
( ~ sQ157_spl
| frontsegP(app(sk4,X0),nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f2036]) ).
fof(f2039,plain,
( ~ sQ54_spl
| ~ sQ6_spl
| ~ sQ8_spl
| sQ157_spl ),
inference(split_clause,[status(thm)],[f2011,f2036,f530,f516,f974]) ).
fof(f2040,definition,
! [X0] :
( sQ158_spl
<=> ( frontsegP(app(sk4,X0),sk4)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f2041,plain,
! [X0] :
( ~ sQ158_spl
| frontsegP(app(sk4,X0),sk4)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f2040]) ).
fof(f2043,plain,
( ~ sQ39_spl
| ~ sQ6_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f2012,f2040,f516,f842]) ).
fof(f2048,definition,
! [X0,X1] :
( sQ160_spl
<=> ( ~ ssList(X1)
| ~ frontsegP(nil,X1)
| frontsegP(app(sk4,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f2051,plain,
( ~ sQ55_spl
| ~ sQ6_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f2014,f2048,f516,f978]) ).
fof(f2054,definition,
! [X0,X1] :
( sQ161_spl
<=> ( ~ ssList(X1)
| frontsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f2057,plain,
( ~ sQ8_spl
| sQ161_spl ),
inference(split_clause,[status(thm)],[f2016,f2054,f530]) ).
fof(f2089,plain,
! [X0] :
( frontsegP(skaf75(X0),skaf75(X0))
| ~ ssList(skaf75(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f764,f1398]) ).
fof(f2090,plain,
! [X0] :
( ssList(skaf75(X0))
| ~ ssList(skaf75(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f764,f283]) ).
fof(f2091,plain,
! [X0,X1] :
( segmentP(app(app(skaf75(X1),nil),X0),nil)
| ~ ssList(app(skaf75(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf75(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f764,f481]) ).
fof(f2092,plain,
! [X0,X1,X2] :
( segmentP(app(skaf75(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf75(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f764,f402]) ).
fof(f2093,definition,
! [X0] :
( sQ162_spl
<=> ( frontsegP(skaf75(X0),skaf75(X0))
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f2096,plain,
( sQ162_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2089,f530,f2093]) ).
fof(f2097,definition,
! [X0] :
( sQ163_spl
<=> ( ssList(skaf75(X0))
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f2100,plain,
( sQ163_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2090,f530,f2097]) ).
fof(f2101,definition,
! [X0,X1] :
( sQ164_spl
<=> ( segmentP(app(app(skaf75(X1),nil),X0),nil)
| ~ ssList(app(skaf75(X1),X0))
| ~ ssList(skaf75(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2104,plain,
( ~ sQ8_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f2091,f2101,f530]) ).
fof(f2105,definition,
! [X0,X1,X2] :
( sQ165_spl
<=> ( segmentP(app(skaf75(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf75(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f2108,plain,
( ~ sQ8_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f2092,f2105,f530]) ).
fof(f2111,plain,
! [X0] :
( frontsegP(skaf76(X0),skaf76(X0))
| ~ ssList(skaf76(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f765,f1398]) ).
fof(f2112,plain,
! [X0] :
( ssList(skaf76(X0))
| ~ ssList(skaf76(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f765,f283]) ).
fof(f2113,plain,
! [X0,X1] :
( segmentP(app(app(skaf76(X1),nil),X0),nil)
| ~ ssList(app(skaf76(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf76(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f765,f481]) ).
fof(f2114,plain,
! [X0,X1,X2] :
( segmentP(app(skaf76(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf76(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f765,f402]) ).
fof(f2115,definition,
! [X0] :
( sQ166_spl
<=> ( frontsegP(skaf76(X0),skaf76(X0))
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f2118,plain,
( sQ166_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2111,f530,f2115]) ).
fof(f2119,definition,
! [X0] :
( sQ167_spl
<=> ( ssList(skaf76(X0))
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f2122,plain,
( sQ167_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2112,f530,f2119]) ).
fof(f2123,definition,
! [X0,X1] :
( sQ168_spl
<=> ( segmentP(app(app(skaf76(X1),nil),X0),nil)
| ~ ssList(app(skaf76(X1),X0))
| ~ ssList(skaf76(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f2126,plain,
( ~ sQ8_spl
| sQ168_spl ),
inference(split_clause,[status(thm)],[f2113,f2123,f530]) ).
fof(f2127,definition,
! [X0,X1,X2] :
( sQ169_spl
<=> ( segmentP(app(skaf76(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf76(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f2130,plain,
( ~ sQ8_spl
| sQ169_spl ),
inference(split_clause,[status(thm)],[f2114,f2127,f530]) ).
fof(f2133,plain,
! [X0] :
( frontsegP(skaf77(X0),skaf77(X0))
| ~ ssList(skaf77(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f766,f1398]) ).
fof(f2134,plain,
! [X0] :
( ssList(skaf77(X0))
| ~ ssList(skaf77(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f766,f283]) ).
fof(f2135,plain,
! [X0,X1] :
( segmentP(app(app(skaf77(X1),nil),X0),nil)
| ~ ssList(app(skaf77(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf77(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f766,f481]) ).
fof(f2136,plain,
! [X0,X1,X2] :
( segmentP(app(skaf77(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf77(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f766,f402]) ).
fof(f2137,definition,
! [X0] :
( sQ170_spl
<=> ( frontsegP(skaf77(X0),skaf77(X0))
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f2140,plain,
( sQ170_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2133,f530,f2137]) ).
fof(f2141,definition,
! [X0] :
( sQ171_spl
<=> ( ssList(skaf77(X0))
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f2144,plain,
( sQ171_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2134,f530,f2141]) ).
fof(f2145,definition,
! [X0,X1] :
( sQ172_spl
<=> ( segmentP(app(app(skaf77(X1),nil),X0),nil)
| ~ ssList(app(skaf77(X1),X0))
| ~ ssList(skaf77(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f2148,plain,
( ~ sQ8_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f2135,f2145,f530]) ).
fof(f2149,definition,
! [X0,X1,X2] :
( sQ173_spl
<=> ( segmentP(app(skaf77(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf77(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f2152,plain,
( ~ sQ8_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f2136,f2149,f530]) ).
fof(f2155,plain,
! [X0] :
( frontsegP(skaf80(X0),skaf80(X0))
| ~ ssList(skaf80(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f767,f1398]) ).
fof(f2156,plain,
! [X0] :
( ssList(skaf80(X0))
| ~ ssList(skaf80(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f767,f283]) ).
fof(f2157,plain,
! [X0,X1] :
( segmentP(app(app(skaf80(X1),nil),X0),nil)
| ~ ssList(app(skaf80(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf80(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f767,f481]) ).
fof(f2158,plain,
! [X0,X1,X2] :
( segmentP(app(skaf80(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf80(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f767,f402]) ).
fof(f2159,definition,
! [X0] :
( sQ174_spl
<=> ( frontsegP(skaf80(X0),skaf80(X0))
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f2162,plain,
( sQ174_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2155,f530,f2159]) ).
fof(f2163,definition,
! [X0] :
( sQ175_spl
<=> ( ssList(skaf80(X0))
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f2166,plain,
( sQ175_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2156,f530,f2163]) ).
fof(f2167,definition,
! [X0,X1] :
( sQ176_spl
<=> ( segmentP(app(app(skaf80(X1),nil),X0),nil)
| ~ ssList(app(skaf80(X1),X0))
| ~ ssList(skaf80(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f2170,plain,
( ~ sQ8_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f2157,f2167,f530]) ).
fof(f2171,definition,
! [X0,X1,X2] :
( sQ177_spl
<=> ( segmentP(app(skaf80(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf80(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f2174,plain,
( ~ sQ8_spl
| sQ177_spl ),
inference(split_clause,[status(thm)],[f2158,f2171,f530]) ).
fof(f2177,plain,
! [X0] :
( frontsegP(skaf81(X0),skaf81(X0))
| ~ ssList(skaf81(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f768,f1398]) ).
fof(f2178,plain,
! [X0] :
( ssList(skaf81(X0))
| ~ ssList(skaf81(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f768,f283]) ).
fof(f2179,plain,
! [X0,X1] :
( segmentP(app(app(skaf81(X1),nil),X0),nil)
| ~ ssList(app(skaf81(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf81(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f768,f481]) ).
fof(f2180,plain,
! [X0,X1,X2] :
( segmentP(app(skaf81(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf81(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f768,f402]) ).
fof(f2181,definition,
! [X0] :
( sQ178_spl
<=> ( frontsegP(skaf81(X0),skaf81(X0))
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f2184,plain,
( sQ178_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2177,f530,f2181]) ).
fof(f2185,definition,
! [X0] :
( sQ179_spl
<=> ( ssList(skaf81(X0))
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f2188,plain,
( sQ179_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2178,f530,f2185]) ).
fof(f2189,definition,
! [X0,X1] :
( sQ180_spl
<=> ( segmentP(app(app(skaf81(X1),nil),X0),nil)
| ~ ssList(app(skaf81(X1),X0))
| ~ ssList(skaf81(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f2192,plain,
( ~ sQ8_spl
| sQ180_spl ),
inference(split_clause,[status(thm)],[f2179,f2189,f530]) ).
fof(f2193,definition,
! [X0,X1,X2] :
( sQ181_spl
<=> ( segmentP(app(skaf81(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf81(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f2196,plain,
( ~ sQ8_spl
| sQ181_spl ),
inference(split_clause,[status(thm)],[f2180,f2193,f530]) ).
fof(f2199,plain,
! [X0] :
( frontsegP(skaf82(X0),skaf82(X0))
| ~ ssList(skaf82(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f769,f1398]) ).
fof(f2200,plain,
! [X0] :
( ssList(skaf82(X0))
| ~ ssList(skaf82(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f769,f283]) ).
fof(f2201,plain,
! [X0,X1] :
( segmentP(app(app(skaf82(X1),nil),X0),nil)
| ~ ssList(app(skaf82(X1),X0))
| ~ ssList(nil)
| ~ ssList(skaf82(X1))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f769,f481]) ).
fof(f2202,plain,
! [X0,X1,X2] :
( segmentP(app(skaf82(X2),X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf82(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f769,f402]) ).
fof(f2203,definition,
! [X0] :
( sQ182_spl
<=> ( frontsegP(skaf82(X0),skaf82(X0))
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2206,plain,
( sQ182_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2199,f530,f2203]) ).
fof(f2207,definition,
! [X0] :
( sQ183_spl
<=> ( ssList(skaf82(X0))
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f2210,plain,
( sQ183_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2200,f530,f2207]) ).
fof(f2211,definition,
! [X0,X1] :
( sQ184_spl
<=> ( segmentP(app(app(skaf82(X1),nil),X0),nil)
| ~ ssList(app(skaf82(X1),X0))
| ~ ssList(skaf82(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f2214,plain,
( ~ sQ8_spl
| sQ184_spl ),
inference(split_clause,[status(thm)],[f2201,f2211,f530]) ).
fof(f2215,definition,
! [X0,X1,X2] :
( sQ185_spl
<=> ( segmentP(app(skaf82(X2),X1),X0)
| ~ ssList(X0)
| ~ ssList(skaf82(X2))
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2218,plain,
( ~ sQ8_spl
| sQ185_spl ),
inference(split_clause,[status(thm)],[f2202,f2215,f530]) ).
fof(f2221,plain,
! [X0] :
( frontsegP(skaf51(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf51(X0)) ),
inference(paramodulation,[status(thm)],[f906,f1398]) ).
fof(f2223,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf51(X1)),X0),skaf51(X1))
| ~ ssList(app(skaf51(X1),X0))
| ~ ssList(skaf51(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f906,f481]) ).
fof(f2224,plain,
! [X0,X1,X2] :
( segmentP(app(skaf51(X0),X2),X1)
| ~ ssList(skaf51(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf51(X0),X1) ),
inference(paramodulation,[status(thm)],[f906,f402]) ).
fof(f2225,definition,
! [X0] :
( sQ186_spl
<=> ( frontsegP(skaf51(X0),nil)
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f2228,plain,
( ~ sQ8_spl
| sQ186_spl ),
inference(split_clause,[status(thm)],[f2221,f2225,f530]) ).
fof(f2230,definition,
! [X0,X1] :
( sQ187_spl
<=> ( segmentP(app(app(nil,skaf51(X1)),X0),skaf51(X1))
| ~ ssList(app(skaf51(X1),X0))
| ~ ssList(skaf51(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f2233,plain,
( ~ sQ8_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f2223,f2230,f530]) ).
fof(f2234,definition,
! [X0,X1,X2] :
( sQ188_spl
<=> ( segmentP(app(skaf51(X0),X2),X1)
| ~ ssList(skaf51(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf51(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2237,plain,
( ~ sQ8_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f2224,f2234,f530]) ).
fof(f2241,plain,
! [X0] :
( frontsegP(skaf52(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf52(X0)) ),
inference(paramodulation,[status(thm)],[f907,f1398]) ).
fof(f2243,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf52(X1)),X0),skaf52(X1))
| ~ ssList(app(skaf52(X1),X0))
| ~ ssList(skaf52(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f907,f481]) ).
fof(f2244,plain,
! [X0,X1,X2] :
( segmentP(app(skaf52(X0),X2),X1)
| ~ ssList(skaf52(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf52(X0),X1) ),
inference(paramodulation,[status(thm)],[f907,f402]) ).
fof(f2245,definition,
! [X0] :
( sQ189_spl
<=> ( frontsegP(skaf52(X0),nil)
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2248,plain,
( ~ sQ8_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f2241,f2245,f530]) ).
fof(f2250,definition,
! [X0,X1] :
( sQ190_spl
<=> ( segmentP(app(app(nil,skaf52(X1)),X0),skaf52(X1))
| ~ ssList(app(skaf52(X1),X0))
| ~ ssList(skaf52(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2253,plain,
( ~ sQ8_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f2243,f2250,f530]) ).
fof(f2254,definition,
! [X0,X1,X2] :
( sQ191_spl
<=> ( segmentP(app(skaf52(X0),X2),X1)
| ~ ssList(skaf52(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf52(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f2257,plain,
( ~ sQ8_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f2244,f2254,f530]) ).
fof(f2261,plain,
! [X0] :
( frontsegP(skaf53(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf53(X0)) ),
inference(paramodulation,[status(thm)],[f908,f1398]) ).
fof(f2263,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf53(X1)),X0),skaf53(X1))
| ~ ssList(app(skaf53(X1),X0))
| ~ ssList(skaf53(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f908,f481]) ).
fof(f2264,plain,
! [X0,X1,X2] :
( segmentP(app(skaf53(X0),X2),X1)
| ~ ssList(skaf53(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf53(X0),X1) ),
inference(paramodulation,[status(thm)],[f908,f402]) ).
fof(f2265,definition,
! [X0] :
( sQ192_spl
<=> ( frontsegP(skaf53(X0),nil)
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2268,plain,
( ~ sQ8_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f2261,f2265,f530]) ).
fof(f2270,definition,
! [X0,X1] :
( sQ193_spl
<=> ( segmentP(app(app(nil,skaf53(X1)),X0),skaf53(X1))
| ~ ssList(app(skaf53(X1),X0))
| ~ ssList(skaf53(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f2273,plain,
( ~ sQ8_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f2263,f2270,f530]) ).
fof(f2274,definition,
! [X0,X1,X2] :
( sQ194_spl
<=> ( segmentP(app(skaf53(X0),X2),X1)
| ~ ssList(skaf53(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf53(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2277,plain,
( ~ sQ8_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f2264,f2274,f530]) ).
fof(f2281,plain,
! [X0] :
( frontsegP(skaf56(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf56(X0)) ),
inference(paramodulation,[status(thm)],[f909,f1398]) ).
fof(f2283,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf56(X1)),X0),skaf56(X1))
| ~ ssList(app(skaf56(X1),X0))
| ~ ssList(skaf56(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f909,f481]) ).
fof(f2284,plain,
! [X0,X1,X2] :
( segmentP(app(skaf56(X0),X2),X1)
| ~ ssList(skaf56(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf56(X0),X1) ),
inference(paramodulation,[status(thm)],[f909,f402]) ).
fof(f2285,definition,
! [X0] :
( sQ195_spl
<=> ( frontsegP(skaf56(X0),nil)
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f2288,plain,
( ~ sQ8_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f2281,f2285,f530]) ).
fof(f2290,definition,
! [X0,X1] :
( sQ196_spl
<=> ( segmentP(app(app(nil,skaf56(X1)),X0),skaf56(X1))
| ~ ssList(app(skaf56(X1),X0))
| ~ ssList(skaf56(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2293,plain,
( ~ sQ8_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f2283,f2290,f530]) ).
fof(f2294,definition,
! [X0,X1,X2] :
( sQ197_spl
<=> ( segmentP(app(skaf56(X0),X2),X1)
| ~ ssList(skaf56(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf56(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f2297,plain,
( ~ sQ8_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f2284,f2294,f530]) ).
fof(f2301,plain,
! [X0] :
( frontsegP(skaf57(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf57(X0)) ),
inference(paramodulation,[status(thm)],[f910,f1398]) ).
fof(f2303,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf57(X1)),X0),skaf57(X1))
| ~ ssList(app(skaf57(X1),X0))
| ~ ssList(skaf57(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f910,f481]) ).
fof(f2304,plain,
! [X0,X1,X2] :
( segmentP(app(skaf57(X0),X2),X1)
| ~ ssList(skaf57(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf57(X0),X1) ),
inference(paramodulation,[status(thm)],[f910,f402]) ).
fof(f2305,definition,
! [X0] :
( sQ198_spl
<=> ( frontsegP(skaf57(X0),nil)
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f2308,plain,
( ~ sQ8_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f2301,f2305,f530]) ).
fof(f2310,definition,
! [X0,X1] :
( sQ199_spl
<=> ( segmentP(app(app(nil,skaf57(X1)),X0),skaf57(X1))
| ~ ssList(app(skaf57(X1),X0))
| ~ ssList(skaf57(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f2313,plain,
( ~ sQ8_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f2303,f2310,f530]) ).
fof(f2314,definition,
! [X0,X1,X2] :
( sQ200_spl
<=> ( segmentP(app(skaf57(X0),X2),X1)
| ~ ssList(skaf57(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf57(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f2317,plain,
( ~ sQ8_spl
| sQ200_spl ),
inference(split_clause,[status(thm)],[f2304,f2314,f530]) ).
fof(f2321,plain,
! [X0] :
( frontsegP(skaf58(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf58(X0)) ),
inference(paramodulation,[status(thm)],[f911,f1398]) ).
fof(f2323,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf58(X1)),X0),skaf58(X1))
| ~ ssList(app(skaf58(X1),X0))
| ~ ssList(skaf58(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f911,f481]) ).
fof(f2324,plain,
! [X0,X1,X2] :
( segmentP(app(skaf58(X0),X2),X1)
| ~ ssList(skaf58(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf58(X0),X1) ),
inference(paramodulation,[status(thm)],[f911,f402]) ).
fof(f2325,definition,
! [X0] :
( sQ201_spl
<=> ( frontsegP(skaf58(X0),nil)
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f2328,plain,
( ~ sQ8_spl
| sQ201_spl ),
inference(split_clause,[status(thm)],[f2321,f2325,f530]) ).
fof(f2330,definition,
! [X0,X1] :
( sQ202_spl
<=> ( segmentP(app(app(nil,skaf58(X1)),X0),skaf58(X1))
| ~ ssList(app(skaf58(X1),X0))
| ~ ssList(skaf58(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f2333,plain,
( ~ sQ8_spl
| sQ202_spl ),
inference(split_clause,[status(thm)],[f2323,f2330,f530]) ).
fof(f2334,definition,
! [X0,X1,X2] :
( sQ203_spl
<=> ( segmentP(app(skaf58(X0),X2),X1)
| ~ ssList(skaf58(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf58(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2337,plain,
( ~ sQ8_spl
| sQ203_spl ),
inference(split_clause,[status(thm)],[f2324,f2334,f530]) ).
fof(f2341,plain,
! [X0] :
( ~ sQ158_spl
| app(sk4,X0) = sk4
| ~ ssList(app(sk4,X0))
| ~ ssList(sk4)
| ~ frontsegP(sk4,app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2041,f339]) ).
fof(f2342,plain,
! [X0,X1] :
( ~ sQ158_spl
| frontsegP(app(app(sk4,X0),X1),sk4)
| ~ ssList(app(sk4,X0))
| ~ ssList(sk4)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2041,f349]) ).
fof(f2343,plain,
( ~ sQ158_spl
| frontsegP(sk4,sk4)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f770,f2041]) ).
fof(f2344,definition,
! [X0] :
( sQ204_spl
<=> ( app(sk4,X0) = sk4
| ~ ssList(app(sk4,X0))
| ~ frontsegP(sk4,app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f2347,plain,
( ~ sQ158_spl
| ~ sQ6_spl
| sQ204_spl ),
inference(split_clause,[status(thm)],[f2341,f2344,f516,f2040]) ).
fof(f2348,definition,
! [X0,X1] :
( sQ205_spl
<=> ( frontsegP(app(app(sk4,X0),X1),sk4)
| ~ ssList(app(sk4,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f2351,plain,
( ~ sQ158_spl
| ~ sQ6_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f2342,f2348,f516,f2040]) ).
fof(f2352,plain,
( ~ sQ158_spl
| sQ41_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2343,f530,f853,f2040]) ).
fof(f2353,plain,
! [X0] :
( ~ sQ157_spl
| app(sk4,X0) = nil
| ~ ssList(app(sk4,X0))
| ~ ssList(nil)
| ~ frontsegP(nil,app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2037,f339]) ).
fof(f2354,plain,
! [X0,X1] :
( ~ sQ157_spl
| frontsegP(app(app(sk4,X0),X1),nil)
| ~ ssList(app(sk4,X0))
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2037,f349]) ).
fof(f2355,plain,
( ~ sQ157_spl
| frontsegP(sk4,nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f770,f2037]) ).
fof(f2356,definition,
! [X0] :
( sQ206_spl
<=> ( app(sk4,X0) = nil
| ~ ssList(app(sk4,X0))
| ~ frontsegP(nil,app(sk4,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f2359,plain,
( ~ sQ157_spl
| ~ sQ8_spl
| sQ206_spl ),
inference(split_clause,[status(thm)],[f2353,f2356,f530,f2036]) ).
fof(f2360,definition,
! [X0,X1] :
( sQ207_spl
<=> ( frontsegP(app(app(sk4,X0),X1),nil)
| ~ ssList(app(sk4,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f2363,plain,
( ~ sQ157_spl
| ~ sQ8_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f2354,f2360,f530,f2036]) ).
fof(f2364,plain,
( ~ sQ157_spl
| sQ76_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2355,f530,f1461,f2036]) ).
fof(f2365,plain,
! [X0] :
( ~ sQ155_spl
| app(sk3,X0) = sk3
| ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ frontsegP(sk3,app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2029,f339]) ).
fof(f2366,plain,
! [X0,X1] :
( ~ sQ155_spl
| frontsegP(app(app(sk3,X0),X1),sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2029,f349]) ).
fof(f2368,definition,
! [X0] :
( sQ208_spl
<=> ( app(sk3,X0) = sk3
| ~ ssList(app(sk3,X0))
| ~ frontsegP(sk3,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f2371,plain,
( ~ sQ155_spl
| ~ sQ10_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f2365,f2368,f541,f2028]) ).
fof(f2372,definition,
! [X0,X1] :
( sQ209_spl
<=> ( frontsegP(app(app(sk3,X0),X1),sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f2375,plain,
( ~ sQ155_spl
| ~ sQ10_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f2366,f2372,f541,f2028]) ).
fof(f2377,plain,
! [X0] :
( ~ sQ154_spl
| app(sk3,X0) = nil
| ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ frontsegP(nil,app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2025,f339]) ).
fof(f2378,plain,
! [X0,X1] :
( ~ sQ154_spl
| frontsegP(app(app(sk3,X0),X1),nil)
| ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2025,f349]) ).
fof(f2379,plain,
( ~ sQ154_spl
| frontsegP(sk3,nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f741,f2025]) ).
fof(f2380,definition,
! [X0] :
( sQ210_spl
<=> ( app(sk3,X0) = nil
| ~ ssList(app(sk3,X0))
| ~ frontsegP(nil,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f2383,plain,
( ~ sQ154_spl
| ~ sQ8_spl
| sQ210_spl ),
inference(split_clause,[status(thm)],[f2377,f2380,f530,f2024]) ).
fof(f2384,definition,
! [X0,X1] :
( sQ211_spl
<=> ( frontsegP(app(app(sk3,X0),X1),nil)
| ~ ssList(app(sk3,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2387,plain,
( ~ sQ154_spl
| ~ sQ8_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f2378,f2384,f530,f2024]) ).
fof(f2388,plain,
( ~ sQ154_spl
| sQ75_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2379,f530,f1457,f2024]) ).
fof(f2440,plain,
! [X0] :
( frontsegP(skaf61(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf61(X0)) ),
inference(paramodulation,[status(thm)],[f912,f1398]) ).
fof(f2442,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf61(X1)),X0),skaf61(X1))
| ~ ssList(app(skaf61(X1),X0))
| ~ ssList(skaf61(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f912,f481]) ).
fof(f2443,plain,
! [X0,X1,X2] :
( segmentP(app(skaf61(X0),X2),X1)
| ~ ssList(skaf61(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf61(X0),X1) ),
inference(paramodulation,[status(thm)],[f912,f402]) ).
fof(f2444,definition,
! [X0] :
( sQ214_spl
<=> ( frontsegP(skaf61(X0),nil)
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f2447,plain,
( ~ sQ8_spl
| sQ214_spl ),
inference(split_clause,[status(thm)],[f2440,f2444,f530]) ).
fof(f2449,definition,
! [X0,X1] :
( sQ215_spl
<=> ( segmentP(app(app(nil,skaf61(X1)),X0),skaf61(X1))
| ~ ssList(app(skaf61(X1),X0))
| ~ ssList(skaf61(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2452,plain,
( ~ sQ8_spl
| sQ215_spl ),
inference(split_clause,[status(thm)],[f2442,f2449,f530]) ).
fof(f2453,definition,
! [X0,X1,X2] :
( sQ216_spl
<=> ( segmentP(app(skaf61(X0),X2),X1)
| ~ ssList(skaf61(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf61(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f2456,plain,
( ~ sQ8_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f2443,f2453,f530]) ).
fof(f2460,plain,
! [X0] :
( frontsegP(skaf62(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf62(X0)) ),
inference(paramodulation,[status(thm)],[f913,f1398]) ).
fof(f2462,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf62(X1)),X0),skaf62(X1))
| ~ ssList(app(skaf62(X1),X0))
| ~ ssList(skaf62(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f913,f481]) ).
fof(f2463,plain,
! [X0,X1,X2] :
( segmentP(app(skaf62(X0),X2),X1)
| ~ ssList(skaf62(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf62(X0),X1) ),
inference(paramodulation,[status(thm)],[f913,f402]) ).
fof(f2464,definition,
! [X0] :
( sQ217_spl
<=> ( frontsegP(skaf62(X0),nil)
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f2467,plain,
( ~ sQ8_spl
| sQ217_spl ),
inference(split_clause,[status(thm)],[f2460,f2464,f530]) ).
fof(f2469,definition,
! [X0,X1] :
( sQ218_spl
<=> ( segmentP(app(app(nil,skaf62(X1)),X0),skaf62(X1))
| ~ ssList(app(skaf62(X1),X0))
| ~ ssList(skaf62(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f2472,plain,
( ~ sQ8_spl
| sQ218_spl ),
inference(split_clause,[status(thm)],[f2462,f2469,f530]) ).
fof(f2473,definition,
! [X0,X1,X2] :
( sQ219_spl
<=> ( segmentP(app(skaf62(X0),X2),X1)
| ~ ssList(skaf62(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf62(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f2476,plain,
( ~ sQ8_spl
| sQ219_spl ),
inference(split_clause,[status(thm)],[f2463,f2473,f530]) ).
fof(f2480,plain,
! [X0] :
( frontsegP(skaf63(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf63(X0)) ),
inference(paramodulation,[status(thm)],[f914,f1398]) ).
fof(f2482,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf63(X1)),X0),skaf63(X1))
| ~ ssList(app(skaf63(X1),X0))
| ~ ssList(skaf63(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f914,f481]) ).
fof(f2483,plain,
! [X0,X1,X2] :
( segmentP(app(skaf63(X0),X2),X1)
| ~ ssList(skaf63(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf63(X0),X1) ),
inference(paramodulation,[status(thm)],[f914,f402]) ).
fof(f2484,definition,
! [X0] :
( sQ220_spl
<=> ( frontsegP(skaf63(X0),nil)
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f2487,plain,
( ~ sQ8_spl
| sQ220_spl ),
inference(split_clause,[status(thm)],[f2480,f2484,f530]) ).
fof(f2489,definition,
! [X0,X1] :
( sQ221_spl
<=> ( segmentP(app(app(nil,skaf63(X1)),X0),skaf63(X1))
| ~ ssList(app(skaf63(X1),X0))
| ~ ssList(skaf63(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2492,plain,
( ~ sQ8_spl
| sQ221_spl ),
inference(split_clause,[status(thm)],[f2482,f2489,f530]) ).
fof(f2493,definition,
! [X0,X1,X2] :
( sQ222_spl
<=> ( segmentP(app(skaf63(X0),X2),X1)
| ~ ssList(skaf63(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf63(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f2496,plain,
( ~ sQ8_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f2483,f2493,f530]) ).
fof(f2500,plain,
! [X0] :
( frontsegP(skaf66(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf66(X0)) ),
inference(paramodulation,[status(thm)],[f915,f1398]) ).
fof(f2502,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf66(X1)),X0),skaf66(X1))
| ~ ssList(app(skaf66(X1),X0))
| ~ ssList(skaf66(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f915,f481]) ).
fof(f2503,plain,
! [X0,X1,X2] :
( segmentP(app(skaf66(X0),X2),X1)
| ~ ssList(skaf66(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf66(X0),X1) ),
inference(paramodulation,[status(thm)],[f915,f402]) ).
fof(f2504,definition,
! [X0] :
( sQ223_spl
<=> ( frontsegP(skaf66(X0),nil)
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2507,plain,
( ~ sQ8_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f2500,f2504,f530]) ).
fof(f2509,definition,
! [X0,X1] :
( sQ224_spl
<=> ( segmentP(app(app(nil,skaf66(X1)),X0),skaf66(X1))
| ~ ssList(app(skaf66(X1),X0))
| ~ ssList(skaf66(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f2512,plain,
( ~ sQ8_spl
| sQ224_spl ),
inference(split_clause,[status(thm)],[f2502,f2509,f530]) ).
fof(f2513,definition,
! [X0,X1,X2] :
( sQ225_spl
<=> ( segmentP(app(skaf66(X0),X2),X1)
| ~ ssList(skaf66(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf66(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f2516,plain,
( ~ sQ8_spl
| sQ225_spl ),
inference(split_clause,[status(thm)],[f2503,f2513,f530]) ).
fof(f2520,plain,
! [X0] :
( frontsegP(skaf67(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf67(X0)) ),
inference(paramodulation,[status(thm)],[f916,f1398]) ).
fof(f2522,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf67(X1)),X0),skaf67(X1))
| ~ ssList(app(skaf67(X1),X0))
| ~ ssList(skaf67(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f916,f481]) ).
fof(f2523,plain,
! [X0,X1,X2] :
( segmentP(app(skaf67(X0),X2),X1)
| ~ ssList(skaf67(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf67(X0),X1) ),
inference(paramodulation,[status(thm)],[f916,f402]) ).
fof(f2524,definition,
! [X0] :
( sQ226_spl
<=> ( frontsegP(skaf67(X0),nil)
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f2527,plain,
( ~ sQ8_spl
| sQ226_spl ),
inference(split_clause,[status(thm)],[f2520,f2524,f530]) ).
fof(f2529,definition,
! [X0,X1] :
( sQ227_spl
<=> ( segmentP(app(app(nil,skaf67(X1)),X0),skaf67(X1))
| ~ ssList(app(skaf67(X1),X0))
| ~ ssList(skaf67(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f2532,plain,
( ~ sQ8_spl
| sQ227_spl ),
inference(split_clause,[status(thm)],[f2522,f2529,f530]) ).
fof(f2533,definition,
! [X0,X1,X2] :
( sQ228_spl
<=> ( segmentP(app(skaf67(X0),X2),X1)
| ~ ssList(skaf67(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf67(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f2536,plain,
( ~ sQ8_spl
| sQ228_spl ),
inference(split_clause,[status(thm)],[f2523,f2533,f530]) ).
fof(f2540,plain,
! [X0] :
( frontsegP(skaf68(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf68(X0)) ),
inference(paramodulation,[status(thm)],[f917,f1398]) ).
fof(f2542,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf68(X1)),X0),skaf68(X1))
| ~ ssList(app(skaf68(X1),X0))
| ~ ssList(skaf68(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f917,f481]) ).
fof(f2543,plain,
! [X0,X1,X2] :
( segmentP(app(skaf68(X0),X2),X1)
| ~ ssList(skaf68(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf68(X0),X1) ),
inference(paramodulation,[status(thm)],[f917,f402]) ).
fof(f2544,definition,
! [X0] :
( sQ229_spl
<=> ( frontsegP(skaf68(X0),nil)
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f2547,plain,
( ~ sQ8_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f2540,f2544,f530]) ).
fof(f2549,definition,
! [X0,X1] :
( sQ230_spl
<=> ( segmentP(app(app(nil,skaf68(X1)),X0),skaf68(X1))
| ~ ssList(app(skaf68(X1),X0))
| ~ ssList(skaf68(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2552,plain,
( ~ sQ8_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f2542,f2549,f530]) ).
fof(f2553,definition,
! [X0,X1,X2] :
( sQ231_spl
<=> ( segmentP(app(skaf68(X0),X2),X1)
| ~ ssList(skaf68(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf68(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f2556,plain,
( ~ sQ8_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f2543,f2553,f530]) ).
fof(f2560,plain,
! [X0] :
( frontsegP(skaf71(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf71(X0)) ),
inference(paramodulation,[status(thm)],[f918,f1398]) ).
fof(f2562,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf71(X1)),X0),skaf71(X1))
| ~ ssList(app(skaf71(X1),X0))
| ~ ssList(skaf71(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f918,f481]) ).
fof(f2563,plain,
! [X0,X1,X2] :
( segmentP(app(skaf71(X0),X2),X1)
| ~ ssList(skaf71(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf71(X0),X1) ),
inference(paramodulation,[status(thm)],[f918,f402]) ).
fof(f2564,definition,
! [X0] :
( sQ232_spl
<=> ( frontsegP(skaf71(X0),nil)
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f2567,plain,
( ~ sQ8_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f2560,f2564,f530]) ).
fof(f2569,definition,
! [X0,X1] :
( sQ233_spl
<=> ( segmentP(app(app(nil,skaf71(X1)),X0),skaf71(X1))
| ~ ssList(app(skaf71(X1),X0))
| ~ ssList(skaf71(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f2572,plain,
( ~ sQ8_spl
| sQ233_spl ),
inference(split_clause,[status(thm)],[f2562,f2569,f530]) ).
fof(f2573,definition,
! [X0,X1,X2] :
( sQ234_spl
<=> ( segmentP(app(skaf71(X0),X2),X1)
| ~ ssList(skaf71(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf71(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f2576,plain,
( ~ sQ8_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f2563,f2573,f530]) ).
fof(f2580,plain,
! [X0] :
( frontsegP(skaf72(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf72(X0)) ),
inference(paramodulation,[status(thm)],[f919,f1398]) ).
fof(f2582,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf72(X1)),X0),skaf72(X1))
| ~ ssList(app(skaf72(X1),X0))
| ~ ssList(skaf72(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f919,f481]) ).
fof(f2583,plain,
! [X0,X1,X2] :
( segmentP(app(skaf72(X0),X2),X1)
| ~ ssList(skaf72(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf72(X0),X1) ),
inference(paramodulation,[status(thm)],[f919,f402]) ).
fof(f2584,definition,
! [X0] :
( sQ235_spl
<=> ( frontsegP(skaf72(X0),nil)
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f2587,plain,
( ~ sQ8_spl
| sQ235_spl ),
inference(split_clause,[status(thm)],[f2580,f2584,f530]) ).
fof(f2589,definition,
! [X0,X1] :
( sQ236_spl
<=> ( segmentP(app(app(nil,skaf72(X1)),X0),skaf72(X1))
| ~ ssList(app(skaf72(X1),X0))
| ~ ssList(skaf72(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f2592,plain,
( ~ sQ8_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f2582,f2589,f530]) ).
fof(f2593,definition,
! [X0,X1,X2] :
( sQ237_spl
<=> ( segmentP(app(skaf72(X0),X2),X1)
| ~ ssList(skaf72(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf72(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f2596,plain,
( ~ sQ8_spl
| sQ237_spl ),
inference(split_clause,[status(thm)],[f2583,f2593,f530]) ).
fof(f2600,plain,
! [X0] :
( frontsegP(skaf73(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf73(X0)) ),
inference(paramodulation,[status(thm)],[f920,f1398]) ).
fof(f2602,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf73(X1)),X0),skaf73(X1))
| ~ ssList(app(skaf73(X1),X0))
| ~ ssList(skaf73(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f920,f481]) ).
fof(f2603,plain,
! [X0,X1,X2] :
( segmentP(app(skaf73(X0),X2),X1)
| ~ ssList(skaf73(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf73(X0),X1) ),
inference(paramodulation,[status(thm)],[f920,f402]) ).
fof(f2604,definition,
! [X0] :
( sQ238_spl
<=> ( frontsegP(skaf73(X0),nil)
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f2607,plain,
( ~ sQ8_spl
| sQ238_spl ),
inference(split_clause,[status(thm)],[f2600,f2604,f530]) ).
fof(f2609,definition,
! [X0,X1] :
( sQ239_spl
<=> ( segmentP(app(app(nil,skaf73(X1)),X0),skaf73(X1))
| ~ ssList(app(skaf73(X1),X0))
| ~ ssList(skaf73(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f2612,plain,
( ~ sQ8_spl
| sQ239_spl ),
inference(split_clause,[status(thm)],[f2602,f2609,f530]) ).
fof(f2613,definition,
! [X0,X1,X2] :
( sQ240_spl
<=> ( segmentP(app(skaf73(X0),X2),X1)
| ~ ssList(skaf73(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf73(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f2616,plain,
( ~ sQ8_spl
| sQ240_spl ),
inference(split_clause,[status(thm)],[f2603,f2613,f530]) ).
fof(f2688,plain,
! [X0,X1,X2] :
( ~ sQ45_spl
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ frontsegP(X2,X1)
| ~ frontsegP(nil,X2)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ),
inference(resolution,[status(thm)],[f888,f376]) ).
fof(f2692,definition,
! [X0,X1,X2] :
( sQ241_spl
<=> ( ~ ssList(X2)
| ~ ssList(X1)
| ~ frontsegP(X2,X1)
| ~ frontsegP(nil,X2)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f2695,plain,
( ~ sQ45_spl
| ~ sQ8_spl
| sQ241_spl ),
inference(split_clause,[status(thm)],[f2688,f2692,f530,f883]) ).
fof(f3509,plain,
! [X0,X1,X2] :
( app(X0,X2) = X1
| ~ frontsegP(X1,app(X0,X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f283]) ).
fof(f3513,plain,
! [X0] :
( app(sk4,nil) = X0
| ~ frontsegP(X0,sk4)
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f770,f3509]) ).
fof(f3514,plain,
! [X0] :
( app(nil,sk4) = X0
| ~ frontsegP(X0,sk4)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f927,f3509]) ).
fof(f3515,plain,
! [X0] :
( app(nil,sk3) = X0
| ~ frontsegP(X0,sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f898,f3509]) ).
fof(f3516,plain,
! [X0] :
( app(nil,nil) = X0
| ~ frontsegP(X0,nil)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f745,f3509]) ).
fof(f3517,plain,
! [X0] :
( app(sk3,nil) = X0
| ~ frontsegP(X0,sk3)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f741,f3509]) ).
fof(f3521,definition,
! [X0] :
( sQ268_spl
<=> ( app(sk4,nil) = X0
| ~ frontsegP(X0,sk4)
| ~ ssList(X0)
| ~ frontsegP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f3524,plain,
( ~ sQ6_spl
| ~ sQ8_spl
| sQ268_spl ),
inference(split_clause,[status(thm)],[f3513,f3521,f530,f516]) ).
fof(f3525,definition,
! [X0] :
( sQ269_spl
<=> ( app(nil,sk4) = X0
| ~ frontsegP(X0,sk4)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f3528,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f3514,f3525,f516,f530]) ).
fof(f3529,definition,
! [X0] :
( sQ270_spl
<=> ( app(nil,sk3) = X0
| ~ frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f3532,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ270_spl ),
inference(split_clause,[status(thm)],[f3515,f3529,f541,f530]) ).
fof(f3533,definition,
! [X0] :
( sQ271_spl
<=> ( app(nil,nil) = X0
| ~ frontsegP(X0,nil)
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f3536,plain,
( ~ sQ8_spl
| sQ271_spl ),
inference(split_clause,[status(thm)],[f3516,f3533,f530]) ).
fof(f3537,definition,
! [X0] :
( sQ272_spl
<=> ( app(sk3,nil) = X0
| ~ frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f3540,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ272_spl ),
inference(split_clause,[status(thm)],[f3517,f3537,f530,f541]) ).
fof(f3665,definition,
( sQ277_spl
<=> ssList(skaf82(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f3667,plain,
( sQ277_spl
| ~ ssList(skaf82(sk4)) ),
inference(component_clause,[status(thm)],[f3665]) ).
fof(f3668,definition,
( sQ278_spl
<=> ssItem(skaf83(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f3670,plain,
( sQ278_spl
| ~ ssItem(skaf83(sk4)) ),
inference(component_clause,[status(thm)],[f3668]) ).
fof(f3693,plain,
( sQ278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3670,f209]) ).
fof(f3694,plain,
sQ278_spl,
inference(contradiction_clause,[status(thm)],[f3693]) ).
fof(f3695,plain,
( sQ277_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3667,f210]) ).
fof(f3696,plain,
sQ277_spl,
inference(contradiction_clause,[status(thm)],[f3695]) ).
fof(f3698,plain,
! [X0] :
( ~ sQ34_spl
| X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ frontsegP(X0,nil) ),
inference(resolution,[status(thm)],[f722,f824]) ).
fof(f3701,plain,
! [X0] :
( ~ sQ48_spl
| X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ frontsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f722,f949]) ).
fof(f3703,plain,
! [X0] :
( ~ sQ28_spl
| X0 = sk3
| ~ frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ frontsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f722,f792]) ).
fof(f3704,plain,
! [X0] :
( ~ sQ54_spl
| X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(nil)
| ~ frontsegP(X0,sk4) ),
inference(resolution,[status(thm)],[f722,f983]) ).
fof(f3706,plain,
! [X0] :
( ~ sQ39_spl
| X0 = sk4
| ~ frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(sk4)
| ~ frontsegP(X0,sk4) ),
inference(resolution,[status(thm)],[f722,f851]) ).
fof(f3708,plain,
! [X0,X1] :
( ~ sQ155_spl
| ~ ssList(X1)
| X0 = sk3
| ~ frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ ssList(app(sk3,X1))
| ~ ssList(sk3)
| ~ frontsegP(X0,app(sk3,X1)) ),
inference(resolution,[status(thm)],[f722,f2029]) ).
fof(f3710,plain,
! [X0,X1] :
( ~ sQ158_spl
| ~ ssList(X1)
| X0 = sk4
| ~ frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ ssList(app(sk4,X1))
| ~ ssList(sk4)
| ~ frontsegP(X0,app(sk4,X1)) ),
inference(resolution,[status(thm)],[f722,f2041]) ).
fof(f3713,plain,
! [X0,X1] :
( ~ ssList(X1)
| X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ frontsegP(X0,X1) ),
inference(resolution,[status(thm)],[f722,f257]) ).
fof(f3722,plain,
! [X0] :
( ~ sQ54_spl
| nil = sk4
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ frontsegP(X0,sk4)
| ~ frontsegP(nil,X0) ),
inference(resolution,[status(thm)],[f722,f983]) ).
fof(f3725,plain,
! [X0,X1] :
( ~ sQ155_spl
| ~ ssList(X1)
| sk3 = app(sk3,X1)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(app(sk3,X1))
| ~ frontsegP(X0,app(sk3,X1))
| ~ frontsegP(sk3,X0) ),
inference(resolution,[status(thm)],[f722,f2029]) ).
fof(f3727,plain,
! [X0,X1] :
( ~ sQ158_spl
| ~ ssList(X1)
| sk4 = app(sk4,X1)
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ ssList(app(sk4,X1))
| ~ frontsegP(X0,app(sk4,X1))
| ~ frontsegP(sk4,X0) ),
inference(resolution,[status(thm)],[f722,f2041]) ).
fof(f3733,definition,
! [X0] :
( sQ284_spl
<=> ( X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f3736,plain,
( ~ sQ34_spl
| ~ sQ8_spl
| sQ284_spl ),
inference(split_clause,[status(thm)],[f3698,f3733,f530,f815]) ).
fof(f3738,definition,
! [X0] :
( sQ285_spl
<=> ( X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f3741,plain,
( ~ sQ48_spl
| ~ sQ10_spl
| ~ sQ8_spl
| sQ285_spl ),
inference(split_clause,[status(thm)],[f3701,f3738,f530,f541,f940]) ).
fof(f3743,definition,
! [X0] :
( sQ286_spl
<=> ( X0 = sk3
| ~ frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition]) ).
fof(f3746,plain,
( ~ sQ28_spl
| ~ sQ10_spl
| sQ286_spl ),
inference(split_clause,[status(thm)],[f3703,f3743,f541,f783]) ).
fof(f3747,definition,
! [X0] :
( sQ287_spl
<=> ( X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition]) ).
fof(f3750,plain,
( ~ sQ54_spl
| ~ sQ6_spl
| ~ sQ8_spl
| sQ287_spl ),
inference(split_clause,[status(thm)],[f3704,f3747,f530,f516,f974]) ).
fof(f3752,definition,
! [X0] :
( sQ288_spl
<=> ( X0 = sk4
| ~ frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ frontsegP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition]) ).
fof(f3755,plain,
( ~ sQ39_spl
| ~ sQ6_spl
| sQ288_spl ),
inference(split_clause,[status(thm)],[f3706,f3752,f516,f842]) ).
fof(f3760,definition,
! [X0,X1] :
( sQ290_spl
<=> ( ~ ssList(X1)
| X0 = sk3
| ~ frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ ssList(app(sk3,X1))
| ~ frontsegP(X0,app(sk3,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f3763,plain,
( ~ sQ155_spl
| ~ sQ10_spl
| sQ290_spl ),
inference(split_clause,[status(thm)],[f3708,f3760,f541,f2028]) ).
fof(f3768,definition,
! [X0,X1] :
( sQ292_spl
<=> ( ~ ssList(X1)
| X0 = sk4
| ~ frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ ssList(app(sk4,X1))
| ~ frontsegP(X0,app(sk4,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f3771,plain,
( ~ sQ158_spl
| ~ sQ6_spl
| sQ292_spl ),
inference(split_clause,[status(thm)],[f3710,f3768,f516,f2040]) ).
fof(f3775,definition,
! [X0,X1] :
( sQ293_spl
<=> ( ~ ssList(X1)
| X0 = nil
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f3778,plain,
( ~ sQ8_spl
| sQ293_spl ),
inference(split_clause,[status(thm)],[f3713,f3775,f530]) ).
fof(f3791,plain,
( ~ sQ54_spl
| sQ2_spl
| ~ sQ8_spl
| ~ sQ6_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f3722,f873,f516,f530,f447,f974]) ).
fof(f3797,definition,
! [X0,X1] :
( sQ297_spl
<=> ( ~ ssList(X1)
| sk3 = app(sk3,X1)
| ~ ssList(X0)
| ~ ssList(app(sk3,X1))
| ~ frontsegP(X0,app(sk3,X1))
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f3800,plain,
( ~ sQ155_spl
| ~ sQ10_spl
| sQ297_spl ),
inference(split_clause,[status(thm)],[f3725,f3797,f541,f2028]) ).
fof(f3805,definition,
! [X0,X1] :
( sQ299_spl
<=> ( ~ ssList(X1)
| sk4 = app(sk4,X1)
| ~ ssList(X0)
| ~ ssList(app(sk4,X1))
| ~ frontsegP(X0,app(sk4,X1))
| ~ frontsegP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f3808,plain,
( ~ sQ158_spl
| ~ sQ6_spl
| sQ299_spl ),
inference(split_clause,[status(thm)],[f3727,f3805,f516,f2040]) ).
fof(f3846,plain,
! [X0,X1] :
( app(nil,skaf75(X1)) = X0
| ~ frontsegP(X0,skaf75(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf75(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f921,f3509]) ).
fof(f3847,plain,
! [X0] :
( frontsegP(skaf75(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf75(X0)) ),
inference(paramodulation,[status(thm)],[f921,f1398]) ).
fof(f3849,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf75(X1)),X0),skaf75(X1))
| ~ ssList(app(skaf75(X1),X0))
| ~ ssList(skaf75(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f921,f481]) ).
fof(f3850,plain,
! [X0,X1,X2] :
( segmentP(app(skaf75(X0),X2),X1)
| ~ ssList(skaf75(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf75(X0),X1) ),
inference(paramodulation,[status(thm)],[f921,f402]) ).
fof(f3851,definition,
! [X0,X1] :
( sQ300_spl
<=> ( app(nil,skaf75(X1)) = X0
| ~ frontsegP(X0,skaf75(X1))
| ~ ssList(X0)
| ~ ssList(skaf75(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition]) ).
fof(f3854,plain,
( ~ sQ8_spl
| sQ300_spl ),
inference(split_clause,[status(thm)],[f3846,f3851,f530]) ).
fof(f3855,definition,
! [X0] :
( sQ301_spl
<=> ( frontsegP(skaf75(X0),nil)
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).
fof(f3858,plain,
( ~ sQ8_spl
| sQ301_spl ),
inference(split_clause,[status(thm)],[f3847,f3855,f530]) ).
fof(f3860,definition,
! [X0,X1] :
( sQ302_spl
<=> ( segmentP(app(app(nil,skaf75(X1)),X0),skaf75(X1))
| ~ ssList(app(skaf75(X1),X0))
| ~ ssList(skaf75(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f3863,plain,
( ~ sQ8_spl
| sQ302_spl ),
inference(split_clause,[status(thm)],[f3849,f3860,f530]) ).
fof(f3864,definition,
! [X0,X1,X2] :
( sQ303_spl
<=> ( segmentP(app(skaf75(X0),X2),X1)
| ~ ssList(skaf75(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf75(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition]) ).
fof(f3867,plain,
( ~ sQ8_spl
| sQ303_spl ),
inference(split_clause,[status(thm)],[f3850,f3864,f530]) ).
fof(f3873,plain,
! [X0,X1] :
( app(nil,skaf76(X1)) = X0
| ~ frontsegP(X0,skaf76(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf76(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f922,f3509]) ).
fof(f3874,plain,
! [X0] :
( frontsegP(skaf76(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf76(X0)) ),
inference(paramodulation,[status(thm)],[f922,f1398]) ).
fof(f3876,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf76(X1)),X0),skaf76(X1))
| ~ ssList(app(skaf76(X1),X0))
| ~ ssList(skaf76(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f922,f481]) ).
fof(f3877,plain,
! [X0,X1,X2] :
( segmentP(app(skaf76(X0),X2),X1)
| ~ ssList(skaf76(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf76(X0),X1) ),
inference(paramodulation,[status(thm)],[f922,f402]) ).
fof(f3878,definition,
! [X0,X1] :
( sQ304_spl
<=> ( app(nil,skaf76(X1)) = X0
| ~ frontsegP(X0,skaf76(X1))
| ~ ssList(X0)
| ~ ssList(skaf76(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f3881,plain,
( ~ sQ8_spl
| sQ304_spl ),
inference(split_clause,[status(thm)],[f3873,f3878,f530]) ).
fof(f3882,definition,
! [X0] :
( sQ305_spl
<=> ( frontsegP(skaf76(X0),nil)
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f3885,plain,
( ~ sQ8_spl
| sQ305_spl ),
inference(split_clause,[status(thm)],[f3874,f3882,f530]) ).
fof(f3887,definition,
! [X0,X1] :
( sQ306_spl
<=> ( segmentP(app(app(nil,skaf76(X1)),X0),skaf76(X1))
| ~ ssList(app(skaf76(X1),X0))
| ~ ssList(skaf76(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f3890,plain,
( ~ sQ8_spl
| sQ306_spl ),
inference(split_clause,[status(thm)],[f3876,f3887,f530]) ).
fof(f3891,definition,
! [X0,X1,X2] :
( sQ307_spl
<=> ( segmentP(app(skaf76(X0),X2),X1)
| ~ ssList(skaf76(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf76(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f3894,plain,
( ~ sQ8_spl
| sQ307_spl ),
inference(split_clause,[status(thm)],[f3877,f3891,f530]) ).
fof(f3900,plain,
! [X0,X1] :
( app(nil,skaf77(X1)) = X0
| ~ frontsegP(X0,skaf77(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf77(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f923,f3509]) ).
fof(f3901,plain,
! [X0] :
( frontsegP(skaf77(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf77(X0)) ),
inference(paramodulation,[status(thm)],[f923,f1398]) ).
fof(f3903,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf77(X1)),X0),skaf77(X1))
| ~ ssList(app(skaf77(X1),X0))
| ~ ssList(skaf77(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f923,f481]) ).
fof(f3904,plain,
! [X0,X1,X2] :
( segmentP(app(skaf77(X0),X2),X1)
| ~ ssList(skaf77(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf77(X0),X1) ),
inference(paramodulation,[status(thm)],[f923,f402]) ).
fof(f3905,definition,
! [X0,X1] :
( sQ308_spl
<=> ( app(nil,skaf77(X1)) = X0
| ~ frontsegP(X0,skaf77(X1))
| ~ ssList(X0)
| ~ ssList(skaf77(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f3908,plain,
( ~ sQ8_spl
| sQ308_spl ),
inference(split_clause,[status(thm)],[f3900,f3905,f530]) ).
fof(f3909,definition,
! [X0] :
( sQ309_spl
<=> ( frontsegP(skaf77(X0),nil)
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f3912,plain,
( ~ sQ8_spl
| sQ309_spl ),
inference(split_clause,[status(thm)],[f3901,f3909,f530]) ).
fof(f3914,definition,
! [X0,X1] :
( sQ310_spl
<=> ( segmentP(app(app(nil,skaf77(X1)),X0),skaf77(X1))
| ~ ssList(app(skaf77(X1),X0))
| ~ ssList(skaf77(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f3917,plain,
( ~ sQ8_spl
| sQ310_spl ),
inference(split_clause,[status(thm)],[f3903,f3914,f530]) ).
fof(f3918,definition,
! [X0,X1,X2] :
( sQ311_spl
<=> ( segmentP(app(skaf77(X0),X2),X1)
| ~ ssList(skaf77(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf77(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f3921,plain,
( ~ sQ8_spl
| sQ311_spl ),
inference(split_clause,[status(thm)],[f3904,f3918,f530]) ).
fof(f3992,definition,
( sQ313_spl
<=> ssList(skaf82(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f3994,plain,
( sQ313_spl
| ~ ssList(skaf82(sk3)) ),
inference(component_clause,[status(thm)],[f3992]) ).
fof(f3995,definition,
( sQ314_spl
<=> ssItem(skaf83(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f3997,plain,
( sQ314_spl
| ~ ssItem(skaf83(sk3)) ),
inference(component_clause,[status(thm)],[f3995]) ).
fof(f4020,plain,
( sQ314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3997,f209]) ).
fof(f4021,plain,
sQ314_spl,
inference(contradiction_clause,[status(thm)],[f4020]) ).
fof(f4022,plain,
( sQ313_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3994,f210]) ).
fof(f4023,plain,
sQ313_spl,
inference(contradiction_clause,[status(thm)],[f4022]) ).
fof(f4024,plain,
! [X0,X1,X2,X3] :
( ~ segmentP(sk4,X1)
| ~ neq(X1,nil)
| ~ ssList(X1)
| ~ ssList(sk3)
| ~ ssList(app(app(X3,X0),X2))
| ~ segmentP(sk3,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(resolution,[status(thm)],[f737,f539]) ).
fof(f4027,plain,
! [X0,X1,X2,X3] :
( nil = X1
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(app(app(X3,X0),X2))
| ~ segmentP(nil,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(resolution,[status(thm)],[f737,f278]) ).
fof(f4031,definition,
! [X0,X1,X2,X3] :
( sQ320_spl
<=> ( ~ segmentP(sk4,X1)
| ~ neq(X1,nil)
| ~ ssList(X1)
| ~ ssList(app(app(X3,X0),X2))
| ~ segmentP(sk3,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f4034,plain,
( ~ sQ10_spl
| sQ320_spl ),
inference(split_clause,[status(thm)],[f4024,f4031,f541]) ).
fof(f4043,definition,
! [X0,X1,X2,X3] :
( sQ323_spl
<=> ( nil = X1
| ~ ssList(X1)
| ~ ssList(app(app(X3,X0),X2))
| ~ segmentP(nil,app(app(X3,X0),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f4046,plain,
( ~ sQ8_spl
| sQ323_spl ),
inference(split_clause,[status(thm)],[f4027,f4043,f530]) ).
fof(f4056,plain,
! [X0,X1] :
( app(app(sk4,nil),X1) = X0
| ~ ssList(app(sk4,X1))
| ~ segmentP(X0,app(app(sk4,nil),X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f770,f738]) ).
fof(f4057,plain,
! [X0,X1,X2] :
( app(app(nil,skaf77(X0)),X2) = X1
| ~ ssList(app(skaf77(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf77(X0)),X2))
| ~ ssList(skaf77(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf77(X0),X1) ),
inference(paramodulation,[status(thm)],[f923,f738]) ).
fof(f4058,plain,
! [X0,X1,X2] :
( app(app(nil,skaf76(X0)),X2) = X1
| ~ ssList(app(skaf76(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf76(X0)),X2))
| ~ ssList(skaf76(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf76(X0),X1) ),
inference(paramodulation,[status(thm)],[f922,f738]) ).
fof(f4059,plain,
! [X0,X1,X2] :
( app(app(nil,skaf75(X0)),X2) = X1
| ~ ssList(app(skaf75(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf75(X0)),X2))
| ~ ssList(skaf75(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf75(X0),X1) ),
inference(paramodulation,[status(thm)],[f921,f738]) ).
fof(f4060,plain,
! [X0,X1] :
( app(app(nil,sk4),X1) = X0
| ~ ssList(app(sk4,X1))
| ~ segmentP(X0,app(app(nil,sk4),X1))
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(sk4,X0) ),
inference(paramodulation,[status(thm)],[f927,f738]) ).
fof(f4061,plain,
! [X0,X1] :
( app(app(nil,sk3),X1) = X0
| ~ ssList(app(sk3,X1))
| ~ segmentP(X0,app(app(nil,sk3),X1))
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f898,f738]) ).
fof(f4062,plain,
! [X0,X1] :
( app(app(nil,nil),X1) = X0
| ~ ssList(app(nil,X1))
| ~ segmentP(X0,app(app(nil,nil),X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f745,f738]) ).
fof(f4063,plain,
! [X0,X1] :
( app(app(sk3,nil),X1) = X0
| ~ ssList(app(sk3,X1))
| ~ segmentP(X0,app(app(sk3,nil),X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f741,f738]) ).
fof(f4066,definition,
! [X0,X1] :
( sQ325_spl
<=> ( app(app(sk4,nil),X1) = X0
| ~ ssList(app(sk4,X1))
| ~ segmentP(X0,app(app(sk4,nil),X1))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f4069,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| sQ325_spl ),
inference(split_clause,[status(thm)],[f4056,f4066,f516,f530]) ).
fof(f4070,definition,
! [X0,X1,X2] :
( sQ326_spl
<=> ( app(app(nil,skaf77(X0)),X2) = X1
| ~ ssList(app(skaf77(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf77(X0)),X2))
| ~ ssList(skaf77(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf77(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition]) ).
fof(f4073,plain,
( ~ sQ8_spl
| sQ326_spl ),
inference(split_clause,[status(thm)],[f4057,f4070,f530]) ).
fof(f4074,definition,
! [X0,X1,X2] :
( sQ327_spl
<=> ( app(app(nil,skaf76(X0)),X2) = X1
| ~ ssList(app(skaf76(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf76(X0)),X2))
| ~ ssList(skaf76(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf76(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f4077,plain,
( ~ sQ8_spl
| sQ327_spl ),
inference(split_clause,[status(thm)],[f4058,f4074,f530]) ).
fof(f4078,definition,
! [X0,X1,X2] :
( sQ328_spl
<=> ( app(app(nil,skaf75(X0)),X2) = X1
| ~ ssList(app(skaf75(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf75(X0)),X2))
| ~ ssList(skaf75(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf75(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f4081,plain,
( ~ sQ8_spl
| sQ328_spl ),
inference(split_clause,[status(thm)],[f4059,f4078,f530]) ).
fof(f4082,definition,
! [X0,X1] :
( sQ329_spl
<=> ( app(app(nil,sk4),X1) = X0
| ~ ssList(app(sk4,X1))
| ~ segmentP(X0,app(app(nil,sk4),X1))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition]) ).
fof(f4085,plain,
( ~ sQ6_spl
| ~ sQ8_spl
| sQ329_spl ),
inference(split_clause,[status(thm)],[f4060,f4082,f530,f516]) ).
fof(f4086,definition,
! [X0,X1] :
( sQ330_spl
<=> ( app(app(nil,sk3),X1) = X0
| ~ ssList(app(sk3,X1))
| ~ segmentP(X0,app(app(nil,sk3),X1))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f4089,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ330_spl ),
inference(split_clause,[status(thm)],[f4061,f4086,f530,f541]) ).
fof(f4090,definition,
! [X0,X1] :
( sQ331_spl
<=> ( app(app(nil,nil),X1) = X0
| ~ ssList(app(nil,X1))
| ~ segmentP(X0,app(app(nil,nil),X1))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition]) ).
fof(f4093,plain,
( ~ sQ8_spl
| sQ331_spl ),
inference(split_clause,[status(thm)],[f4062,f4090,f530]) ).
fof(f4094,definition,
! [X0,X1] :
( sQ332_spl
<=> ( app(app(sk3,nil),X1) = X0
| ~ ssList(app(sk3,X1))
| ~ segmentP(X0,app(app(sk3,nil),X1))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f4097,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ332_spl ),
inference(split_clause,[status(thm)],[f4063,f4094,f541,f530]) ).
fof(f4243,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ rearsegP(nil,X0) ),
inference(resolution,[status(thm)],[f338,f255]) ).
fof(f4245,definition,
! [X0] :
( sQ349_spl
<=> ( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f4248,plain,
( ~ sQ8_spl
| sQ349_spl ),
inference(split_clause,[status(thm)],[f4243,f4245,f530]) ).
fof(f4315,plain,
! [X0,X1,X2] :
( app(app(nil,skaf80(X0)),X2) = X1
| ~ ssList(app(skaf80(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf80(X0)),X2))
| ~ ssList(skaf80(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf80(X0),X1) ),
inference(paramodulation,[status(thm)],[f924,f738]) ).
fof(f4316,plain,
! [X0,X1] :
( app(nil,skaf80(X1)) = X0
| ~ frontsegP(X0,skaf80(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf80(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f924,f3509]) ).
fof(f4317,plain,
! [X0] :
( frontsegP(skaf80(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf80(X0)) ),
inference(paramodulation,[status(thm)],[f924,f1398]) ).
fof(f4319,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf80(X1)),X0),skaf80(X1))
| ~ ssList(app(skaf80(X1),X0))
| ~ ssList(skaf80(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f924,f481]) ).
fof(f4320,plain,
! [X0,X1,X2] :
( segmentP(app(skaf80(X0),X2),X1)
| ~ ssList(skaf80(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf80(X0),X1) ),
inference(paramodulation,[status(thm)],[f924,f402]) ).
fof(f4325,definition,
! [X0,X1,X2] :
( sQ355_spl
<=> ( app(app(nil,skaf80(X0)),X2) = X1
| ~ ssList(app(skaf80(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf80(X0)),X2))
| ~ ssList(skaf80(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf80(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition]) ).
fof(f4328,plain,
( ~ sQ8_spl
| sQ355_spl ),
inference(split_clause,[status(thm)],[f4315,f4325,f530]) ).
fof(f4329,definition,
! [X0,X1] :
( sQ356_spl
<=> ( app(nil,skaf80(X1)) = X0
| ~ frontsegP(X0,skaf80(X1))
| ~ ssList(X0)
| ~ ssList(skaf80(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f4332,plain,
( ~ sQ8_spl
| sQ356_spl ),
inference(split_clause,[status(thm)],[f4316,f4329,f530]) ).
fof(f4333,definition,
! [X0] :
( sQ357_spl
<=> ( frontsegP(skaf80(X0),nil)
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition]) ).
fof(f4336,plain,
( ~ sQ8_spl
| sQ357_spl ),
inference(split_clause,[status(thm)],[f4317,f4333,f530]) ).
fof(f4338,definition,
! [X0,X1] :
( sQ358_spl
<=> ( segmentP(app(app(nil,skaf80(X1)),X0),skaf80(X1))
| ~ ssList(app(skaf80(X1),X0))
| ~ ssList(skaf80(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition]) ).
fof(f4341,plain,
( ~ sQ8_spl
| sQ358_spl ),
inference(split_clause,[status(thm)],[f4319,f4338,f530]) ).
fof(f4342,definition,
! [X0,X1,X2] :
( sQ359_spl
<=> ( segmentP(app(skaf80(X0),X2),X1)
| ~ ssList(skaf80(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf80(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f4345,plain,
( ~ sQ8_spl
| sQ359_spl ),
inference(split_clause,[status(thm)],[f4320,f4342,f530]) ).
fof(f4355,plain,
! [X0,X1,X2] :
( app(app(nil,skaf81(X0)),X2) = X1
| ~ ssList(app(skaf81(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf81(X0)),X2))
| ~ ssList(skaf81(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf81(X0),X1) ),
inference(paramodulation,[status(thm)],[f925,f738]) ).
fof(f4356,plain,
! [X0,X1] :
( app(nil,skaf81(X1)) = X0
| ~ frontsegP(X0,skaf81(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf81(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f925,f3509]) ).
fof(f4357,plain,
! [X0] :
( frontsegP(skaf81(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf81(X0)) ),
inference(paramodulation,[status(thm)],[f925,f1398]) ).
fof(f4359,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf81(X1)),X0),skaf81(X1))
| ~ ssList(app(skaf81(X1),X0))
| ~ ssList(skaf81(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f925,f481]) ).
fof(f4360,plain,
! [X0,X1,X2] :
( segmentP(app(skaf81(X0),X2),X1)
| ~ ssList(skaf81(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf81(X0),X1) ),
inference(paramodulation,[status(thm)],[f925,f402]) ).
fof(f4365,definition,
! [X0,X1,X2] :
( sQ361_spl
<=> ( app(app(nil,skaf81(X0)),X2) = X1
| ~ ssList(app(skaf81(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf81(X0)),X2))
| ~ ssList(skaf81(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf81(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f4368,plain,
( ~ sQ8_spl
| sQ361_spl ),
inference(split_clause,[status(thm)],[f4355,f4365,f530]) ).
fof(f4369,definition,
! [X0,X1] :
( sQ362_spl
<=> ( app(nil,skaf81(X1)) = X0
| ~ frontsegP(X0,skaf81(X1))
| ~ ssList(X0)
| ~ ssList(skaf81(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f4372,plain,
( ~ sQ8_spl
| sQ362_spl ),
inference(split_clause,[status(thm)],[f4356,f4369,f530]) ).
fof(f4373,definition,
! [X0] :
( sQ363_spl
<=> ( frontsegP(skaf81(X0),nil)
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f4376,plain,
( ~ sQ8_spl
| sQ363_spl ),
inference(split_clause,[status(thm)],[f4357,f4373,f530]) ).
fof(f4378,definition,
! [X0,X1] :
( sQ364_spl
<=> ( segmentP(app(app(nil,skaf81(X1)),X0),skaf81(X1))
| ~ ssList(app(skaf81(X1),X0))
| ~ ssList(skaf81(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ364_spl])],[split_symbol_definition]) ).
fof(f4381,plain,
( ~ sQ8_spl
| sQ364_spl ),
inference(split_clause,[status(thm)],[f4359,f4378,f530]) ).
fof(f4382,definition,
! [X0,X1,X2] :
( sQ365_spl
<=> ( segmentP(app(skaf81(X0),X2),X1)
| ~ ssList(skaf81(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf81(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition]) ).
fof(f4385,plain,
( ~ sQ8_spl
| sQ365_spl ),
inference(split_clause,[status(thm)],[f4360,f4382,f530]) ).
fof(f4395,plain,
! [X0,X1,X2] :
( app(app(nil,skaf82(X0)),X2) = X1
| ~ ssList(app(skaf82(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf82(X0)),X2))
| ~ ssList(skaf82(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf82(X0),X1) ),
inference(paramodulation,[status(thm)],[f926,f738]) ).
fof(f4396,plain,
! [X0,X1] :
( app(nil,skaf82(X1)) = X0
| ~ frontsegP(X0,skaf82(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf82(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f926,f3509]) ).
fof(f4397,plain,
! [X0] :
( frontsegP(skaf82(X0),nil)
| ~ ssList(nil)
| ~ ssList(skaf82(X0)) ),
inference(paramodulation,[status(thm)],[f926,f1398]) ).
fof(f4399,plain,
! [X0,X1] :
( segmentP(app(app(nil,skaf82(X1)),X0),skaf82(X1))
| ~ ssList(app(skaf82(X1),X0))
| ~ ssList(skaf82(X1))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f926,f481]) ).
fof(f4400,plain,
! [X0,X1,X2] :
( segmentP(app(skaf82(X0),X2),X1)
| ~ ssList(skaf82(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf82(X0),X1) ),
inference(paramodulation,[status(thm)],[f926,f402]) ).
fof(f4405,definition,
! [X0,X1,X2] :
( sQ367_spl
<=> ( app(app(nil,skaf82(X0)),X2) = X1
| ~ ssList(app(skaf82(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf82(X0)),X2))
| ~ ssList(skaf82(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf82(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ367_spl])],[split_symbol_definition]) ).
fof(f4408,plain,
( ~ sQ8_spl
| sQ367_spl ),
inference(split_clause,[status(thm)],[f4395,f4405,f530]) ).
fof(f4409,definition,
! [X0,X1] :
( sQ368_spl
<=> ( app(nil,skaf82(X1)) = X0
| ~ frontsegP(X0,skaf82(X1))
| ~ ssList(X0)
| ~ ssList(skaf82(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ368_spl])],[split_symbol_definition]) ).
fof(f4412,plain,
( ~ sQ8_spl
| sQ368_spl ),
inference(split_clause,[status(thm)],[f4396,f4409,f530]) ).
fof(f4413,definition,
! [X0] :
( sQ369_spl
<=> ( frontsegP(skaf82(X0),nil)
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f4416,plain,
( ~ sQ8_spl
| sQ369_spl ),
inference(split_clause,[status(thm)],[f4397,f4413,f530]) ).
fof(f4418,definition,
! [X0,X1] :
( sQ370_spl
<=> ( segmentP(app(app(nil,skaf82(X1)),X0),skaf82(X1))
| ~ ssList(app(skaf82(X1),X0))
| ~ ssList(skaf82(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition]) ).
fof(f4421,plain,
( ~ sQ8_spl
| sQ370_spl ),
inference(split_clause,[status(thm)],[f4399,f4418,f530]) ).
fof(f4422,definition,
! [X0,X1,X2] :
( sQ371_spl
<=> ( segmentP(app(skaf82(X0),X2),X1)
| ~ ssList(skaf82(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf82(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition]) ).
fof(f4425,plain,
( ~ sQ8_spl
| sQ371_spl ),
inference(split_clause,[status(thm)],[f4400,f4422,f530]) ).
fof(f4435,plain,
! [X0,X1,X2] :
( app(app(nil,skaf51(X0)),X2) = X1
| ~ ssList(app(skaf51(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf51(X0)),X2))
| ~ ssList(skaf51(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf51(X0),X1) ),
inference(paramodulation,[status(thm)],[f1206,f738]) ).
fof(f4436,plain,
! [X0,X1] :
( app(nil,skaf51(X1)) = X0
| ~ frontsegP(X0,skaf51(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf51(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f1206,f3509]) ).
fof(f4445,definition,
! [X0,X1,X2] :
( sQ373_spl
<=> ( app(app(nil,skaf51(X0)),X2) = X1
| ~ ssList(app(skaf51(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf51(X0)),X2))
| ~ ssList(skaf51(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf51(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition]) ).
fof(f4448,plain,
( ~ sQ8_spl
| sQ373_spl ),
inference(split_clause,[status(thm)],[f4435,f4445,f530]) ).
fof(f4449,definition,
! [X0,X1] :
( sQ374_spl
<=> ( app(nil,skaf51(X1)) = X0
| ~ frontsegP(X0,skaf51(X1))
| ~ ssList(X0)
| ~ ssList(skaf51(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition]) ).
fof(f4452,plain,
( ~ sQ8_spl
| sQ374_spl ),
inference(split_clause,[status(thm)],[f4436,f4449,f530]) ).
fof(f4463,plain,
! [X0,X1,X2] :
( app(app(nil,skaf52(X0)),X2) = X1
| ~ ssList(app(skaf52(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf52(X0)),X2))
| ~ ssList(skaf52(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf52(X0),X1) ),
inference(paramodulation,[status(thm)],[f1207,f738]) ).
fof(f4464,plain,
! [X0,X1] :
( app(nil,skaf52(X1)) = X0
| ~ frontsegP(X0,skaf52(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf52(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f1207,f3509]) ).
fof(f4473,definition,
! [X0,X1,X2] :
( sQ376_spl
<=> ( app(app(nil,skaf52(X0)),X2) = X1
| ~ ssList(app(skaf52(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf52(X0)),X2))
| ~ ssList(skaf52(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf52(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition]) ).
fof(f4476,plain,
( ~ sQ8_spl
| sQ376_spl ),
inference(split_clause,[status(thm)],[f4463,f4473,f530]) ).
fof(f4477,definition,
! [X0,X1] :
( sQ377_spl
<=> ( app(nil,skaf52(X1)) = X0
| ~ frontsegP(X0,skaf52(X1))
| ~ ssList(X0)
| ~ ssList(skaf52(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition]) ).
fof(f4480,plain,
( ~ sQ8_spl
| sQ377_spl ),
inference(split_clause,[status(thm)],[f4464,f4477,f530]) ).
fof(f4491,plain,
! [X0,X1,X2] :
( app(app(nil,skaf53(X0)),X2) = X1
| ~ ssList(app(skaf53(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf53(X0)),X2))
| ~ ssList(skaf53(X0))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ segmentP(skaf53(X0),X1) ),
inference(paramodulation,[status(thm)],[f1208,f738]) ).
fof(f4492,plain,
! [X0,X1] :
( app(nil,skaf53(X1)) = X0
| ~ frontsegP(X0,skaf53(X1))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(skaf53(X1))
| ~ frontsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f1208,f3509]) ).
fof(f4501,definition,
! [X0,X1,X2] :
( sQ379_spl
<=> ( app(app(nil,skaf53(X0)),X2) = X1
| ~ ssList(app(skaf53(X0),X2))
| ~ segmentP(X1,app(app(nil,skaf53(X0)),X2))
| ~ ssList(skaf53(X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(skaf53(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition]) ).
fof(f4504,plain,
( ~ sQ8_spl
| sQ379_spl ),
inference(split_clause,[status(thm)],[f4491,f4501,f530]) ).
fof(f4505,definition,
! [X0,X1] :
( sQ380_spl
<=> ( app(nil,skaf53(X1)) = X0
| ~ frontsegP(X0,skaf53(X1))
| ~ ssList(X0)
| ~ ssList(skaf53(X1))
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition]) ).
fof(f4508,plain,
( ~ sQ8_spl
| sQ380_spl ),
inference(split_clause,[status(thm)],[f4492,f4505,f530]) ).
fof(f4518,plain,
! [X0] :
( ~ ssList(X0)
| app(skaf46(X0,nil),nil) = X0
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f341,f255]) ).
fof(f4520,definition,
! [X0] :
( sQ381_spl
<=> ( ~ ssList(X0)
| app(skaf46(X0,nil),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f4523,plain,
( sQ381_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4518,f530,f4520]) ).
fof(f4526,plain,
( ~ sQ34_spl
| app(nil,skaf45(nil,nil)) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f342,f824]) ).
fof(f4528,plain,
( ~ sQ48_spl
| app(nil,skaf45(sk3,nil)) = sk3
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f342,f949]) ).
fof(f4529,plain,
( ~ sQ28_spl
| app(sk3,skaf45(sk3,sk3)) = sk3
| ~ ssList(sk3)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f342,f792]) ).
fof(f4530,plain,
( ~ sQ54_spl
| app(nil,skaf45(sk4,nil)) = sk4
| ~ ssList(sk4)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f342,f983]) ).
fof(f4531,plain,
( ~ sQ39_spl
| app(sk4,skaf45(sk4,sk4)) = sk4
| ~ ssList(sk4)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f342,f851]) ).
fof(f4532,plain,
( ~ sQ4_spl
| app(sk3,skaf45(sk4,sk3)) = sk4
| ~ ssList(sk4)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f342,f455]) ).
fof(f4533,plain,
! [X0] :
( ~ sQ155_spl
| ~ ssList(X0)
| app(sk3,skaf45(app(sk3,X0),sk3)) = app(sk3,X0)
| ~ ssList(app(sk3,X0))
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f342,f2029]) ).
fof(f4535,plain,
! [X0] :
( ~ sQ158_spl
| ~ ssList(X0)
| app(sk4,skaf45(app(sk4,X0),sk4)) = app(sk4,X0)
| ~ ssList(app(sk4,X0))
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f342,f2041]) ).
fof(f4537,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,skaf45(X0,nil)) = X0
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f342,f257]) ).
fof(f4540,definition,
( sQ382_spl
<=> app(nil,skaf45(nil,nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ382_spl])],[split_symbol_definition]) ).
fof(f4543,plain,
( ~ sQ34_spl
| sQ382_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4526,f530,f4540,f815]) ).
fof(f4545,definition,
( sQ383_spl
<=> app(nil,skaf45(sk3,nil)) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f4548,plain,
( ~ sQ48_spl
| sQ383_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4528,f530,f541,f4545,f940]) ).
fof(f4549,definition,
( sQ384_spl
<=> app(sk3,skaf45(sk3,sk3)) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f4552,plain,
( ~ sQ28_spl
| sQ384_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f4529,f541,f4549,f783]) ).
fof(f4553,definition,
( sQ385_spl
<=> app(nil,skaf45(sk4,nil)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition]) ).
fof(f4556,plain,
( ~ sQ54_spl
| sQ385_spl
| ~ sQ6_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4530,f530,f516,f4553,f974]) ).
fof(f4557,definition,
( sQ386_spl
<=> app(sk4,skaf45(sk4,sk4)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f4560,plain,
( ~ sQ39_spl
| sQ386_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4531,f516,f4557,f842]) ).
fof(f4561,definition,
( sQ387_spl
<=> app(sk3,skaf45(sk4,sk3)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f4562,plain,
( ~ sQ387_spl
| app(sk3,skaf45(sk4,sk3)) = sk4 ),
inference(component_clause,[status(thm)],[f4561]) ).
fof(f4564,plain,
( ~ sQ4_spl
| sQ387_spl
| ~ sQ6_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f4532,f541,f516,f4561,f454]) ).
fof(f4565,definition,
! [X0] :
( sQ388_spl
<=> ( ~ ssList(X0)
| app(sk3,skaf45(app(sk3,X0),sk3)) = app(sk3,X0)
| ~ ssList(app(sk3,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition]) ).
fof(f4568,plain,
( ~ sQ155_spl
| sQ388_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f4533,f541,f4565,f2028]) ).
fof(f4573,definition,
! [X0] :
( sQ390_spl
<=> ( ~ ssList(X0)
| app(sk4,skaf45(app(sk4,X0),sk4)) = app(sk4,X0)
| ~ ssList(app(sk4,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f4576,plain,
( ~ sQ158_spl
| sQ390_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4535,f516,f4573,f2040]) ).
fof(f4579,definition,
! [X0] :
( sQ391_spl
<=> ( ~ ssList(X0)
| app(nil,skaf45(X0,nil)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition]) ).
fof(f4582,plain,
( sQ391_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4537,f530,f4579]) ).
fof(f4588,plain,
( ~ sQ387_spl
| ~ sQ71_spl
| segmentP(sk4,sk3)
| ~ ssList(skaf45(sk4,sk3)) ),
inference(paramodulation,[status(thm)],[f4562,f1432]) ).
fof(f4596,definition,
( sQ392_spl
<=> ssList(skaf45(sk4,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f4598,plain,
( sQ392_spl
| ~ ssList(skaf45(sk4,sk3)) ),
inference(component_clause,[status(thm)],[f4596]) ).
fof(f4604,plain,
( ~ sQ387_spl
| ~ sQ71_spl
| sQ11_spl
| ~ sQ392_spl ),
inference(split_clause,[status(thm)],[f4588,f4596,f544,f1424,f4561]) ).
fof(f4627,plain,
( sQ392_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4598,f248]) ).
fof(f4628,plain,
sQ392_spl,
inference(contradiction_clause,[status(thm)],[f4627]) ).
fof(f4629,plain,
$false,
inference(sat_refutation,[status(thm)],[f453,f461,f462,f522,f526,f528,f536,f538,f547,f549,f558,f607,f623,f627,f667,f691,f695,f707,f714,f721,f732,f778,f782,f786,f790,f800,f802,f810,f814,f818,f822,f837,f841,f845,f849,f865,f876,f882,f886,f935,f939,f943,f947,f969,f973,f977,f981,f1037,f1069,f1154,f1172,f1179,f1190,f1265,f1269,f1273,f1281,f1299,f1427,f1431,f1441,f1456,f1539,f1543,f1547,f1551,f1555,f1566,f1570,f1574,f1578,f1582,f1593,f1597,f1601,f1605,f1609,f1618,f1622,f1630,f1634,f1635,f1644,f1665,f1700,f1704,f1708,f1712,f1722,f1726,f1730,f1734,f1744,f1748,f1752,f1756,f1766,f1770,f1774,f1778,f1788,f1792,f1796,f1800,f1810,f1814,f1818,f1822,f1832,f1836,f1840,f1844,f1854,f1858,f1862,f1866,f1876,f1880,f1884,f1888,f1898,f1902,f1906,f1910,f1920,f1924,f1928,f1932,f1942,f1946,f1950,f1954,f1962,f1966,f1975,f1979,f1989,f2023,f2027,f2031,f2035,f2039,f2043,f2051,f2057,f2096,f2100,f2104,f2108,f2118,f2122,f2126,f2130,f2140,f2144,f2148,f2152,f2162,f2166,f2170,f2174,f2184,f2188,f2192,f2196,f2206,f2210,f2214,f2218,f2228,f2233,f2237,f2248,f2253,f2257,f2268,f2273,f2277,f2288,f2293,f2297,f2308,f2313,f2317,f2328,f2333,f2337,f2347,f2351,f2352,f2359,f2363,f2364,f2371,f2375,f2383,f2387,f2388,f2447,f2452,f2456,f2467,f2472,f2476,f2487,f2492,f2496,f2507,f2512,f2516,f2527,f2532,f2536,f2547,f2552,f2556,f2567,f2572,f2576,f2587,f2592,f2596,f2607,f2612,f2616,f2695,f3524,f3528,f3532,f3536,f3540,f3694,f3696,f3736,f3741,f3746,f3750,f3755,f3763,f3771,f3778,f3791,f3800,f3808,f3854,f3858,f3863,f3867,f3881,f3885,f3890,f3894,f3908,f3912,f3917,f3921,f4021,f4023,f4034,f4046,f4069,f4073,f4077,f4081,f4085,f4089,f4093,f4097,f4248,f4328,f4332,f4336,f4341,f4345,f4368,f4372,f4376,f4381,f4385,f4408,f4412,f4416,f4421,f4425,f4448,f4452,f4476,f4480,f4504,f4508,f4523,f4543,f4548,f4552,f4556,f4560,f4564,f4568,f4576,f4582,f4604,f4628]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC085-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 07:55:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 1.27/0.71 % Refutation found
% 1.27/0.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.27/0.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.27/0.75 % Elapsed time: 0.372218 seconds
% 1.27/0.75 % CPU time: 2.482254 seconds
% 1.27/0.75 % Total memory used: 148.396 MB
% 1.27/0.75 % Net memory used: 145.150 MB
%------------------------------------------------------------------------------