%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC065-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:49 PM UTC 2026
% Result : Unsatisfiable 18.94s 2.85s
% Output : CNFRefutation 18.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 363
% Syntax : Number of formulae : 1197 ( 140 unt; 287 def)
% Number of atoms : 3606 ( 746 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 4432 (2023 ~;2122 |; 0 &)
% ( 287 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 297 ( 295 usr; 288 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 6 con; 0-2 aty)
% Number of variables : 1227 (1227 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [U] : ssList(skaf81(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] : ssList(skaf80(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [U] : ssList(skaf77(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [U] : ssList(skaf76(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [U] : ssList(skaf75(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] : ssList(skaf73(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [U] : ssList(skaf72(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U] : ssList(skaf71(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [U] : ssList(skaf68(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] : ssList(skaf67(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [U] : ssList(skaf66(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [U] : ssList(skaf63(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [U] : ssList(skaf62(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [U] : ssList(skaf61(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] : ssList(skaf58(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [U] : ssList(skaf57(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [U] : ssList(skaf56(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] : ssList(skaf53(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [U] : ssList(skaf52(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [U] : ssList(skaf51(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U,V] : ssList(skaf48(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [U,V] : ssList(skaf47(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U,V] : ssList(skaf46(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [U,V] : ssList(skaf43(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [U,V] : ssList(skaf42(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [U] :
( rearsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ segmentP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ rearsegP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ frontsegP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [U,V] :
( hd(app(V,U)) = hd(V)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ segmentP(V,U)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ rearsegP(V,U)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,axiom,
! [U,V] :
( app(skaf46(U,V),V) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [U,V] :
( app(V,skaf45(U,V)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [U,V] :
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,axiom,
! [U,V,W] :
( rearsegP(app(W,U),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [U,V,W] :
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,axiom,
! [U,V,W] :
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [U,V,W] :
( segmentP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,axiom,
! [U,V,W] :
( rearsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,axiom,
! [U,V,W] :
( frontsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [U,V,W] :
( memberP(U,W)
| memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
! [U,V] :
( app(app(skaf47(U,V),V),skaf48(V,U)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [U,V,W,X] :
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [U,V,W,X] :
( frontsegP(V,X)
| ~ ssItem(U)
| ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [U,V,W,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,axiom,
! [U,V,W,X,Y] :
( V = W
| ~ ssList(Y)
| ~ equalelemsP(Y)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(X)
| app(U,cons(V,cons(W,X))) != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssList(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
app(sk3,sk5) = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( nil != sk3
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
! [A] :
( ~ segmentP(sk1,A)
| ~ segmentP(sk2,A)
| ~ neq(A,nil)
| ~ ssList(A)
| nil = sk2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
( neq(sk2,nil)
| nil != sk1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f213,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f214,plain,
! [X0] : ssList(skaf81(X0)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f215,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f218,plain,
! [X0] : ssList(skaf77(X0)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f219,plain,
! [X0] : ssList(skaf76(X0)),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f220,plain,
! [X0] : ssList(skaf75(X0)),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f222,plain,
! [X0] : ssList(skaf73(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f223,plain,
! [X0] : ssList(skaf72(X0)),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f224,plain,
! [X0] : ssList(skaf71(X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f227,plain,
! [X0] : ssList(skaf68(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f228,plain,
! [X0] : ssList(skaf67(X0)),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f229,plain,
! [X0] : ssList(skaf66(X0)),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f232,plain,
! [X0] : ssList(skaf63(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f233,plain,
! [X0] : ssList(skaf62(X0)),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f234,plain,
! [X0] : ssList(skaf61(X0)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f237,plain,
! [X0] : ssList(skaf58(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f238,plain,
! [X0] : ssList(skaf57(X0)),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f239,plain,
! [X0] : ssList(skaf56(X0)),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f242,plain,
! [X0] : ssList(skaf53(X0)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f243,plain,
! [X0] : ssList(skaf52(X0)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f244,plain,
! [X0] : ssList(skaf51(X0)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f248,plain,
! [X0,X1] : ssList(skaf48(X0,X1)),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f249,plain,
! [X0,X1] : ssList(skaf47(X0,X1)),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f250,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f251,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f252,plain,
! [X0,X1] : ssList(skaf43(X0,X1)),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f253,plain,
! [X0,X1] : ssList(skaf42(X0,X1)),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f256,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f257,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f258,plain,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f260,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f271,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f274,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f275,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f281,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f283,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f285,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f286,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f303,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f321,plain,
! [U] :
( ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ neq(U,V)
| U != V ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f322,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ neq(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f327,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f328,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f329,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f330,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f334,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f340,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f341,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f342,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f344,plain,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f345,plain,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f346,plain,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f351,plain,
! [X0,X1,X2] :
( rearsegP(app(X2,X0),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f352,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(f369,plain,
! [X0,X1,X2] :
( app(app(X2,X1),X0) = app(X2,app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f370,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f371,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f372,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f373,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f374,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(f375,plain,
! [X0,X1,X2] :
( segmentP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
! [U,W] :
( rearsegP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V) ) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f377,plain,
! [X0,X1,X2] :
( rearsegP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X1,X2)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,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(f379,plain,
! [X0,X1,X2] :
( frontsegP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f385,plain,
! [U,W] :
( memberP(U,W)
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f158]) ).
fof(f386,plain,
! [X0,X1,X2] :
( memberP(X0,X2)
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ memberP(app(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f399,plain,
! [X0,X1] :
( app(app(skaf47(X0,X1),X1),skaf48(X1,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f405,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(f406,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(f407,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)],[f406]) ).
fof(f408,plain,
! [V,X] :
( frontsegP(V,X)
| ! [U] :
( ~ ssItem(U)
| ! [W] :
( ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ) ) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f409,plain,
! [X0,X1,X2,X3] :
( frontsegP(X1,X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ frontsegP(cons(X0,X1),cons(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f410,plain,
! [V,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(U,cons(V,W)) != X ) ) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f411,plain,
! [X0,X1,X2,X3] :
( memberP(X3,X1)
| ~ ssList(X3)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(X0,cons(X1,X2)) != X3 ),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f412,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(f413,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)],[f412]) ).
fof(f416,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(f419,plain,
! [V,W] :
( V = W
| ! [Y] :
( ~ ssList(Y)
| ~ equalelemsP(Y)
| ~ ssItem(V)
| ~ ssItem(W)
| ! [U] :
( ~ ssList(U)
| ! [X] :
( ~ ssList(X)
| app(U,cons(V,cons(W,X))) != Y ) ) ) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f420,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X2
| ~ ssList(X4)
| ~ equalelemsP(X4)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X3)
| app(X0,cons(X1,cons(X2,X3))) != X4 ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f431,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f432,plain,
ssList(sk2),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f435,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f436,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f437,plain,
ssList(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f438,plain,
app(sk3,sk5) = sk4,
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f442,plain,
( nil != sk3
| nil = sk4 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f444,plain,
! [X0] :
( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0)
| nil = sk2 ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f445,plain,
( neq(sk2,nil)
| nil != sk1 ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f454,definition,
( sQ2_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ2_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f457,definition,
( sQ3_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f459,plain,
( sQ3_spl
| nil != sk3 ),
inference(component_clause,[status(thm)],[f457]) ).
fof(f460,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f442,f454,f457]) ).
fof(f461,definition,
( sQ4_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ4_spl
| nil = sk2 ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f463,plain,
( sQ4_spl
| nil != sk2 ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
( sQ5_spl
<=> neq(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( ~ sQ5_spl
| neq(sk2,nil) ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f468,definition,
! [X0] :
( sQ6_spl
<=> ( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f469,plain,
! [X0] :
( ~ sQ6_spl
| ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,plain,
( sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f444,f461,f468]) ).
fof(f472,definition,
( sQ7_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ5_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f445,f472,f464]) ).
fof(f484,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f322]) ).
fof(f485,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f484]) ).
fof(f495,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)],[f407]) ).
fof(f496,plain,
! [X0,X1,X2] :
( memberP(app(X1,cons(X2,X0)),X2)
| ~ ssList(app(X1,cons(X2,X0)))
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f411]) ).
fof(f497,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)],[f416]) ).
fof(f498,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)],[f497]) ).
fof(f500,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ ssList(app(X1,cons(X3,cons(X2,X0))))
| ~ equalelemsP(app(X1,cons(X3,cons(X2,X0))))
| ~ ssItem(X3)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f420]) ).
fof(f511,plain,
app(sk1,sk5) = sk4,
inference(forward_demodulation,[status(thm)],[f436,f438]) ).
fof(f513,plain,
! [X0] : app(skaf81(X0),nil) = skaf81(X0),
inference(resolution,[status(thm)],[f274,f214]) ).
fof(f514,plain,
! [X0] : app(skaf82(X0),nil) = skaf82(X0),
inference(resolution,[status(thm)],[f274,f213]) ).
fof(f515,plain,
app(sk5,nil) = sk5,
inference(resolution,[status(thm)],[f274,f437]) ).
fof(f516,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f274,f208]) ).
fof(f517,plain,
app(sk1,nil) = sk1,
inference(resolution,[status(thm)],[f274,f431]) ).
fof(f518,plain,
! [X0] : app(nil,skaf81(X0)) = skaf81(X0),
inference(resolution,[status(thm)],[f275,f214]) ).
fof(f519,plain,
! [X0] : app(nil,skaf82(X0)) = skaf82(X0),
inference(resolution,[status(thm)],[f275,f213]) ).
fof(f520,plain,
app(nil,sk5) = sk5,
inference(resolution,[status(thm)],[f275,f437]) ).
fof(f522,plain,
app(nil,sk1) = sk1,
inference(resolution,[status(thm)],[f275,f431]) ).
fof(f523,plain,
! [X0] : app(nil,skaf80(X0)) = skaf80(X0),
inference(resolution,[status(thm)],[f215,f275]) ).
fof(f524,plain,
! [X0] : app(skaf80(X0),nil) = skaf80(X0),
inference(resolution,[status(thm)],[f215,f274]) ).
fof(f525,plain,
! [X0] : app(nil,skaf77(X0)) = skaf77(X0),
inference(resolution,[status(thm)],[f218,f275]) ).
fof(f526,plain,
! [X0] : app(skaf77(X0),nil) = skaf77(X0),
inference(resolution,[status(thm)],[f218,f274]) ).
fof(f527,plain,
! [X0] : app(nil,skaf76(X0)) = skaf76(X0),
inference(resolution,[status(thm)],[f219,f275]) ).
fof(f528,plain,
! [X0] : app(skaf76(X0),nil) = skaf76(X0),
inference(resolution,[status(thm)],[f219,f274]) ).
fof(f529,plain,
! [X0] : app(nil,skaf75(X0)) = skaf75(X0),
inference(resolution,[status(thm)],[f220,f275]) ).
fof(f530,plain,
! [X0] : app(skaf75(X0),nil) = skaf75(X0),
inference(resolution,[status(thm)],[f220,f274]) ).
fof(f531,plain,
! [X0] : app(nil,skaf73(X0)) = skaf73(X0),
inference(resolution,[status(thm)],[f222,f275]) ).
fof(f532,plain,
! [X0] : app(skaf73(X0),nil) = skaf73(X0),
inference(resolution,[status(thm)],[f222,f274]) ).
fof(f533,plain,
! [X0] : app(nil,skaf72(X0)) = skaf72(X0),
inference(resolution,[status(thm)],[f223,f275]) ).
fof(f534,plain,
! [X0] : app(skaf72(X0),nil) = skaf72(X0),
inference(resolution,[status(thm)],[f223,f274]) ).
fof(f535,plain,
! [X0] : app(nil,skaf71(X0)) = skaf71(X0),
inference(resolution,[status(thm)],[f224,f275]) ).
fof(f536,plain,
! [X0] : app(skaf71(X0),nil) = skaf71(X0),
inference(resolution,[status(thm)],[f224,f274]) ).
fof(f538,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f281,f256]) ).
fof(f540,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f543,definition,
( sQ9_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f538,f540,f543]) ).
fof(f548,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f208]) ).
fof(f549,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f548]) ).
fof(f550,plain,
! [X0,X1] :
( ssList(app(skaf71(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f224]) ).
fof(f551,plain,
! [X0,X1] :
( ssList(app(skaf72(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f223]) ).
fof(f552,plain,
! [X0,X1] :
( ssList(app(skaf73(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f222]) ).
fof(f553,plain,
! [X0,X1] :
( ssList(app(skaf75(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f220]) ).
fof(f554,plain,
! [X0,X1] :
( ssList(app(skaf76(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f219]) ).
fof(f555,plain,
! [X0,X1] :
( ssList(app(skaf77(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f218]) ).
fof(f556,plain,
! [X0,X1] :
( ssList(app(skaf80(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f215]) ).
fof(f557,plain,
! [X0,X1] :
( ssList(app(skaf81(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f214]) ).
fof(f558,plain,
! [X0,X1] :
( ssList(app(skaf82(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f213]) ).
fof(f559,plain,
! [X0] :
( ssList(app(sk5,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f437]) ).
fof(f561,plain,
! [X0] :
( ssList(app(sk1,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f431]) ).
fof(f562,plain,
! [X0,X1] :
( ssList(app(skaf68(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f227,f286]) ).
fof(f563,plain,
! [X0] : app(nil,skaf68(X0)) = skaf68(X0),
inference(resolution,[status(thm)],[f227,f275]) ).
fof(f564,plain,
! [X0] : app(skaf68(X0),nil) = skaf68(X0),
inference(resolution,[status(thm)],[f227,f274]) ).
fof(f565,plain,
! [X0,X1] :
( ssList(app(skaf67(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f228,f286]) ).
fof(f566,plain,
! [X0] : app(nil,skaf67(X0)) = skaf67(X0),
inference(resolution,[status(thm)],[f228,f275]) ).
fof(f567,plain,
! [X0] : app(skaf67(X0),nil) = skaf67(X0),
inference(resolution,[status(thm)],[f228,f274]) ).
fof(f568,plain,
! [X0,X1] :
( ssList(app(skaf66(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f229,f286]) ).
fof(f569,plain,
! [X0] : app(nil,skaf66(X0)) = skaf66(X0),
inference(resolution,[status(thm)],[f229,f275]) ).
fof(f570,plain,
! [X0] : app(skaf66(X0),nil) = skaf66(X0),
inference(resolution,[status(thm)],[f229,f274]) ).
fof(f571,plain,
! [X0,X1] :
( ssList(app(skaf63(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f232,f286]) ).
fof(f572,plain,
! [X0] : app(nil,skaf63(X0)) = skaf63(X0),
inference(resolution,[status(thm)],[f232,f275]) ).
fof(f573,plain,
! [X0] : app(skaf63(X0),nil) = skaf63(X0),
inference(resolution,[status(thm)],[f232,f274]) ).
fof(f574,plain,
! [X0,X1] :
( ssList(app(skaf62(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f233,f286]) ).
fof(f575,plain,
! [X0] : app(nil,skaf62(X0)) = skaf62(X0),
inference(resolution,[status(thm)],[f233,f275]) ).
fof(f576,plain,
! [X0] : app(skaf62(X0),nil) = skaf62(X0),
inference(resolution,[status(thm)],[f233,f274]) ).
fof(f578,plain,
! [X0] : app(nil,skaf61(X0)) = skaf61(X0),
inference(resolution,[status(thm)],[f234,f275]) ).
fof(f579,plain,
! [X0] : app(skaf61(X0),nil) = skaf61(X0),
inference(resolution,[status(thm)],[f234,f274]) ).
fof(f581,plain,
! [X0] : app(nil,skaf58(X0)) = skaf58(X0),
inference(resolution,[status(thm)],[f237,f275]) ).
fof(f582,plain,
! [X0] : app(skaf58(X0),nil) = skaf58(X0),
inference(resolution,[status(thm)],[f237,f274]) ).
fof(f583,plain,
! [X0,X1] :
( ssList(app(app(sk5,X0),X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f559,f286]) ).
fof(f586,plain,
( ssList(sk5)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f515,f559]) ).
fof(f587,definition,
( sQ10_spl
<=> ssList(sk5) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f590,plain,
( sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f586,f540,f587]) ).
fof(f591,plain,
! [X0,X1] :
( ssList(app(app(sk1,X0),X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f561,f286]) ).
fof(f594,plain,
( ssList(sk1)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f517,f561]) ).
fof(f596,definition,
( sQ11_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( sQ11_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f594,f540,f596]) ).
fof(f601,plain,
( sQ3_spl
| nil != sk1 ),
inference(forward_demodulation,[status(thm)],[f436,f459]) ).
fof(f606,plain,
app(nil,sk2) = sk2,
inference(resolution,[status(thm)],[f432,f275]) ).
fof(f607,plain,
app(sk2,nil) = sk2,
inference(resolution,[status(thm)],[f432,f274]) ).
fof(f608,plain,
app(sk1,sk5) = sk2,
inference(forward_demodulation,[status(thm)],[f435,f511]) ).
fof(f609,plain,
( ssList(sk2)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f608,f561]) ).
fof(f610,definition,
( sQ12_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( sQ12_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f609,f587,f610]) ).
fof(f629,plain,
! [X0,X1] :
( ssList(app(skaf57(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f238,f286]) ).
fof(f630,plain,
! [X0] : app(nil,skaf57(X0)) = skaf57(X0),
inference(resolution,[status(thm)],[f238,f275]) ).
fof(f631,plain,
! [X0] : app(skaf57(X0),nil) = skaf57(X0),
inference(resolution,[status(thm)],[f238,f274]) ).
fof(f632,plain,
! [X0,X1] :
( ssList(app(skaf56(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f239,f286]) ).
fof(f633,plain,
! [X0] : app(nil,skaf56(X0)) = skaf56(X0),
inference(resolution,[status(thm)],[f239,f275]) ).
fof(f634,plain,
! [X0] : app(skaf56(X0),nil) = skaf56(X0),
inference(resolution,[status(thm)],[f239,f274]) ).
fof(f637,plain,
! [X0,X1] :
( ssList(app(skaf53(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f242,f286]) ).
fof(f638,plain,
! [X0] : app(nil,skaf53(X0)) = skaf53(X0),
inference(resolution,[status(thm)],[f242,f275]) ).
fof(f639,plain,
! [X0] : app(skaf53(X0),nil) = skaf53(X0),
inference(resolution,[status(thm)],[f242,f274]) ).
fof(f640,plain,
! [X0,X1] :
( ssList(app(skaf52(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f243,f286]) ).
fof(f641,plain,
! [X0] : app(nil,skaf52(X0)) = skaf52(X0),
inference(resolution,[status(thm)],[f243,f275]) ).
fof(f642,plain,
! [X0] : app(skaf52(X0),nil) = skaf52(X0),
inference(resolution,[status(thm)],[f243,f274]) ).
fof(f643,plain,
! [X0,X1] :
( ssList(app(skaf51(X1),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f244,f286]) ).
fof(f644,plain,
! [X0] : app(nil,skaf51(X0)) = skaf51(X0),
inference(resolution,[status(thm)],[f244,f275]) ).
fof(f645,plain,
! [X0] : app(skaf51(X0),nil) = skaf51(X0),
inference(resolution,[status(thm)],[f244,f274]) ).
fof(f650,plain,
! [X0,X1] : app(nil,skaf48(X0,X1)) = skaf48(X0,X1),
inference(resolution,[status(thm)],[f248,f275]) ).
fof(f651,plain,
! [X0,X1] : app(skaf48(X0,X1),nil) = skaf48(X0,X1),
inference(resolution,[status(thm)],[f248,f274]) ).
fof(f653,plain,
! [X0,X1] : app(nil,skaf47(X0,X1)) = skaf47(X0,X1),
inference(resolution,[status(thm)],[f249,f275]) ).
fof(f654,plain,
! [X0,X1] : app(skaf47(X0,X1),nil) = skaf47(X0,X1),
inference(resolution,[status(thm)],[f249,f274]) ).
fof(f663,plain,
! [X0] :
( ssList(app(sk5,X0))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f515,f583]) ).
fof(f664,definition,
! [X0] :
( sQ13_spl
<=> ( ssList(app(sk5,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f667,plain,
( sQ13_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f663,f540,f664]) ).
fof(f671,plain,
! [X0] :
( ssList(app(sk2,X0))
| ~ ssList(X0)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f608,f591]) ).
fof(f672,plain,
! [X0] :
( ssList(app(sk1,X0))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f517,f591]) ).
fof(f673,definition,
! [X0] :
( sQ14_spl
<=> ( ssList(app(sk2,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f676,plain,
( sQ14_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f671,f587,f673]) ).
fof(f677,definition,
! [X0] :
( sQ15_spl
<=> ( ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f680,plain,
( sQ15_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f672,f540,f677]) ).
fof(f682,definition,
( sQ16_spl
<=> segmentP(sk2,sk2) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f683,plain,
( ~ sQ16_spl
| segmentP(sk2,sk2) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f684,plain,
( sQ16_spl
| ~ segmentP(sk2,sk2) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f694,plain,
( ~ sQ4_spl
| app(sk1,sk5) = nil ),
inference(backward_demodulation,[status(thm)],[f462,f608]) ).
fof(f726,plain,
! [X0,X1] : app(nil,skaf46(X0,X1)) = skaf46(X0,X1),
inference(resolution,[status(thm)],[f250,f275]) ).
fof(f727,plain,
! [X0,X1] : app(skaf46(X0,X1),nil) = skaf46(X0,X1),
inference(resolution,[status(thm)],[f250,f274]) ).
fof(f729,plain,
! [X0,X1] : app(nil,skaf45(X0,X1)) = skaf45(X0,X1),
inference(resolution,[status(thm)],[f251,f275]) ).
fof(f730,plain,
! [X0,X1] : app(skaf45(X0,X1),nil) = skaf45(X0,X1),
inference(resolution,[status(thm)],[f251,f274]) ).
fof(f732,plain,
! [X0,X1] : app(nil,skaf43(X0,X1)) = skaf43(X0,X1),
inference(resolution,[status(thm)],[f252,f275]) ).
fof(f733,plain,
! [X0,X1] : app(skaf43(X0,X1),nil) = skaf43(X0,X1),
inference(resolution,[status(thm)],[f252,f274]) ).
fof(f735,plain,
! [X0,X1] : app(nil,skaf42(X0,X1)) = skaf42(X0,X1),
inference(resolution,[status(thm)],[f253,f275]) ).
fof(f736,plain,
! [X0,X1] : app(skaf42(X0,X1),nil) = skaf42(X0,X1),
inference(resolution,[status(thm)],[f253,f274]) ).
fof(f737,plain,
( sQ16_spl
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f684,f257]) ).
fof(f738,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f432]) ).
fof(f739,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f738]) ).
fof(f743,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| neq(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f462,f465]) ).
fof(f745,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f743,f485]) ).
fof(f746,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f745,f540,f461,f464]) ).
fof(f747,plain,
! [X0] :
( ssList(app(sk2,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f432,f286]) ).
fof(f785,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| app(X0,sk5) != nil ),
inference(resolution,[status(thm)],[f328,f437]) ).
fof(f793,plain,
( ~ sQ6_spl
| ~ ssList(sk1)
| ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f469,f257]) ).
fof(f797,definition,
( sQ19_spl
<=> segmentP(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f798,plain,
( ~ sQ19_spl
| segmentP(sk2,nil) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f799,plain,
( sQ19_spl
| ~ segmentP(sk2,nil) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f801,definition,
( sQ20_spl
<=> neq(sk1,nil) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f803,plain,
( sQ20_spl
| ~ neq(sk1,nil) ),
inference(component_clause,[status(thm)],[f801]) ).
fof(f804,definition,
( sQ21_spl
<=> segmentP(sk2,sk1) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( ~ sQ6_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f793,f596,f801,f804,f468]) ).
fof(f816,plain,
( sQ20_spl
| sk1 = nil
| ~ ssList(sk1)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f803,f303]) ).
fof(f821,plain,
( sQ20_spl
| sQ7_spl
| ~ sQ11_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f816,f540,f596,f472,f801]) ).
fof(f822,plain,
( sQ19_spl
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f799,f256]) ).
fof(f823,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f432]) ).
fof(f824,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f823]) ).
fof(f825,plain,
( ~ sQ4_spl
| sk2 = nil ),
inference(forward_demodulation,[status(thm)],[f608,f694]) ).
fof(f827,plain,
( ~ sQ4_spl
| app(sk1,sk5) = nil ),
inference(backward_demodulation,[status(thm)],[f825,f608]) ).
fof(f836,plain,
! [X0,X1,X2] :
( nil = skaf42(X1,X2)
| ~ ssList(X0)
| app(X0,skaf42(X1,X2)) != nil ),
inference(resolution,[status(thm)],[f330,f253]) ).
fof(f837,plain,
! [X0,X1,X2] :
( nil = skaf43(X1,X2)
| ~ ssList(X0)
| app(X0,skaf43(X1,X2)) != nil ),
inference(resolution,[status(thm)],[f330,f252]) ).
fof(f838,plain,
! [X0,X1,X2] :
( nil = skaf45(X1,X2)
| ~ ssList(X0)
| app(X0,skaf45(X1,X2)) != nil ),
inference(resolution,[status(thm)],[f330,f251]) ).
fof(f839,plain,
! [X0,X1,X2] :
( nil = skaf46(X1,X2)
| ~ ssList(X0)
| app(X0,skaf46(X1,X2)) != nil ),
inference(resolution,[status(thm)],[f330,f250]) ).
fof(f840,plain,
! [X0,X1,X2] :
( nil = skaf47(X1,X2)
| ~ ssList(X0)
| app(X0,skaf47(X1,X2)) != nil ),
inference(resolution,[status(thm)],[f330,f249]) ).
fof(f841,plain,
! [X0,X1,X2] :
( nil = skaf48(X1,X2)
| ~ ssList(X0)
| app(X0,skaf48(X1,X2)) != nil ),
inference(resolution,[status(thm)],[f330,f248]) ).
fof(f853,plain,
! [X0,X1] :
( nil = skaf61(X1)
| ~ ssList(X0)
| app(X0,skaf61(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f234]) ).
fof(f854,plain,
! [X0,X1] :
( nil = skaf62(X1)
| ~ ssList(X0)
| app(X0,skaf62(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f233]) ).
fof(f855,plain,
! [X0,X1] :
( nil = skaf63(X1)
| ~ ssList(X0)
| app(X0,skaf63(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f232]) ).
fof(f856,plain,
! [X0,X1] :
( nil = skaf66(X1)
| ~ ssList(X0)
| app(X0,skaf66(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f229]) ).
fof(f857,plain,
! [X0,X1] :
( nil = skaf67(X1)
| ~ ssList(X0)
| app(X0,skaf67(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f228]) ).
fof(f858,plain,
! [X0,X1] :
( nil = skaf68(X1)
| ~ ssList(X0)
| app(X0,skaf68(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f227]) ).
fof(f859,plain,
! [X0,X1] :
( nil = skaf71(X1)
| ~ ssList(X0)
| app(X0,skaf71(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f224]) ).
fof(f860,plain,
! [X0,X1] :
( nil = skaf72(X1)
| ~ ssList(X0)
| app(X0,skaf72(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f223]) ).
fof(f861,plain,
! [X0,X1] :
( nil = skaf73(X1)
| ~ ssList(X0)
| app(X0,skaf73(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f222]) ).
fof(f862,plain,
! [X0,X1] :
( nil = skaf75(X1)
| ~ ssList(X0)
| app(X0,skaf75(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f220]) ).
fof(f863,plain,
! [X0,X1] :
( nil = skaf76(X1)
| ~ ssList(X0)
| app(X0,skaf76(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f219]) ).
fof(f864,plain,
! [X0,X1] :
( nil = skaf77(X1)
| ~ ssList(X0)
| app(X0,skaf77(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f218]) ).
fof(f865,plain,
! [X0,X1] :
( nil = skaf80(X1)
| ~ ssList(X0)
| app(X0,skaf80(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f215]) ).
fof(f866,plain,
! [X0,X1] :
( nil = skaf81(X1)
| ~ ssList(X0)
| app(X0,skaf81(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f214]) ).
fof(f867,plain,
! [X0,X1] :
( nil = skaf82(X1)
| ~ ssList(X0)
| app(X0,skaf82(X1)) != nil ),
inference(resolution,[status(thm)],[f330,f213]) ).
fof(f995,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(nil,X0) ),
inference(resolution,[status(thm)],[f340,f256]) ).
fof(f1005,definition,
! [X0] :
( sQ31_spl
<=> ( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1008,plain,
( ~ sQ8_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f995,f1005,f540]) ).
fof(f1138,plain,
! [X0] :
( app(app(sk5,sk5),X0) = app(sk5,app(sk5,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f369,f437]) ).
fof(f1139,plain,
! [X0,X1] :
( app(app(X1,sk5),X0) = app(X1,app(sk5,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f369,f437]) ).
fof(f1206,plain,
! [X0] :
( app(app(sk1,sk1),X0) = app(sk1,app(sk1,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f369,f431]) ).
fof(f1207,plain,
! [X0,X1] :
( app(app(X1,sk1),X0) = app(X1,app(sk1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f369,f431]) ).
fof(f1278,plain,
! [X0,X1] :
( X1 = sk1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,sk1) ),
inference(resolution,[status(thm)],[f371,f431]) ).
fof(f1294,plain,
! [X0] :
( X0 = sk5
| ~ ssList(X0)
| app(X0,sk5) != app(sk5,sk5) ),
inference(resolution,[status(thm)],[f373,f437]) ).
fof(f1401,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(X0,X1)
| ~ segmentP(nil,X0) ),
inference(resolution,[status(thm)],[f375,f281]) ).
fof(f1407,definition,
! [X0,X1] :
( sQ36_spl
<=> ( nil = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(X0,X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1410,plain,
( ~ sQ8_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1401,f1407,f540]) ).
fof(f1447,plain,
( nil = sk1
| app(sk1,sk5) != nil ),
inference(resolution,[status(thm)],[f785,f431]) ).
fof(f1457,definition,
( sQ39_spl
<=> app(sk1,sk5) = nil ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1459,plain,
( sQ39_spl
| app(sk1,sk5) != nil ),
inference(component_clause,[status(thm)],[f1457]) ).
fof(f1460,plain,
( sQ7_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1447,f1457,f472]) ).
fof(f1461,plain,
( sQ39_spl
| ~ sQ4_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f827,f1459]) ).
fof(f1462,plain,
( sQ39_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1461]) ).
fof(f1463,plain,
( sQ39_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1462]) ).
fof(f1477,plain,
! [X0] :
( X0 = sk2
| ~ ssList(X0)
| app(X0,sk2) != app(sk2,sk2) ),
inference(resolution,[status(thm)],[f432,f373]) ).
fof(f1482,plain,
! [X0] :
( app(app(sk2,sk2),X0) = app(sk2,app(sk2,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f432,f369]) ).
fof(f1485,plain,
! [X0,X1] :
( app(app(X1,sk2),X0) = app(X1,app(sk2,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f432,f369]) ).
fof(f1498,plain,
( ~ sQ2_spl
| sk2 = nil ),
inference(forward_demodulation,[status(thm)],[f455,f435]) ).
fof(f1535,plain,
( sQ4_spl
| ~ sQ2_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f1498,f463]) ).
fof(f1536,plain,
( sQ4_spl
| ~ sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1535]) ).
fof(f1537,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1536]) ).
fof(f1538,plain,
( sQ3_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f601,f472,f457]) ).
fof(f1569,definition,
( sQ42_spl
<=> sk2 = sk2 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1610,plain,
! [X0,X1] :
( ~ sQ16_spl
| segmentP(app(app(X1,sk2),X0),sk2)
| ~ ssList(sk2)
| ~ ssList(sk2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f405,f683]) ).
fof(f1611,plain,
! [X0,X1] :
( ~ sQ19_spl
| segmentP(app(app(X1,sk2),X0),nil)
| ~ ssList(sk2)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f405,f798]) ).
fof(f1612,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| segmentP(app(app(X1,X2),X0),nil)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f405,f256]) ).
fof(f1615,definition,
! [X0,X1] :
( sQ46_spl
<=> ( segmentP(app(app(X1,sk2),X0),sk2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1618,plain,
( ~ sQ16_spl
| ~ sQ12_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f1610,f1615,f610,f682]) ).
fof(f1619,definition,
! [X0,X1] :
( sQ47_spl
<=> ( segmentP(app(app(X1,sk2),X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1622,plain,
( ~ sQ19_spl
| ~ sQ12_spl
| ~ sQ8_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1611,f1619,f540,f610,f797]) ).
fof(f1623,definition,
! [X0,X1,X2] :
( sQ48_spl
<=> ( ~ ssList(X2)
| segmentP(app(app(X1,X2),X0),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1626,plain,
( ~ sQ8_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1612,f1623,f540]) ).
fof(f1649,plain,
! [X0,X1] :
( X0 = X1
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,sk2) != app(X1,sk2) ),
inference(resolution,[status(thm)],[f432,f373]) ).
fof(f1666,plain,
! [X0,X1] :
( X0 = X1
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,sk5) != app(X1,sk5) ),
inference(resolution,[status(thm)],[f437,f373]) ).
fof(f1669,plain,
! [X0,X1] :
( app(app(sk5,X1),X0) = app(sk5,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f437,f369]) ).
fof(f1676,plain,
! [X0] :
( ssList(app(sk5,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f437,f286]) ).
fof(f1687,definition,
( sQ49_spl
<=> segmentP(sk1,nil) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1688,plain,
( ~ sQ49_spl
| segmentP(sk1,nil) ),
inference(component_clause,[status(thm)],[f1687]) ).
fof(f1689,plain,
( sQ49_spl
| ~ segmentP(sk1,nil) ),
inference(component_clause,[status(thm)],[f1687]) ).
fof(f1711,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| segmentP(app(app(sk1,X1),X0),X1)
| ~ ssList(X1)
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f495,f591]) ).
fof(f1712,plain,
! [X0] :
( segmentP(app(app(sk2,nil),X0),nil)
| ~ ssList(app(sk2,X0))
| ~ ssList(nil)
| ~ ssList(sk2)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f607,f495]) ).
fof(f1713,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)],[f530,f495]) ).
fof(f1714,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)],[f528,f495]) ).
fof(f1715,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)],[f526,f495]) ).
fof(f1716,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)],[f524,f495]) ).
fof(f1717,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)],[f514,f495]) ).
fof(f1718,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)],[f513,f495]) ).
fof(f1719,plain,
! [X0] :
( segmentP(app(app(nil,sk2),X0),sk2)
| ~ ssList(app(sk2,X0))
| ~ ssList(sk2)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f606,f495]) ).
fof(f1720,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)],[f529,f495]) ).
fof(f1721,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)],[f527,f495]) ).
fof(f1722,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)],[f525,f495]) ).
fof(f1723,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)],[f523,f495]) ).
fof(f1724,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)],[f519,f495]) ).
fof(f1725,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)],[f518,f495]) ).
fof(f1726,plain,
! [X0] :
( segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f522,f495]) ).
fof(f1727,plain,
! [X0] :
( segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0))
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f516,f495]) ).
fof(f1728,plain,
! [X0] :
( segmentP(app(app(sk1,nil),X0),nil)
| ~ ssList(app(sk1,X0))
| ~ ssList(nil)
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f517,f495]) ).
fof(f1729,definition,
! [X0,X1] :
( sQ51_spl
<=> ( ~ ssList(X0)
| ~ ssList(X1)
| segmentP(app(app(sk1,X1),X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1732,plain,
( ~ sQ11_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1711,f1729,f596]) ).
fof(f1733,definition,
! [X0] :
( sQ52_spl
<=> ( segmentP(app(app(sk2,nil),X0),nil)
| ~ ssList(app(sk2,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1736,plain,
( ~ sQ8_spl
| ~ sQ12_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1712,f1733,f610,f540]) ).
fof(f1737,definition,
! [X0,X1] :
( sQ53_spl
<=> ( segmentP(app(app(skaf75(X1),nil),X0),nil)
| ~ ssList(app(skaf75(X1),X0))
| ~ ssList(skaf75(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1740,plain,
( ~ sQ8_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1713,f1737,f540]) ).
fof(f1741,definition,
! [X0,X1] :
( sQ54_spl
<=> ( segmentP(app(app(skaf76(X1),nil),X0),nil)
| ~ ssList(app(skaf76(X1),X0))
| ~ ssList(skaf76(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1744,plain,
( ~ sQ8_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1714,f1741,f540]) ).
fof(f1745,definition,
! [X0,X1] :
( sQ55_spl
<=> ( segmentP(app(app(skaf77(X1),nil),X0),nil)
| ~ ssList(app(skaf77(X1),X0))
| ~ ssList(skaf77(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1748,plain,
( ~ sQ8_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1715,f1745,f540]) ).
fof(f1749,definition,
! [X0,X1] :
( sQ56_spl
<=> ( segmentP(app(app(skaf80(X1),nil),X0),nil)
| ~ ssList(app(skaf80(X1),X0))
| ~ ssList(skaf80(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1752,plain,
( ~ sQ8_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1716,f1749,f540]) ).
fof(f1753,definition,
! [X0,X1] :
( sQ57_spl
<=> ( segmentP(app(app(skaf82(X1),nil),X0),nil)
| ~ ssList(app(skaf82(X1),X0))
| ~ ssList(skaf82(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1756,plain,
( ~ sQ8_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1717,f1753,f540]) ).
fof(f1757,definition,
! [X0,X1] :
( sQ58_spl
<=> ( segmentP(app(app(skaf81(X1),nil),X0),nil)
| ~ ssList(app(skaf81(X1),X0))
| ~ ssList(skaf81(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1760,plain,
( ~ sQ8_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1718,f1757,f540]) ).
fof(f1761,definition,
! [X0] :
( sQ59_spl
<=> ( segmentP(app(app(nil,sk2),X0),sk2)
| ~ ssList(app(sk2,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1764,plain,
( ~ sQ12_spl
| ~ sQ8_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1719,f1761,f540,f610]) ).
fof(f1765,definition,
! [X0,X1] :
( sQ60_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,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1768,plain,
( ~ sQ8_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1720,f1765,f540]) ).
fof(f1769,definition,
! [X0,X1] :
( sQ61_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,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1772,plain,
( ~ sQ8_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1721,f1769,f540]) ).
fof(f1773,definition,
! [X0,X1] :
( sQ62_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,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1776,plain,
( ~ sQ8_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1722,f1773,f540]) ).
fof(f1777,definition,
! [X0,X1] :
( sQ63_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,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1780,plain,
( ~ sQ8_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1723,f1777,f540]) ).
fof(f1781,definition,
! [X0,X1] :
( sQ64_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,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1784,plain,
( ~ sQ8_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1724,f1781,f540]) ).
fof(f1785,definition,
! [X0,X1] :
( sQ65_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,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1788,plain,
( ~ sQ8_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1725,f1785,f540]) ).
fof(f1789,definition,
! [X0] :
( sQ66_spl
<=> ( segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1790,plain,
! [X0] :
( ~ sQ66_spl
| segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1789]) ).
fof(f1792,plain,
( ~ sQ11_spl
| ~ sQ8_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1726,f1789,f540,f596]) ).
fof(f1793,definition,
! [X0] :
( sQ67_spl
<=> ( segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1796,plain,
( ~ sQ8_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1727,f1793,f540]) ).
fof(f1797,definition,
! [X0] :
( sQ68_spl
<=> ( segmentP(app(app(sk1,nil),X0),nil)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1800,plain,
( ~ sQ8_spl
| ~ sQ11_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1728,f1797,f596,f540]) ).
fof(f1804,plain,
! [X0] :
( ~ sQ66_spl
| segmentP(app(sk1,X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f522,f1790]) ).
fof(f1805,plain,
! [X0] :
( ~ sQ66_spl
| segmentP(app(sk1,X0),sk1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1804,f561]) ).
fof(f1866,plain,
! [X0] :
( segmentP(app(app(sk1,sk5),X0),sk5)
| ~ ssList(app(sk2,X0))
| ~ ssList(sk5)
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f608,f495]) ).
fof(f1869,definition,
! [X0] :
( sQ69_spl
<=> ( segmentP(app(app(sk1,sk5),X0),sk5)
| ~ ssList(app(sk2,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1872,plain,
( ~ sQ10_spl
| ~ sQ11_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1866,f1869,f596,f587]) ).
fof(f1875,plain,
! [X0] :
( segmentP(app(app(sk5,nil),X0),nil)
| ~ ssList(app(sk5,X0))
| ~ ssList(nil)
| ~ ssList(sk5)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f515,f495]) ).
fof(f1876,definition,
! [X0] :
( sQ70_spl
<=> ( segmentP(app(app(sk5,nil),X0),nil)
| ~ ssList(app(sk5,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1879,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1875,f1876,f587,f540]) ).
fof(f1881,plain,
! [X0] :
( segmentP(app(app(nil,sk5),X0),sk5)
| ~ ssList(app(sk5,X0))
| ~ ssList(sk5)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f520,f495]) ).
fof(f1882,definition,
! [X0] :
( sQ71_spl
<=> ( segmentP(app(app(nil,sk5),X0),sk5)
| ~ ssList(app(sk5,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1885,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1881,f1882,f540,f587]) ).
fof(f1887,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)],[f531,f495]) ).
fof(f1888,definition,
! [X0,X1] :
( sQ72_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,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1891,plain,
( ~ sQ8_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1887,f1888,f540]) ).
fof(f1894,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)],[f532,f495]) ).
fof(f1895,definition,
! [X0,X1] :
( sQ73_spl
<=> ( segmentP(app(app(skaf73(X1),nil),X0),nil)
| ~ ssList(app(skaf73(X1),X0))
| ~ ssList(skaf73(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1898,plain,
( ~ sQ8_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1894,f1895,f540]) ).
fof(f2033,plain,
! [X0] :
( ssList(app(sk2,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f432,f286]) ).
fof(f2057,plain,
( sQ49_spl
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f1689,f256]) ).
fof(f2059,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2057,f431]) ).
fof(f2060,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f2059]) ).
fof(f2064,definition,
( sQ82_spl
<=> segmentP(sk1,sk1) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f2093,plain,
! [X0,X1] :
( ~ sQ49_spl
| segmentP(app(app(X1,sk1),X0),nil)
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1688,f405]) ).
fof(f2095,definition,
! [X0,X1] :
( sQ85_spl
<=> ( segmentP(app(app(X1,sk1),X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2098,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| ~ sQ8_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f2093,f2095,f540,f596,f1687]) ).
fof(f2119,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)],[f533,f495]) ).
fof(f2120,definition,
! [X0,X1] :
( sQ86_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,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2123,plain,
( ~ sQ8_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f2119,f2120,f540]) ).
fof(f2126,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)],[f534,f495]) ).
fof(f2127,definition,
! [X0,X1] :
( sQ87_spl
<=> ( segmentP(app(app(skaf72(X1),nil),X0),nil)
| ~ ssList(app(skaf72(X1),X0))
| ~ ssList(skaf72(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2130,plain,
( ~ sQ8_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f2126,f2127,f540]) ).
fof(f2390,plain,
! [X0] :
( hd(skaf72(X0)) = hd(skaf72(X0))
| nil = skaf72(X0)
| ~ ssList(skaf72(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f534,f334]) ).
fof(f2391,plain,
! [X0] :
( hd(skaf73(X0)) = hd(skaf73(X0))
| nil = skaf73(X0)
| ~ ssList(skaf73(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f532,f334]) ).
fof(f2392,plain,
! [X0] :
( hd(skaf75(X0)) = hd(skaf75(X0))
| nil = skaf75(X0)
| ~ ssList(skaf75(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f530,f334]) ).
fof(f2393,plain,
! [X0] :
( hd(skaf76(X0)) = hd(skaf76(X0))
| nil = skaf76(X0)
| ~ ssList(skaf76(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f528,f334]) ).
fof(f2394,plain,
! [X0] :
( hd(skaf77(X0)) = hd(skaf77(X0))
| nil = skaf77(X0)
| ~ ssList(skaf77(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f526,f334]) ).
fof(f2395,plain,
! [X0] :
( hd(skaf80(X0)) = hd(skaf80(X0))
| nil = skaf80(X0)
| ~ ssList(skaf80(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f524,f334]) ).
fof(f2396,plain,
! [X0] :
( hd(skaf82(X0)) = hd(skaf82(X0))
| nil = skaf82(X0)
| ~ ssList(skaf82(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f514,f334]) ).
fof(f2397,plain,
! [X0] :
( hd(skaf81(X0)) = hd(skaf81(X0))
| nil = skaf81(X0)
| ~ ssList(skaf81(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f513,f334]) ).
fof(f2420,definition,
! [X0] :
( sQ99_spl
<=> ( hd(skaf72(X0)) = hd(skaf72(X0))
| nil = skaf72(X0)
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2423,plain,
( sQ99_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2390,f540,f2420]) ).
fof(f2424,definition,
! [X0] :
( sQ100_spl
<=> ( hd(skaf73(X0)) = hd(skaf73(X0))
| nil = skaf73(X0)
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2427,plain,
( sQ100_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2391,f540,f2424]) ).
fof(f2428,definition,
! [X0] :
( sQ101_spl
<=> ( hd(skaf75(X0)) = hd(skaf75(X0))
| nil = skaf75(X0)
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2431,plain,
( sQ101_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2392,f540,f2428]) ).
fof(f2432,definition,
! [X0] :
( sQ102_spl
<=> ( hd(skaf76(X0)) = hd(skaf76(X0))
| nil = skaf76(X0)
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2435,plain,
( sQ102_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2393,f540,f2432]) ).
fof(f2436,definition,
! [X0] :
( sQ103_spl
<=> ( hd(skaf77(X0)) = hd(skaf77(X0))
| nil = skaf77(X0)
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2439,plain,
( sQ103_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2394,f540,f2436]) ).
fof(f2440,definition,
! [X0] :
( sQ104_spl
<=> ( hd(skaf80(X0)) = hd(skaf80(X0))
| nil = skaf80(X0)
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f2443,plain,
( sQ104_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2395,f540,f2440]) ).
fof(f2444,definition,
! [X0] :
( sQ105_spl
<=> ( hd(skaf82(X0)) = hd(skaf82(X0))
| nil = skaf82(X0)
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f2447,plain,
( sQ105_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2396,f540,f2444]) ).
fof(f2448,definition,
! [X0] :
( sQ106_spl
<=> ( hd(skaf81(X0)) = hd(skaf81(X0))
| nil = skaf81(X0)
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2451,plain,
( sQ106_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2397,f540,f2448]) ).
fof(f2542,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)],[f535,f495]) ).
fof(f2547,definition,
! [X0,X1] :
( sQ123_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,[sQ123_spl])],[split_symbol_definition]) ).
fof(f2550,plain,
( ~ sQ8_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f2542,f2547,f540]) ).
fof(f2553,plain,
! [X0] :
( hd(skaf71(X0)) = hd(skaf71(X0))
| nil = skaf71(X0)
| ~ ssList(skaf71(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f536,f334]) ).
fof(f2554,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)],[f536,f495]) ).
fof(f2555,definition,
! [X0] :
( sQ124_spl
<=> ( hd(skaf71(X0)) = hd(skaf71(X0))
| nil = skaf71(X0)
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f2558,plain,
( sQ124_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2553,f540,f2555]) ).
fof(f2559,definition,
! [X0,X1] :
( sQ125_spl
<=> ( segmentP(app(app(skaf71(X1),nil),X0),nil)
| ~ ssList(app(skaf71(X1),X0))
| ~ ssList(skaf71(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2562,plain,
( ~ sQ8_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f2554,f2559,f540]) ).
fof(f2650,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)],[f563,f495]) ).
fof(f2655,definition,
! [X0,X1] :
( sQ128_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,[sQ128_spl])],[split_symbol_definition]) ).
fof(f2658,plain,
( ~ sQ8_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f2650,f2655,f540]) ).
fof(f2661,plain,
! [X0] :
( hd(skaf68(X0)) = hd(skaf68(X0))
| nil = skaf68(X0)
| ~ ssList(skaf68(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f564,f334]) ).
fof(f2662,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)],[f564,f495]) ).
fof(f2663,definition,
! [X0] :
( sQ129_spl
<=> ( hd(skaf68(X0)) = hd(skaf68(X0))
| nil = skaf68(X0)
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2666,plain,
( sQ129_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2661,f540,f2663]) ).
fof(f2667,definition,
! [X0,X1] :
( sQ130_spl
<=> ( segmentP(app(app(skaf68(X1),nil),X0),nil)
| ~ ssList(app(skaf68(X1),X0))
| ~ ssList(skaf68(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f2670,plain,
( ~ sQ8_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f2662,f2667,f540]) ).
fof(f2674,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)],[f566,f495]) ).
fof(f2679,definition,
! [X0,X1] :
( sQ132_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,[sQ132_spl])],[split_symbol_definition]) ).
fof(f2682,plain,
( ~ sQ8_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f2674,f2679,f540]) ).
fof(f2705,plain,
! [X0] :
( ssList(skaf71(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f536,f550]) ).
fof(f2706,definition,
! [X0] :
( sQ133_spl
<=> ssList(skaf71(X0)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f2709,plain,
( sQ133_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2705,f540,f2706]) ).
fof(f2730,plain,
! [X0] :
( ssList(skaf72(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f534,f551]) ).
fof(f2731,definition,
! [X0] :
( sQ134_spl
<=> ssList(skaf72(X0)) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f2734,plain,
( sQ134_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2730,f540,f2731]) ).
fof(f2735,plain,
! [X0] :
( hd(skaf67(X0)) = hd(skaf67(X0))
| nil = skaf67(X0)
| ~ ssList(skaf67(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f567,f334]) ).
fof(f2736,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)],[f567,f495]) ).
fof(f2737,definition,
! [X0] :
( sQ135_spl
<=> ( hd(skaf67(X0)) = hd(skaf67(X0))
| nil = skaf67(X0)
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f2740,plain,
( sQ135_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2735,f540,f2737]) ).
fof(f2741,definition,
! [X0,X1] :
( sQ136_spl
<=> ( segmentP(app(app(skaf67(X1),nil),X0),nil)
| ~ ssList(app(skaf67(X1),X0))
| ~ ssList(skaf67(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f2744,plain,
( ~ sQ8_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f2736,f2741,f540]) ).
fof(f2748,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)],[f569,f495]) ).
fof(f2753,definition,
! [X0,X1] :
( sQ138_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,[sQ138_spl])],[split_symbol_definition]) ).
fof(f2756,plain,
( ~ sQ8_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f2748,f2753,f540]) ).
fof(f2759,plain,
! [X0] :
( hd(skaf66(X0)) = hd(skaf66(X0))
| nil = skaf66(X0)
| ~ ssList(skaf66(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f570,f334]) ).
fof(f2760,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)],[f570,f495]) ).
fof(f2761,definition,
! [X0] :
( sQ139_spl
<=> ( hd(skaf66(X0)) = hd(skaf66(X0))
| nil = skaf66(X0)
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f2764,plain,
( sQ139_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2759,f540,f2761]) ).
fof(f2765,definition,
! [X0,X1] :
( sQ140_spl
<=> ( segmentP(app(app(skaf66(X1),nil),X0),nil)
| ~ ssList(app(skaf66(X1),X0))
| ~ ssList(skaf66(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f2768,plain,
( ~ sQ8_spl
| sQ140_spl ),
inference(split_clause,[status(thm)],[f2760,f2765,f540]) ).
fof(f2772,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)],[f572,f495]) ).
fof(f2777,definition,
! [X0,X1] :
( sQ142_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,[sQ142_spl])],[split_symbol_definition]) ).
fof(f2780,plain,
( ~ sQ8_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f2772,f2777,f540]) ).
fof(f2783,plain,
! [X0] :
( hd(skaf63(X0)) = hd(skaf63(X0))
| nil = skaf63(X0)
| ~ ssList(skaf63(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f573,f334]) ).
fof(f2784,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)],[f573,f495]) ).
fof(f2785,definition,
! [X0] :
( sQ143_spl
<=> ( hd(skaf63(X0)) = hd(skaf63(X0))
| nil = skaf63(X0)
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f2788,plain,
( sQ143_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2783,f540,f2785]) ).
fof(f2789,definition,
! [X0,X1] :
( sQ144_spl
<=> ( segmentP(app(app(skaf63(X1),nil),X0),nil)
| ~ ssList(app(skaf63(X1),X0))
| ~ ssList(skaf63(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f2792,plain,
( ~ sQ8_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f2784,f2789,f540]) ).
fof(f2796,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)],[f575,f495]) ).
fof(f2801,definition,
! [X0,X1] :
( sQ146_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,[sQ146_spl])],[split_symbol_definition]) ).
fof(f2804,plain,
( ~ sQ8_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f2796,f2801,f540]) ).
fof(f2807,plain,
! [X0] :
( hd(skaf62(X0)) = hd(skaf62(X0))
| nil = skaf62(X0)
| ~ ssList(skaf62(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f576,f334]) ).
fof(f2808,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)],[f576,f495]) ).
fof(f2809,definition,
! [X0] :
( sQ147_spl
<=> ( hd(skaf62(X0)) = hd(skaf62(X0))
| nil = skaf62(X0)
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f2812,plain,
( sQ147_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2807,f540,f2809]) ).
fof(f2813,definition,
! [X0,X1] :
( sQ148_spl
<=> ( segmentP(app(app(skaf62(X1),nil),X0),nil)
| ~ ssList(app(skaf62(X1),X0))
| ~ ssList(skaf62(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f2816,plain,
( ~ sQ8_spl
| sQ148_spl ),
inference(split_clause,[status(thm)],[f2808,f2813,f540]) ).
fof(f2820,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)],[f578,f495]) ).
fof(f2825,definition,
! [X0,X1] :
( sQ150_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,[sQ150_spl])],[split_symbol_definition]) ).
fof(f2828,plain,
( ~ sQ8_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f2820,f2825,f540]) ).
fof(f2831,plain,
! [X0] :
( hd(skaf61(X0)) = hd(skaf61(X0))
| nil = skaf61(X0)
| ~ ssList(skaf61(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f579,f334]) ).
fof(f2832,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)],[f579,f495]) ).
fof(f2833,definition,
! [X0] :
( sQ151_spl
<=> ( hd(skaf61(X0)) = hd(skaf61(X0))
| nil = skaf61(X0)
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2836,plain,
( sQ151_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2831,f540,f2833]) ).
fof(f2837,definition,
! [X0,X1] :
( sQ152_spl
<=> ( segmentP(app(app(skaf61(X1),nil),X0),nil)
| ~ ssList(app(skaf61(X1),X0))
| ~ ssList(skaf61(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f2840,plain,
( ~ sQ8_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f2832,f2837,f540]) ).
fof(f2842,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ rearsegP(nil,X0) ),
inference(resolution,[status(thm)],[f341,f258]) ).
fof(f2844,definition,
! [X0] :
( sQ153_spl
<=> ( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f2847,plain,
( ~ sQ8_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f2842,f2844,f540]) ).
fof(f2849,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(nil,X0) ),
inference(resolution,[status(thm)],[f342,f260]) ).
fof(f2851,definition,
! [X0] :
( sQ154_spl
<=> ( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f2854,plain,
( ~ sQ8_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f2849,f2851,f540]) ).
fof(f2883,plain,
( app(app(sk5,sk5),nil) = app(sk5,sk5)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f515,f1138]) ).
fof(f2884,definition,
( sQ155_spl
<=> app(app(sk5,sk5),nil) = app(sk5,sk5) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f2887,plain,
( sQ155_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2883,f540,f2884]) ).
fof(f2890,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)],[f581,f495]) ).
fof(f2895,definition,
! [X0,X1] :
( sQ157_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,[sQ157_spl])],[split_symbol_definition]) ).
fof(f2898,plain,
( ~ sQ8_spl
| sQ157_spl ),
inference(split_clause,[status(thm)],[f2890,f2895,f540]) ).
fof(f2901,plain,
! [X0] :
( hd(skaf58(X0)) = hd(skaf58(X0))
| nil = skaf58(X0)
| ~ ssList(skaf58(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f582,f334]) ).
fof(f2902,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)],[f582,f495]) ).
fof(f2903,definition,
! [X0] :
( sQ158_spl
<=> ( hd(skaf58(X0)) = hd(skaf58(X0))
| nil = skaf58(X0)
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f2906,plain,
( sQ158_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2901,f540,f2903]) ).
fof(f2907,definition,
! [X0,X1] :
( sQ159_spl
<=> ( segmentP(app(app(skaf58(X1),nil),X0),nil)
| ~ ssList(app(skaf58(X1),X0))
| ~ ssList(skaf58(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f2910,plain,
( ~ sQ8_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f2902,f2907,f540]) ).
fof(f2973,plain,
! [X0] :
( ssList(skaf73(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f532,f552]) ).
fof(f2974,definition,
! [X0] :
( sQ160_spl
<=> ssList(skaf73(X0)) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f2977,plain,
( sQ160_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2973,f540,f2974]) ).
fof(f2999,plain,
! [X0] :
( ssList(skaf75(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f530,f553]) ).
fof(f3000,definition,
! [X0] :
( sQ161_spl
<=> ssList(skaf75(X0)) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f3003,plain,
( sQ161_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2999,f540,f3000]) ).
fof(f3004,plain,
! [X0] :
( ~ ssList(X0)
| app(skaf46(X0,nil),nil) = X0
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f344,f258]) ).
fof(f3006,definition,
! [X0] :
( sQ162_spl
<=> ( ~ ssList(X0)
| app(skaf46(X0,nil),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f3009,plain,
( sQ162_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3004,f540,f3006]) ).
fof(f3012,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,skaf45(X0,nil)) = X0
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f345,f260]) ).
fof(f3014,definition,
! [X0] :
( sQ163_spl
<=> ( ~ ssList(X0)
| app(nil,skaf45(X0,nil)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f3017,plain,
( sQ163_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3012,f540,f3014]) ).
fof(f3122,plain,
! [X0] :
( app(sk5,X0) = app(nil,app(sk5,X0))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f520,f1139]) ).
fof(f3123,plain,
! [X0] :
( app(app(X0,sk5),nil) = app(X0,sk5)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f515,f1139]) ).
fof(f3124,definition,
! [X0] :
( sQ168_spl
<=> ( app(sk5,X0) = app(nil,app(sk5,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f3127,plain,
( ~ sQ8_spl
| sQ168_spl ),
inference(split_clause,[status(thm)],[f3122,f3124,f540]) ).
fof(f3128,definition,
! [X0] :
( sQ169_spl
<=> ( app(app(X0,sk5),nil) = app(X0,sk5)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f3131,plain,
( sQ169_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3123,f540,f3128]) ).
fof(f3155,plain,
! [X0] :
( ssList(skaf76(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f528,f554]) ).
fof(f3156,definition,
! [X0] :
( sQ170_spl
<=> ssList(skaf76(X0)) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f3159,plain,
( sQ170_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3155,f540,f3156]) ).
fof(f3183,plain,
! [X0] :
( ssList(skaf77(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f526,f555]) ).
fof(f3184,definition,
! [X0] :
( sQ171_spl
<=> ssList(skaf77(X0)) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f3187,plain,
( sQ171_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3183,f540,f3184]) ).
fof(f3202,plain,
! [X0,X1] :
( ~ ssList(X1)
| rearsegP(app(X0,X1),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f351,f258]) ).
fof(f3204,definition,
! [X0,X1] :
( sQ174_spl
<=> ( ~ ssList(X1)
| rearsegP(app(X0,X1),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f3207,plain,
( ~ sQ8_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f3202,f3204,f540]) ).
fof(f3210,plain,
( app(app(sk1,sk1),sk5) = app(sk1,sk2)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f608,f1206]) ).
fof(f3211,plain,
( app(app(sk1,sk1),nil) = app(sk1,sk1)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f517,f1206]) ).
fof(f3212,definition,
( sQ175_spl
<=> app(app(sk1,sk1),sk5) = app(sk1,sk2) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f3215,plain,
( sQ175_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f3210,f587,f3212]) ).
fof(f3216,definition,
( sQ176_spl
<=> app(app(sk1,sk1),nil) = app(sk1,sk1) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f3219,plain,
( sQ176_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3211,f540,f3216]) ).
fof(f3243,plain,
! [X0] :
( ssList(skaf80(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f524,f556]) ).
fof(f3244,definition,
! [X0] :
( sQ177_spl
<=> ssList(skaf80(X0)) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f3247,plain,
( sQ177_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3243,f540,f3244]) ).
fof(f3271,plain,
! [X0] :
( ssList(skaf81(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f513,f557]) ).
fof(f3272,definition,
! [X0] :
( sQ178_spl
<=> ssList(skaf81(X0)) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f3275,plain,
( sQ178_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3271,f540,f3272]) ).
fof(f3276,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f352,f260]) ).
fof(f3278,definition,
! [X0,X1] :
( sQ179_spl
<=> ( ~ ssList(X1)
| frontsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f3281,plain,
( ~ sQ8_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f3276,f3278,f540]) ).
fof(f3284,plain,
! [X0] :
( app(sk1,X0) = app(nil,app(sk1,X0))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f522,f1207]) ).
fof(f3285,plain,
! [X0] :
( app(app(X0,sk1),sk5) = app(X0,sk2)
| ~ ssList(X0)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f608,f1207]) ).
fof(f3286,plain,
! [X0] :
( app(app(X0,sk1),nil) = app(X0,sk1)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f517,f1207]) ).
fof(f3287,definition,
! [X0] :
( sQ180_spl
<=> ( app(sk1,X0) = app(nil,app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f3290,plain,
( ~ sQ8_spl
| sQ180_spl ),
inference(split_clause,[status(thm)],[f3284,f3287,f540]) ).
fof(f3291,definition,
! [X0] :
( sQ181_spl
<=> ( app(app(X0,sk1),sk5) = app(X0,sk2)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f3294,plain,
( sQ181_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f3285,f587,f3291]) ).
fof(f3295,definition,
! [X0] :
( sQ182_spl
<=> ( app(app(X0,sk1),nil) = app(X0,sk1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f3298,plain,
( sQ182_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3286,f540,f3295]) ).
fof(f3369,plain,
! [X0] :
( ssList(skaf82(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f514,f558]) ).
fof(f3370,definition,
! [X0] :
( sQ183_spl
<=> ssList(skaf82(X0)) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f3373,plain,
( sQ183_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3369,f540,f3370]) ).
fof(f3398,plain,
! [X0] :
( ssList(skaf68(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f564,f562]) ).
fof(f3399,definition,
! [X0] :
( sQ184_spl
<=> ssList(skaf68(X0)) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f3402,plain,
( sQ184_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3398,f540,f3399]) ).
fof(f3540,plain,
! [X0] :
( ssList(skaf67(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f567,f565]) ).
fof(f3541,definition,
! [X0] :
( sQ185_spl
<=> ssList(skaf67(X0)) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f3544,plain,
( sQ185_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3540,f540,f3541]) ).
fof(f3570,plain,
! [X0] :
( ssList(skaf66(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f570,f568]) ).
fof(f3571,definition,
! [X0] :
( sQ186_spl
<=> ssList(skaf66(X0)) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f3574,plain,
( sQ186_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3570,f540,f3571]) ).
fof(f3577,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)],[f630,f495]) ).
fof(f3582,definition,
! [X0,X1] :
( sQ188_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,[sQ188_spl])],[split_symbol_definition]) ).
fof(f3585,plain,
( ~ sQ8_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f3577,f3582,f540]) ).
fof(f3588,plain,
! [X0] :
( hd(skaf57(X0)) = hd(skaf57(X0))
| nil = skaf57(X0)
| ~ ssList(skaf57(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f631,f334]) ).
fof(f3589,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)],[f631,f495]) ).
fof(f3590,definition,
! [X0] :
( sQ189_spl
<=> ( hd(skaf57(X0)) = hd(skaf57(X0))
| nil = skaf57(X0)
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f3593,plain,
( sQ189_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3588,f540,f3590]) ).
fof(f3594,definition,
! [X0,X1] :
( sQ190_spl
<=> ( segmentP(app(app(skaf57(X1),nil),X0),nil)
| ~ ssList(app(skaf57(X1),X0))
| ~ ssList(skaf57(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f3597,plain,
( ~ sQ8_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f3589,f3594,f540]) ).
fof(f3601,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)],[f633,f495]) ).
fof(f3606,definition,
! [X0,X1] :
( sQ192_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,[sQ192_spl])],[split_symbol_definition]) ).
fof(f3609,plain,
( ~ sQ8_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f3601,f3606,f540]) ).
fof(f3612,plain,
! [X0] :
( hd(skaf56(X0)) = hd(skaf56(X0))
| nil = skaf56(X0)
| ~ ssList(skaf56(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f634,f334]) ).
fof(f3613,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)],[f634,f495]) ).
fof(f3614,definition,
! [X0] :
( sQ193_spl
<=> ( hd(skaf56(X0)) = hd(skaf56(X0))
| nil = skaf56(X0)
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f3617,plain,
( sQ193_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3612,f540,f3614]) ).
fof(f3618,definition,
! [X0,X1] :
( sQ194_spl
<=> ( segmentP(app(app(skaf56(X1),nil),X0),nil)
| ~ ssList(app(skaf56(X1),X0))
| ~ ssList(skaf56(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f3621,plain,
( ~ sQ8_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f3613,f3618,f540]) ).
fof(f3625,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)],[f638,f495]) ).
fof(f3630,definition,
! [X0,X1] :
( sQ196_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,[sQ196_spl])],[split_symbol_definition]) ).
fof(f3633,plain,
( ~ sQ8_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f3625,f3630,f540]) ).
fof(f3790,plain,
! [X0] :
( hd(skaf53(X0)) = hd(skaf53(X0))
| nil = skaf53(X0)
| ~ ssList(skaf53(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f639,f334]) ).
fof(f3791,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)],[f639,f495]) ).
fof(f3792,definition,
! [X0] :
( sQ197_spl
<=> ( hd(skaf53(X0)) = hd(skaf53(X0))
| nil = skaf53(X0)
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f3795,plain,
( sQ197_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3790,f540,f3792]) ).
fof(f3796,definition,
! [X0,X1] :
( sQ198_spl
<=> ( segmentP(app(app(skaf53(X1),nil),X0),nil)
| ~ ssList(app(skaf53(X1),X0))
| ~ ssList(skaf53(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f3799,plain,
( ~ sQ8_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f3791,f3796,f540]) ).
fof(f3803,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)],[f641,f495]) ).
fof(f3808,definition,
! [X0,X1] :
( sQ200_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,[sQ200_spl])],[split_symbol_definition]) ).
fof(f3811,plain,
( ~ sQ8_spl
| sQ200_spl ),
inference(split_clause,[status(thm)],[f3803,f3808,f540]) ).
fof(f3814,plain,
! [X0] :
( hd(skaf52(X0)) = hd(skaf52(X0))
| nil = skaf52(X0)
| ~ ssList(skaf52(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f334]) ).
fof(f3815,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)],[f642,f495]) ).
fof(f3816,definition,
! [X0] :
( sQ201_spl
<=> ( hd(skaf52(X0)) = hd(skaf52(X0))
| nil = skaf52(X0)
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f3819,plain,
( sQ201_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3814,f540,f3816]) ).
fof(f3820,definition,
! [X0,X1] :
( sQ202_spl
<=> ( segmentP(app(app(skaf52(X1),nil),X0),nil)
| ~ ssList(app(skaf52(X1),X0))
| ~ ssList(skaf52(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f3823,plain,
( ~ sQ8_spl
| sQ202_spl ),
inference(split_clause,[status(thm)],[f3815,f3820,f540]) ).
fof(f3827,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)],[f644,f495]) ).
fof(f3832,definition,
! [X0,X1] :
( sQ204_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,[sQ204_spl])],[split_symbol_definition]) ).
fof(f3835,plain,
( ~ sQ8_spl
| sQ204_spl ),
inference(split_clause,[status(thm)],[f3827,f3832,f540]) ).
fof(f3838,plain,
! [X0] :
( hd(skaf51(X0)) = hd(skaf51(X0))
| nil = skaf51(X0)
| ~ ssList(skaf51(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f645,f334]) ).
fof(f3839,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)],[f645,f495]) ).
fof(f3840,definition,
! [X0] :
( sQ205_spl
<=> ( hd(skaf51(X0)) = hd(skaf51(X0))
| nil = skaf51(X0)
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f3843,plain,
( sQ205_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3838,f540,f3840]) ).
fof(f3844,definition,
! [X0,X1] :
( sQ206_spl
<=> ( segmentP(app(app(skaf51(X1),nil),X0),nil)
| ~ ssList(app(skaf51(X1),X0))
| ~ ssList(skaf51(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f3847,plain,
( ~ sQ8_spl
| sQ206_spl ),
inference(split_clause,[status(thm)],[f3839,f3844,f540]) ).
fof(f3928,plain,
! [X0] :
( ssList(skaf63(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f573,f571]) ).
fof(f3929,definition,
! [X0] :
( sQ207_spl
<=> ssList(skaf63(X0)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f3932,plain,
( sQ207_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3928,f540,f3929]) ).
fof(f3962,plain,
! [X0] :
( ssList(skaf62(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f576,f574]) ).
fof(f3963,definition,
! [X0] :
( sQ208_spl
<=> ssList(skaf62(X0)) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f3966,plain,
( sQ208_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3962,f540,f3963]) ).
fof(f4030,plain,
! [X0,X1] :
( ~ ssList(X1)
| rearsegP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ rearsegP(X0,X1) ),
inference(resolution,[status(thm)],[f377,f258]) ).
fof(f4032,definition,
! [X0,X1] :
( sQ209_spl
<=> ( ~ ssList(X1)
| rearsegP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f4035,plain,
( ~ sQ8_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f4030,f4032,f540]) ).
fof(f4089,definition,
! [X0] :
( sQ210_spl
<=> ( ~ ssList(X0)
| app(X0,sk5) != app(X0,sk5) ) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f4090,plain,
! [X0] :
( ~ sQ210_spl
| ~ ssList(X0)
| app(X0,sk5) != app(X0,sk5) ),
inference(component_clause,[status(thm)],[f4089]) ).
fof(f4092,definition,
( sQ211_spl
<=> sk5 = sk5 ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f4114,plain,
! [X0] :
( ~ sQ210_spl
| ~ ssList(X0) ),
inference(trivial_equality_resolution,[status(thm)],[f4090]) ).
fof(f4115,plain,
( ~ sQ210_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f437,f4114]) ).
fof(f4146,plain,
~ sQ210_spl,
inference(contradiction_clause,[status(thm)],[f4115]) ).
fof(f4166,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ equalelemsP(app(sk5,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(sk5)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ),
inference(resolution,[status(thm)],[f1676,f500]) ).
fof(f4169,definition,
! [X0,X1,X2] :
( sQ217_spl
<=> ( X0 = X1
| ~ equalelemsP(app(sk5,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f4172,plain,
( ~ sQ10_spl
| sQ217_spl ),
inference(split_clause,[status(thm)],[f4166,f4169,f587]) ).
fof(f4174,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ equalelemsP(app(sk2,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(sk2)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ),
inference(resolution,[status(thm)],[f2033,f500]) ).
fof(f4177,definition,
! [X0,X1,X2] :
( sQ218_spl
<=> ( X0 = X1
| ~ equalelemsP(app(sk2,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f4180,plain,
( ~ sQ12_spl
| sQ218_spl ),
inference(split_clause,[status(thm)],[f4174,f4177,f610]) ).
fof(f4341,plain,
! [X0,X1] :
( ~ ssItem(X1)
| memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ memberP(app(X0,nil),X1) ),
inference(resolution,[status(thm)],[f386,f271]) ).
fof(f4342,definition,
! [X0,X1] :
( sQ219_spl
<=> ( ~ ssItem(X1)
| memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ memberP(app(X0,nil),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f4345,plain,
( ~ sQ8_spl
| sQ219_spl ),
inference(split_clause,[status(thm)],[f4341,f4342,f540]) ).
fof(f4393,plain,
! [X0] :
( sk1 = sk1
| ~ ssList(X0)
| app(X0,sk1) != app(X0,sk1) ),
inference(resolution,[status(thm)],[f1278,f431]) ).
fof(f4397,definition,
! [X0] :
( sQ220_spl
<=> ( ~ ssList(X0)
| app(X0,sk1) != app(X0,sk1) ) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f4398,plain,
! [X0] :
( ~ sQ220_spl
| ~ ssList(X0)
| app(X0,sk1) != app(X0,sk1) ),
inference(component_clause,[status(thm)],[f4397]) ).
fof(f4400,definition,
( sQ221_spl
<=> sk1 = sk1 ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f4403,plain,
( sQ221_spl
| sQ220_spl ),
inference(split_clause,[status(thm)],[f4393,f4397,f4400]) ).
fof(f4416,plain,
! [X0] :
( ~ sQ220_spl
| ~ ssList(X0) ),
inference(trivial_equality_resolution,[status(thm)],[f4398]) ).
fof(f4417,plain,
( ~ sQ220_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f218,f4416]) ).
fof(f4439,plain,
~ sQ220_spl,
inference(contradiction_clause,[status(thm)],[f4417]) ).
fof(f4650,plain,
! [X0] :
( ~ sQ19_spl
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk2)
| ~ ssList(nil)
| ~ segmentP(X0,sk2) ),
inference(resolution,[status(thm)],[f375,f798]) ).
fof(f4651,plain,
! [X0] :
( ~ sQ16_spl
| segmentP(X0,sk2)
| ~ ssList(X0)
| ~ ssList(sk2)
| ~ ssList(sk2)
| ~ segmentP(X0,sk2) ),
inference(resolution,[status(thm)],[f375,f683]) ).
fof(f4652,plain,
! [X0] :
( ~ sQ49_spl
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ segmentP(X0,sk1) ),
inference(resolution,[status(thm)],[f375,f1688]) ).
fof(f4653,plain,
! [X0,X1] :
( ~ ssList(X1)
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ segmentP(X0,X1) ),
inference(resolution,[status(thm)],[f375,f256]) ).
fof(f4662,definition,
! [X0] :
( sQ229_spl
<=> ( segmentP(X0,nil)
| ~ ssList(X0)
| ~ segmentP(X0,sk2) ) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f4665,plain,
( ~ sQ19_spl
| ~ sQ12_spl
| ~ sQ8_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f4650,f4662,f540,f610,f797]) ).
fof(f4666,definition,
! [X0] :
( sQ230_spl
<=> ( segmentP(X0,sk2)
| ~ ssList(X0)
| ~ segmentP(X0,sk2) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f4669,plain,
( ~ sQ16_spl
| ~ sQ12_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f4651,f4666,f610,f682]) ).
fof(f4670,definition,
! [X0] :
( sQ231_spl
<=> ( segmentP(X0,nil)
| ~ ssList(X0)
| ~ segmentP(X0,sk1) ) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f4673,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| ~ sQ8_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f4652,f4670,f540,f596,f1687]) ).
fof(f4674,definition,
! [X0,X1] :
( sQ232_spl
<=> ( ~ ssList(X1)
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f4677,plain,
( ~ sQ8_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f4653,f4674,f540]) ).
fof(f4746,plain,
( ~ sQ19_spl
| app(app(skaf47(sk2,nil),nil),skaf48(nil,sk2)) = sk2
| ~ ssList(sk2)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f399,f798]) ).
fof(f4747,plain,
( ~ sQ16_spl
| app(app(skaf47(sk2,sk2),sk2),skaf48(sk2,sk2)) = sk2
| ~ ssList(sk2)
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f399,f683]) ).
fof(f4748,plain,
( ~ sQ49_spl
| app(app(skaf47(sk1,nil),nil),skaf48(nil,sk1)) = sk1
| ~ ssList(sk1)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f399,f1688]) ).
fof(f4749,plain,
! [X0] :
( ~ ssList(X0)
| app(app(skaf47(X0,nil),nil),skaf48(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f399,f256]) ).
fof(f4752,definition,
( sQ234_spl
<=> app(app(skaf47(sk2,nil),nil),skaf48(nil,sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f4755,plain,
( ~ sQ19_spl
| sQ234_spl
| ~ sQ12_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4746,f540,f610,f4752,f797]) ).
fof(f4756,definition,
( sQ235_spl
<=> app(app(skaf47(sk2,sk2),sk2),skaf48(sk2,sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f4759,plain,
( ~ sQ16_spl
| sQ235_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f4747,f610,f4756,f682]) ).
fof(f4760,definition,
( sQ236_spl
<=> app(app(skaf47(sk1,nil),nil),skaf48(nil,sk1)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f4763,plain,
( ~ sQ49_spl
| sQ236_spl
| ~ sQ11_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4748,f540,f596,f4760,f1687]) ).
fof(f4764,definition,
! [X0] :
( sQ237_spl
<=> ( ~ ssList(X0)
| app(app(skaf47(X0,nil),nil),skaf48(nil,X0)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f4767,plain,
( sQ237_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4749,f540,f4764]) ).
fof(f4789,plain,
( sk5 = sk5
| ~ ssList(sk5) ),
inference(equality_resolution,[status(thm)],[f1294]) ).
fof(f4790,plain,
( sQ211_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f4789,f587,f4092]) ).
fof(f5380,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)],[f498,f413]) ).
fof(f5381,definition,
! [X0,X1] :
( sQ238_spl
<=> ( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f5382,plain,
! [X0,X1] :
( ~ sQ238_spl
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(component_clause,[status(thm)],[f5381]) ).
fof(f5384,definition,
! [X2] :
( sQ239_spl
<=> ( X2 = X2
| ~ ssItem(X2)
| ~ ssItem(X2)
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f5387,plain,
( sQ239_spl
| sQ238_spl ),
inference(split_clause,[status(thm)],[f5380,f5381,f5384]) ).
fof(f5388,plain,
! [X0,X1] :
( ~ sQ238_spl
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f5382]) ).
fof(f5883,plain,
! [X0] :
( ssList(app(nil,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f286,f208]) ).
fof(f6792,plain,
( sk2 = sk2
| ~ ssList(sk2) ),
inference(equality_resolution,[status(thm)],[f1477]) ).
fof(f6793,plain,
( sQ42_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f6792,f610,f1569]) ).
fof(f7197,plain,
! [X0,X1] : ssList(app(sk2,skaf42(X0,X1))),
inference(resolution,[status(thm)],[f747,f253]) ).
fof(f8986,plain,
! [X0,X1,X2] :
( ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(cons(X1,nil),cons(X2,X0))
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f285,f409]) ).
fof(f8989,definition,
! [X0,X1,X2] :
( sQ283_spl
<=> ( ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ frontsegP(cons(X1,nil),cons(X2,X0))
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f8992,plain,
( ~ sQ8_spl
| sQ283_spl ),
inference(split_clause,[status(thm)],[f8986,f8989,f540]) ).
fof(f8996,plain,
! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f283,f377]) ).
fof(f8999,definition,
! [X0,X1] :
( sQ284_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f9002,plain,
( ~ sQ8_spl
| sQ284_spl ),
inference(split_clause,[status(thm)],[f8996,f8999,f540]) ).
fof(f9082,plain,
( app(app(sk2,sk2),nil) = app(sk2,sk2)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f607,f1482]) ).
fof(f9083,definition,
( sQ285_spl
<=> app(app(sk2,sk2),nil) = app(sk2,sk2) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f9086,plain,
( sQ285_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f9082,f540,f9083]) ).
fof(f9211,plain,
! [X0] :
( ssList(skaf57(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f631,f629]) ).
fof(f9213,definition,
! [X0] :
( sQ286_spl
<=> ssList(skaf57(X0)) ),
introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition]) ).
fof(f9216,plain,
( sQ286_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f9211,f540,f9213]) ).
fof(f9450,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ equalelemsP(app(sk1,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(sk1)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ),
inference(resolution,[status(thm)],[f561,f500]) ).
fof(f9516,definition,
! [X0,X1,X2] :
( sQ293_spl
<=> ( X0 = X1
| ~ equalelemsP(app(sk1,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f9519,plain,
( ~ sQ11_spl
| sQ293_spl ),
inference(split_clause,[status(thm)],[f9450,f9516,f596]) ).
fof(f9786,plain,
! [X0] :
( ssList(skaf56(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f634,f632]) ).
fof(f9788,definition,
! [X0] :
( sQ294_spl
<=> ssList(skaf56(X0)) ),
introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition]) ).
fof(f9791,plain,
( sQ294_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f9786,f540,f9788]) ).
fof(f10076,plain,
! [X0] :
( ssList(skaf53(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f639,f637]) ).
fof(f10078,definition,
! [X0] :
( sQ295_spl
<=> ssList(skaf53(X0)) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f10081,plain,
( sQ295_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f10076,f540,f10078]) ).
fof(f10083,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ frontsegP(X0,X1) ),
inference(resolution,[status(thm)],[f379,f260]) ).
fof(f10087,definition,
! [X0,X1] :
( sQ296_spl
<=> ( ~ ssList(X1)
| frontsegP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f10090,plain,
( ~ sQ8_spl
| sQ296_spl ),
inference(split_clause,[status(thm)],[f10083,f10087,f540]) ).
fof(f10162,plain,
! [X0] :
( ssList(skaf52(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f640]) ).
fof(f10164,definition,
! [X0] :
( sQ297_spl
<=> ssList(skaf52(X0)) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f10167,plain,
( sQ297_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f10162,f540,f10164]) ).
fof(f10237,plain,
! [X0] :
( ssList(skaf51(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f645,f643]) ).
fof(f10239,definition,
! [X0] :
( sQ298_spl
<=> ssList(skaf51(X0)) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f10242,plain,
( sQ298_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f10237,f540,f10239]) ).
fof(f10243,plain,
! [X0] :
( app(sk2,X0) = app(nil,app(sk2,X0))
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f606,f1485]) ).
fof(f10244,plain,
! [X0] :
( app(app(X0,sk2),nil) = app(X0,sk2)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f607,f1485]) ).
fof(f10245,definition,
! [X0] :
( sQ299_spl
<=> ( app(sk2,X0) = app(nil,app(sk2,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f10248,plain,
( ~ sQ8_spl
| sQ299_spl ),
inference(split_clause,[status(thm)],[f10243,f10245,f540]) ).
fof(f10249,definition,
! [X0] :
( sQ300_spl
<=> ( app(app(X0,sk2),nil) = app(X0,sk2)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition]) ).
fof(f10252,plain,
( sQ300_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f10244,f540,f10249]) ).
fof(f13421,plain,
! [X0] :
( ~ sQ238_spl
| ~ ssList(X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f5388,f260]) ).
fof(f13423,definition,
! [X0] :
( sQ406_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f13424,plain,
! [X0] :
( ~ sQ406_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f13423]) ).
fof(f13426,plain,
( ~ sQ238_spl
| sQ406_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f13421,f540,f13423,f5381]) ).
fof(f13428,plain,
! [X0] :
( ~ sQ406_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f13424]) ).
fof(f13429,plain,
( ~ sQ406_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f7197,f13428]) ).
fof(f13496,plain,
~ sQ406_spl,
inference(contradiction_clause,[status(thm)],[f13429]) ).
fof(f14450,plain,
! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f285,f379]) ).
fof(f14453,definition,
! [X0,X1] :
( sQ409_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(nil,X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition]) ).
fof(f14456,plain,
( ~ sQ8_spl
| sQ409_spl ),
inference(split_clause,[status(thm)],[f14450,f14453,f540]) ).
fof(f15100,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ equalelemsP(app(nil,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ),
inference(resolution,[status(thm)],[f5883,f500]) ).
fof(f15101,plain,
! [X0,X1] :
( memberP(app(nil,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f5883,f496]) ).
fof(f15156,definition,
! [X0,X1,X2] :
( sQ410_spl
<=> ( X0 = X1
| ~ equalelemsP(app(nil,cons(X0,cons(X1,X2))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f15159,plain,
( ~ sQ8_spl
| sQ410_spl ),
inference(split_clause,[status(thm)],[f15100,f15156,f540]) ).
fof(f15160,definition,
! [X0,X1] :
( sQ411_spl
<=> ( memberP(app(nil,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition]) ).
fof(f15163,plain,
( ~ sQ8_spl
| sQ411_spl ),
inference(split_clause,[status(thm)],[f15101,f15160,f540]) ).
fof(f17869,plain,
! [X0,X1] :
( hd(skaf42(X0,X1)) = hd(skaf42(X0,X1))
| nil = skaf42(X0,X1)
| ~ ssList(skaf42(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f736,f334]) ).
fof(f17870,plain,
! [X0,X1] :
( hd(skaf43(X0,X1)) = hd(skaf43(X0,X1))
| nil = skaf43(X0,X1)
| ~ ssList(skaf43(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f733,f334]) ).
fof(f17871,plain,
! [X0,X1] :
( hd(skaf45(X0,X1)) = hd(skaf45(X0,X1))
| nil = skaf45(X0,X1)
| ~ ssList(skaf45(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f730,f334]) ).
fof(f17872,plain,
! [X0,X1] :
( hd(skaf46(X0,X1)) = hd(skaf46(X0,X1))
| nil = skaf46(X0,X1)
| ~ ssList(skaf46(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f727,f334]) ).
fof(f17873,plain,
! [X0,X1] :
( hd(skaf47(X0,X1)) = hd(skaf47(X0,X1))
| nil = skaf47(X0,X1)
| ~ ssList(skaf47(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f654,f334]) ).
fof(f17874,plain,
! [X0,X1] :
( hd(skaf48(X0,X1)) = hd(skaf48(X0,X1))
| nil = skaf48(X0,X1)
| ~ ssList(skaf48(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f651,f334]) ).
fof(f17931,definition,
! [X0,X1] :
( sQ415_spl
<=> ( hd(skaf42(X0,X1)) = hd(skaf42(X0,X1))
| nil = skaf42(X0,X1)
| ~ ssList(skaf42(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition]) ).
fof(f17934,plain,
( sQ415_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f17869,f540,f17931]) ).
fof(f17935,definition,
! [X0,X1] :
( sQ416_spl
<=> ( hd(skaf43(X0,X1)) = hd(skaf43(X0,X1))
| nil = skaf43(X0,X1)
| ~ ssList(skaf43(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition]) ).
fof(f17938,plain,
( sQ416_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f17870,f540,f17935]) ).
fof(f17939,definition,
! [X0,X1] :
( sQ417_spl
<=> ( hd(skaf45(X0,X1)) = hd(skaf45(X0,X1))
| nil = skaf45(X0,X1)
| ~ ssList(skaf45(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f17942,plain,
( sQ417_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f17871,f540,f17939]) ).
fof(f17943,definition,
! [X0,X1] :
( sQ418_spl
<=> ( hd(skaf46(X0,X1)) = hd(skaf46(X0,X1))
| nil = skaf46(X0,X1)
| ~ ssList(skaf46(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f17946,plain,
( sQ418_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f17872,f540,f17943]) ).
fof(f17947,definition,
! [X0,X1] :
( sQ419_spl
<=> ( hd(skaf47(X0,X1)) = hd(skaf47(X0,X1))
| nil = skaf47(X0,X1)
| ~ ssList(skaf47(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition]) ).
fof(f17950,plain,
( sQ419_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f17873,f540,f17947]) ).
fof(f17951,definition,
! [X0,X1] :
( sQ420_spl
<=> ( hd(skaf48(X0,X1)) = hd(skaf48(X0,X1))
| nil = skaf48(X0,X1)
| ~ ssList(skaf48(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f17954,plain,
( sQ420_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f17874,f540,f17951]) ).
fof(f18194,plain,
! [X0,X1] :
( tl(skaf42(X0,X1)) = app(tl(skaf42(X0,X1)),nil)
| nil = skaf42(X0,X1)
| ~ ssList(skaf42(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f736,f346]) ).
fof(f18195,plain,
! [X0,X1] :
( tl(skaf43(X0,X1)) = app(tl(skaf43(X0,X1)),nil)
| nil = skaf43(X0,X1)
| ~ ssList(skaf43(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f733,f346]) ).
fof(f18196,plain,
! [X0,X1] :
( tl(skaf45(X0,X1)) = app(tl(skaf45(X0,X1)),nil)
| nil = skaf45(X0,X1)
| ~ ssList(skaf45(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f730,f346]) ).
fof(f18197,plain,
! [X0,X1] :
( tl(skaf46(X0,X1)) = app(tl(skaf46(X0,X1)),nil)
| nil = skaf46(X0,X1)
| ~ ssList(skaf46(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f727,f346]) ).
fof(f18198,plain,
! [X0,X1] :
( tl(skaf47(X0,X1)) = app(tl(skaf47(X0,X1)),nil)
| nil = skaf47(X0,X1)
| ~ ssList(skaf47(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f654,f346]) ).
fof(f18199,plain,
! [X0,X1] :
( tl(skaf48(X0,X1)) = app(tl(skaf48(X0,X1)),nil)
| nil = skaf48(X0,X1)
| ~ ssList(skaf48(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f651,f346]) ).
fof(f18202,plain,
! [X0] :
( tl(skaf51(X0)) = app(tl(skaf51(X0)),nil)
| nil = skaf51(X0)
| ~ ssList(skaf51(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f645,f346]) ).
fof(f18203,plain,
! [X0] :
( tl(skaf52(X0)) = app(tl(skaf52(X0)),nil)
| nil = skaf52(X0)
| ~ ssList(skaf52(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f346]) ).
fof(f18204,plain,
! [X0] :
( tl(skaf53(X0)) = app(tl(skaf53(X0)),nil)
| nil = skaf53(X0)
| ~ ssList(skaf53(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f639,f346]) ).
fof(f18205,plain,
! [X0] :
( tl(skaf56(X0)) = app(tl(skaf56(X0)),nil)
| nil = skaf56(X0)
| ~ ssList(skaf56(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f634,f346]) ).
fof(f18206,plain,
! [X0] :
( tl(skaf57(X0)) = app(tl(skaf57(X0)),nil)
| nil = skaf57(X0)
| ~ ssList(skaf57(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f631,f346]) ).
fof(f18207,plain,
! [X0] :
( tl(skaf58(X0)) = app(tl(skaf58(X0)),nil)
| nil = skaf58(X0)
| ~ ssList(skaf58(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f582,f346]) ).
fof(f18208,plain,
! [X0] :
( tl(skaf61(X0)) = app(tl(skaf61(X0)),nil)
| nil = skaf61(X0)
| ~ ssList(skaf61(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f579,f346]) ).
fof(f18209,plain,
! [X0] :
( tl(skaf62(X0)) = app(tl(skaf62(X0)),nil)
| nil = skaf62(X0)
| ~ ssList(skaf62(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f576,f346]) ).
fof(f18210,plain,
! [X0] :
( tl(skaf63(X0)) = app(tl(skaf63(X0)),nil)
| nil = skaf63(X0)
| ~ ssList(skaf63(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f573,f346]) ).
fof(f18211,plain,
! [X0] :
( tl(skaf66(X0)) = app(tl(skaf66(X0)),nil)
| nil = skaf66(X0)
| ~ ssList(skaf66(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f570,f346]) ).
fof(f18212,plain,
! [X0] :
( tl(skaf67(X0)) = app(tl(skaf67(X0)),nil)
| nil = skaf67(X0)
| ~ ssList(skaf67(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f567,f346]) ).
fof(f18213,plain,
! [X0] :
( tl(skaf68(X0)) = app(tl(skaf68(X0)),nil)
| nil = skaf68(X0)
| ~ ssList(skaf68(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f564,f346]) ).
fof(f18214,plain,
! [X0] :
( tl(skaf71(X0)) = app(tl(skaf71(X0)),nil)
| nil = skaf71(X0)
| ~ ssList(skaf71(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f536,f346]) ).
fof(f18215,plain,
! [X0] :
( tl(skaf72(X0)) = app(tl(skaf72(X0)),nil)
| nil = skaf72(X0)
| ~ ssList(skaf72(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f534,f346]) ).
fof(f18216,plain,
! [X0] :
( tl(skaf73(X0)) = app(tl(skaf73(X0)),nil)
| nil = skaf73(X0)
| ~ ssList(skaf73(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f532,f346]) ).
fof(f18217,plain,
! [X0] :
( tl(skaf75(X0)) = app(tl(skaf75(X0)),nil)
| nil = skaf75(X0)
| ~ ssList(skaf75(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f530,f346]) ).
fof(f18218,plain,
! [X0] :
( tl(skaf76(X0)) = app(tl(skaf76(X0)),nil)
| nil = skaf76(X0)
| ~ ssList(skaf76(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f528,f346]) ).
fof(f18219,plain,
! [X0] :
( tl(skaf77(X0)) = app(tl(skaf77(X0)),nil)
| nil = skaf77(X0)
| ~ ssList(skaf77(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f526,f346]) ).
fof(f18220,plain,
! [X0] :
( tl(skaf80(X0)) = app(tl(skaf80(X0)),nil)
| nil = skaf80(X0)
| ~ ssList(skaf80(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f524,f346]) ).
fof(f18221,plain,
! [X0] :
( tl(skaf82(X0)) = app(tl(skaf82(X0)),nil)
| nil = skaf82(X0)
| ~ ssList(skaf82(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f514,f346]) ).
fof(f18222,plain,
! [X0] :
( tl(skaf81(X0)) = app(tl(skaf81(X0)),nil)
| nil = skaf81(X0)
| ~ ssList(skaf81(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f513,f346]) ).
fof(f18256,definition,
! [X0,X1] :
( sQ427_spl
<=> ( tl(skaf42(X0,X1)) = app(tl(skaf42(X0,X1)),nil)
| nil = skaf42(X0,X1)
| ~ ssList(skaf42(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f18259,plain,
( sQ427_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18194,f540,f18256]) ).
fof(f18260,definition,
! [X0,X1] :
( sQ428_spl
<=> ( tl(skaf43(X0,X1)) = app(tl(skaf43(X0,X1)),nil)
| nil = skaf43(X0,X1)
| ~ ssList(skaf43(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f18263,plain,
( sQ428_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18195,f540,f18260]) ).
fof(f18264,definition,
! [X0,X1] :
( sQ429_spl
<=> ( tl(skaf45(X0,X1)) = app(tl(skaf45(X0,X1)),nil)
| nil = skaf45(X0,X1)
| ~ ssList(skaf45(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f18267,plain,
( sQ429_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18196,f540,f18264]) ).
fof(f18268,definition,
! [X0,X1] :
( sQ430_spl
<=> ( tl(skaf46(X0,X1)) = app(tl(skaf46(X0,X1)),nil)
| nil = skaf46(X0,X1)
| ~ ssList(skaf46(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f18271,plain,
( sQ430_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18197,f540,f18268]) ).
fof(f18272,definition,
! [X0,X1] :
( sQ431_spl
<=> ( tl(skaf47(X0,X1)) = app(tl(skaf47(X0,X1)),nil)
| nil = skaf47(X0,X1)
| ~ ssList(skaf47(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition]) ).
fof(f18275,plain,
( sQ431_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18198,f540,f18272]) ).
fof(f18276,definition,
! [X0,X1] :
( sQ432_spl
<=> ( tl(skaf48(X0,X1)) = app(tl(skaf48(X0,X1)),nil)
| nil = skaf48(X0,X1)
| ~ ssList(skaf48(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f18279,plain,
( sQ432_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18199,f540,f18276]) ).
fof(f18288,definition,
! [X0] :
( sQ435_spl
<=> ( tl(skaf51(X0)) = app(tl(skaf51(X0)),nil)
| nil = skaf51(X0)
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f18291,plain,
( sQ435_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18202,f540,f18288]) ).
fof(f18292,definition,
! [X0] :
( sQ436_spl
<=> ( tl(skaf52(X0)) = app(tl(skaf52(X0)),nil)
| nil = skaf52(X0)
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f18295,plain,
( sQ436_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18203,f540,f18292]) ).
fof(f18296,definition,
! [X0] :
( sQ437_spl
<=> ( tl(skaf53(X0)) = app(tl(skaf53(X0)),nil)
| nil = skaf53(X0)
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f18299,plain,
( sQ437_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18204,f540,f18296]) ).
fof(f18300,definition,
! [X0] :
( sQ438_spl
<=> ( tl(skaf56(X0)) = app(tl(skaf56(X0)),nil)
| nil = skaf56(X0)
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition]) ).
fof(f18303,plain,
( sQ438_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18205,f540,f18300]) ).
fof(f18304,definition,
! [X0] :
( sQ439_spl
<=> ( tl(skaf57(X0)) = app(tl(skaf57(X0)),nil)
| nil = skaf57(X0)
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f18307,plain,
( sQ439_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18206,f540,f18304]) ).
fof(f18308,definition,
! [X0] :
( sQ440_spl
<=> ( tl(skaf58(X0)) = app(tl(skaf58(X0)),nil)
| nil = skaf58(X0)
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition]) ).
fof(f18311,plain,
( sQ440_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18207,f540,f18308]) ).
fof(f18312,definition,
! [X0] :
( sQ441_spl
<=> ( tl(skaf61(X0)) = app(tl(skaf61(X0)),nil)
| nil = skaf61(X0)
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition]) ).
fof(f18315,plain,
( sQ441_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18208,f540,f18312]) ).
fof(f18316,definition,
! [X0] :
( sQ442_spl
<=> ( tl(skaf62(X0)) = app(tl(skaf62(X0)),nil)
| nil = skaf62(X0)
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition]) ).
fof(f18319,plain,
( sQ442_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18209,f540,f18316]) ).
fof(f18320,definition,
! [X0] :
( sQ443_spl
<=> ( tl(skaf63(X0)) = app(tl(skaf63(X0)),nil)
| nil = skaf63(X0)
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition]) ).
fof(f18323,plain,
( sQ443_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18210,f540,f18320]) ).
fof(f18324,definition,
! [X0] :
( sQ444_spl
<=> ( tl(skaf66(X0)) = app(tl(skaf66(X0)),nil)
| nil = skaf66(X0)
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).
fof(f18327,plain,
( sQ444_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18211,f540,f18324]) ).
fof(f18328,definition,
! [X0] :
( sQ445_spl
<=> ( tl(skaf67(X0)) = app(tl(skaf67(X0)),nil)
| nil = skaf67(X0)
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition]) ).
fof(f18331,plain,
( sQ445_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18212,f540,f18328]) ).
fof(f18332,definition,
! [X0] :
( sQ446_spl
<=> ( tl(skaf68(X0)) = app(tl(skaf68(X0)),nil)
| nil = skaf68(X0)
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ446_spl])],[split_symbol_definition]) ).
fof(f18335,plain,
( sQ446_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18213,f540,f18332]) ).
fof(f18336,definition,
! [X0] :
( sQ447_spl
<=> ( tl(skaf71(X0)) = app(tl(skaf71(X0)),nil)
| nil = skaf71(X0)
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ447_spl])],[split_symbol_definition]) ).
fof(f18339,plain,
( sQ447_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18214,f540,f18336]) ).
fof(f18340,definition,
! [X0] :
( sQ448_spl
<=> ( tl(skaf72(X0)) = app(tl(skaf72(X0)),nil)
| nil = skaf72(X0)
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition]) ).
fof(f18343,plain,
( sQ448_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18215,f540,f18340]) ).
fof(f18344,definition,
! [X0] :
( sQ449_spl
<=> ( tl(skaf73(X0)) = app(tl(skaf73(X0)),nil)
| nil = skaf73(X0)
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition]) ).
fof(f18347,plain,
( sQ449_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18216,f540,f18344]) ).
fof(f18348,definition,
! [X0] :
( sQ450_spl
<=> ( tl(skaf75(X0)) = app(tl(skaf75(X0)),nil)
| nil = skaf75(X0)
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition]) ).
fof(f18351,plain,
( sQ450_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18217,f540,f18348]) ).
fof(f18352,definition,
! [X0] :
( sQ451_spl
<=> ( tl(skaf76(X0)) = app(tl(skaf76(X0)),nil)
| nil = skaf76(X0)
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition]) ).
fof(f18355,plain,
( sQ451_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18218,f540,f18352]) ).
fof(f18356,definition,
! [X0] :
( sQ452_spl
<=> ( tl(skaf77(X0)) = app(tl(skaf77(X0)),nil)
| nil = skaf77(X0)
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f18359,plain,
( sQ452_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18219,f540,f18356]) ).
fof(f18360,definition,
! [X0] :
( sQ453_spl
<=> ( tl(skaf80(X0)) = app(tl(skaf80(X0)),nil)
| nil = skaf80(X0)
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition]) ).
fof(f18363,plain,
( sQ453_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18220,f540,f18360]) ).
fof(f18364,definition,
! [X0] :
( sQ454_spl
<=> ( tl(skaf82(X0)) = app(tl(skaf82(X0)),nil)
| nil = skaf82(X0)
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition]) ).
fof(f18367,plain,
( sQ454_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18221,f540,f18364]) ).
fof(f18368,definition,
! [X0] :
( sQ455_spl
<=> ( tl(skaf81(X0)) = app(tl(skaf81(X0)),nil)
| nil = skaf81(X0)
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ455_spl])],[split_symbol_definition]) ).
fof(f18371,plain,
( sQ455_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f18222,f540,f18368]) ).
fof(f18651,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(nil)
| sk2 != app(X0,sk2) ),
inference(paramodulation,[status(thm)],[f606,f1649]) ).
fof(f18654,definition,
! [X0] :
( sQ489_spl
<=> ( nil = X0
| ~ ssList(X0)
| sk2 != app(X0,sk2) ) ),
introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition]) ).
fof(f18657,plain,
( ~ sQ8_spl
| sQ489_spl ),
inference(split_clause,[status(thm)],[f18651,f18654,f540]) ).
fof(f19694,plain,
! [X0,X1] :
( nil = skaf42(X0,X1)
| ~ ssList(nil)
| skaf42(X0,X1) != nil ),
inference(paramodulation,[status(thm)],[f735,f836]) ).
fof(f19695,definition,
! [X0,X1] :
( sQ518_spl
<=> ( nil = skaf42(X0,X1)
| skaf42(X0,X1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ518_spl])],[split_symbol_definition]) ).
fof(f19698,plain,
( ~ sQ8_spl
| sQ518_spl ),
inference(split_clause,[status(thm)],[f19694,f19695,f540]) ).
fof(f19704,plain,
! [X0,X1] :
( memberP(app(sk1,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(sk1)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f561,f496]) ).
fof(f19749,definition,
! [X0,X1] :
( sQ519_spl
<=> ( memberP(app(sk1,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition]) ).
fof(f19752,plain,
( ~ sQ11_spl
| sQ519_spl ),
inference(split_clause,[status(thm)],[f19704,f19749,f596]) ).
fof(f19884,plain,
! [X0,X1] :
( nil = skaf43(X0,X1)
| ~ ssList(nil)
| skaf43(X0,X1) != nil ),
inference(paramodulation,[status(thm)],[f732,f837]) ).
fof(f19885,definition,
! [X0,X1] :
( sQ520_spl
<=> ( nil = skaf43(X0,X1)
| skaf43(X0,X1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition]) ).
fof(f19888,plain,
( ~ sQ8_spl
| sQ520_spl ),
inference(split_clause,[status(thm)],[f19884,f19885,f540]) ).
fof(f19889,plain,
! [X0,X1] :
( nil = skaf45(X0,X1)
| ~ ssList(nil)
| skaf45(X0,X1) != nil ),
inference(paramodulation,[status(thm)],[f729,f838]) ).
fof(f19890,definition,
! [X0,X1] :
( sQ521_spl
<=> ( nil = skaf45(X0,X1)
| skaf45(X0,X1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition]) ).
fof(f19893,plain,
( ~ sQ8_spl
| sQ521_spl ),
inference(split_clause,[status(thm)],[f19889,f19890,f540]) ).
fof(f20244,plain,
! [X0,X1] :
( memberP(app(sk5,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(sk5)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f559,f496]) ).
fof(f20291,definition,
! [X0,X1] :
( sQ522_spl
<=> ( memberP(app(sk5,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ522_spl])],[split_symbol_definition]) ).
fof(f20294,plain,
( ~ sQ10_spl
| sQ522_spl ),
inference(split_clause,[status(thm)],[f20244,f20291,f587]) ).
fof(f20556,plain,
! [X0,X1] :
( nil = skaf46(X0,X1)
| ~ ssList(nil)
| skaf46(X0,X1) != nil ),
inference(paramodulation,[status(thm)],[f726,f839]) ).
fof(f20557,definition,
! [X0,X1] :
( sQ523_spl
<=> ( nil = skaf46(X0,X1)
| skaf46(X0,X1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f20560,plain,
( ~ sQ8_spl
| sQ523_spl ),
inference(split_clause,[status(thm)],[f20556,f20557,f540]) ).
fof(f20561,plain,
! [X0,X1] :
( nil = skaf47(X0,X1)
| ~ ssList(nil)
| skaf47(X0,X1) != nil ),
inference(paramodulation,[status(thm)],[f653,f840]) ).
fof(f20562,definition,
! [X0,X1] :
( sQ524_spl
<=> ( nil = skaf47(X0,X1)
| skaf47(X0,X1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ524_spl])],[split_symbol_definition]) ).
fof(f20565,plain,
( ~ sQ8_spl
| sQ524_spl ),
inference(split_clause,[status(thm)],[f20561,f20562,f540]) ).
fof(f20566,plain,
! [X0,X1] :
( nil = skaf48(X0,X1)
| ~ ssList(nil)
| skaf48(X0,X1) != nil ),
inference(paramodulation,[status(thm)],[f650,f841]) ).
fof(f20567,definition,
! [X0,X1] :
( sQ525_spl
<=> ( nil = skaf48(X0,X1)
| skaf48(X0,X1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition]) ).
fof(f20570,plain,
( ~ sQ8_spl
| sQ525_spl ),
inference(split_clause,[status(thm)],[f20566,f20567,f540]) ).
fof(f20957,plain,
! [X0,X1] :
( memberP(app(sk2,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(sk2)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f747,f496]) ).
fof(f21007,definition,
! [X0,X1] :
( sQ526_spl
<=> ( memberP(app(sk2,cons(X0,X1)),X0)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition]) ).
fof(f21010,plain,
( ~ sQ12_spl
| sQ526_spl ),
inference(split_clause,[status(thm)],[f20957,f21007,f610]) ).
fof(f21066,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(nil)
| sk5 != app(X0,sk5) ),
inference(paramodulation,[status(thm)],[f520,f1666]) ).
fof(f21067,plain,
! [X0] :
( sk1 = X0
| ~ ssList(X0)
| ~ ssList(sk1)
| sk2 != app(X0,sk5) ),
inference(paramodulation,[status(thm)],[f608,f1666]) ).
fof(f21071,definition,
! [X0] :
( sQ527_spl
<=> ( nil = X0
| ~ ssList(X0)
| sk5 != app(X0,sk5) ) ),
introduced(definition,[new_symbols(definition,[sQ527_spl])],[split_symbol_definition]) ).
fof(f21074,plain,
( ~ sQ8_spl
| sQ527_spl ),
inference(split_clause,[status(thm)],[f21066,f21071,f540]) ).
fof(f21075,definition,
! [X0] :
( sQ528_spl
<=> ( sk1 = X0
| ~ ssList(X0)
| sk2 != app(X0,sk5) ) ),
introduced(definition,[new_symbols(definition,[sQ528_spl])],[split_symbol_definition]) ).
fof(f21078,plain,
( ~ sQ11_spl
| sQ528_spl ),
inference(split_clause,[status(thm)],[f21067,f21075,f596]) ).
fof(f21949,plain,
! [X0] :
( nil = skaf61(X0)
| ~ ssList(nil)
| skaf61(X0) != nil ),
inference(paramodulation,[status(thm)],[f578,f853]) ).
fof(f21950,definition,
! [X0] :
( sQ535_spl
<=> ( nil = skaf61(X0)
| skaf61(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ535_spl])],[split_symbol_definition]) ).
fof(f21953,plain,
( ~ sQ8_spl
| sQ535_spl ),
inference(split_clause,[status(thm)],[f21949,f21950,f540]) ).
fof(f21954,plain,
! [X0] :
( nil = skaf62(X0)
| ~ ssList(nil)
| skaf62(X0) != nil ),
inference(paramodulation,[status(thm)],[f575,f854]) ).
fof(f21955,definition,
! [X0] :
( sQ536_spl
<=> ( nil = skaf62(X0)
| skaf62(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f21958,plain,
( ~ sQ8_spl
| sQ536_spl ),
inference(split_clause,[status(thm)],[f21954,f21955,f540]) ).
fof(f21959,plain,
! [X0] :
( nil = skaf63(X0)
| ~ ssList(nil)
| skaf63(X0) != nil ),
inference(paramodulation,[status(thm)],[f572,f855]) ).
fof(f21960,definition,
! [X0] :
( sQ537_spl
<=> ( nil = skaf63(X0)
| skaf63(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ537_spl])],[split_symbol_definition]) ).
fof(f21963,plain,
( ~ sQ8_spl
| sQ537_spl ),
inference(split_clause,[status(thm)],[f21959,f21960,f540]) ).
fof(f21964,plain,
! [X0] :
( nil = skaf66(X0)
| ~ ssList(nil)
| skaf66(X0) != nil ),
inference(paramodulation,[status(thm)],[f569,f856]) ).
fof(f21965,definition,
! [X0] :
( sQ538_spl
<=> ( nil = skaf66(X0)
| skaf66(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition]) ).
fof(f21968,plain,
( ~ sQ8_spl
| sQ538_spl ),
inference(split_clause,[status(thm)],[f21964,f21965,f540]) ).
fof(f21969,plain,
! [X0] :
( nil = skaf67(X0)
| ~ ssList(nil)
| skaf67(X0) != nil ),
inference(paramodulation,[status(thm)],[f566,f857]) ).
fof(f21970,definition,
! [X0] :
( sQ539_spl
<=> ( nil = skaf67(X0)
| skaf67(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ539_spl])],[split_symbol_definition]) ).
fof(f21973,plain,
( ~ sQ8_spl
| sQ539_spl ),
inference(split_clause,[status(thm)],[f21969,f21970,f540]) ).
fof(f22092,plain,
! [X0] :
( nil = skaf68(X0)
| ~ ssList(nil)
| skaf68(X0) != nil ),
inference(paramodulation,[status(thm)],[f563,f858]) ).
fof(f22093,definition,
! [X0] :
( sQ540_spl
<=> ( nil = skaf68(X0)
| skaf68(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ540_spl])],[split_symbol_definition]) ).
fof(f22096,plain,
( ~ sQ8_spl
| sQ540_spl ),
inference(split_clause,[status(thm)],[f22092,f22093,f540]) ).
fof(f22097,plain,
! [X0] :
( nil = skaf71(X0)
| ~ ssList(nil)
| skaf71(X0) != nil ),
inference(paramodulation,[status(thm)],[f535,f859]) ).
fof(f22098,definition,
! [X0] :
( sQ541_spl
<=> ( nil = skaf71(X0)
| skaf71(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition]) ).
fof(f22101,plain,
( ~ sQ8_spl
| sQ541_spl ),
inference(split_clause,[status(thm)],[f22097,f22098,f540]) ).
fof(f22102,plain,
! [X0] :
( nil = skaf72(X0)
| ~ ssList(nil)
| skaf72(X0) != nil ),
inference(paramodulation,[status(thm)],[f533,f860]) ).
fof(f22103,definition,
! [X0] :
( sQ542_spl
<=> ( nil = skaf72(X0)
| skaf72(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ542_spl])],[split_symbol_definition]) ).
fof(f22106,plain,
( ~ sQ8_spl
| sQ542_spl ),
inference(split_clause,[status(thm)],[f22102,f22103,f540]) ).
fof(f22107,plain,
! [X0] :
( nil = skaf73(X0)
| ~ ssList(nil)
| skaf73(X0) != nil ),
inference(paramodulation,[status(thm)],[f531,f861]) ).
fof(f22108,definition,
! [X0] :
( sQ543_spl
<=> ( nil = skaf73(X0)
| skaf73(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ543_spl])],[split_symbol_definition]) ).
fof(f22111,plain,
( ~ sQ8_spl
| sQ543_spl ),
inference(split_clause,[status(thm)],[f22107,f22108,f540]) ).
fof(f22112,plain,
! [X0] :
( nil = skaf75(X0)
| ~ ssList(nil)
| skaf75(X0) != nil ),
inference(paramodulation,[status(thm)],[f529,f862]) ).
fof(f22113,definition,
! [X0] :
( sQ544_spl
<=> ( nil = skaf75(X0)
| skaf75(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ544_spl])],[split_symbol_definition]) ).
fof(f22116,plain,
( ~ sQ8_spl
| sQ544_spl ),
inference(split_clause,[status(thm)],[f22112,f22113,f540]) ).
fof(f22252,plain,
! [X0,X1] :
( app(app(sk5,skaf42(X0,X1)),nil) = app(sk5,skaf42(X0,X1))
| ~ ssList(skaf42(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f736,f1669]) ).
fof(f22253,plain,
! [X0,X1] :
( app(app(sk5,skaf43(X0,X1)),nil) = app(sk5,skaf43(X0,X1))
| ~ ssList(skaf43(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f733,f1669]) ).
fof(f22254,plain,
! [X0,X1] :
( app(app(sk5,skaf45(X0,X1)),nil) = app(sk5,skaf45(X0,X1))
| ~ ssList(skaf45(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f730,f1669]) ).
fof(f22255,plain,
! [X0,X1] :
( app(app(sk5,skaf46(X0,X1)),nil) = app(sk5,skaf46(X0,X1))
| ~ ssList(skaf46(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f727,f1669]) ).
fof(f22256,plain,
! [X0,X1] :
( app(app(sk5,skaf47(X0,X1)),nil) = app(sk5,skaf47(X0,X1))
| ~ ssList(skaf47(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f654,f1669]) ).
fof(f22257,plain,
! [X0,X1] :
( app(app(sk5,skaf48(X0,X1)),nil) = app(sk5,skaf48(X0,X1))
| ~ ssList(skaf48(X0,X1))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f651,f1669]) ).
fof(f22259,plain,
( app(app(sk5,sk2),nil) = app(sk5,sk2)
| ~ ssList(sk2)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f607,f1669]) ).
fof(f22260,plain,
! [X0] :
( app(app(sk5,skaf51(X0)),nil) = app(sk5,skaf51(X0))
| ~ ssList(skaf51(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f645,f1669]) ).
fof(f22261,plain,
! [X0] :
( app(app(sk5,skaf52(X0)),nil) = app(sk5,skaf52(X0))
| ~ ssList(skaf52(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f1669]) ).
fof(f22262,plain,
! [X0] :
( app(app(sk5,skaf53(X0)),nil) = app(sk5,skaf53(X0))
| ~ ssList(skaf53(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f639,f1669]) ).
fof(f22263,plain,
! [X0] :
( app(app(sk5,skaf56(X0)),nil) = app(sk5,skaf56(X0))
| ~ ssList(skaf56(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f634,f1669]) ).
fof(f22264,plain,
! [X0] :
( app(app(sk5,skaf57(X0)),nil) = app(sk5,skaf57(X0))
| ~ ssList(skaf57(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f631,f1669]) ).
fof(f22265,plain,
! [X0] :
( app(app(sk5,skaf58(X0)),nil) = app(sk5,skaf58(X0))
| ~ ssList(skaf58(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f582,f1669]) ).
fof(f22266,plain,
! [X0] :
( app(app(sk5,skaf61(X0)),nil) = app(sk5,skaf61(X0))
| ~ ssList(skaf61(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f579,f1669]) ).
fof(f22267,plain,
! [X0] :
( app(app(sk5,skaf62(X0)),nil) = app(sk5,skaf62(X0))
| ~ ssList(skaf62(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f576,f1669]) ).
fof(f22268,plain,
! [X0] :
( app(app(sk5,skaf63(X0)),nil) = app(sk5,skaf63(X0))
| ~ ssList(skaf63(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f573,f1669]) ).
fof(f22269,plain,
! [X0] :
( app(app(sk5,skaf66(X0)),nil) = app(sk5,skaf66(X0))
| ~ ssList(skaf66(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f570,f1669]) ).
fof(f22270,plain,
! [X0] :
( app(app(sk5,skaf67(X0)),nil) = app(sk5,skaf67(X0))
| ~ ssList(skaf67(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f567,f1669]) ).
fof(f22271,plain,
! [X0] :
( app(app(sk5,skaf68(X0)),nil) = app(sk5,skaf68(X0))
| ~ ssList(skaf68(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f564,f1669]) ).
fof(f22272,plain,
! [X0] :
( app(app(sk5,skaf71(X0)),nil) = app(sk5,skaf71(X0))
| ~ ssList(skaf71(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f536,f1669]) ).
fof(f22273,plain,
! [X0] :
( app(app(sk5,skaf72(X0)),nil) = app(sk5,skaf72(X0))
| ~ ssList(skaf72(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f534,f1669]) ).
fof(f22274,plain,
! [X0] :
( app(app(sk5,skaf73(X0)),nil) = app(sk5,skaf73(X0))
| ~ ssList(skaf73(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f532,f1669]) ).
fof(f22275,plain,
! [X0] :
( app(app(sk5,skaf75(X0)),nil) = app(sk5,skaf75(X0))
| ~ ssList(skaf75(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f530,f1669]) ).
fof(f22276,plain,
! [X0] :
( app(app(sk5,skaf76(X0)),nil) = app(sk5,skaf76(X0))
| ~ ssList(skaf76(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f528,f1669]) ).
fof(f22277,plain,
! [X0] :
( app(app(sk5,skaf77(X0)),nil) = app(sk5,skaf77(X0))
| ~ ssList(skaf77(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f526,f1669]) ).
fof(f22278,plain,
! [X0] :
( app(app(sk5,skaf80(X0)),nil) = app(sk5,skaf80(X0))
| ~ ssList(skaf80(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f524,f1669]) ).
fof(f22279,plain,
! [X0] :
( app(app(sk5,skaf82(X0)),nil) = app(sk5,skaf82(X0))
| ~ ssList(skaf82(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f514,f1669]) ).
fof(f22280,plain,
! [X0] :
( app(app(sk5,skaf81(X0)),nil) = app(sk5,skaf81(X0))
| ~ ssList(skaf81(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f513,f1669]) ).
fof(f22281,plain,
! [X0,X1] :
( app(app(sk5,nil),skaf42(X0,X1)) = app(sk5,skaf42(X0,X1))
| ~ ssList(nil)
| ~ ssList(skaf42(X0,X1)) ),
inference(paramodulation,[status(thm)],[f735,f1669]) ).
fof(f22282,plain,
! [X0,X1] :
( app(app(sk5,nil),skaf43(X0,X1)) = app(sk5,skaf43(X0,X1))
| ~ ssList(nil)
| ~ ssList(skaf43(X0,X1)) ),
inference(paramodulation,[status(thm)],[f732,f1669]) ).
fof(f22283,plain,
! [X0,X1] :
( app(app(sk5,nil),skaf45(X0,X1)) = app(sk5,skaf45(X0,X1))
| ~ ssList(nil)
| ~ ssList(skaf45(X0,X1)) ),
inference(paramodulation,[status(thm)],[f729,f1669]) ).
fof(f22284,plain,
! [X0,X1] :
( app(app(sk5,nil),skaf46(X0,X1)) = app(sk5,skaf46(X0,X1))
| ~ ssList(nil)
| ~ ssList(skaf46(X0,X1)) ),
inference(paramodulation,[status(thm)],[f726,f1669]) ).
fof(f22285,plain,
! [X0,X1] :
( app(app(sk5,nil),skaf47(X0,X1)) = app(sk5,skaf47(X0,X1))
| ~ ssList(nil)
| ~ ssList(skaf47(X0,X1)) ),
inference(paramodulation,[status(thm)],[f653,f1669]) ).
fof(f22286,plain,
! [X0,X1] :
( app(app(sk5,nil),skaf48(X0,X1)) = app(sk5,skaf48(X0,X1))
| ~ ssList(nil)
| ~ ssList(skaf48(X0,X1)) ),
inference(paramodulation,[status(thm)],[f650,f1669]) ).
fof(f22287,plain,
( app(app(sk5,nil),sk5) = app(sk5,sk5)
| ~ ssList(nil)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f520,f1669]) ).
fof(f22288,plain,
( app(app(sk5,nil),sk2) = app(sk5,sk2)
| ~ ssList(nil)
| ~ ssList(sk2) ),
inference(paramodulation,[status(thm)],[f606,f1669]) ).
fof(f22289,plain,
! [X0] :
( app(app(sk5,nil),skaf51(X0)) = app(sk5,skaf51(X0))
| ~ ssList(nil)
| ~ ssList(skaf51(X0)) ),
inference(paramodulation,[status(thm)],[f644,f1669]) ).
fof(f22290,plain,
! [X0] :
( app(app(sk5,nil),skaf52(X0)) = app(sk5,skaf52(X0))
| ~ ssList(nil)
| ~ ssList(skaf52(X0)) ),
inference(paramodulation,[status(thm)],[f641,f1669]) ).
fof(f22291,plain,
! [X0] :
( app(app(sk5,nil),skaf53(X0)) = app(sk5,skaf53(X0))
| ~ ssList(nil)
| ~ ssList(skaf53(X0)) ),
inference(paramodulation,[status(thm)],[f638,f1669]) ).
fof(f22292,plain,
! [X0] :
( app(app(sk5,nil),skaf56(X0)) = app(sk5,skaf56(X0))
| ~ ssList(nil)
| ~ ssList(skaf56(X0)) ),
inference(paramodulation,[status(thm)],[f633,f1669]) ).
fof(f22293,plain,
! [X0] :
( app(app(sk5,nil),skaf57(X0)) = app(sk5,skaf57(X0))
| ~ ssList(nil)
| ~ ssList(skaf57(X0)) ),
inference(paramodulation,[status(thm)],[f630,f1669]) ).
fof(f22294,plain,
! [X0] :
( app(app(sk5,nil),skaf58(X0)) = app(sk5,skaf58(X0))
| ~ ssList(nil)
| ~ ssList(skaf58(X0)) ),
inference(paramodulation,[status(thm)],[f581,f1669]) ).
fof(f22295,plain,
! [X0] :
( app(app(sk5,nil),skaf61(X0)) = app(sk5,skaf61(X0))
| ~ ssList(nil)
| ~ ssList(skaf61(X0)) ),
inference(paramodulation,[status(thm)],[f578,f1669]) ).
fof(f22296,plain,
! [X0] :
( app(app(sk5,nil),skaf62(X0)) = app(sk5,skaf62(X0))
| ~ ssList(nil)
| ~ ssList(skaf62(X0)) ),
inference(paramodulation,[status(thm)],[f575,f1669]) ).
fof(f22297,plain,
! [X0] :
( app(app(sk5,nil),skaf63(X0)) = app(sk5,skaf63(X0))
| ~ ssList(nil)
| ~ ssList(skaf63(X0)) ),
inference(paramodulation,[status(thm)],[f572,f1669]) ).
fof(f22298,plain,
! [X0] :
( app(app(sk5,nil),skaf66(X0)) = app(sk5,skaf66(X0))
| ~ ssList(nil)
| ~ ssList(skaf66(X0)) ),
inference(paramodulation,[status(thm)],[f569,f1669]) ).
fof(f22299,plain,
! [X0] :
( app(app(sk5,nil),skaf67(X0)) = app(sk5,skaf67(X0))
| ~ ssList(nil)
| ~ ssList(skaf67(X0)) ),
inference(paramodulation,[status(thm)],[f566,f1669]) ).
fof(f22300,plain,
! [X0] :
( app(app(sk5,nil),skaf68(X0)) = app(sk5,skaf68(X0))
| ~ ssList(nil)
| ~ ssList(skaf68(X0)) ),
inference(paramodulation,[status(thm)],[f563,f1669]) ).
fof(f22301,plain,
! [X0] :
( app(app(sk5,nil),skaf71(X0)) = app(sk5,skaf71(X0))
| ~ ssList(nil)
| ~ ssList(skaf71(X0)) ),
inference(paramodulation,[status(thm)],[f535,f1669]) ).
fof(f22302,plain,
! [X0] :
( app(app(sk5,nil),skaf72(X0)) = app(sk5,skaf72(X0))
| ~ ssList(nil)
| ~ ssList(skaf72(X0)) ),
inference(paramodulation,[status(thm)],[f533,f1669]) ).
fof(f22303,plain,
! [X0] :
( app(app(sk5,nil),skaf73(X0)) = app(sk5,skaf73(X0))
| ~ ssList(nil)
| ~ ssList(skaf73(X0)) ),
inference(paramodulation,[status(thm)],[f531,f1669]) ).
fof(f22304,plain,
! [X0] :
( app(app(sk5,nil),skaf75(X0)) = app(sk5,skaf75(X0))
| ~ ssList(nil)
| ~ ssList(skaf75(X0)) ),
inference(paramodulation,[status(thm)],[f529,f1669]) ).
fof(f22305,plain,
! [X0] :
( app(app(sk5,nil),skaf76(X0)) = app(sk5,skaf76(X0))
| ~ ssList(nil)
| ~ ssList(skaf76(X0)) ),
inference(paramodulation,[status(thm)],[f527,f1669]) ).
fof(f22306,plain,
! [X0] :
( app(app(sk5,nil),skaf77(X0)) = app(sk5,skaf77(X0))
| ~ ssList(nil)
| ~ ssList(skaf77(X0)) ),
inference(paramodulation,[status(thm)],[f525,f1669]) ).
fof(f22307,plain,
! [X0] :
( app(app(sk5,nil),skaf80(X0)) = app(sk5,skaf80(X0))
| ~ ssList(nil)
| ~ ssList(skaf80(X0)) ),
inference(paramodulation,[status(thm)],[f523,f1669]) ).
fof(f22308,plain,
! [X0] :
( app(app(sk5,nil),skaf82(X0)) = app(sk5,skaf82(X0))
| ~ ssList(nil)
| ~ ssList(skaf82(X0)) ),
inference(paramodulation,[status(thm)],[f519,f1669]) ).
fof(f22309,plain,
! [X0] :
( app(app(sk5,nil),skaf81(X0)) = app(sk5,skaf81(X0))
| ~ ssList(nil)
| ~ ssList(skaf81(X0)) ),
inference(paramodulation,[status(thm)],[f518,f1669]) ).
fof(f22310,plain,
( app(app(sk5,nil),sk1) = app(sk5,sk1)
| ~ ssList(nil)
| ~ ssList(sk1) ),
inference(paramodulation,[status(thm)],[f522,f1669]) ).
fof(f22311,plain,
( app(app(sk5,nil),nil) = app(sk5,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f516,f1669]) ).
fof(f22312,plain,
( app(app(sk5,sk1),sk5) = app(sk5,sk2)
| ~ ssList(sk1)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f608,f1669]) ).
fof(f22313,plain,
( app(app(sk5,sk1),nil) = app(sk5,sk1)
| ~ ssList(sk1)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f517,f1669]) ).
fof(f22314,definition,
! [X0,X1] :
( sQ545_spl
<=> ( app(app(sk5,skaf42(X0,X1)),nil) = app(sk5,skaf42(X0,X1))
| ~ ssList(skaf42(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ545_spl])],[split_symbol_definition]) ).
fof(f22317,plain,
( sQ545_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22252,f540,f22314]) ).
fof(f22318,definition,
! [X0,X1] :
( sQ546_spl
<=> ( app(app(sk5,skaf43(X0,X1)),nil) = app(sk5,skaf43(X0,X1))
| ~ ssList(skaf43(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ546_spl])],[split_symbol_definition]) ).
fof(f22321,plain,
( sQ546_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22253,f540,f22318]) ).
fof(f22322,definition,
! [X0,X1] :
( sQ547_spl
<=> ( app(app(sk5,skaf45(X0,X1)),nil) = app(sk5,skaf45(X0,X1))
| ~ ssList(skaf45(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ547_spl])],[split_symbol_definition]) ).
fof(f22325,plain,
( sQ547_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22254,f540,f22322]) ).
fof(f22326,definition,
! [X0,X1] :
( sQ548_spl
<=> ( app(app(sk5,skaf46(X0,X1)),nil) = app(sk5,skaf46(X0,X1))
| ~ ssList(skaf46(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition]) ).
fof(f22329,plain,
( sQ548_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22255,f540,f22326]) ).
fof(f22330,definition,
! [X0,X1] :
( sQ549_spl
<=> ( app(app(sk5,skaf47(X0,X1)),nil) = app(sk5,skaf47(X0,X1))
| ~ ssList(skaf47(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition]) ).
fof(f22333,plain,
( sQ549_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22256,f540,f22330]) ).
fof(f22334,definition,
! [X0,X1] :
( sQ550_spl
<=> ( app(app(sk5,skaf48(X0,X1)),nil) = app(sk5,skaf48(X0,X1))
| ~ ssList(skaf48(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f22337,plain,
( sQ550_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22257,f540,f22334]) ).
fof(f22339,definition,
( sQ551_spl
<=> app(app(sk5,sk2),nil) = app(sk5,sk2) ),
introduced(definition,[new_symbols(definition,[sQ551_spl])],[split_symbol_definition]) ).
fof(f22342,plain,
( sQ551_spl
| ~ sQ12_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22259,f540,f610,f22339]) ).
fof(f22343,definition,
! [X0] :
( sQ552_spl
<=> ( app(app(sk5,skaf51(X0)),nil) = app(sk5,skaf51(X0))
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ552_spl])],[split_symbol_definition]) ).
fof(f22346,plain,
( sQ552_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22260,f540,f22343]) ).
fof(f22347,definition,
! [X0] :
( sQ553_spl
<=> ( app(app(sk5,skaf52(X0)),nil) = app(sk5,skaf52(X0))
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition]) ).
fof(f22350,plain,
( sQ553_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22261,f540,f22347]) ).
fof(f22351,definition,
! [X0] :
( sQ554_spl
<=> ( app(app(sk5,skaf53(X0)),nil) = app(sk5,skaf53(X0))
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ554_spl])],[split_symbol_definition]) ).
fof(f22354,plain,
( sQ554_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22262,f540,f22351]) ).
fof(f22355,definition,
! [X0] :
( sQ555_spl
<=> ( app(app(sk5,skaf56(X0)),nil) = app(sk5,skaf56(X0))
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ555_spl])],[split_symbol_definition]) ).
fof(f22358,plain,
( sQ555_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22263,f540,f22355]) ).
fof(f22359,definition,
! [X0] :
( sQ556_spl
<=> ( app(app(sk5,skaf57(X0)),nil) = app(sk5,skaf57(X0))
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ556_spl])],[split_symbol_definition]) ).
fof(f22362,plain,
( sQ556_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22264,f540,f22359]) ).
fof(f22363,definition,
! [X0] :
( sQ557_spl
<=> ( app(app(sk5,skaf58(X0)),nil) = app(sk5,skaf58(X0))
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition]) ).
fof(f22366,plain,
( sQ557_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22265,f540,f22363]) ).
fof(f22367,definition,
! [X0] :
( sQ558_spl
<=> ( app(app(sk5,skaf61(X0)),nil) = app(sk5,skaf61(X0))
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition]) ).
fof(f22370,plain,
( sQ558_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22266,f540,f22367]) ).
fof(f22371,definition,
! [X0] :
( sQ559_spl
<=> ( app(app(sk5,skaf62(X0)),nil) = app(sk5,skaf62(X0))
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ559_spl])],[split_symbol_definition]) ).
fof(f22374,plain,
( sQ559_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22267,f540,f22371]) ).
fof(f22375,definition,
! [X0] :
( sQ560_spl
<=> ( app(app(sk5,skaf63(X0)),nil) = app(sk5,skaf63(X0))
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ560_spl])],[split_symbol_definition]) ).
fof(f22378,plain,
( sQ560_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22268,f540,f22375]) ).
fof(f22379,definition,
! [X0] :
( sQ561_spl
<=> ( app(app(sk5,skaf66(X0)),nil) = app(sk5,skaf66(X0))
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ561_spl])],[split_symbol_definition]) ).
fof(f22382,plain,
( sQ561_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22269,f540,f22379]) ).
fof(f22383,definition,
! [X0] :
( sQ562_spl
<=> ( app(app(sk5,skaf67(X0)),nil) = app(sk5,skaf67(X0))
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ562_spl])],[split_symbol_definition]) ).
fof(f22386,plain,
( sQ562_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22270,f540,f22383]) ).
fof(f22387,definition,
! [X0] :
( sQ563_spl
<=> ( app(app(sk5,skaf68(X0)),nil) = app(sk5,skaf68(X0))
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ563_spl])],[split_symbol_definition]) ).
fof(f22390,plain,
( sQ563_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22271,f540,f22387]) ).
fof(f22391,definition,
! [X0] :
( sQ564_spl
<=> ( app(app(sk5,skaf71(X0)),nil) = app(sk5,skaf71(X0))
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition]) ).
fof(f22394,plain,
( sQ564_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22272,f540,f22391]) ).
fof(f22395,definition,
! [X0] :
( sQ565_spl
<=> ( app(app(sk5,skaf72(X0)),nil) = app(sk5,skaf72(X0))
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ565_spl])],[split_symbol_definition]) ).
fof(f22398,plain,
( sQ565_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22273,f540,f22395]) ).
fof(f22399,definition,
! [X0] :
( sQ566_spl
<=> ( app(app(sk5,skaf73(X0)),nil) = app(sk5,skaf73(X0))
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition]) ).
fof(f22402,plain,
( sQ566_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22274,f540,f22399]) ).
fof(f22403,definition,
! [X0] :
( sQ567_spl
<=> ( app(app(sk5,skaf75(X0)),nil) = app(sk5,skaf75(X0))
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition]) ).
fof(f22406,plain,
( sQ567_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22275,f540,f22403]) ).
fof(f22407,definition,
! [X0] :
( sQ568_spl
<=> ( app(app(sk5,skaf76(X0)),nil) = app(sk5,skaf76(X0))
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ568_spl])],[split_symbol_definition]) ).
fof(f22410,plain,
( sQ568_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22276,f540,f22407]) ).
fof(f22411,definition,
! [X0] :
( sQ569_spl
<=> ( app(app(sk5,skaf77(X0)),nil) = app(sk5,skaf77(X0))
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ569_spl])],[split_symbol_definition]) ).
fof(f22414,plain,
( sQ569_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22277,f540,f22411]) ).
fof(f22415,definition,
! [X0] :
( sQ570_spl
<=> ( app(app(sk5,skaf80(X0)),nil) = app(sk5,skaf80(X0))
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f22418,plain,
( sQ570_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22278,f540,f22415]) ).
fof(f22419,definition,
! [X0] :
( sQ571_spl
<=> ( app(app(sk5,skaf82(X0)),nil) = app(sk5,skaf82(X0))
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ571_spl])],[split_symbol_definition]) ).
fof(f22422,plain,
( sQ571_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22279,f540,f22419]) ).
fof(f22423,definition,
! [X0] :
( sQ572_spl
<=> ( app(app(sk5,skaf81(X0)),nil) = app(sk5,skaf81(X0))
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition]) ).
fof(f22426,plain,
( sQ572_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22280,f540,f22423]) ).
fof(f22427,definition,
! [X0,X1] :
( sQ573_spl
<=> ( app(app(sk5,nil),skaf42(X0,X1)) = app(sk5,skaf42(X0,X1))
| ~ ssList(skaf42(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition]) ).
fof(f22430,plain,
( ~ sQ8_spl
| sQ573_spl ),
inference(split_clause,[status(thm)],[f22281,f22427,f540]) ).
fof(f22431,definition,
! [X0,X1] :
( sQ574_spl
<=> ( app(app(sk5,nil),skaf43(X0,X1)) = app(sk5,skaf43(X0,X1))
| ~ ssList(skaf43(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition]) ).
fof(f22434,plain,
( ~ sQ8_spl
| sQ574_spl ),
inference(split_clause,[status(thm)],[f22282,f22431,f540]) ).
fof(f22435,definition,
! [X0,X1] :
( sQ575_spl
<=> ( app(app(sk5,nil),skaf45(X0,X1)) = app(sk5,skaf45(X0,X1))
| ~ ssList(skaf45(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ575_spl])],[split_symbol_definition]) ).
fof(f22438,plain,
( ~ sQ8_spl
| sQ575_spl ),
inference(split_clause,[status(thm)],[f22283,f22435,f540]) ).
fof(f22439,definition,
! [X0,X1] :
( sQ576_spl
<=> ( app(app(sk5,nil),skaf46(X0,X1)) = app(sk5,skaf46(X0,X1))
| ~ ssList(skaf46(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ576_spl])],[split_symbol_definition]) ).
fof(f22442,plain,
( ~ sQ8_spl
| sQ576_spl ),
inference(split_clause,[status(thm)],[f22284,f22439,f540]) ).
fof(f22443,definition,
! [X0,X1] :
( sQ577_spl
<=> ( app(app(sk5,nil),skaf47(X0,X1)) = app(sk5,skaf47(X0,X1))
| ~ ssList(skaf47(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f22446,plain,
( ~ sQ8_spl
| sQ577_spl ),
inference(split_clause,[status(thm)],[f22285,f22443,f540]) ).
fof(f22447,definition,
! [X0,X1] :
( sQ578_spl
<=> ( app(app(sk5,nil),skaf48(X0,X1)) = app(sk5,skaf48(X0,X1))
| ~ ssList(skaf48(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition]) ).
fof(f22450,plain,
( ~ sQ8_spl
| sQ578_spl ),
inference(split_clause,[status(thm)],[f22286,f22447,f540]) ).
fof(f22451,definition,
( sQ579_spl
<=> app(app(sk5,nil),sk5) = app(sk5,sk5) ),
introduced(definition,[new_symbols(definition,[sQ579_spl])],[split_symbol_definition]) ).
fof(f22454,plain,
( sQ579_spl
| ~ sQ8_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f22287,f587,f540,f22451]) ).
fof(f22455,definition,
( sQ580_spl
<=> app(app(sk5,nil),sk2) = app(sk5,sk2) ),
introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition]) ).
fof(f22458,plain,
( sQ580_spl
| ~ sQ8_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f22288,f610,f540,f22455]) ).
fof(f22459,definition,
! [X0] :
( sQ581_spl
<=> ( app(app(sk5,nil),skaf51(X0)) = app(sk5,skaf51(X0))
| ~ ssList(skaf51(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ581_spl])],[split_symbol_definition]) ).
fof(f22462,plain,
( ~ sQ8_spl
| sQ581_spl ),
inference(split_clause,[status(thm)],[f22289,f22459,f540]) ).
fof(f22463,definition,
! [X0] :
( sQ582_spl
<=> ( app(app(sk5,nil),skaf52(X0)) = app(sk5,skaf52(X0))
| ~ ssList(skaf52(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f22466,plain,
( ~ sQ8_spl
| sQ582_spl ),
inference(split_clause,[status(thm)],[f22290,f22463,f540]) ).
fof(f22467,definition,
! [X0] :
( sQ583_spl
<=> ( app(app(sk5,nil),skaf53(X0)) = app(sk5,skaf53(X0))
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ583_spl])],[split_symbol_definition]) ).
fof(f22470,plain,
( ~ sQ8_spl
| sQ583_spl ),
inference(split_clause,[status(thm)],[f22291,f22467,f540]) ).
fof(f22471,definition,
! [X0] :
( sQ584_spl
<=> ( app(app(sk5,nil),skaf56(X0)) = app(sk5,skaf56(X0))
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition]) ).
fof(f22474,plain,
( ~ sQ8_spl
| sQ584_spl ),
inference(split_clause,[status(thm)],[f22292,f22471,f540]) ).
fof(f22475,definition,
! [X0] :
( sQ585_spl
<=> ( app(app(sk5,nil),skaf57(X0)) = app(sk5,skaf57(X0))
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition]) ).
fof(f22478,plain,
( ~ sQ8_spl
| sQ585_spl ),
inference(split_clause,[status(thm)],[f22293,f22475,f540]) ).
fof(f22479,definition,
! [X0] :
( sQ586_spl
<=> ( app(app(sk5,nil),skaf58(X0)) = app(sk5,skaf58(X0))
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f22482,plain,
( ~ sQ8_spl
| sQ586_spl ),
inference(split_clause,[status(thm)],[f22294,f22479,f540]) ).
fof(f22483,definition,
! [X0] :
( sQ587_spl
<=> ( app(app(sk5,nil),skaf61(X0)) = app(sk5,skaf61(X0))
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ587_spl])],[split_symbol_definition]) ).
fof(f22486,plain,
( ~ sQ8_spl
| sQ587_spl ),
inference(split_clause,[status(thm)],[f22295,f22483,f540]) ).
fof(f22487,definition,
! [X0] :
( sQ588_spl
<=> ( app(app(sk5,nil),skaf62(X0)) = app(sk5,skaf62(X0))
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition]) ).
fof(f22490,plain,
( ~ sQ8_spl
| sQ588_spl ),
inference(split_clause,[status(thm)],[f22296,f22487,f540]) ).
fof(f22491,definition,
! [X0] :
( sQ589_spl
<=> ( app(app(sk5,nil),skaf63(X0)) = app(sk5,skaf63(X0))
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition]) ).
fof(f22494,plain,
( ~ sQ8_spl
| sQ589_spl ),
inference(split_clause,[status(thm)],[f22297,f22491,f540]) ).
fof(f22495,definition,
! [X0] :
( sQ590_spl
<=> ( app(app(sk5,nil),skaf66(X0)) = app(sk5,skaf66(X0))
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ590_spl])],[split_symbol_definition]) ).
fof(f22498,plain,
( ~ sQ8_spl
| sQ590_spl ),
inference(split_clause,[status(thm)],[f22298,f22495,f540]) ).
fof(f22499,definition,
! [X0] :
( sQ591_spl
<=> ( app(app(sk5,nil),skaf67(X0)) = app(sk5,skaf67(X0))
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition]) ).
fof(f22502,plain,
( ~ sQ8_spl
| sQ591_spl ),
inference(split_clause,[status(thm)],[f22299,f22499,f540]) ).
fof(f22503,definition,
! [X0] :
( sQ592_spl
<=> ( app(app(sk5,nil),skaf68(X0)) = app(sk5,skaf68(X0))
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition]) ).
fof(f22506,plain,
( ~ sQ8_spl
| sQ592_spl ),
inference(split_clause,[status(thm)],[f22300,f22503,f540]) ).
fof(f22507,definition,
! [X0] :
( sQ593_spl
<=> ( app(app(sk5,nil),skaf71(X0)) = app(sk5,skaf71(X0))
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ593_spl])],[split_symbol_definition]) ).
fof(f22510,plain,
( ~ sQ8_spl
| sQ593_spl ),
inference(split_clause,[status(thm)],[f22301,f22507,f540]) ).
fof(f22511,definition,
! [X0] :
( sQ594_spl
<=> ( app(app(sk5,nil),skaf72(X0)) = app(sk5,skaf72(X0))
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ594_spl])],[split_symbol_definition]) ).
fof(f22514,plain,
( ~ sQ8_spl
| sQ594_spl ),
inference(split_clause,[status(thm)],[f22302,f22511,f540]) ).
fof(f22515,definition,
! [X0] :
( sQ595_spl
<=> ( app(app(sk5,nil),skaf73(X0)) = app(sk5,skaf73(X0))
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition]) ).
fof(f22518,plain,
( ~ sQ8_spl
| sQ595_spl ),
inference(split_clause,[status(thm)],[f22303,f22515,f540]) ).
fof(f22519,definition,
! [X0] :
( sQ596_spl
<=> ( app(app(sk5,nil),skaf75(X0)) = app(sk5,skaf75(X0))
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition]) ).
fof(f22522,plain,
( ~ sQ8_spl
| sQ596_spl ),
inference(split_clause,[status(thm)],[f22304,f22519,f540]) ).
fof(f22523,definition,
! [X0] :
( sQ597_spl
<=> ( app(app(sk5,nil),skaf76(X0)) = app(sk5,skaf76(X0))
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ597_spl])],[split_symbol_definition]) ).
fof(f22526,plain,
( ~ sQ8_spl
| sQ597_spl ),
inference(split_clause,[status(thm)],[f22305,f22523,f540]) ).
fof(f22527,definition,
! [X0] :
( sQ598_spl
<=> ( app(app(sk5,nil),skaf77(X0)) = app(sk5,skaf77(X0))
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ598_spl])],[split_symbol_definition]) ).
fof(f22530,plain,
( ~ sQ8_spl
| sQ598_spl ),
inference(split_clause,[status(thm)],[f22306,f22527,f540]) ).
fof(f22531,definition,
! [X0] :
( sQ599_spl
<=> ( app(app(sk5,nil),skaf80(X0)) = app(sk5,skaf80(X0))
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ599_spl])],[split_symbol_definition]) ).
fof(f22534,plain,
( ~ sQ8_spl
| sQ599_spl ),
inference(split_clause,[status(thm)],[f22307,f22531,f540]) ).
fof(f22535,definition,
! [X0] :
( sQ600_spl
<=> ( app(app(sk5,nil),skaf82(X0)) = app(sk5,skaf82(X0))
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition]) ).
fof(f22538,plain,
( ~ sQ8_spl
| sQ600_spl ),
inference(split_clause,[status(thm)],[f22308,f22535,f540]) ).
fof(f22539,definition,
! [X0] :
( sQ601_spl
<=> ( app(app(sk5,nil),skaf81(X0)) = app(sk5,skaf81(X0))
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition]) ).
fof(f22542,plain,
( ~ sQ8_spl
| sQ601_spl ),
inference(split_clause,[status(thm)],[f22309,f22539,f540]) ).
fof(f22543,definition,
( sQ602_spl
<=> app(app(sk5,nil),sk1) = app(sk5,sk1) ),
introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition]) ).
fof(f22546,plain,
( sQ602_spl
| ~ sQ8_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f22310,f596,f540,f22543]) ).
fof(f22547,definition,
( sQ603_spl
<=> app(app(sk5,nil),nil) = app(sk5,nil) ),
introduced(definition,[new_symbols(definition,[sQ603_spl])],[split_symbol_definition]) ).
fof(f22550,plain,
( sQ603_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22311,f540,f22547]) ).
fof(f22551,definition,
( sQ604_spl
<=> app(app(sk5,sk1),sk5) = app(sk5,sk2) ),
introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition]) ).
fof(f22554,plain,
( sQ604_spl
| ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f22312,f587,f596,f22551]) ).
fof(f22555,definition,
( sQ605_spl
<=> app(app(sk5,sk1),nil) = app(sk5,sk1) ),
introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition]) ).
fof(f22558,plain,
( sQ605_spl
| ~ sQ11_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22313,f540,f596,f22555]) ).
fof(f22586,plain,
! [X0] :
( nil = skaf76(X0)
| ~ ssList(nil)
| skaf76(X0) != nil ),
inference(paramodulation,[status(thm)],[f527,f863]) ).
fof(f22587,definition,
! [X0] :
( sQ606_spl
<=> ( nil = skaf76(X0)
| skaf76(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ606_spl])],[split_symbol_definition]) ).
fof(f22590,plain,
( ~ sQ8_spl
| sQ606_spl ),
inference(split_clause,[status(thm)],[f22586,f22587,f540]) ).
fof(f22591,plain,
! [X0] :
( nil = skaf77(X0)
| ~ ssList(nil)
| skaf77(X0) != nil ),
inference(paramodulation,[status(thm)],[f525,f864]) ).
fof(f22592,definition,
! [X0] :
( sQ607_spl
<=> ( nil = skaf77(X0)
| skaf77(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition]) ).
fof(f22595,plain,
( ~ sQ8_spl
| sQ607_spl ),
inference(split_clause,[status(thm)],[f22591,f22592,f540]) ).
fof(f22596,plain,
! [X0] :
( nil = skaf80(X0)
| ~ ssList(nil)
| skaf80(X0) != nil ),
inference(paramodulation,[status(thm)],[f523,f865]) ).
fof(f22597,definition,
! [X0] :
( sQ608_spl
<=> ( nil = skaf80(X0)
| skaf80(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition]) ).
fof(f22600,plain,
( ~ sQ8_spl
| sQ608_spl ),
inference(split_clause,[status(thm)],[f22596,f22597,f540]) ).
fof(f22601,plain,
! [X0] :
( nil = skaf81(X0)
| ~ ssList(nil)
| skaf81(X0) != nil ),
inference(paramodulation,[status(thm)],[f518,f866]) ).
fof(f22602,definition,
! [X0] :
( sQ609_spl
<=> ( nil = skaf81(X0)
| skaf81(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition]) ).
fof(f22605,plain,
( ~ sQ8_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f22601,f22602,f540]) ).
fof(f22606,plain,
! [X0] :
( nil = skaf82(X0)
| ~ ssList(nil)
| skaf82(X0) != nil ),
inference(paramodulation,[status(thm)],[f519,f867]) ).
fof(f22607,definition,
! [X0] :
( sQ610_spl
<=> ( nil = skaf82(X0)
| skaf82(X0) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition]) ).
fof(f22610,plain,
( ~ sQ8_spl
| sQ610_spl ),
inference(split_clause,[status(thm)],[f22606,f22607,f540]) ).
fof(f22950,plain,
! [X0] :
( ~ sQ66_spl
| app(app(skaf47(app(sk1,X0),sk1),sk1),skaf48(sk1,app(sk1,X0))) = app(sk1,X0)
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1805,f399]) ).
fof(f22951,plain,
! [X0,X1,X2] :
( ~ sQ66_spl
| segmentP(app(app(X2,app(sk1,X0)),X1),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1805,f405]) ).
fof(f22952,plain,
! [X0,X1] :
( ~ sQ66_spl
| segmentP(X1,sk1)
| ~ ssList(X1)
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ segmentP(X1,app(sk1,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1805,f375]) ).
fof(f22953,plain,
! [X0] :
( ~ sQ66_spl
| app(sk1,X0) = sk1
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ segmentP(sk1,app(sk1,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1805,f340]) ).
fof(f22954,plain,
( ~ sQ66_spl
| segmentP(sk2,sk1)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f608,f1805]) ).
fof(f22955,plain,
( ~ sQ66_spl
| segmentP(sk1,sk1)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f517,f1805]) ).
fof(f22956,definition,
! [X0] :
( sQ611_spl
<=> ( app(app(skaf47(app(sk1,X0),sk1),sk1),skaf48(sk1,app(sk1,X0))) = app(sk1,X0)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition]) ).
fof(f22959,plain,
( ~ sQ66_spl
| ~ sQ11_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f22950,f22956,f596,f1789]) ).
fof(f22960,definition,
! [X0,X1,X2] :
( sQ612_spl
<=> ( segmentP(app(app(X2,app(sk1,X0)),X1),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f22963,plain,
( ~ sQ66_spl
| ~ sQ11_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f22951,f22960,f596,f1789]) ).
fof(f22964,definition,
! [X0,X1] :
( sQ613_spl
<=> ( segmentP(X1,sk1)
| ~ ssList(X1)
| ~ ssList(app(sk1,X0))
| ~ segmentP(X1,app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f22967,plain,
( ~ sQ66_spl
| ~ sQ11_spl
| sQ613_spl ),
inference(split_clause,[status(thm)],[f22952,f22964,f596,f1789]) ).
fof(f22968,definition,
! [X0] :
( sQ614_spl
<=> ( app(sk1,X0) = sk1
| ~ ssList(app(sk1,X0))
| ~ segmentP(sk1,app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f22971,plain,
( ~ sQ66_spl
| ~ sQ11_spl
| sQ614_spl ),
inference(split_clause,[status(thm)],[f22953,f22968,f596,f1789]) ).
fof(f22972,plain,
( ~ sQ66_spl
| sQ21_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f22954,f587,f804,f1789]) ).
fof(f22973,plain,
( ~ sQ66_spl
| sQ82_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f22955,f540,f2064,f1789]) ).
fof(f22974,plain,
$false,
inference(sat_refutation,[status(thm)],[f460,f471,f475,f546,f549,f590,f599,f613,f667,f676,f680,f739,f746,f807,f821,f824,f1008,f1410,f1460,f1463,f1537,f1538,f1618,f1622,f1626,f1732,f1736,f1740,f1744,f1748,f1752,f1756,f1760,f1764,f1768,f1772,f1776,f1780,f1784,f1788,f1792,f1796,f1800,f1872,f1879,f1885,f1891,f1898,f2060,f2098,f2123,f2130,f2423,f2427,f2431,f2435,f2439,f2443,f2447,f2451,f2550,f2558,f2562,f2658,f2666,f2670,f2682,f2709,f2734,f2740,f2744,f2756,f2764,f2768,f2780,f2788,f2792,f2804,f2812,f2816,f2828,f2836,f2840,f2847,f2854,f2887,f2898,f2906,f2910,f2977,f3003,f3009,f3017,f3127,f3131,f3159,f3187,f3207,f3215,f3219,f3247,f3275,f3281,f3290,f3294,f3298,f3373,f3402,f3544,f3574,f3585,f3593,f3597,f3609,f3617,f3621,f3633,f3795,f3799,f3811,f3819,f3823,f3835,f3843,f3847,f3932,f3966,f4035,f4146,f4172,f4180,f4345,f4403,f4439,f4665,f4669,f4673,f4677,f4755,f4759,f4763,f4767,f4790,f5387,f6793,f8992,f9002,f9086,f9216,f9519,f9791,f10081,f10090,f10167,f10242,f10248,f10252,f13426,f13496,f14456,f15159,f15163,f17934,f17938,f17942,f17946,f17950,f17954,f18259,f18263,f18267,f18271,f18275,f18279,f18291,f18295,f18299,f18303,f18307,f18311,f18315,f18319,f18323,f18327,f18331,f18335,f18339,f18343,f18347,f18351,f18355,f18359,f18363,f18367,f18371,f18657,f19698,f19752,f19888,f19893,f20294,f20560,f20565,f20570,f21010,f21074,f21078,f21953,f21958,f21963,f21968,f21973,f22096,f22101,f22106,f22111,f22116,f22317,f22321,f22325,f22329,f22333,f22337,f22342,f22346,f22350,f22354,f22358,f22362,f22366,f22370,f22374,f22378,f22382,f22386,f22390,f22394,f22398,f22402,f22406,f22410,f22414,f22418,f22422,f22426,f22430,f22434,f22438,f22442,f22446,f22450,f22454,f22458,f22462,f22466,f22470,f22474,f22478,f22482,f22486,f22490,f22494,f22498,f22502,f22506,f22510,f22514,f22518,f22522,f22526,f22530,f22534,f22538,f22542,f22546,f22550,f22554,f22558,f22590,f22595,f22600,f22605,f22610,f22959,f22963,f22967,f22971,f22972,f22973]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC065-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:52:19 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 18.94/2.85 % Refutation found
% 18.94/2.85 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.94/2.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.17/2.90 % Elapsed time: 2.530495 seconds
% 10.17/2.90 % CPU time: 19.548287 seconds
% 10.17/2.90 % Total memory used: 280.607 MB
% 10.17/2.90 % Net memory used: 268.007 MB
%------------------------------------------------------------------------------