%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC183-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:40:18 PM UTC 2026
% Result : Unsatisfiable 33.38s 19.80s
% Output : CNFRefutation 32.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 330
% Syntax : Number of formulae : 1174 ( 99 unt; 236 def)
% Number of atoms : 4048 ( 479 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 5440 (2566 ~;2638 |; 0 &)
% ( 236 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 254 ( 252 usr; 237 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 8 con; 0-2 aty)
% Number of variables : 767 ( 767 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f20,axiom,
! [U] : ssList(skaf75(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [U] : ssItem(skaf74(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] : ssList(skaf73(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] : ssItem(skaf70(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [U] : ssList(skaf68(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U] : ssItem(skaf65(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [U] : ssList(skaf63(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [U] : ssItem(skaf60(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] : ssList(skaf58(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [U] : ssList(skaf56(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [U] : ssItem(skaf55(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] : ssList(skaf53(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U] : ssItem(skaf50(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U] : ssItem(skaf44(U)),
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(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ 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(f59,axiom,
! [U] :
( rearsegP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [U] :
( frontsegP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [U] :
( ~ ssItem(U)
| ~ lt(U,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [U] :
( equalelemsP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [U] :
( duplicatefreeP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [U] :
( strictorderedP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [U] :
( totalorderedP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [U] :
( strictorderP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [U] :
( totalorderP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [U] :
( cyclefreeP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [U,V] :
( ssItem(V)
| duplicatefreeP(U)
| ~ ssList(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(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [U,V] :
( hd(cons(U,V)) = U
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [U] :
( cons(skaf44(U),nil) = U
| ~ ssList(U)
| ~ singletonP(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f120,axiom,
! [U,V] :
( app(cons(U,nil),V) = cons(U,V)
| ~ ssList(V)
| ~ ssItem(U) ),
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(f136,axiom,
! [U,V,W] :
( rearsegP(app(W,U),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [U,V,W] :
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W] :
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [U] :
( app(skaf80(U),cons(skaf78(U),cons(skaf79(U),skaf81(U)))) = U
| equalelemsP(U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [U,V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != W ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [U,V,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
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(f157,axiom,
! [U,V,W] :
( cons(U,app(V,W)) = app(cons(U,V),W)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [U,V,W] :
( memberP(U,W)
| memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [U,V,W] :
( W = U
| memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
! [U,V] :
( app(app(skaf47(U,V),V),skaf48(V,U)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
! [U,V,W,X] :
( U = W
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [U,V,W,X] :
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [U,V,W,X] :
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [U,V,W,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [U,V,W,X,Y] :
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( memberP(sk7,sk5)
| memberP(sk6,sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
( nil = sk4
| ssItem(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
( nil = sk3
| ssItem(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
( nil = sk4
| cons(sk8,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( nil = sk3
| cons(sk8,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
( nil = sk3
| memberP(sk4,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,negated_conjecture,
! [A] :
( nil = sk3
| ~ leq(sk8,A)
| ~ memberP(sk4,A)
| sk8 = A
| ~ ssItem(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f212,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f216,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f217,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f219,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f222,plain,
! [X0] : ssList(skaf77(X0)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f224,plain,
! [X0] : ssList(skaf75(X0)),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f225,plain,
! [X0] : ssItem(skaf74(X0)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f226,plain,
! [X0] : ssList(skaf73(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f229,plain,
! [X0] : ssItem(skaf70(X0)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f231,plain,
! [X0] : ssList(skaf68(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f234,plain,
! [X0] : ssItem(skaf65(X0)),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f236,plain,
! [X0] : ssList(skaf63(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f239,plain,
! [X0] : ssItem(skaf60(X0)),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f241,plain,
! [X0] : ssList(skaf58(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f243,plain,
! [X0] : ssList(skaf56(X0)),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f244,plain,
! [X0] : ssItem(skaf55(X0)),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f246,plain,
! [X0] : ssList(skaf53(X0)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f249,plain,
! [X0] : ssItem(skaf50(X0)),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f251,plain,
! [X0] : ssItem(skaf44(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f254,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f255,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f260,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f262,plain,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f263,plain,
! [X0] :
( rearsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f264,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f265,plain,
! [X0] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f267,plain,
! [X0] :
( ~ ssItem(X0)
| ~ lt(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f268,plain,
! [X0] :
( equalelemsP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f269,plain,
! [X0] :
( duplicatefreeP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f270,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f271,plain,
! [X0] :
( totalorderedP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f272,plain,
! [X0] :
( strictorderP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f273,plain,
! [X0] :
( totalorderP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f274,plain,
! [X0] :
( cyclefreeP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f275,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f276,plain,
( ! [V] : ssItem(V)
| ! [U] :
( duplicatefreeP(U)
| ~ ssList(U) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f277,plain,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f278,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f279,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f280,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f281,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f290,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f291,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f302,plain,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f303,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f304,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f305,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f306,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f308,plain,
! [X0] :
( cons(skaf44(X0),nil) = X0
| ~ ssList(X0)
| ~ singletonP(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f311,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f331,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f332,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f333,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f334,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f335,plain,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f338,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f344,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f345,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f346,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f348,plain,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f349,plain,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f355,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(f356,plain,
! [X0,X1,X2] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f357,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f359,plain,
! [X0,X1,X2] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f360,plain,
! [X0,X1,X2] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f361,plain,
! [X0] :
( app(skaf80(X0),cons(skaf78(X0),cons(skaf79(X0),skaf81(X0)))) = X0
| equalelemsP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f362,plain,
! [V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f363,plain,
! [X0,X1,X2] :
( rearsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f364,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f365,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f373,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(f374,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f375,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f377,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,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(f379,plain,
! [X0,X1,X2] :
( segmentP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f380,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(f381,plain,
! [X0,X1,X2] :
( rearsegP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X1,X2)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f382,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(f383,plain,
! [X0,X1,X2] :
( frontsegP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f388,plain,
! [X0,X1,X2] :
( cons(X0,app(X1,X2)) = app(cons(X0,X1),X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f389,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(f390,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)],[f389]) ).
fof(f395,plain,
! [U,W] :
( W = U
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f396,plain,
! [X0,X1,X2] :
( X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f403,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,
! [U,W] :
( U = W
| ! [V] :
( ~ ssList(V)
| ! [X] :
( ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f406,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| cons(X0,X1) != cons(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f405]) ).
fof(f407,plain,
! [V,X] :
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ! [U] :
( ~ ssItem(U)
| ! [W] :
( ~ ssItem(W)
| cons(U,V) != cons(W,X) ) ) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f408,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| cons(X0,X1) != cons(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f409,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(f410,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(f411,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)],[f410]) ).
fof(f414,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(f415,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)],[f414]) ).
fof(f421,plain,
! [Y] :
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [X] :
( ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ) ) ) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f422,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(X4)
| ~ duplicatefreeP(X4)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3)
| app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4 ),
inference(cnf_transformation,[status(thm)],[f421]) ).
fof(f437,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f438,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f440,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f441,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f442,plain,
ssList(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f443,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f444,plain,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f445,plain,
( memberP(sk7,sk5)
| memberP(sk6,sk5) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f446,plain,
( nil = sk4
| ssItem(sk8) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f447,plain,
( nil = sk3
| ssItem(sk8) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f448,plain,
( nil = sk4
| cons(sk8,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f452,plain,
( nil = sk3
| cons(sk8,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f453,plain,
( nil = sk3
| memberP(sk4,sk8) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f454,plain,
( nil = sk3
| ! [A] :
( ~ leq(sk8,A)
| ~ memberP(sk4,A)
| sk8 = A
| ~ ssItem(A) ) ),
inference(miniscoping,[status(thm)],[f204]) ).
fof(f455,plain,
! [X0] :
( nil = sk3
| ~ leq(sk8,X0)
| ~ memberP(sk4,X0)
| sk8 = X0
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f456,definition,
! [X0] :
( sQ0_spl
<=> ( duplicatefreeP(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f457,plain,
! [X0] :
( ~ sQ0_spl
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
! [X1] :
( sQ1_spl
<=> ssItem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f460,plain,
! [X0] :
( ~ sQ1_spl
| ssItem(X0) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f277,f456,f459]) ).
fof(f463,definition,
( sQ2_spl
<=> memberP(sk6,sk5) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( ~ sQ2_spl
| memberP(sk6,sk5) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f465,plain,
( sQ2_spl
| ~ memberP(sk6,sk5) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,definition,
( sQ3_spl
<=> memberP(sk7,sk5) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ3_spl
| memberP(sk7,sk5) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f445,f463,f466]) ).
fof(f470,definition,
( sQ4_spl
<=> ssItem(sk8) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( sQ4_spl
| ~ ssItem(sk8) ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,definition,
( sQ5_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( ~ sQ5_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f446,f470,f473]) ).
fof(f477,definition,
( sQ6_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( ~ sQ6_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f479,plain,
( sQ6_spl
| nil != sk3 ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,plain,
( sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f447,f470,f477]) ).
fof(f481,definition,
( sQ7_spl
<=> cons(sk8,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f482,plain,
( ~ sQ7_spl
| cons(sk8,nil) = sk3 ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f484,plain,
( sQ5_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f448,f481,f473]) ).
fof(f485,definition,
( sQ8_spl
<=> memberP(sk4,sk8) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f489,definition,
! [X0] :
( sQ9_spl
<=> ( ~ leq(sk8,X0)
| ~ memberP(sk4,X0)
| sk8 = X0
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ6_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f452,f481,f477]) ).
fof(f494,plain,
( sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f453,f485,f477]) ).
fof(f495,plain,
( sQ6_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f455,f489,f477]) ).
fof(f508,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f357]) ).
fof(f509,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f508]) ).
fof(f510,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f363]) ).
fof(f511,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f510,f290]) ).
fof(f512,plain,
! [X1,X0] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f365]) ).
fof(f513,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f512,f290]) ).
fof(f516,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)],[f411]) ).
fof(f517,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)],[f415]) ).
fof(f520,plain,
! [X0,X1,X2,X3] :
( ~ ssList(app(app(X2,cons(X3,X1)),cons(X3,X0)))
| ~ duplicatefreeP(app(app(X2,cons(X3,X1)),cons(X3,X0)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f422]) ).
fof(f529,plain,
app(app(sk6,cons(sk5,nil)),sk7) = sk3,
inference(forward_demodulation,[status(thm)],[f440,f444]) ).
fof(f575,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sk4 = sk3 ),
inference(backward_demodulation,[status(thm)],[f474,f478]) ).
fof(f576,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(app(X2,cons(X3,X1)),cons(X3,X0)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f520,f457]) ).
fof(f632,definition,
( sQ10_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( sQ10_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f639,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f634,f438]) ).
fof(f640,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f639]) ).
fof(f655,definition,
( sQ12_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ12_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f659,definition,
( sQ13_spl
<=> memberP(sk3,sk8) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( ~ sQ13_spl
| memberP(sk3,sk8) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f663,definition,
( sQ14_spl
<=> sk3 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f437]) ).
fof(f669,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f668]) ).
fof(f754,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ ssList(X0)
| ~ ssList(X1)
| duplicatefreeP(app(X0,X1)) ),
inference(resolution,[status(thm)],[f457,f290]) ).
fof(f786,plain,
( ~ sQ7_spl
| memberP(sk3,sk8)
| ~ ssItem(sk8)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f482,f509]) ).
fof(f789,definition,
! [X0] :
( sQ17_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f792,definition,
( sQ18_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f794,plain,
( sQ18_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f792]) ).
fof(f796,plain,
( ~ sQ7_spl
| sQ13_spl
| ~ sQ4_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f786,f792,f470,f659,f481]) ).
fof(f950,plain,
! [X0,X1] :
( X0 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f375]) ).
fof(f956,definition,
! [X0] :
( sQ24_spl
<=> ( X0 = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f959,definition,
! [X1] :
( sQ25_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f960,plain,
! [X0] :
( ~ sQ25_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f962,plain,
( sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f950,f956,f959]) ).
fof(f973,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f212,f794]) ).
fof(f974,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f973]) ).
fof(f982,definition,
( sQ27_spl
<=> duplicatefreeP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1236,definition,
( sQ29_spl
<=> sk8 = sk8 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1241,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(nil,X0))
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f279,f375]) ).
fof(f1243,definition,
! [X0] :
( sQ30_spl
<=> ( app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(nil,X0))
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1246,plain,
( ~ sQ18_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1241,f1243,f792]) ).
fof(f1249,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(X0,nil))
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f278,f377]) ).
fof(f1251,definition,
! [X0] :
( sQ31_spl
<=> ( app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil))
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1254,plain,
( ~ sQ18_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1249,f1251,f792]) ).
fof(f1259,plain,
( sk3 = app(sk6,app(cons(sk5,nil),sk7))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f529,f373]) ).
fof(f1260,plain,
! [X0] :
( X0 = app(sk6,cons(sk5,nil))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ ssList(X0)
| app(X0,sk7) != sk3 ),
inference(paramodulation,[status(thm)],[f529,f377]) ).
fof(f1262,plain,
! [X0] :
( X0 = sk7
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(X0)
| app(app(sk6,cons(sk5,nil)),X0) != sk3 ),
inference(paramodulation,[status(thm)],[f529,f375]) ).
fof(f1264,plain,
! [X0] :
( app(sk3,X0) = app(app(sk6,cons(sk5,nil)),app(sk7,X0))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f529,f373]) ).
fof(f1265,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f529,f513]) ).
fof(f1266,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(paramodulation,[status(thm)],[f529,f511]) ).
fof(f1268,definition,
( sQ32_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1270,plain,
( sQ32_spl
| ~ ssList(sk7) ),
inference(component_clause,[status(thm)],[f1268]) ).
fof(f1271,definition,
( sQ33_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1273,plain,
( sQ33_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f1271]) ).
fof(f1274,definition,
( sQ34_spl
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1276,plain,
( sQ34_spl
| ~ ssList(sk6) ),
inference(component_clause,[status(thm)],[f1274]) ).
fof(f1277,definition,
( sQ35_spl
<=> sk3 = app(sk6,app(cons(sk5,nil),sk7)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1278,plain,
( ~ sQ35_spl
| sk3 = app(sk6,app(cons(sk5,nil),sk7)) ),
inference(component_clause,[status(thm)],[f1277]) ).
fof(f1280,plain,
( sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1259,f1268,f1271,f1274,f1277]) ).
fof(f1281,definition,
! [X0] :
( sQ36_spl
<=> ( X0 = app(sk6,cons(sk5,nil))
| ~ ssList(X0)
| app(X0,sk7) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1284,definition,
( sQ37_spl
<=> ssList(app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1286,plain,
( sQ37_spl
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f1284]) ).
fof(f1287,plain,
( ~ sQ37_spl
| ~ sQ32_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1260,f1281,f1268,f1284]) ).
fof(f1289,definition,
! [X0] :
( sQ38_spl
<=> ( X0 = sk7
| ~ ssList(X0)
| app(app(sk6,cons(sk5,nil)),X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1292,plain,
( ~ sQ32_spl
| ~ sQ37_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1262,f1289,f1284,f1268]) ).
fof(f1294,definition,
! [X0] :
( sQ39_spl
<=> ( app(sk3,X0) = app(app(sk6,cons(sk5,nil)),app(sk7,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1297,plain,
( ~ sQ37_spl
| ~ sQ32_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1264,f1294,f1268,f1284]) ).
fof(f1298,definition,
( sQ40_spl
<=> frontsegP(sk3,app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1299,plain,
( ~ sQ40_spl
| frontsegP(sk3,app(sk6,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f1298]) ).
fof(f1301,plain,
( sQ40_spl
| ~ sQ37_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1265,f1268,f1284,f1298]) ).
fof(f1302,definition,
( sQ41_spl
<=> rearsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( ~ sQ41_spl
| rearsegP(sk3,sk7) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1305,plain,
( sQ41_spl
| ~ sQ32_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f1266,f1284,f1268,f1302]) ).
fof(f1307,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1270,f443]) ).
fof(f1308,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1307]) ).
fof(f1311,plain,
( nil = sk7
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f529,f334]) ).
fof(f1312,definition,
( sQ42_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1317,definition,
( sQ43_spl
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1318,plain,
( ~ sQ43_spl
| nil = sk7 ),
inference(component_clause,[status(thm)],[f1317]) ).
fof(f1320,plain,
( sQ43_spl
| ~ sQ37_spl
| ~ sQ32_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1311,f477,f1268,f1284,f1317]) ).
fof(f1325,plain,
! [X0] :
( ~ sQ43_spl
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(backward_demodulation,[status(thm)],[f1318,f275]) ).
fof(f1329,plain,
( ~ sQ35_spl
| ~ sQ43_spl
| sk3 = app(sk6,app(cons(sk5,sk7),sk7)) ),
inference(backward_demodulation,[status(thm)],[f1318,f1278]) ).
fof(f1381,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(X1,X0) = X0
| ~ ssList(app(X1,X0))
| ~ ssList(X0)
| ~ rearsegP(X0,app(X1,X0)) ),
inference(resolution,[status(thm)],[f345,f511]) ).
fof(f1383,plain,
! [X0,X1] :
( ~ ssList(X1)
| app(X1,X0) = X0
| ~ ssList(app(X1,X0))
| ~ ssList(X0)
| ~ rearsegP(X0,app(X1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1381]) ).
fof(f1384,plain,
! [X0,X1] :
( ~ ssList(X1)
| app(X1,X0) = X0
| ~ ssList(X0)
| ~ rearsegP(X0,app(X1,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1383,f290]) ).
fof(f1389,plain,
! [X0,X1] :
( skaf46(app(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(skaf46(app(X0,X1),X1))
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ rearsegP(app(X0,X1),X1) ),
inference(resolution,[status(thm)],[f348,f377]) ).
fof(f1391,plain,
! [X0,X1] :
( skaf46(app(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(skaf46(app(X0,X1),X1))
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ rearsegP(app(X0,X1),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1389]) ).
fof(f1392,plain,
! [X0,X1] :
( skaf46(app(X1,X0),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf46(app(X1,X0),X0))
| ~ ssList(app(X1,X0))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1391,f511]) ).
fof(f1395,definition,
( sQ44_spl
<=> rearsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1406,plain,
( sQ37_spl
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f1286,f290]) ).
fof(f1407,plain,
( sQ37_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1406,f1271,f1274,f1284]) ).
fof(f1408,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1276,f442]) ).
fof(f1409,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1408]) ).
fof(f1422,plain,
( sQ33_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f291,f1273]) ).
fof(f1424,definition,
( sQ46_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1426,plain,
( sQ46_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f1424]) ).
fof(f1427,plain,
( sQ33_spl
| ~ sQ18_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1422,f1424,f792,f1271]) ).
fof(f1429,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1426,f441]) ).
fof(f1430,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f1429]) ).
fof(f1435,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0) ),
inference(resolution,[status(thm)],[f349,f375]) ).
fof(f1437,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1435]) ).
fof(f1438,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(app(X0,X1))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1437,f513]) ).
fof(f1440,plain,
! [X0,X1,X2] :
( app(X2,X0) = X1
| ~ ssList(app(X2,X0))
| ~ ssList(X1)
| ~ rearsegP(X1,app(X2,X0))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X0,X1) ),
inference(resolution,[status(thm)],[f355,f345]) ).
fof(f1441,plain,
! [X0,X1,X2] :
( app(X2,X0) = X1
| ~ ssList(app(X2,X0))
| ~ rearsegP(X1,app(X2,X0))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1440]) ).
fof(f1442,plain,
! [X0,X1,X2] :
( app(X2,X0) = X1
| ~ rearsegP(X1,app(X2,X0))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1441,f290]) ).
fof(f1443,plain,
! [X0,X1,X2] :
( app(X0,X2) = X1
| ~ ssList(app(X0,X2))
| ~ ssList(X1)
| ~ frontsegP(X1,app(X0,X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(resolution,[status(thm)],[f356,f346]) ).
fof(f1444,plain,
! [X0,X1,X2] :
( app(X0,X2) = X1
| ~ ssList(app(X0,X2))
| ~ frontsegP(X1,app(X0,X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1443]) ).
fof(f1445,plain,
! [X0,X1,X2] :
( app(X0,X2) = X1
| ~ frontsegP(X1,app(X0,X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1444,f290]) ).
fof(f1455,definition,
( sQ49_spl
<=> frontsegP(sk6,sk3) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1466,definition,
( sQ50_spl
<=> frontsegP(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1467,plain,
( ~ sQ50_spl
| frontsegP(sk3,sk3) ),
inference(component_clause,[status(thm)],[f1466]) ).
fof(f1468,plain,
( sQ50_spl
| ~ frontsegP(sk3,sk3) ),
inference(component_clause,[status(thm)],[f1466]) ).
fof(f1470,plain,
( sQ50_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f1468,f265]) ).
fof(f1471,plain,
( sQ50_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1470,f655,f1466]) ).
fof(f1472,plain,
( ~ sQ50_spl
| sk3 = sk3
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ frontsegP(sk3,sk3) ),
inference(resolution,[status(thm)],[f1467,f346]) ).
fof(f1473,plain,
( sQ14_spl
| ~ sQ12_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1472,f1466,f655,f663]) ).
fof(f1475,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(X0)
| ~ ssList(sk7)
| ~ frontsegP(app(sk6,cons(sk5,nil)),X0) ),
inference(paramodulation,[status(thm)],[f529,f356]) ).
fof(f1476,plain,
! [X0] :
( rearsegP(sk3,X0)
| ~ ssList(sk7)
| ~ ssList(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ rearsegP(sk7,X0) ),
inference(paramodulation,[status(thm)],[f529,f355]) ).
fof(f1477,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(paramodulation,[status(thm)],[f529,f359]) ).
fof(f1478,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(sk7,X0) ),
inference(paramodulation,[status(thm)],[f529,f360]) ).
fof(f1479,plain,
( ~ sQ0_spl
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| duplicatefreeP(sk3) ),
inference(paramodulation,[status(thm)],[f529,f754]) ).
fof(f1489,definition,
! [X0] :
( sQ51_spl
<=> ( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(app(sk6,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1492,plain,
( ~ sQ37_spl
| ~ sQ32_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1475,f1489,f1268,f1284]) ).
fof(f1493,definition,
! [X0] :
( sQ52_spl
<=> ( rearsegP(sk3,X0)
| ~ ssList(X0)
| ~ rearsegP(sk7,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1496,plain,
( ~ sQ32_spl
| ~ sQ37_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1476,f1493,f1284,f1268]) ).
fof(f1497,definition,
! [X0] :
( sQ53_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1500,plain,
( ~ sQ37_spl
| ~ sQ32_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1477,f1497,f1268,f1284]) ).
fof(f1501,definition,
! [X0] :
( sQ54_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1502,plain,
! [X0] :
( ~ sQ54_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(component_clause,[status(thm)],[f1501]) ).
fof(f1504,plain,
( ~ sQ37_spl
| ~ sQ32_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1478,f1501,f1268,f1284]) ).
fof(f1505,plain,
( ~ sQ0_spl
| ~ sQ37_spl
| ~ sQ32_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1479,f982,f1268,f1284,f456]) ).
fof(f1523,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(X0)
| ~ rearsegP(nil,X0)
| nil = X0
| ~ ssList(skaf46(nil,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f334,f348]) ).
fof(f1524,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(nil,X0)
| nil = skaf45(nil,X0)
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0)) ),
inference(resolution,[status(thm)],[f334,f349]) ).
fof(f1528,definition,
! [X0] :
( sQ55_spl
<=> ( ~ ssList(X0)
| ~ rearsegP(nil,X0)
| nil = X0
| ~ ssList(skaf46(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1531,plain,
( ~ sQ18_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1523,f1528,f792]) ).
fof(f1532,definition,
! [X0] :
( sQ56_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(nil,X0)
| nil = skaf45(nil,X0)
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1535,plain,
( ~ sQ18_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1524,f1532,f792]) ).
fof(f1542,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(X0)
| ~ rearsegP(nil,X0)
| nil = skaf46(nil,X0)
| ~ ssList(skaf46(nil,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f332,f348]) ).
fof(f1543,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(nil,X0)
| nil = X0
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0)) ),
inference(resolution,[status(thm)],[f332,f349]) ).
fof(f1547,definition,
! [X0] :
( sQ57_spl
<=> ( ~ ssList(X0)
| ~ rearsegP(nil,X0)
| nil = skaf46(nil,X0)
| ~ ssList(skaf46(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1550,plain,
( ~ sQ18_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1542,f1547,f792]) ).
fof(f1551,definition,
! [X0] :
( sQ58_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(nil,X0)
| nil = X0
| ~ ssList(X0)
| ~ ssList(skaf45(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1554,plain,
( ~ sQ18_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1543,f1551,f792]) ).
fof(f1566,plain,
( ~ sQ35_spl
| nil = sk6
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f1278,f332]) ).
fof(f1568,plain,
! [X0] :
( ~ sQ35_spl
| frontsegP(sk3,X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ frontsegP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f1278,f356]) ).
fof(f1569,plain,
! [X0] :
( ~ sQ35_spl
| rearsegP(sk3,X0)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ rearsegP(app(cons(sk5,nil),sk7),X0) ),
inference(paramodulation,[status(thm)],[f1278,f355]) ).
fof(f1570,plain,
! [X0] :
( ~ sQ35_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ memberP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f1278,f359]) ).
fof(f1571,plain,
! [X0] :
( ~ sQ35_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ memberP(app(cons(sk5,nil),sk7),X0) ),
inference(paramodulation,[status(thm)],[f1278,f360]) ).
fof(f1573,plain,
! [X0] :
( ~ sQ35_spl
| X0 = sk6
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(X0)
| app(X0,app(cons(sk5,nil),sk7)) != sk3 ),
inference(paramodulation,[status(thm)],[f1278,f377]) ).
fof(f1575,plain,
! [X0] :
( ~ sQ35_spl
| X0 = app(cons(sk5,nil),sk7)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(sk6)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ),
inference(paramodulation,[status(thm)],[f1278,f375]) ).
fof(f1577,plain,
! [X0] :
( ~ sQ35_spl
| app(sk3,X0) = app(sk6,app(app(cons(sk5,nil),sk7),X0))
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1278,f373]) ).
fof(f1579,plain,
( ~ sQ35_spl
| rearsegP(sk3,app(cons(sk5,nil),sk7))
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1278,f511]) ).
fof(f1581,definition,
( sQ60_spl
<=> ssList(app(cons(sk5,nil),sk7)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1582,plain,
( ~ sQ60_spl
| ssList(app(cons(sk5,nil),sk7)) ),
inference(component_clause,[status(thm)],[f1581]) ).
fof(f1583,plain,
( sQ60_spl
| ~ ssList(app(cons(sk5,nil),sk7)) ),
inference(component_clause,[status(thm)],[f1581]) ).
fof(f1584,definition,
( sQ61_spl
<=> nil = sk6 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1585,plain,
( ~ sQ61_spl
| nil = sk6 ),
inference(component_clause,[status(thm)],[f1584]) ).
fof(f1587,plain,
( ~ sQ35_spl
| sQ61_spl
| ~ sQ34_spl
| ~ sQ60_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1566,f477,f1581,f1274,f1584,f1277]) ).
fof(f1592,definition,
! [X0] :
( sQ63_spl
<=> ( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
! [X0] :
( ~ sQ63_spl
| frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(sk6,X0) ),
inference(component_clause,[status(thm)],[f1592]) ).
fof(f1595,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ60_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1568,f1592,f1581,f1274,f1277]) ).
fof(f1596,definition,
! [X0] :
( sQ64_spl
<=> ( rearsegP(sk3,X0)
| ~ ssList(X0)
| ~ rearsegP(app(cons(sk5,nil),sk7),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1599,plain,
( ~ sQ35_spl
| ~ sQ60_spl
| ~ sQ34_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1569,f1596,f1274,f1581,f1277]) ).
fof(f1600,definition,
! [X0] :
( sQ65_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1601,plain,
! [X0] :
( ~ sQ65_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ),
inference(component_clause,[status(thm)],[f1600]) ).
fof(f1603,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ60_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1570,f1600,f1581,f1274,f1277]) ).
fof(f1604,definition,
! [X0] :
( sQ66_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(cons(sk5,nil),sk7),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1607,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ60_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1571,f1604,f1581,f1274,f1277]) ).
fof(f1609,definition,
! [X0] :
( sQ67_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| app(X0,app(cons(sk5,nil),sk7)) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1610,plain,
! [X0] :
( ~ sQ67_spl
| X0 = sk6
| ~ ssList(X0)
| app(X0,app(cons(sk5,nil),sk7)) != sk3 ),
inference(component_clause,[status(thm)],[f1609]) ).
fof(f1612,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ60_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1573,f1609,f1581,f1274,f1277]) ).
fof(f1614,definition,
! [X0] :
( sQ68_spl
<=> ( X0 = app(cons(sk5,nil),sk7)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1615,plain,
! [X0] :
( ~ sQ68_spl
| X0 = app(cons(sk5,nil),sk7)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ),
inference(component_clause,[status(thm)],[f1614]) ).
fof(f1617,plain,
( ~ sQ35_spl
| ~ sQ60_spl
| ~ sQ34_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1575,f1614,f1274,f1581,f1277]) ).
fof(f1619,definition,
! [X0] :
( sQ69_spl
<=> ( app(sk3,X0) = app(sk6,app(app(cons(sk5,nil),sk7),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1622,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ60_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1577,f1619,f1581,f1274,f1277]) ).
fof(f1623,definition,
( sQ70_spl
<=> frontsegP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1624,plain,
( ~ sQ70_spl
| frontsegP(sk3,sk6) ),
inference(component_clause,[status(thm)],[f1623]) ).
fof(f1627,definition,
( sQ71_spl
<=> rearsegP(sk3,app(cons(sk5,nil),sk7)) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1628,plain,
( ~ sQ71_spl
| rearsegP(sk3,app(cons(sk5,nil),sk7)) ),
inference(component_clause,[status(thm)],[f1627]) ).
fof(f1630,plain,
( ~ sQ35_spl
| sQ71_spl
| ~ sQ60_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f1579,f1274,f1581,f1627,f1277]) ).
fof(f1634,plain,
! [X0] :
( ~ sQ7_spl
| memberP(app(X0,sk3),sk8)
| ~ ssList(app(X0,cons(sk8,nil)))
| ~ ssItem(sk8)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f482,f517]) ).
fof(f1635,definition,
! [X0] :
( sQ72_spl
<=> ( memberP(app(X0,sk3),sk8)
| ~ ssList(app(X0,cons(sk8,nil)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1638,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ72_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1634,f792,f1635,f470,f481]) ).
fof(f1648,definition,
( sQ75_spl
<=> ssList(skaf80(nil)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1650,plain,
( sQ75_spl
| ~ ssList(skaf80(nil)) ),
inference(component_clause,[status(thm)],[f1648]) ).
fof(f1659,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1650,f219]) ).
fof(f1660,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1659]) ).
fof(f1662,plain,
! [X0] :
( ~ sQ41_spl
| rearsegP(X0,sk7)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk7)
| ~ rearsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f381,f1303]) ).
fof(f1663,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ rearsegP(X2,X3)
| rearsegP(X0,X3)
| ~ ssList(X0)
| ~ ssList(app(X1,X2))
| ~ ssList(X3)
| ~ rearsegP(X0,app(X1,X2)) ),
inference(resolution,[status(thm)],[f381,f355]) ).
fof(f1666,definition,
! [X0] :
( sQ78_spl
<=> ( rearsegP(X0,sk7)
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1667,plain,
! [X0] :
( ~ sQ78_spl
| rearsegP(X0,sk7)
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ),
inference(component_clause,[status(thm)],[f1666]) ).
fof(f1669,plain,
( ~ sQ41_spl
| ~ sQ12_spl
| ~ sQ32_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1662,f1666,f1268,f655,f1302]) ).
fof(f1670,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X2)
| ~ ssList(X1)
| ~ rearsegP(X2,X3)
| rearsegP(X0,X3)
| ~ ssList(X0)
| ~ ssList(app(X1,X2))
| ~ ssList(X3)
| ~ rearsegP(X0,app(X1,X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f1663]) ).
fof(f1671,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X2)
| ~ ssList(X1)
| ~ rearsegP(X2,X3)
| rearsegP(X0,X3)
| ~ ssList(X0)
| ~ ssList(X3)
| ~ rearsegP(X0,app(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1670,f290]) ).
fof(f1674,plain,
( sQ60_spl
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f1583,f290]) ).
fof(f1675,plain,
( sQ60_spl
| ~ sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1674,f1268,f1271,f1581]) ).
fof(f1676,plain,
( ~ sQ70_spl
| sk3 = sk6
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ frontsegP(sk6,sk3) ),
inference(resolution,[status(thm)],[f1624,f346]) ).
fof(f1677,definition,
( sQ79_spl
<=> sk3 = sk6 ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1678,plain,
( ~ sQ79_spl
| sk3 = sk6 ),
inference(component_clause,[status(thm)],[f1677]) ).
fof(f1680,plain,
( ~ sQ70_spl
| sQ79_spl
| ~ sQ12_spl
| ~ sQ34_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f1676,f1455,f1274,f655,f1677,f1623]) ).
fof(f1681,plain,
! [X0,X1] :
( ~ sQ78_spl
| ~ ssList(X1)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ rearsegP(X1,sk3)
| rearsegP(app(X0,X1),sk7)
| ~ ssList(app(X0,X1)) ),
inference(resolution,[status(thm)],[f1667,f355]) ).
fof(f1682,plain,
! [X0] :
( ~ sQ78_spl
| ~ ssList(sk3)
| ~ ssList(X0)
| rearsegP(app(X0,sk3),sk7)
| ~ ssList(app(X0,sk3)) ),
inference(resolution,[status(thm)],[f1667,f511]) ).
fof(f1684,definition,
! [X0,X1] :
( sQ80_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,sk3)
| rearsegP(app(X0,X1),sk7)
| ~ ssList(app(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1687,plain,
( ~ sQ78_spl
| ~ sQ12_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1681,f1684,f655,f1666]) ).
fof(f1688,definition,
! [X0] :
( sQ81_spl
<=> ( ~ ssList(X0)
| rearsegP(app(X0,sk3),sk7)
| ~ ssList(app(X0,sk3)) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1691,plain,
( ~ sQ78_spl
| ~ sQ12_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1682,f1688,f655,f1666]) ).
fof(f1694,plain,
( ~ sQ63_spl
| ~ ssList(sk6)
| frontsegP(sk3,sk6)
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f1593,f265]) ).
fof(f1695,plain,
( ~ sQ63_spl
| sQ70_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f1694,f1274,f1623,f1592]) ).
fof(f1696,plain,
( ~ sQ2_spl
| ~ sQ65_spl
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1601,f464]) ).
fof(f1697,definition,
( sQ82_spl
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1698,plain,
( ~ sQ82_spl
| memberP(sk3,sk5) ),
inference(component_clause,[status(thm)],[f1697]) ).
fof(f1700,plain,
( ~ sQ2_spl
| ~ sQ65_spl
| sQ82_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1696,f1424,f1697,f1600,f463]) ).
fof(f1701,plain,
( ~ sQ54_spl
| ~ sQ3_spl
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f467,f1502]) ).
fof(f1702,plain,
( ~ sQ54_spl
| ~ sQ3_spl
| sQ82_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1701,f1424,f1697,f466,f1501]) ).
fof(f1705,plain,
! [X0] :
( ~ sQ71_spl
| rearsegP(X0,app(cons(sk5,nil),sk7))
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ rearsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f1628,f381]) ).
fof(f1706,plain,
( ~ sQ71_spl
| sk3 = app(cons(sk5,nil),sk7)
| ~ ssList(sk3)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ rearsegP(app(cons(sk5,nil),sk7),sk3) ),
inference(resolution,[status(thm)],[f1628,f345]) ).
fof(f1707,definition,
! [X0] :
( sQ83_spl
<=> ( rearsegP(X0,app(cons(sk5,nil),sk7))
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1710,plain,
( ~ sQ71_spl
| ~ sQ12_spl
| ~ sQ60_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1705,f1707,f1581,f655,f1627]) ).
fof(f1711,definition,
( sQ84_spl
<=> rearsegP(app(cons(sk5,nil),sk7),sk3) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1713,plain,
( sQ84_spl
| ~ rearsegP(app(cons(sk5,nil),sk7),sk3) ),
inference(component_clause,[status(thm)],[f1711]) ).
fof(f1714,definition,
( sQ85_spl
<=> sk3 = app(cons(sk5,nil),sk7) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1715,plain,
( ~ sQ85_spl
| sk3 = app(cons(sk5,nil),sk7) ),
inference(component_clause,[status(thm)],[f1714]) ).
fof(f1716,plain,
( sQ85_spl
| sk3 != app(cons(sk5,nil),sk7) ),
inference(component_clause,[status(thm)],[f1714]) ).
fof(f1717,plain,
( ~ sQ71_spl
| sQ85_spl
| ~ sQ12_spl
| ~ sQ60_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f1706,f1711,f1581,f655,f1714,f1627]) ).
fof(f1718,plain,
( sQ84_spl
| ~ ssList(sk7)
| ~ ssList(sk3)
| ~ ssList(cons(sk5,nil))
| ~ rearsegP(sk7,sk3) ),
inference(resolution,[status(thm)],[f1713,f355]) ).
fof(f1719,plain,
( sQ84_spl
| ~ sQ32_spl
| ~ sQ12_spl
| ~ sQ33_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1718,f1395,f1271,f655,f1268,f1711]) ).
fof(f1726,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ85_spl
| X0 = sk6
| ~ ssList(X0)
| app(X0,sk3) != sk3 ),
inference(backward_demodulation,[status(thm)],[f1715,f1610]) ).
fof(f1733,definition,
! [X0] :
( sQ86_spl
<=> ( rearsegP(X0,sk3)
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1737,definition,
( sQ87_spl
<=> rearsegP(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1738,plain,
( ~ sQ87_spl
| rearsegP(sk3,sk3) ),
inference(component_clause,[status(thm)],[f1737]) ).
fof(f1739,plain,
( sQ87_spl
| ~ rearsegP(sk3,sk3) ),
inference(component_clause,[status(thm)],[f1737]) ).
fof(f1764,definition,
! [X0] :
( sQ89_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1769,definition,
! [X0] :
( sQ90_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| app(X0,sk3) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1770,plain,
! [X0] :
( ~ sQ90_spl
| X0 = sk6
| ~ ssList(X0)
| app(X0,sk3) != sk3 ),
inference(component_clause,[status(thm)],[f1769]) ).
fof(f1788,plain,
! [X0,X1] :
( ~ sQ61_spl
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(backward_demodulation,[status(thm)],[f1585,f332]) ).
fof(f1789,plain,
! [X0,X1] :
( ~ sQ61_spl
| sk6 = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(backward_demodulation,[status(thm)],[f1585,f334]) ).
fof(f1804,plain,
! [X0] :
( ~ sQ61_spl
| app(sk6,X0) = X0
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f279]) ).
fof(f1805,plain,
! [X0] :
( ~ sQ61_spl
| app(X0,sk6) = X0
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f278]) ).
fof(f1806,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f275]) ).
fof(f1828,plain,
! [X0] :
( ~ sQ61_spl
| frontsegP(X0,sk6)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f264]) ).
fof(f1829,plain,
! [X0] :
( ~ sQ61_spl
| rearsegP(X0,sk6)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f262]) ).
fof(f1830,plain,
! [X0] :
( ~ sQ61_spl
| segmentP(X0,sk6)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f260]) ).
fof(f1851,plain,
! [X0,X1] :
( ~ sQ61_spl
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != sk6 ),
inference(forward_demodulation,[status(thm)],[f1585,f1788]) ).
fof(f1852,plain,
! [X0,X1] :
( ~ sQ61_spl
| sk6 = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != sk6 ),
inference(forward_demodulation,[status(thm)],[f1585,f1789]) ).
fof(f1865,plain,
! [X0,X1] :
( X0 = X0
| ~ ssList(X1)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(equality_resolution,[status(thm)],[f406]) ).
fof(f1866,definition,
! [X0] :
( sQ94_spl
<=> ( X0 = X0
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1869,definition,
! [X1] :
( sQ95_spl
<=> ( ~ ssList(X1)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1870,plain,
! [X0] :
( ~ sQ95_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1869]) ).
fof(f1872,plain,
( sQ95_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1865,f1866,f1869]) ).
fof(f1907,plain,
( ~ sQ2_spl
| ~ sQ61_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1806,f464]) ).
fof(f1908,plain,
( ~ sQ2_spl
| ~ sQ61_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1907,f1424,f1584,f463]) ).
fof(f1909,plain,
! [X0] :
( ~ sQ70_spl
| frontsegP(X0,sk6)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ frontsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f383,f1624]) ).
fof(f1910,plain,
! [X0] :
( ~ sQ50_spl
| frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ frontsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f383,f1467]) ).
fof(f1914,definition,
! [X0] :
( sQ96_spl
<=> ( frontsegP(X0,sk6)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1915,plain,
! [X0] :
( ~ sQ96_spl
| frontsegP(X0,sk6)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3) ),
inference(component_clause,[status(thm)],[f1914]) ).
fof(f1917,plain,
( ~ sQ70_spl
| ~ sQ12_spl
| ~ sQ34_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1909,f1914,f1274,f655,f1623]) ).
fof(f1918,definition,
! [X0] :
( sQ97_spl
<=> ( frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1921,plain,
( ~ sQ50_spl
| ~ sQ12_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1910,f1918,f655,f1466]) ).
fof(f1927,plain,
! [X0,X1] :
( ~ sQ7_spl
| X0 = sk8
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| cons(X0,X1) != sk3 ),
inference(paramodulation,[status(thm)],[f482,f406]) ).
fof(f1929,plain,
! [X0,X1] :
( ~ sQ7_spl
| nil = X1
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| cons(X0,X1) != sk3 ),
inference(paramodulation,[status(thm)],[f482,f408]) ).
fof(f1937,definition,
! [X0,X1] :
( sQ98_spl
<=> ( X0 = sk8
| ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1940,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ4_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1927,f1937,f470,f792,f481]) ).
fof(f1942,definition,
! [X0,X1] :
( sQ99_spl
<=> ( nil = X1
| ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1945,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ4_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f1929,f1942,f470,f792,f481]) ).
fof(f2000,plain,
! [X0] :
( ~ sQ85_spl
| X0 = sk7
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(X0)
| app(cons(sk5,nil),X0) != sk3 ),
inference(paramodulation,[status(thm)],[f1715,f375]) ).
fof(f2022,definition,
! [X0] :
( sQ103_spl
<=> ( X0 = sk7
| ~ ssList(X0)
| app(cons(sk5,nil),X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2023,plain,
! [X0] :
( ~ sQ103_spl
| X0 = sk7
| ~ ssList(X0)
| app(cons(sk5,nil),X0) != sk3 ),
inference(component_clause,[status(thm)],[f2022]) ).
fof(f2025,plain,
( ~ sQ85_spl
| ~ sQ32_spl
| ~ sQ33_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f2000,f2022,f1271,f1268,f1714]) ).
fof(f2053,definition,
( sQ109_spl
<=> ssList(skaf45(sk3,sk6)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f2055,plain,
( sQ109_spl
| ~ ssList(skaf45(sk3,sk6)) ),
inference(component_clause,[status(thm)],[f2053]) ).
fof(f2056,definition,
( sQ110_spl
<=> skaf45(sk3,sk6) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2057,plain,
( ~ sQ110_spl
| skaf45(sk3,sk6) = sk3 ),
inference(component_clause,[status(thm)],[f2056]) ).
fof(f2062,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2055,f255]) ).
fof(f2063,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f2062]) ).
fof(f2066,plain,
( ~ sQ110_spl
| app(sk6,sk3) = sk3
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ frontsegP(sk3,sk6) ),
inference(paramodulation,[status(thm)],[f2057,f349]) ).
fof(f2068,definition,
( sQ111_spl
<=> app(sk6,sk3) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( ~ sQ111_spl
| app(sk6,sk3) = sk3 ),
inference(component_clause,[status(thm)],[f2068]) ).
fof(f2070,plain,
( sQ111_spl
| app(sk6,sk3) != sk3 ),
inference(component_clause,[status(thm)],[f2068]) ).
fof(f2071,plain,
( ~ sQ110_spl
| sQ111_spl
| ~ sQ12_spl
| ~ sQ34_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f2066,f1623,f1274,f655,f2068,f2056]) ).
fof(f2074,plain,
! [X0] :
( ~ sQ7_spl
| X0 = sk8
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f482,f396]) ).
fof(f2075,definition,
! [X0] :
( sQ112_spl
<=> ( X0 = sk8
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f2076,plain,
! [X0] :
( ~ sQ112_spl
| X0 = sk8
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(component_clause,[status(thm)],[f2075]) ).
fof(f2078,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| ~ sQ18_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f2074,f2075,f792,f470,f481]) ).
fof(f2079,plain,
! [X0] :
( ~ sQ112_spl
| X0 = sk8
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f275]) ).
fof(f2085,plain,
! [X0] :
( memberP(app(sk6,cons(sk5,nil)),X0)
| memberP(sk7,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f529,f390]) ).
fof(f2091,definition,
! [X0] :
( sQ114_spl
<=> ( memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f2095,definition,
! [X0] :
( sQ115_spl
<=> ( memberP(app(sk6,cons(sk5,nil)),X0)
| memberP(sk7,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f2098,plain,
( ~ sQ37_spl
| ~ sQ32_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f2085,f2095,f1268,f1284]) ).
fof(f2099,plain,
( ~ sQ63_spl
| frontsegP(sk3,nil)
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f264,f1593]) ).
fof(f2100,plain,
! [X0,X1] :
( frontsegP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f264,f383]) ).
fof(f2101,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f264,f346]) ).
fof(f2102,definition,
( sQ116_spl
<=> frontsegP(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f2103,plain,
( ~ sQ116_spl
| frontsegP(sk3,nil) ),
inference(component_clause,[status(thm)],[f2102]) ).
fof(f2105,plain,
( ~ sQ63_spl
| sQ116_spl
| ~ sQ18_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f2099,f1274,f792,f2102,f1592]) ).
fof(f2106,definition,
! [X0,X1] :
( sQ117_spl
<=> ( frontsegP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2109,plain,
( ~ sQ18_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2100,f2106,f792]) ).
fof(f2110,definition,
! [X0] :
( sQ118_spl
<=> ( X0 = nil
| ~ ssList(X0)
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f2113,plain,
( ~ sQ18_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f2101,f2110,f792]) ).
fof(f2116,plain,
! [X0] :
( ~ sQ116_spl
| frontsegP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ frontsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f2103,f383]) ).
fof(f2117,plain,
( ~ sQ116_spl
| sk3 = nil
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ frontsegP(nil,sk3) ),
inference(resolution,[status(thm)],[f2103,f346]) ).
fof(f2118,definition,
! [X0] :
( sQ119_spl
<=> ( frontsegP(X0,nil)
| ~ ssList(X0)
| ~ frontsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f2121,plain,
( ~ sQ116_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2116,f2118,f792,f655,f2102]) ).
fof(f2122,definition,
( sQ120_spl
<=> frontsegP(nil,sk3) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f2125,plain,
( ~ sQ116_spl
| sQ6_spl
| ~ sQ12_spl
| ~ sQ18_spl
| ~ sQ120_spl ),
inference(split_clause,[status(thm)],[f2117,f2122,f792,f655,f477,f2102]) ).
fof(f2127,plain,
! [X0,X1] :
( rearsegP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ rearsegP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f262,f381]) ).
fof(f2128,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f262,f345]) ).
fof(f2129,definition,
( sQ121_spl
<=> rearsegP(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f2130,plain,
( ~ sQ121_spl
| rearsegP(sk3,nil) ),
inference(component_clause,[status(thm)],[f2129]) ).
fof(f2133,definition,
! [X0,X1] :
( sQ122_spl
<=> ( rearsegP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f2136,plain,
( ~ sQ18_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f2127,f2133,f792]) ).
fof(f2137,definition,
! [X0] :
( sQ123_spl
<=> ( X0 = nil
| ~ ssList(X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f2140,plain,
( ~ sQ18_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f2128,f2137,f792]) ).
fof(f2143,plain,
! [X0] :
( ~ sQ121_spl
| rearsegP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ rearsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f2130,f381]) ).
fof(f2144,plain,
( ~ sQ121_spl
| sk3 = nil
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ rearsegP(nil,sk3) ),
inference(resolution,[status(thm)],[f2130,f345]) ).
fof(f2145,definition,
! [X0] :
( sQ124_spl
<=> ( rearsegP(X0,nil)
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f2148,plain,
( ~ sQ121_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ124_spl ),
inference(split_clause,[status(thm)],[f2143,f2145,f792,f655,f2129]) ).
fof(f2149,definition,
( sQ125_spl
<=> rearsegP(nil,sk3) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2152,plain,
( ~ sQ121_spl
| sQ6_spl
| ~ sQ12_spl
| ~ sQ18_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f2144,f2149,f792,f655,f477,f2129]) ).
fof(f2153,plain,
! [X0,X1] :
( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f260,f379]) ).
fof(f2154,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f260,f344]) ).
fof(f2155,definition,
! [X0,X1] :
( sQ126_spl
<=> ( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2158,plain,
( ~ sQ18_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f2153,f2155,f792]) ).
fof(f2159,definition,
! [X0] :
( sQ127_spl
<=> ( X0 = nil
| ~ ssList(X0)
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f2162,plain,
( ~ sQ18_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f2154,f2159,f792]) ).
fof(f2165,plain,
( ~ sQ7_spl
| cyclefreeP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f274]) ).
fof(f2166,definition,
( sQ128_spl
<=> cyclefreeP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f2169,plain,
( ~ sQ7_spl
| sQ128_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2165,f470,f2166,f481]) ).
fof(f2170,plain,
( ~ sQ7_spl
| totalorderP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f273]) ).
fof(f2171,definition,
( sQ129_spl
<=> totalorderP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2174,plain,
( ~ sQ7_spl
| sQ129_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2170,f470,f2171,f481]) ).
fof(f2175,plain,
( ~ sQ82_spl
| ~ sQ112_spl
| sk5 = sk8
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f2079,f1698]) ).
fof(f2176,plain,
( ~ sQ13_spl
| ~ sQ112_spl
| sk8 = sk8
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f2079,f660]) ).
fof(f2177,definition,
( sQ130_spl
<=> sk5 = sk8 ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f2178,plain,
( ~ sQ130_spl
| sk5 = sk8 ),
inference(component_clause,[status(thm)],[f2177]) ).
fof(f2180,plain,
( ~ sQ82_spl
| ~ sQ112_spl
| sQ130_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f2175,f1424,f2177,f2075,f1697]) ).
fof(f2181,plain,
( ~ sQ13_spl
| ~ sQ112_spl
| sQ29_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2176,f470,f1236,f2075,f659]) ).
fof(f2187,plain,
( ~ sQ130_spl
| app(app(sk6,cons(sk8,nil)),sk7) = sk3 ),
inference(backward_demodulation,[status(thm)],[f2178,f529]) ).
fof(f2207,plain,
( ~ sQ40_spl
| ~ sQ130_spl
| frontsegP(sk3,app(sk6,cons(sk8,nil))) ),
inference(backward_demodulation,[status(thm)],[f2178,f1299]) ).
fof(f2217,plain,
( ~ sQ130_spl
| ~ sQ7_spl
| app(app(sk6,sk3),sk7) = sk3 ),
inference(forward_demodulation,[status(thm)],[f482,f2187]) ).
fof(f2265,definition,
! [X0] :
( sQ132_spl
<=> ( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f2278,definition,
! [X0] :
( sQ134_spl
<=> ( X0 = sk7
| ~ ssList(X0)
| app(sk3,X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f2279,plain,
! [X0] :
( ~ sQ134_spl
| X0 = sk7
| ~ ssList(X0)
| app(sk3,X0) != sk3 ),
inference(component_clause,[status(thm)],[f2278]) ).
fof(f2290,plain,
( ~ sQ67_spl
| ~ sQ85_spl
| ~ ssList(sk3)
| nil = sk6
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1726,f279]) ).
fof(f2294,plain,
( ~ sQ67_spl
| ~ sQ85_spl
| ~ sQ12_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f2290,f792,f1584,f655,f1714,f1609]) ).
fof(f2295,definition,
( sQ136_spl
<=> ssList(skaf46(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f2297,plain,
( sQ136_spl
| ~ ssList(skaf46(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f2295]) ).
fof(f2298,definition,
( sQ137_spl
<=> skaf46(sk3,sk3) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2299,plain,
( ~ sQ137_spl
| skaf46(sk3,sk3) = sk6 ),
inference(component_clause,[status(thm)],[f2298]) ).
fof(f2302,definition,
( sQ138_spl
<=> sk6 = sk6 ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f2310,plain,
( sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2297,f254]) ).
fof(f2311,plain,
sQ136_spl,
inference(contradiction_clause,[status(thm)],[f2310]) ).
fof(f2555,plain,
( ~ sQ5_spl
| ~ sQ61_spl
| sk6 = sk4 ),
inference(forward_demodulation,[status(thm)],[f1585,f474]) ).
fof(f2557,plain,
( ~ sQ3_spl
| ~ sQ130_spl
| memberP(sk7,sk8) ),
inference(forward_demodulation,[status(thm)],[f2178,f467]) ).
fof(f2561,plain,
( ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sk4 = app(sk6,app(cons(sk5,sk7),sk7)) ),
inference(forward_demodulation,[status(thm)],[f575,f1329]) ).
fof(f2562,plain,
( ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ61_spl
| sk6 = app(sk6,app(cons(sk5,sk7),sk7)) ),
inference(forward_demodulation,[status(thm)],[f2555,f2561]) ).
fof(f2582,plain,
( ~ sQ40_spl
| ~ sQ130_spl
| ~ sQ7_spl
| frontsegP(sk3,app(sk6,sk3)) ),
inference(backward_demodulation,[status(thm)],[f482,f2207]) ).
fof(f2590,plain,
( ~ sQ130_spl
| ~ sQ7_spl
| app(app(sk6,sk3),sk7) = sk3 ),
inference(backward_demodulation,[status(thm)],[f482,f2187]) ).
fof(f2674,plain,
( ~ sQ121_spl
| ~ sQ61_spl
| rearsegP(sk3,sk6) ),
inference(backward_demodulation,[status(thm)],[f1585,f2130]) ).
fof(f2724,plain,
! [X0] :
( ~ sQ121_spl
| ~ sQ61_spl
| rearsegP(X0,sk6)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ rearsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f2674,f381]) ).
fof(f2726,definition,
! [X0] :
( sQ139_spl
<=> ( rearsegP(X0,sk6)
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f2727,plain,
! [X0] :
( ~ sQ139_spl
| rearsegP(X0,sk6)
| ~ ssList(X0)
| ~ rearsegP(X0,sk3) ),
inference(component_clause,[status(thm)],[f2726]) ).
fof(f2729,plain,
( ~ sQ121_spl
| ~ sQ61_spl
| ~ sQ12_spl
| ~ sQ34_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f2724,f2726,f1274,f655,f1584,f2129]) ).
fof(f2744,plain,
! [X0,X1] :
( ~ sQ61_spl
| frontsegP(X1,sk6)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1828,f383]) ).
fof(f2745,plain,
! [X0] :
( ~ sQ61_spl
| X0 = sk6
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ frontsegP(sk6,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1828,f346]) ).
fof(f2746,definition,
! [X0,X1] :
( sQ141_spl
<=> ( frontsegP(X1,sk6)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f2749,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f2744,f2746,f1274,f1584]) ).
fof(f2750,definition,
! [X0] :
( sQ142_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| ~ frontsegP(sk6,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f2753,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f2745,f2750,f1274,f1584]) ).
fof(f2756,plain,
! [X0,X1] :
( ~ sQ61_spl
| rearsegP(X1,sk6)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ rearsegP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1829,f381]) ).
fof(f2757,plain,
! [X0] :
( ~ sQ61_spl
| X0 = sk6
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ rearsegP(sk6,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1829,f345]) ).
fof(f2758,definition,
! [X0,X1] :
( sQ143_spl
<=> ( rearsegP(X1,sk6)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f2761,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f2756,f2758,f1274,f1584]) ).
fof(f2762,definition,
! [X0] :
( sQ144_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| ~ rearsegP(sk6,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f2765,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f2757,f2762,f1274,f1584]) ).
fof(f2768,plain,
! [X0,X1] :
( ~ sQ61_spl
| segmentP(X1,sk6)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1830,f379]) ).
fof(f2769,plain,
! [X0] :
( ~ sQ61_spl
| X0 = sk6
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ segmentP(sk6,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1830,f344]) ).
fof(f2770,definition,
! [X0,X1] :
( sQ145_spl
<=> ( segmentP(X1,sk6)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f2773,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ145_spl ),
inference(split_clause,[status(thm)],[f2768,f2770,f1274,f1584]) ).
fof(f2774,definition,
! [X0] :
( sQ146_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| ~ segmentP(sk6,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f2777,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f2769,f2774,f1274,f1584]) ).
fof(f2781,plain,
( ~ sQ137_spl
| app(sk6,sk3) = sk3
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ rearsegP(sk3,sk3) ),
inference(paramodulation,[status(thm)],[f2299,f348]) ).
fof(f2783,plain,
( ~ sQ137_spl
| sQ111_spl
| ~ sQ12_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f2781,f1737,f655,f2068,f2298]) ).
fof(f2829,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ rearsegP(sk6,X0)
| sk6 = skaf46(sk6,X0)
| ~ ssList(skaf46(sk6,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1851,f348]) ).
fof(f2830,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ segmentP(sk6,X0)
| sk6 = app(skaf47(sk6,X0),X0)
| ~ ssList(app(skaf47(sk6,X0),X0))
| ~ ssList(skaf48(X0,sk6)) ),
inference(resolution,[status(thm)],[f1851,f403]) ).
fof(f2836,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ frontsegP(sk6,X0)
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(skaf45(sk6,X0)) ),
inference(resolution,[status(thm)],[f1851,f349]) ).
fof(f2841,definition,
( sQ151_spl
<=> ssList(skaf80(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2843,plain,
( sQ151_spl
| ~ ssList(skaf80(sk6)) ),
inference(component_clause,[status(thm)],[f2841]) ).
fof(f2844,definition,
( sQ152_spl
<=> sk6 = skaf80(sk6) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f2845,plain,
( ~ sQ152_spl
| sk6 = skaf80(sk6) ),
inference(component_clause,[status(thm)],[f2844]) ).
fof(f2847,definition,
( sQ153_spl
<=> equalelemsP(sk6) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f2851,definition,
! [X0] :
( sQ154_spl
<=> ( ~ ssList(X0)
| ~ rearsegP(sk6,X0)
| sk6 = skaf46(sk6,X0)
| ~ ssList(skaf46(sk6,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f2854,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f2829,f2851,f1274,f1584]) ).
fof(f2855,definition,
! [X0] :
( sQ155_spl
<=> ( ~ ssList(X0)
| ~ segmentP(sk6,X0)
| sk6 = app(skaf47(sk6,X0),X0)
| ~ ssList(app(skaf47(sk6,X0),X0))
| ~ ssList(skaf48(X0,sk6)) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f2858,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f2830,f2855,f1274,f1584]) ).
fof(f2859,definition,
( sQ156_spl
<=> ssList(cons(skaf50(sk6),skaf53(sk6))) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f2861,plain,
( sQ156_spl
| ~ ssList(cons(skaf50(sk6),skaf53(sk6))) ),
inference(component_clause,[status(thm)],[f2859]) ).
fof(f2872,definition,
( sQ160_spl
<=> ssList(cons(skaf55(sk6),skaf58(sk6))) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f2873,plain,
( ~ sQ160_spl
| ssList(cons(skaf55(sk6),skaf58(sk6))) ),
inference(component_clause,[status(thm)],[f2872]) ).
fof(f2874,plain,
( sQ160_spl
| ~ ssList(cons(skaf55(sk6),skaf58(sk6))) ),
inference(component_clause,[status(thm)],[f2872]) ).
fof(f2885,definition,
( sQ164_spl
<=> ssList(cons(skaf60(sk6),skaf63(sk6))) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2887,plain,
( sQ164_spl
| ~ ssList(cons(skaf60(sk6),skaf63(sk6))) ),
inference(component_clause,[status(thm)],[f2885]) ).
fof(f2898,definition,
( sQ168_spl
<=> ssList(cons(skaf65(sk6),skaf68(sk6))) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f2900,plain,
( sQ168_spl
| ~ ssList(cons(skaf65(sk6),skaf68(sk6))) ),
inference(component_clause,[status(thm)],[f2898]) ).
fof(f2911,definition,
( sQ172_spl
<=> ssList(cons(skaf70(sk6),skaf73(sk6))) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f2912,plain,
( ~ sQ172_spl
| ssList(cons(skaf70(sk6),skaf73(sk6))) ),
inference(component_clause,[status(thm)],[f2911]) ).
fof(f2913,plain,
( sQ172_spl
| ~ ssList(cons(skaf70(sk6),skaf73(sk6))) ),
inference(component_clause,[status(thm)],[f2911]) ).
fof(f2924,definition,
! [X0] :
( sQ176_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(sk6,X0)
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(skaf45(sk6,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f2925,plain,
! [X0] :
( ~ sQ176_spl
| ~ ssList(X0)
| ~ frontsegP(sk6,X0)
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(skaf45(sk6,X0)) ),
inference(component_clause,[status(thm)],[f2924]) ).
fof(f2927,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f2836,f2924,f1274,f1584]) ).
fof(f2932,plain,
! [X0] :
( ~ sQ176_spl
| ~ frontsegP(sk6,X0)
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(skaf45(sk6,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2925]) ).
fof(f3031,plain,
! [X0] :
( ~ sQ61_spl
| app(sk6,X0) = X0
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(app(sk6,X0))
| ~ ssList(app(sk6,X0)) ),
inference(resolution,[status(thm)],[f1804,f375]) ).
fof(f3035,definition,
! [X0] :
( sQ183_spl
<=> ( app(sk6,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(sk6,X0))
| ~ ssList(app(sk6,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f3038,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f3031,f3035,f1274,f1584]) ).
fof(f3043,plain,
! [X0] :
( ~ sQ61_spl
| app(X0,sk6) = X0
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(app(X0,sk6))
| ~ ssList(app(X0,sk6)) ),
inference(resolution,[status(thm)],[f1805,f377]) ).
fof(f3046,definition,
! [X0] :
( sQ184_spl
<=> ( app(X0,sk6) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,sk6))
| ~ ssList(app(X0,sk6)) ) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f3049,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ184_spl ),
inference(split_clause,[status(thm)],[f3043,f3046,f1274,f1584]) ).
fof(f3057,definition,
( sQ185_spl
<=> strictorderP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f3062,definition,
( sQ186_spl
<=> totalorderedP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f3067,definition,
( sQ187_spl
<=> strictorderedP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f3073,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ rearsegP(sk6,X0)
| sk6 = X0
| ~ ssList(skaf46(sk6,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1852,f348]) ).
fof(f3074,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ segmentP(sk6,X0)
| sk6 = skaf48(X0,sk6)
| ~ ssList(app(skaf47(sk6,X0),X0))
| ~ ssList(skaf48(X0,sk6)) ),
inference(resolution,[status(thm)],[f1852,f403]) ).
fof(f3081,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ frontsegP(sk6,X0)
| sk6 = skaf45(sk6,X0)
| ~ ssList(X0)
| ~ ssList(skaf45(sk6,X0)) ),
inference(resolution,[status(thm)],[f1852,f349]) ).
fof(f3085,definition,
( sQ188_spl
<=> sk6 = cons(skaf78(sk6),cons(skaf79(sk6),skaf81(sk6))) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f3086,plain,
( ~ sQ188_spl
| sk6 = cons(skaf78(sk6),cons(skaf79(sk6),skaf81(sk6))) ),
inference(component_clause,[status(thm)],[f3085]) ).
fof(f3089,definition,
! [X0] :
( sQ189_spl
<=> ( ~ ssList(X0)
| ~ rearsegP(sk6,X0)
| sk6 = X0
| ~ ssList(skaf46(sk6,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f3090,plain,
! [X0] :
( ~ sQ189_spl
| ~ ssList(X0)
| ~ rearsegP(sk6,X0)
| sk6 = X0
| ~ ssList(skaf46(sk6,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f3089]) ).
fof(f3092,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f3073,f3089,f1274,f1584]) ).
fof(f3093,definition,
! [X0] :
( sQ190_spl
<=> ( ~ ssList(X0)
| ~ segmentP(sk6,X0)
| sk6 = skaf48(X0,sk6)
| ~ ssList(app(skaf47(sk6,X0),X0))
| ~ ssList(skaf48(X0,sk6)) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f3096,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f3074,f3093,f1274,f1584]) ).
fof(f3118,definition,
! [X0] :
( sQ196_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(sk6,X0)
| sk6 = skaf45(sk6,X0)
| ~ ssList(X0)
| ~ ssList(skaf45(sk6,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f3121,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f3081,f3118,f1274,f1584]) ).
fof(f3127,plain,
( sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2843,f219]) ).
fof(f3128,plain,
sQ151_spl,
inference(contradiction_clause,[status(thm)],[f3127]) ).
fof(f3129,plain,
! [X0] :
( ~ sQ189_spl
| ~ rearsegP(sk6,X0)
| sk6 = X0
| ~ ssList(skaf46(sk6,X0))
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3090]) ).
fof(f3137,definition,
( sQ198_spl
<=> equalelemsP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f3160,plain,
( sQ172_spl
| ~ ssList(skaf73(sk6))
| ~ ssItem(skaf70(sk6)) ),
inference(resolution,[status(thm)],[f2913,f291]) ).
fof(f3161,definition,
( sQ199_spl
<=> ssItem(skaf70(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f3163,plain,
( sQ199_spl
| ~ ssItem(skaf70(sk6)) ),
inference(component_clause,[status(thm)],[f3161]) ).
fof(f3164,definition,
( sQ200_spl
<=> ssList(skaf73(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f3166,plain,
( sQ200_spl
| ~ ssList(skaf73(sk6)) ),
inference(component_clause,[status(thm)],[f3164]) ).
fof(f3167,plain,
( sQ172_spl
| ~ sQ200_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f3160,f3161,f3164,f2911]) ).
fof(f3168,plain,
( sQ200_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3166,f226]) ).
fof(f3169,plain,
sQ200_spl,
inference(contradiction_clause,[status(thm)],[f3168]) ).
fof(f3170,plain,
( sQ199_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3163,f229]) ).
fof(f3171,plain,
sQ199_spl,
inference(contradiction_clause,[status(thm)],[f3170]) ).
fof(f3172,plain,
( sQ168_spl
| ~ ssList(skaf68(sk6))
| ~ ssItem(skaf65(sk6)) ),
inference(resolution,[status(thm)],[f2900,f291]) ).
fof(f3173,definition,
( sQ201_spl
<=> ssItem(skaf65(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f3175,plain,
( sQ201_spl
| ~ ssItem(skaf65(sk6)) ),
inference(component_clause,[status(thm)],[f3173]) ).
fof(f3176,definition,
( sQ202_spl
<=> ssList(skaf68(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f3178,plain,
( sQ202_spl
| ~ ssList(skaf68(sk6)) ),
inference(component_clause,[status(thm)],[f3176]) ).
fof(f3179,plain,
( sQ168_spl
| ~ sQ202_spl
| ~ sQ201_spl ),
inference(split_clause,[status(thm)],[f3172,f3173,f3176,f2898]) ).
fof(f3180,plain,
( sQ202_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3178,f231]) ).
fof(f3181,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f3180]) ).
fof(f3182,plain,
( sQ201_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3175,f234]) ).
fof(f3183,plain,
sQ201_spl,
inference(contradiction_clause,[status(thm)],[f3182]) ).
fof(f3184,plain,
( sQ164_spl
| ~ ssList(skaf63(sk6))
| ~ ssItem(skaf60(sk6)) ),
inference(resolution,[status(thm)],[f2887,f291]) ).
fof(f3185,definition,
( sQ203_spl
<=> ssItem(skaf60(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f3187,plain,
( sQ203_spl
| ~ ssItem(skaf60(sk6)) ),
inference(component_clause,[status(thm)],[f3185]) ).
fof(f3188,definition,
( sQ204_spl
<=> ssList(skaf63(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f3190,plain,
( sQ204_spl
| ~ ssList(skaf63(sk6)) ),
inference(component_clause,[status(thm)],[f3188]) ).
fof(f3191,plain,
( sQ164_spl
| ~ sQ204_spl
| ~ sQ203_spl ),
inference(split_clause,[status(thm)],[f3184,f3185,f3188,f2885]) ).
fof(f3192,plain,
( sQ204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3190,f236]) ).
fof(f3193,plain,
sQ204_spl,
inference(contradiction_clause,[status(thm)],[f3192]) ).
fof(f3194,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3187,f239]) ).
fof(f3195,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f3194]) ).
fof(f3196,plain,
( sQ160_spl
| ~ ssList(skaf58(sk6))
| ~ ssItem(skaf55(sk6)) ),
inference(resolution,[status(thm)],[f2874,f291]) ).
fof(f3197,definition,
( sQ205_spl
<=> ssItem(skaf55(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f3199,plain,
( sQ205_spl
| ~ ssItem(skaf55(sk6)) ),
inference(component_clause,[status(thm)],[f3197]) ).
fof(f3200,definition,
( sQ206_spl
<=> ssList(skaf58(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f3202,plain,
( sQ206_spl
| ~ ssList(skaf58(sk6)) ),
inference(component_clause,[status(thm)],[f3200]) ).
fof(f3203,plain,
( sQ160_spl
| ~ sQ206_spl
| ~ sQ205_spl ),
inference(split_clause,[status(thm)],[f3196,f3197,f3200,f2872]) ).
fof(f3204,plain,
( sQ206_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3202,f241]) ).
fof(f3205,plain,
sQ206_spl,
inference(contradiction_clause,[status(thm)],[f3204]) ).
fof(f3206,plain,
( sQ205_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3199,f244]) ).
fof(f3207,plain,
sQ205_spl,
inference(contradiction_clause,[status(thm)],[f3206]) ).
fof(f3208,plain,
( sQ156_spl
| ~ ssList(skaf53(sk6))
| ~ ssItem(skaf50(sk6)) ),
inference(resolution,[status(thm)],[f2861,f291]) ).
fof(f3209,definition,
( sQ207_spl
<=> ssItem(skaf50(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f3211,plain,
( sQ207_spl
| ~ ssItem(skaf50(sk6)) ),
inference(component_clause,[status(thm)],[f3209]) ).
fof(f3212,definition,
( sQ208_spl
<=> ssList(skaf53(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f3214,plain,
( sQ208_spl
| ~ ssList(skaf53(sk6)) ),
inference(component_clause,[status(thm)],[f3212]) ).
fof(f3215,plain,
( sQ156_spl
| ~ sQ208_spl
| ~ sQ207_spl ),
inference(split_clause,[status(thm)],[f3208,f3209,f3212,f2859]) ).
fof(f3216,plain,
( sQ208_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3214,f246]) ).
fof(f3217,plain,
sQ208_spl,
inference(contradiction_clause,[status(thm)],[f3216]) ).
fof(f3218,plain,
( sQ207_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3211,f249]) ).
fof(f3219,plain,
sQ207_spl,
inference(contradiction_clause,[status(thm)],[f3218]) ).
fof(f3220,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(X2,cons(X3,X1)))
| ~ ssList(cons(X3,X0))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f576,f290]) ).
fof(f3223,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(X2,cons(X3,X1)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3220,f291]) ).
fof(f3303,definition,
( sQ211_spl
<=> hd(sk3) = hd(sk6) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f3304,plain,
( ~ sQ211_spl
| hd(sk3) = hd(sk6) ),
inference(component_clause,[status(thm)],[f3303]) ).
fof(f3307,definition,
( sQ212_spl
<=> hd(sk3) = hd(sk3) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f3328,definition,
( sQ213_spl
<=> ssList(skaf82(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f3330,plain,
( sQ213_spl
| ~ ssList(skaf82(sk6)) ),
inference(component_clause,[status(thm)],[f3328]) ).
fof(f3333,definition,
( sQ214_spl
<=> ssList(tl(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f3335,plain,
( sQ214_spl
| ~ ssList(tl(sk6)) ),
inference(component_clause,[status(thm)],[f3333]) ).
fof(f3347,definition,
( sQ215_spl
<=> hd(sk3) = sk8 ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f3348,plain,
( ~ sQ215_spl
| hd(sk3) = sk8 ),
inference(component_clause,[status(thm)],[f3347]) ).
fof(f3352,definition,
( sQ216_spl
<=> cons(sk8,tl(sk3)) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f3384,definition,
! [X1,X2,X3] :
( sQ221_spl
<=> ( ~ ssList(app(X2,cons(X3,X1)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f3387,plain,
( ~ sQ0_spl
| sQ221_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f3223,f959,f3384,f456]) ).
fof(f3391,plain,
( ~ sQ172_spl
| ~ sQ25_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2912,f960]) ).
fof(f3432,plain,
( ~ sQ172_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f3391]) ).
fof(f3449,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1438,f290]) ).
fof(f3450,plain,
! [X0,X1] :
( skaf46(app(X1,X0),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf46(app(X1,X0),X0))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1392,f290]) ).
fof(f3451,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3449,f255]) ).
fof(f3452,plain,
! [X0,X1] :
( skaf46(app(X1,X0),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3450,f254]) ).
fof(f3543,plain,
( ~ sQ111_spl
| ~ sQ79_spl
| app(sk6,sk6) = sk3 ),
inference(forward_demodulation,[status(thm)],[f1678,f2069]) ).
fof(f3554,plain,
( ~ sQ111_spl
| ~ sQ79_spl
| app(sk6,sk6) = sk6 ),
inference(forward_demodulation,[status(thm)],[f1678,f3543]) ).
fof(f3558,plain,
( ~ sQ60_spl
| ~ sQ130_spl
| ssList(app(cons(sk8,nil),sk7)) ),
inference(forward_demodulation,[status(thm)],[f2178,f1582]) ).
fof(f3600,plain,
( sQ85_spl
| ~ sQ130_spl
| sk3 != app(cons(sk8,nil),sk7) ),
inference(forward_demodulation,[status(thm)],[f2178,f1716]) ).
fof(f3602,plain,
! [X0] :
( ~ sQ68_spl
| ~ sQ130_spl
| X0 = app(cons(sk8,nil),sk7)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ),
inference(forward_demodulation,[status(thm)],[f2178,f1615]) ).
fof(f3605,plain,
( ~ sQ35_spl
| ~ sQ130_spl
| sk3 = app(sk6,app(cons(sk8,nil),sk7)) ),
inference(forward_demodulation,[status(thm)],[f2178,f1278]) ).
fof(f3608,plain,
( ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ111_spl
| app(sk3,sk7) = sk3 ),
inference(forward_demodulation,[status(thm)],[f2069,f2217]) ).
fof(f3625,plain,
( ~ sQ60_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ssList(app(sk3,sk7)) ),
inference(backward_demodulation,[status(thm)],[f482,f3558]) ).
fof(f3626,plain,
( ~ sQ35_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sk3 = app(sk6,app(sk3,sk7)) ),
inference(backward_demodulation,[status(thm)],[f482,f3605]) ).
fof(f3629,plain,
! [X0] :
( ~ sQ68_spl
| ~ sQ130_spl
| ~ sQ7_spl
| X0 = app(sk3,sk7)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ),
inference(backward_demodulation,[status(thm)],[f482,f3602]) ).
fof(f3633,plain,
( sQ85_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sk3 != app(sk3,sk7) ),
inference(backward_demodulation,[status(thm)],[f482,f3600]) ).
fof(f3643,plain,
( sQ85_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ111_spl
| sk3 != sk3 ),
inference(forward_demodulation,[status(thm)],[f3608,f3633]) ).
fof(f3644,plain,
( sQ85_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ111_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3643]) ).
fof(f3645,plain,
( sQ85_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f3644]) ).
fof(f3773,plain,
( ~ sQ95_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f243,f3804]) ).
fof(f3804,plain,
! [X0] :
( ~ sQ95_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1870]) ).
fof(f3984,plain,
( sQ4_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f460]) ).
fof(f3985,plain,
( sQ4_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3984]) ).
fof(f4176,plain,
( ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ61_spl
| sk4 = sk6 ),
inference(forward_demodulation,[status(thm)],[f2562,f2561]) ).
fof(f4325,plain,
( ~ sQ5_spl
| ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ61_spl
| nil = sk6 ),
inference(forward_demodulation,[status(thm)],[f4176,f474]) ).
fof(f4388,plain,
! [X0] :
( ~ sQ43_spl
| ~ sQ1_spl
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1325,f460]) ).
fof(f4405,plain,
( ~ sQ5_spl
| ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ61_spl
| sk7 = sk6 ),
inference(backward_demodulation,[status(thm)],[f1318,f4325]) ).
fof(f4702,plain,
( ~ sQ61_spl
| ~ sQ43_spl
| sk7 = sk6 ),
inference(forward_demodulation,[status(thm)],[f1318,f1585]) ).
fof(f4976,plain,
( ~ sQ3_spl
| ~ sQ43_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f467,f4388]) ).
fof(f4977,plain,
( ~ sQ3_spl
| ~ sQ43_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f4976]) ).
fof(f5092,plain,
( sQ87_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f263,f1739]) ).
fof(f5093,plain,
( sQ87_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f5092,f655,f1737]) ).
fof(f5112,definition,
( sQ237_spl
<=> ssList(app(sk3,sk7)) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f5114,plain,
( sQ237_spl
| ~ ssList(app(sk3,sk7)) ),
inference(component_clause,[status(thm)],[f5112]) ).
fof(f5128,plain,
( sQ237_spl
| ~ sQ60_spl
| ~ sQ130_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5114,f3625]) ).
fof(f5129,plain,
( sQ237_spl
| ~ sQ60_spl
| ~ sQ130_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f5128]) ).
fof(f5139,plain,
! [X0] :
( ~ sQ96_spl
| ~ ssList(sk3)
| ~ ssList(X0)
| frontsegP(app(sk3,X0),sk6)
| ~ ssList(app(sk3,X0)) ),
inference(resolution,[status(thm)],[f1915,f513]) ).
fof(f5142,definition,
! [X0] :
( sQ242_spl
<=> ( ~ ssList(X0)
| frontsegP(app(sk3,X0),sk6)
| ~ ssList(app(sk3,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f5145,plain,
( ~ sQ96_spl
| ~ sQ12_spl
| sQ242_spl ),
inference(split_clause,[status(thm)],[f5139,f5142,f655,f1914]) ).
fof(f5282,definition,
( sQ255_spl
<=> app(sk3,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f5283,plain,
( ~ sQ255_spl
| app(sk3,nil) = sk3 ),
inference(component_clause,[status(thm)],[f5282]) ).
fof(f5284,plain,
( sQ255_spl
| app(sk3,nil) != sk3 ),
inference(component_clause,[status(thm)],[f5282]) ).
fof(f5287,plain,
! [X0] :
( ~ sQ255_spl
| X0 = nil
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0)
| app(sk3,X0) != sk3 ),
inference(paramodulation,[status(thm)],[f5283,f375]) ).
fof(f5289,plain,
! [X0] :
( ~ sQ255_spl
| app(sk3,X0) = app(sk3,app(nil,X0))
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f5283,f373]) ).
fof(f5290,plain,
( ~ sQ255_spl
| skaf45(sk3,sk3) = nil
| ~ ssList(nil)
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f5283,f3451]) ).
fof(f5291,plain,
( ~ sQ255_spl
| skaf46(sk3,nil) = sk3
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f5283,f3452]) ).
fof(f5293,plain,
( ~ sQ255_spl
| rearsegP(sk3,nil)
| ~ ssList(nil)
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f5283,f511]) ).
fof(f5298,definition,
! [X0] :
( sQ256_spl
<=> ( X0 = nil
| ~ ssList(X0)
| app(sk3,X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f5299,plain,
! [X0] :
( ~ sQ256_spl
| X0 = nil
| ~ ssList(X0)
| app(sk3,X0) != sk3 ),
inference(component_clause,[status(thm)],[f5298]) ).
fof(f5301,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f5287,f5298,f655,f792,f5282]) ).
fof(f5303,definition,
! [X0] :
( sQ257_spl
<=> ( app(sk3,X0) = app(sk3,app(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f5304,plain,
! [X0] :
( ~ sQ257_spl
| app(sk3,X0) = app(sk3,app(nil,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f5303]) ).
fof(f5306,plain,
( ~ sQ255_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ257_spl ),
inference(split_clause,[status(thm)],[f5289,f5303,f792,f655,f5282]) ).
fof(f5307,definition,
( sQ258_spl
<=> skaf45(sk3,sk3) = nil ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f5308,plain,
( ~ sQ258_spl
| skaf45(sk3,sk3) = nil ),
inference(component_clause,[status(thm)],[f5307]) ).
fof(f5310,plain,
( ~ sQ255_spl
| sQ258_spl
| ~ sQ18_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f5290,f655,f792,f5307,f5282]) ).
fof(f5311,definition,
( sQ259_spl
<=> skaf46(sk3,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f5312,plain,
( ~ sQ259_spl
| skaf46(sk3,nil) = sk3 ),
inference(component_clause,[status(thm)],[f5311]) ).
fof(f5314,plain,
( ~ sQ255_spl
| sQ259_spl
| ~ sQ12_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f5291,f792,f655,f5311,f5282]) ).
fof(f5316,plain,
( ~ sQ255_spl
| sQ121_spl
| ~ sQ18_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f5293,f655,f792,f2129,f5282]) ).
fof(f5324,plain,
( ~ sQ68_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ256_spl
| ~ ssList(sk3)
| app(sk6,sk3) != sk3
| sk7 = nil
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f5299,f3629]) ).
fof(f5325,plain,
( ~ sQ255_spl
| ~ sQ256_spl
| nil = nil
| ~ ssList(nil)
| sk3 != sk3 ),
inference(paramodulation,[status(thm)],[f5283,f5299]) ).
fof(f5328,plain,
( ~ sQ68_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ256_spl
| ~ sQ12_spl
| ~ sQ111_spl
| sQ43_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f5324,f1268,f1317,f2068,f655,f5298,f481,f2177,f1614]) ).
fof(f5329,plain,
( ~ sQ255_spl
| ~ sQ256_spl
| sQ42_spl
| ~ sQ18_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f5325,f663,f792,f1312,f5298,f5282]) ).
fof(f5374,plain,
! [X0] :
( ~ sQ255_spl
| sk3 = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sk3)
| sk3 != app(X0,nil) ),
inference(paramodulation,[status(thm)],[f5283,f377]) ).
fof(f5388,definition,
! [X0] :
( sQ265_spl
<=> ( sk3 = X0
| ~ ssList(X0)
| sk3 != app(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f5391,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f5374,f5388,f655,f792,f5282]) ).
fof(f5677,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f3773]) ).
fof(f5743,definition,
( sQ308_spl
<=> ssList(skaf82(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f5745,plain,
( sQ308_spl
| ~ ssList(skaf82(sk3)) ),
inference(component_clause,[status(thm)],[f5743]) ).
fof(f5758,plain,
( sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5745,f217]) ).
fof(f5759,plain,
sQ308_spl,
inference(contradiction_clause,[status(thm)],[f5758]) ).
fof(f5781,plain,
( ~ sQ215_spl
| nil = sk3
| cons(sk8,tl(sk3)) = sk3
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f3348,f311]) ).
fof(f5792,plain,
( ~ sQ215_spl
| sQ6_spl
| sQ216_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f5781,f655,f3352,f477,f3347]) ).
fof(f5882,plain,
! [X0] :
( ~ sQ257_spl
| X0 = app(nil,X0)
| ~ ssList(app(nil,X0))
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f5304,f375]) ).
fof(f5884,definition,
! [X0] :
( sQ324_spl
<=> ( X0 = app(nil,X0)
| ~ ssList(app(nil,X0))
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f5887,plain,
( ~ sQ257_spl
| ~ sQ12_spl
| sQ324_spl ),
inference(split_clause,[status(thm)],[f5882,f5884,f655,f5303]) ).
fof(f5936,plain,
! [X0] :
( ~ sQ255_spl
| segmentP(app(sk3,X0),nil)
| ~ ssList(app(app(sk3,nil),X0))
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f5283,f516]) ).
fof(f5954,definition,
! [X0] :
( sQ332_spl
<=> ( segmentP(app(sk3,X0),nil)
| ~ ssList(app(app(sk3,nil),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f5957,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ332_spl ),
inference(split_clause,[status(thm)],[f5936,f5954,f655,f792,f5282]) ).
fof(f6336,plain,
! [X0] :
( ~ sQ255_spl
| rearsegP(sk3,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ rearsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f5283,f355]) ).
fof(f6353,definition,
! [X0] :
( sQ356_spl
<=> ( rearsegP(sk3,X0)
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f6356,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ356_spl ),
inference(split_clause,[status(thm)],[f6336,f6353,f655,f792,f5282]) ).
fof(f6420,definition,
( sQ358_spl
<=> ssList(skaf46(sk3,nil)) ),
introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition]) ).
fof(f6422,plain,
( sQ358_spl
| ~ ssList(skaf46(sk3,nil)) ),
inference(component_clause,[status(thm)],[f6420]) ).
fof(f6434,definition,
( sQ359_spl
<=> ssList(skaf45(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f6436,plain,
( sQ359_spl
| ~ ssList(skaf45(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f6434]) ).
fof(f6532,definition,
( sQ365_spl
<=> app(sk3,nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition]) ).
fof(f6533,plain,
( ~ sQ365_spl
| app(sk3,nil) = nil ),
inference(component_clause,[status(thm)],[f6532]) ).
fof(f6650,definition,
( sQ370_spl
<=> app(app(sk6,sk3),sk7) = app(sk6,sk3) ),
introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition]) ).
fof(f6651,plain,
( ~ sQ370_spl
| app(app(sk6,sk3),sk7) = app(sk6,sk3) ),
inference(component_clause,[status(thm)],[f6650]) ).
fof(f6652,plain,
( sQ370_spl
| app(app(sk6,sk3),sk7) != app(sk6,sk3) ),
inference(component_clause,[status(thm)],[f6650]) ).
fof(f6664,plain,
! [X0,X1] :
( ~ sQ96_spl
| frontsegP(app(X0,X1),sk6)
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ frontsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f356,f1915]) ).
fof(f6669,plain,
! [X0] :
( ~ sQ255_spl
| frontsegP(sk3,X0)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f5283,f356]) ).
fof(f6677,definition,
! [X0,X1] :
( sQ372_spl
<=> ( frontsegP(app(X0,X1),sk6)
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f6680,plain,
( ~ sQ96_spl
| ~ sQ12_spl
| sQ372_spl ),
inference(split_clause,[status(thm)],[f6664,f6677,f655,f1914]) ).
fof(f6691,plain,
( ~ sQ255_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f6669,f2265,f792,f655,f5282]) ).
fof(f6867,definition,
( sQ402_spl
<=> ssList(skaf75(nil)) ),
introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition]) ).
fof(f6869,plain,
( sQ402_spl
| ~ ssList(skaf75(nil)) ),
inference(component_clause,[status(thm)],[f6867]) ).
fof(f6871,plain,
( sQ402_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6869,f224]) ).
fof(f6872,plain,
sQ402_spl,
inference(contradiction_clause,[status(thm)],[f6871]) ).
fof(f6890,plain,
! [X0] :
( ~ sQ255_spl
| app(sk3,nil) = X0
| ~ rearsegP(X0,sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ rearsegP(nil,X0) ),
inference(paramodulation,[status(thm)],[f5283,f1442]) ).
fof(f6915,definition,
! [X0] :
( sQ408_spl
<=> ( app(sk3,nil) = X0
| ~ rearsegP(X0,sk3)
| ~ ssList(X0)
| ~ rearsegP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition]) ).
fof(f6918,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ408_spl ),
inference(split_clause,[status(thm)],[f6890,f6915,f655,f792,f5282]) ).
fof(f6932,plain,
( ~ sQ40_spl
| ~ sQ130_spl
| ~ sQ7_spl
| app(sk6,sk3) = sk3
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ frontsegP(sk6,sk3) ),
inference(resolution,[status(thm)],[f1445,f2582]) ).
fof(f6938,plain,
! [X0] :
( ~ sQ255_spl
| app(sk3,nil) = X0
| ~ frontsegP(X0,sk3)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f5283,f1445]) ).
fof(f6941,plain,
( ~ sQ40_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sQ111_spl
| ~ sQ34_spl
| ~ sQ12_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f6932,f1455,f655,f1274,f2068,f481,f2177,f1298]) ).
fof(f6958,definition,
! [X0] :
( sQ414_spl
<=> ( app(sk3,nil) = X0
| ~ frontsegP(X0,sk3)
| ~ ssList(X0)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition]) ).
fof(f6961,plain,
( ~ sQ255_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ414_spl ),
inference(split_clause,[status(thm)],[f6938,f6958,f792,f655,f5282]) ).
fof(f7021,plain,
( ~ sQ35_spl
| ~ sQ130_spl
| ~ sQ7_spl
| hd(sk3) = hd(sk6)
| nil = sk6
| ~ ssList(sk6)
| ~ ssList(app(sk3,sk7)) ),
inference(paramodulation,[status(thm)],[f3626,f338]) ).
fof(f7025,plain,
( ~ sQ255_spl
| hd(sk3) = hd(sk3)
| nil = sk3
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f5283,f338]) ).
fof(f7027,plain,
( ~ sQ35_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sQ211_spl
| sQ61_spl
| ~ sQ34_spl
| ~ sQ237_spl ),
inference(split_clause,[status(thm)],[f7021,f5112,f1274,f1584,f3303,f481,f2177,f1277]) ).
fof(f7040,plain,
( ~ sQ255_spl
| sQ212_spl
| sQ6_spl
| ~ sQ12_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f7025,f792,f655,f477,f3307,f5282]) ).
fof(f7080,plain,
( ~ sQ211_spl
| ~ sQ215_spl
| sk8 = hd(sk6) ),
inference(forward_demodulation,[status(thm)],[f3348,f3304]) ).
fof(f7130,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| app(sk3,sk6) = sk3 ),
inference(backward_demodulation,[status(thm)],[f1585,f5283]) ).
fof(f7133,plain,
( ~ sQ259_spl
| ~ sQ61_spl
| skaf46(sk3,sk6) = sk3 ),
inference(backward_demodulation,[status(thm)],[f1585,f5312]) ).
fof(f7259,plain,
( sQ2_spl
| ~ sQ130_spl
| ~ memberP(sk6,sk8) ),
inference(forward_demodulation,[status(thm)],[f2178,f465]) ).
fof(f7375,plain,
! [X0] :
( ~ sQ87_spl
| rearsegP(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ rearsegP(X0,sk3) ),
inference(resolution,[status(thm)],[f381,f1738]) ).
fof(f7385,plain,
( ~ sQ87_spl
| ~ sQ12_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f7375,f1733,f655,f1737]) ).
fof(f7533,definition,
( sQ436_spl
<=> ssList(cons(skaf55(nil),skaf58(nil))) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f7535,plain,
( sQ436_spl
| ~ ssList(cons(skaf55(nil),skaf58(nil))) ),
inference(component_clause,[status(thm)],[f7533]) ).
fof(f7855,plain,
! [X0] :
( nil = skaf48(X0,nil)
| ~ ssList(app(skaf47(nil,X0),X0))
| ~ ssList(skaf48(X0,nil))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(resolution,[status(thm)],[f403,f334]) ).
fof(f7856,plain,
! [X0] :
( nil = app(skaf47(nil,X0),X0)
| ~ ssList(app(skaf47(nil,X0),X0))
| ~ ssList(skaf48(X0,nil))
| ~ ssList(nil)
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(resolution,[status(thm)],[f403,f332]) ).
fof(f7857,definition,
! [X0] :
( sQ449_spl
<=> ( nil = skaf48(X0,nil)
| ~ ssList(app(skaf47(nil,X0),X0))
| ~ ssList(skaf48(X0,nil))
| ~ ssList(X0)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition]) ).
fof(f7860,plain,
( ~ sQ18_spl
| sQ449_spl ),
inference(split_clause,[status(thm)],[f7855,f7857,f792]) ).
fof(f7861,definition,
! [X0] :
( sQ450_spl
<=> ( nil = app(skaf47(nil,X0),X0)
| ~ ssList(app(skaf47(nil,X0),X0))
| ~ ssList(skaf48(X0,nil))
| ~ ssList(X0)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition]) ).
fof(f7864,plain,
( ~ sQ18_spl
| sQ450_spl ),
inference(split_clause,[status(thm)],[f7856,f7861,f792]) ).
fof(f7872,plain,
! [X0,X1] :
( ~ sQ255_spl
| segmentP(app(sk3,X1),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ),
inference(paramodulation,[status(thm)],[f5283,f409]) ).
fof(f7888,definition,
! [X0,X1] :
( sQ454_spl
<=> ( segmentP(app(sk3,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition]) ).
fof(f7891,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ454_spl ),
inference(split_clause,[status(thm)],[f7872,f7888,f655,f792,f5282]) ).
fof(f8013,plain,
! [X0,X1] :
( ~ sQ255_spl
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ rearsegP(nil,X1)
| rearsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,sk3) ),
inference(paramodulation,[status(thm)],[f5283,f1671]) ).
fof(f8035,definition,
! [X0,X1] :
( sQ461_spl
<=> ( ~ rearsegP(nil,X1)
| rearsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ461_spl])],[split_symbol_definition]) ).
fof(f8038,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ461_spl ),
inference(split_clause,[status(thm)],[f8013,f8035,f655,f792,f5282]) ).
fof(f8123,plain,
( ~ sQ211_spl
| ~ sQ215_spl
| nil = sk6
| cons(sk8,tl(sk6)) = sk6
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f7080,f311]) ).
fof(f8133,definition,
( sQ467_spl
<=> cons(sk8,tl(sk6)) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition]) ).
fof(f8134,plain,
( ~ sQ467_spl
| cons(sk8,tl(sk6)) = sk6 ),
inference(component_clause,[status(thm)],[f8133]) ).
fof(f8136,plain,
( ~ sQ211_spl
| ~ sQ215_spl
| sQ61_spl
| sQ467_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f8123,f1274,f8133,f1584,f3347,f3303]) ).
fof(f8183,definition,
( sQ469_spl
<=> app(sk3,tl(sk6)) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition]) ).
fof(f8184,plain,
( ~ sQ469_spl
| app(sk3,tl(sk6)) = sk6 ),
inference(component_clause,[status(thm)],[f8183]) ).
fof(f8199,definition,
( sQ473_spl
<=> singletonP(sk6) ),
introduced(definition,[new_symbols(definition,[sQ473_spl])],[split_symbol_definition]) ).
fof(f8238,definition,
( sQ482_spl
<=> skaf44(sk6) = sk8 ),
introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition]) ).
fof(f8239,plain,
( ~ sQ482_spl
| skaf44(sk6) = sk8 ),
inference(component_clause,[status(thm)],[f8238]) ).
fof(f8326,plain,
( sQ214_spl
| nil = sk6
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f3335,f280]) ).
fof(f8327,plain,
( sQ214_spl
| sQ61_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f8326,f1274,f1584,f3333]) ).
fof(f8344,definition,
( sQ502_spl
<=> cons(sk8,skaf82(sk6)) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f8345,plain,
( ~ sQ502_spl
| cons(sk8,skaf82(sk6)) = sk6 ),
inference(component_clause,[status(thm)],[f8344]) ).
fof(f8350,plain,
( ~ sQ482_spl
| cons(sk8,nil) = sk6
| ~ ssList(sk6)
| ~ singletonP(sk6) ),
inference(paramodulation,[status(thm)],[f8239,f308]) ).
fof(f8351,definition,
( sQ503_spl
<=> cons(sk8,nil) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ503_spl])],[split_symbol_definition]) ).
fof(f8352,plain,
( ~ sQ503_spl
| cons(sk8,nil) = sk6 ),
inference(component_clause,[status(thm)],[f8351]) ).
fof(f8354,plain,
( ~ sQ482_spl
| sQ503_spl
| ~ sQ34_spl
| ~ sQ473_spl ),
inference(split_clause,[status(thm)],[f8350,f8199,f1274,f8351,f8238]) ).
fof(f8484,definition,
! [X0,X1] :
( sQ509_spl
<=> ( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition]) ).
fof(f8485,plain,
! [X0,X1] :
( ~ sQ509_spl
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(component_clause,[status(thm)],[f8484]) ).
fof(f8607,plain,
! [X0] :
( ~ sQ469_spl
| frontsegP(sk6,X0)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(tl(sk6))
| ~ frontsegP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f8184,f356]) ).
fof(f8621,plain,
( ~ sQ469_spl
| frontsegP(sk6,sk3)
| ~ ssList(sk3)
| ~ ssList(tl(sk6)) ),
inference(paramodulation,[status(thm)],[f8184,f513]) ).
fof(f8649,definition,
! [X0] :
( sQ521_spl
<=> ( frontsegP(sk6,X0)
| ~ ssList(X0)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition]) ).
fof(f8650,plain,
! [X0] :
( ~ sQ521_spl
| frontsegP(sk6,X0)
| ~ ssList(X0)
| ~ frontsegP(sk3,X0) ),
inference(component_clause,[status(thm)],[f8649]) ).
fof(f8652,plain,
( ~ sQ469_spl
| ~ sQ12_spl
| ~ sQ214_spl
| sQ521_spl ),
inference(split_clause,[status(thm)],[f8607,f8649,f3333,f655,f8183]) ).
fof(f8702,plain,
( ~ sQ469_spl
| sQ49_spl
| ~ sQ12_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f8621,f3333,f655,f1455,f8183]) ).
fof(f8787,plain,
( sQ436_spl
| ~ sQ61_spl
| ~ ssList(cons(skaf55(nil),skaf58(sk6))) ),
inference(backward_demodulation,[status(thm)],[f1585,f7535]) ).
fof(f8841,plain,
( sQ436_spl
| ~ sQ61_spl
| ~ ssList(cons(skaf55(sk6),skaf58(sk6))) ),
inference(forward_demodulation,[status(thm)],[f1585,f8787]) ).
fof(f8842,plain,
( sQ436_spl
| ~ sQ61_spl
| ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8841,f2873]) ).
fof(f8843,plain,
( sQ436_spl
| ~ sQ61_spl
| ~ sQ160_spl ),
inference(contradiction_clause,[status(thm)],[f8842]) ).
fof(f8844,plain,
( sQ358_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6422,f254]) ).
fof(f8845,plain,
sQ358_spl,
inference(contradiction_clause,[status(thm)],[f8844]) ).
fof(f8880,plain,
( ~ sQ7_spl
| equalelemsP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f268]) ).
fof(f8884,plain,
( ~ sQ7_spl
| sQ198_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f8880,f470,f3137,f481]) ).
fof(f8890,plain,
! [X0] :
( ~ sQ7_spl
| app(sk3,X0) = cons(sk8,X0)
| ~ ssList(X0)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f335]) ).
fof(f8891,definition,
! [X0] :
( sQ536_spl
<=> ( app(sk3,X0) = cons(sk8,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f8892,plain,
! [X0] :
( ~ sQ536_spl
| app(sk3,X0) = cons(sk8,X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f8891]) ).
fof(f8894,plain,
( ~ sQ7_spl
| sQ536_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f8890,f470,f8891,f481]) ).
fof(f8899,plain,
( ~ sQ7_spl
| duplicatefreeP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f269]) ).
fof(f8900,plain,
( ~ sQ7_spl
| sQ27_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f8899,f470,f982,f481]) ).
fof(f8901,plain,
( ~ sQ7_spl
| strictorderedP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f270]) ).
fof(f8902,plain,
( ~ sQ7_spl
| sQ187_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f8901,f470,f3067,f481]) ).
fof(f8903,plain,
( ~ sQ7_spl
| totalorderedP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f271]) ).
fof(f8904,plain,
( ~ sQ7_spl
| sQ186_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f8903,f470,f3062,f481]) ).
fof(f8905,plain,
( ~ sQ502_spl
| ~ ssList(skaf82(sk6))
| ~ ssItem(sk8)
| sk6 != nil ),
inference(paramodulation,[status(thm)],[f8345,f304]) ).
fof(f8906,plain,
( ~ sQ502_spl
| ~ sQ213_spl
| ~ sQ4_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f8905,f1584,f470,f3328,f8344]) ).
fof(f8907,plain,
( sQ213_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3330,f217]) ).
fof(f8908,plain,
sQ213_spl,
inference(contradiction_clause,[status(thm)],[f8907]) ).
fof(f8915,definition,
( sQ538_spl
<=> lt(sk8,sk8) ),
introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition]) ).
fof(f8916,plain,
( ~ sQ538_spl
| lt(sk8,sk8) ),
inference(component_clause,[status(thm)],[f8915]) ).
fof(f8925,plain,
( sQ255_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f278,f5284]) ).
fof(f8928,plain,
( sQ255_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f8925,f655,f5282]) ).
fof(f8995,definition,
( sQ540_spl
<=> ssItem(hd(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ540_spl])],[split_symbol_definition]) ).
fof(f8997,plain,
( sQ540_spl
| ~ ssItem(hd(sk6)) ),
inference(component_clause,[status(thm)],[f8995]) ).
fof(f9015,plain,
! [X0] :
( ~ sQ255_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ memberP(nil,X0) ),
inference(paramodulation,[status(thm)],[f5283,f360]) ).
fof(f9021,plain,
( ~ sQ255_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f9015,f789,f792,f655,f5282]) ).
fof(f9078,plain,
( ~ sQ7_spl
| strictorderP(sk3)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f272]) ).
fof(f9080,plain,
( ~ sQ7_spl
| sQ185_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f9078,f470,f3057,f481]) ).
fof(f9153,definition,
( sQ548_spl
<=> ssItem(skaf83(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition]) ).
fof(f9155,plain,
( sQ548_spl
| ~ ssItem(skaf83(sk6)) ),
inference(component_clause,[status(thm)],[f9153]) ).
fof(f9160,plain,
( sQ548_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9155,f216]) ).
fof(f9161,plain,
sQ548_spl,
inference(contradiction_clause,[status(thm)],[f9160]) ).
fof(f9184,plain,
! [X0] :
( ~ sQ255_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f5283,f359]) ).
fof(f9187,plain,
( ~ sQ255_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f9184,f1764,f792,f655,f5282]) ).
fof(f9194,plain,
( ~ sQ538_spl
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f267,f8916]) ).
fof(f9195,plain,
( ~ sQ538_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f9194,f470,f8915]) ).
fof(f9231,plain,
( sQ540_spl
| nil = sk6
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f281,f8997]) ).
fof(f9233,plain,
( sQ540_spl
| sQ61_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f9231,f1274,f1584,f8995]) ).
fof(f9385,definition,
( sQ569_spl
<=> duplicatefreeP(sk6) ),
introduced(definition,[new_symbols(definition,[sQ569_spl])],[split_symbol_definition]) ).
fof(f9445,plain,
! [X0,X1] :
( ~ sQ509_spl
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f8485]) ).
fof(f9446,plain,
( ~ sQ7_spl
| ~ sQ503_spl
| sk6 = sk3 ),
inference(backward_demodulation,[status(thm)],[f8352,f482]) ).
fof(f9451,plain,
( ~ sQ370_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sk3 = app(sk6,sk3) ),
inference(forward_demodulation,[status(thm)],[f2590,f6651]) ).
fof(f9452,plain,
( ~ sQ370_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9451,f2070]) ).
fof(f9453,plain,
( ~ sQ370_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f9452]) ).
fof(f9456,plain,
( ~ sQ365_spl
| ~ sQ255_spl
| sk3 = nil ),
inference(forward_demodulation,[status(thm)],[f5283,f6533]) ).
fof(f9457,plain,
( ~ sQ365_spl
| ~ sQ255_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9456,f479]) ).
fof(f9458,plain,
( ~ sQ365_spl
| ~ sQ255_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f9457]) ).
fof(f9501,plain,
( sQ359_spl
| ~ sQ258_spl
| ~ ssList(nil) ),
inference(forward_demodulation,[status(thm)],[f5308,f6436]) ).
fof(f9502,plain,
( sQ359_spl
| ~ sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9501,f212]) ).
fof(f9503,plain,
( sQ359_spl
| ~ sQ258_spl ),
inference(contradiction_clause,[status(thm)],[f9502]) ).
fof(f9587,plain,
( ~ sQ7_spl
| ~ sQ503_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f9446,f1677,f8351,f481]) ).
fof(f9883,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ130_spl
| X0 = sk7
| ~ ssList(X0)
| app(cons(sk8,nil),X0) != sk3 ),
inference(forward_demodulation,[status(thm)],[f2178,f2023]) ).
fof(f9948,plain,
( sQ370_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sk3 != app(sk6,sk3) ),
inference(backward_demodulation,[status(thm)],[f2590,f6652]) ).
fof(f9956,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ130_spl
| ~ sQ7_spl
| X0 = sk7
| ~ ssList(X0)
| app(sk3,X0) != sk3 ),
inference(backward_demodulation,[status(thm)],[f482,f9883]) ).
fof(f9979,plain,
( ~ sQ152_spl
| app(sk6,cons(skaf78(sk6),cons(skaf79(sk6),skaf81(sk6)))) = sk6
| equalelemsP(sk6)
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f2845,f361]) ).
fof(f9981,definition,
( sQ578_spl
<=> app(sk6,cons(skaf78(sk6),cons(skaf79(sk6),skaf81(sk6)))) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition]) ).
fof(f9982,plain,
( ~ sQ578_spl
| app(sk6,cons(skaf78(sk6),cons(skaf79(sk6),skaf81(sk6)))) = sk6 ),
inference(component_clause,[status(thm)],[f9981]) ).
fof(f9984,plain,
( ~ sQ152_spl
| sQ578_spl
| sQ153_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f9979,f1274,f2847,f9981,f2844]) ).
fof(f9985,plain,
( ~ sQ578_spl
| ~ sQ188_spl
| app(sk6,sk6) = sk6 ),
inference(forward_demodulation,[status(thm)],[f3086,f9982]) ).
fof(f10574,plain,
( ~ sQ578_spl
| ~ sQ188_spl
| ~ ssList(sk6)
| app(sk6,sk6) = sk6
| ~ ssList(sk6)
| ~ rearsegP(sk6,sk6) ),
inference(paramodulation,[status(thm)],[f9985,f1384]) ).
fof(f10587,definition,
! [X0] :
( sQ585_spl
<=> ( cons(X0,sk6) = app(cons(X0,sk6),sk6)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition]) ).
fof(f10591,definition,
! [X0] :
( sQ586_spl
<=> ( memberP(sk6,X0)
| memberP(sk6,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f10596,definition,
! [X0] :
( sQ587_spl
<=> ( memberP(sk6,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ587_spl])],[split_symbol_definition]) ).
fof(f10601,definition,
! [X0] :
( sQ588_spl
<=> ( rearsegP(X0,sk6)
| ~ ssList(X0)
| ~ rearsegP(X0,sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition]) ).
fof(f10605,definition,
! [X0,X1] :
( sQ589_spl
<=> ( ~ rearsegP(sk6,X1)
| rearsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition]) ).
fof(f10609,definition,
! [X0,X1] :
( sQ590_spl
<=> ( segmentP(app(sk6,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ590_spl])],[split_symbol_definition]) ).
fof(f10613,definition,
! [X0] :
( sQ591_spl
<=> ( app(sk6,sk6) = X0
| ~ rearsegP(X0,sk6)
| ~ ssList(X0)
| ~ rearsegP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition]) ).
fof(f10617,definition,
( sQ592_spl
<=> frontsegP(sk6,sk6) ),
introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition]) ).
fof(f10618,plain,
( ~ sQ592_spl
| frontsegP(sk6,sk6) ),
inference(component_clause,[status(thm)],[f10617]) ).
fof(f10620,definition,
( sQ593_spl
<=> app(sk6,sk6) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ593_spl])],[split_symbol_definition]) ).
fof(f10621,plain,
( ~ sQ593_spl
| app(sk6,sk6) = sk6 ),
inference(component_clause,[status(thm)],[f10620]) ).
fof(f10622,plain,
( sQ593_spl
| app(sk6,sk6) != sk6 ),
inference(component_clause,[status(thm)],[f10620]) ).
fof(f10624,definition,
( sQ594_spl
<=> rearsegP(sk6,sk6) ),
introduced(definition,[new_symbols(definition,[sQ594_spl])],[split_symbol_definition]) ).
fof(f10625,plain,
( ~ sQ594_spl
| rearsegP(sk6,sk6) ),
inference(component_clause,[status(thm)],[f10624]) ).
fof(f10626,plain,
( sQ594_spl
| ~ rearsegP(sk6,sk6) ),
inference(component_clause,[status(thm)],[f10624]) ).
fof(f10627,plain,
( ~ sQ578_spl
| ~ sQ188_spl
| sQ593_spl
| ~ sQ34_spl
| ~ sQ594_spl ),
inference(split_clause,[status(thm)],[f10574,f10624,f1274,f10620,f3085,f9981]) ).
fof(f10628,definition,
! [X0] :
( sQ595_spl
<=> ( rearsegP(sk6,X0)
| ~ ssList(X0)
| ~ rearsegP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition]) ).
fof(f10632,definition,
! [X0] :
( sQ596_spl
<=> ( segmentP(app(sk6,X0),sk6)
| ~ ssList(app(app(sk6,sk6),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition]) ).
fof(f10636,definition,
! [X0] :
( sQ597_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| app(X0,sk6) != sk6 ) ),
introduced(definition,[new_symbols(definition,[sQ597_spl])],[split_symbol_definition]) ).
fof(f10637,plain,
! [X0] :
( ~ sQ597_spl
| X0 = sk6
| ~ ssList(X0)
| app(X0,sk6) != sk6 ),
inference(component_clause,[status(thm)],[f10636]) ).
fof(f10641,definition,
! [X0] :
( sQ598_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| app(sk6,X0) != sk6 ) ),
introduced(definition,[new_symbols(definition,[sQ598_spl])],[split_symbol_definition]) ).
fof(f10642,plain,
! [X0] :
( ~ sQ598_spl
| X0 = sk6
| ~ ssList(X0)
| app(sk6,X0) != sk6 ),
inference(component_clause,[status(thm)],[f10641]) ).
fof(f10646,definition,
! [X0] :
( sQ599_spl
<=> ( app(sk6,X0) = app(sk6,app(sk6,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ599_spl])],[split_symbol_definition]) ).
fof(f10650,definition,
( sQ600_spl
<=> skaf45(sk6,sk6) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition]) ).
fof(f10654,definition,
( sQ601_spl
<=> skaf46(sk6,sk6) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition]) ).
fof(f10655,plain,
( ~ sQ601_spl
| skaf46(sk6,sk6) = sk6 ),
inference(component_clause,[status(thm)],[f10654]) ).
fof(f10738,plain,
! [X0] :
( ~ sQ255_spl
| cons(X0,sk3) = app(cons(X0,sk3),nil)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f5283,f388]) ).
fof(f10739,plain,
! [X0] :
( ~ sQ255_spl
| memberP(sk3,X0)
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f5283,f390]) ).
fof(f10762,definition,
! [X0] :
( sQ604_spl
<=> ( cons(X0,sk3) = app(cons(X0,sk3),nil)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition]) ).
fof(f10765,plain,
( ~ sQ255_spl
| ~ sQ18_spl
| ~ sQ12_spl
| sQ604_spl ),
inference(split_clause,[status(thm)],[f10738,f10762,f655,f792,f5282]) ).
fof(f10766,definition,
! [X0] :
( sQ605_spl
<=> ( memberP(sk3,X0)
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition]) ).
fof(f10769,plain,
( ~ sQ255_spl
| ~ sQ12_spl
| ~ sQ18_spl
| sQ605_spl ),
inference(split_clause,[status(thm)],[f10739,f10766,f792,f655,f5282]) ).
fof(f10812,plain,
! [X0] :
( ~ sQ593_spl
| cons(X0,sk6) = app(cons(X0,sk6),sk6)
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f10621,f388]) ).
fof(f10813,plain,
! [X0] :
( ~ sQ593_spl
| memberP(sk6,X0)
| memberP(sk6,X0)
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ memberP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f10621,f390]) ).
fof(f10814,plain,
( ~ sQ593_spl
| ~ sQ0_spl
| ~ ssList(sk6)
| ~ ssList(sk6)
| duplicatefreeP(sk6) ),
inference(paramodulation,[status(thm)],[f10621,f754]) ).
fof(f10815,plain,
! [X0] :
( ~ sQ593_spl
| memberP(sk6,X0)
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ memberP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f10621,f359]) ).
fof(f10818,plain,
! [X0,X1] :
( ~ sQ593_spl
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ rearsegP(sk6,X1)
| rearsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,sk6) ),
inference(paramodulation,[status(thm)],[f10621,f1671]) ).
fof(f10819,plain,
! [X0,X1] :
( ~ sQ593_spl
| segmentP(app(sk6,X1),X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(X1)
| ~ segmentP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f10621,f409]) ).
fof(f10820,plain,
! [X0] :
( ~ sQ593_spl
| app(sk6,sk6) = X0
| ~ rearsegP(X0,sk6)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ rearsegP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f10621,f1442]) ).
fof(f10823,plain,
! [X0] :
( ~ sQ593_spl
| rearsegP(sk6,X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ rearsegP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f10621,f355]) ).
fof(f10824,plain,
! [X0] :
( ~ sQ593_spl
| segmentP(app(sk6,X0),sk6)
| ~ ssList(app(app(sk6,sk6),X0))
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f10621,f516]) ).
fof(f10825,plain,
! [X0] :
( ~ sQ593_spl
| X0 = sk6
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ ssList(X0)
| app(X0,sk6) != sk6 ),
inference(paramodulation,[status(thm)],[f10621,f377]) ).
fof(f10827,plain,
! [X0] :
( ~ sQ593_spl
| X0 = sk6
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ ssList(X0)
| app(sk6,X0) != sk6 ),
inference(paramodulation,[status(thm)],[f10621,f375]) ).
fof(f10829,plain,
! [X0] :
( ~ sQ593_spl
| app(sk6,X0) = app(sk6,app(sk6,X0))
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f10621,f373]) ).
fof(f10830,plain,
( ~ sQ593_spl
| skaf45(sk6,sk6) = sk6
| ~ ssList(sk6)
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f10621,f3451]) ).
fof(f10832,plain,
( ~ sQ593_spl
| frontsegP(sk6,sk6)
| ~ ssList(sk6)
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f10621,f513]) ).
fof(f10835,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ585_spl ),
inference(split_clause,[status(thm)],[f10812,f10587,f1274,f10620]) ).
fof(f10836,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ586_spl ),
inference(split_clause,[status(thm)],[f10813,f10591,f1274,f10620]) ).
fof(f10837,plain,
( ~ sQ593_spl
| ~ sQ0_spl
| ~ sQ34_spl
| sQ569_spl ),
inference(split_clause,[status(thm)],[f10814,f9385,f1274,f456,f10620]) ).
fof(f10838,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ587_spl ),
inference(split_clause,[status(thm)],[f10815,f10596,f1274,f10620]) ).
fof(f10841,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ589_spl ),
inference(split_clause,[status(thm)],[f10818,f10605,f1274,f10620]) ).
fof(f10842,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ590_spl ),
inference(split_clause,[status(thm)],[f10819,f10609,f1274,f10620]) ).
fof(f10843,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ591_spl ),
inference(split_clause,[status(thm)],[f10820,f10613,f1274,f10620]) ).
fof(f10846,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ595_spl ),
inference(split_clause,[status(thm)],[f10823,f10628,f1274,f10620]) ).
fof(f10847,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ596_spl ),
inference(split_clause,[status(thm)],[f10824,f10632,f1274,f10620]) ).
fof(f10848,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ597_spl ),
inference(split_clause,[status(thm)],[f10825,f10636,f1274,f10620]) ).
fof(f10850,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ598_spl ),
inference(split_clause,[status(thm)],[f10827,f10641,f1274,f10620]) ).
fof(f10852,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ599_spl ),
inference(split_clause,[status(thm)],[f10829,f10646,f1274,f10620]) ).
fof(f10853,plain,
( ~ sQ593_spl
| sQ600_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f10830,f1274,f10650,f10620]) ).
fof(f10855,plain,
( ~ sQ593_spl
| sQ592_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f10832,f1274,f10617,f10620]) ).
fof(f10859,plain,
( ~ sQ601_spl
| app(sk6,sk6) = sk6
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ rearsegP(sk6,sk6) ),
inference(paramodulation,[status(thm)],[f10655,f348]) ).
fof(f10861,plain,
( ~ sQ601_spl
| sQ593_spl
| ~ sQ34_spl
| ~ sQ594_spl ),
inference(split_clause,[status(thm)],[f10859,f10624,f1274,f10620,f10654]) ).
fof(f10873,plain,
! [X0] :
( ~ sQ509_spl
| ~ ssList(X0)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f9445,f265]) ).
fof(f10883,plain,
( ~ sQ509_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f437,f10929]) ).
fof(f10929,plain,
! [X0] :
( ~ sQ509_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10873]) ).
fof(f10934,plain,
~ sQ509_spl,
inference(contradiction_clause,[status(thm)],[f10883]) ).
fof(f11147,definition,
( sQ613_spl
<=> ssItem(skaf74(nil)) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f11149,plain,
( sQ613_spl
| ~ ssItem(skaf74(nil)) ),
inference(component_clause,[status(thm)],[f11147]) ).
fof(f11150,definition,
( sQ614_spl
<=> ssList(skaf77(nil)) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f11152,plain,
( sQ614_spl
| ~ ssList(skaf77(nil)) ),
inference(component_clause,[status(thm)],[f11150]) ).
fof(f11154,plain,
( sQ614_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11152,f222]) ).
fof(f11155,plain,
sQ614_spl,
inference(contradiction_clause,[status(thm)],[f11154]) ).
fof(f11156,plain,
( sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11149,f225]) ).
fof(f11157,plain,
sQ613_spl,
inference(contradiction_clause,[status(thm)],[f11156]) ).
fof(f11162,definition,
( sQ616_spl
<=> ssItem(skaf55(nil)) ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f11164,plain,
( sQ616_spl
| ~ ssItem(skaf55(nil)) ),
inference(component_clause,[status(thm)],[f11162]) ).
fof(f11165,definition,
( sQ617_spl
<=> ssList(skaf58(nil)) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f11167,plain,
( sQ617_spl
| ~ ssList(skaf58(nil)) ),
inference(component_clause,[status(thm)],[f11165]) ).
fof(f11169,plain,
( sQ617_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11167,f241]) ).
fof(f11170,plain,
sQ617_spl,
inference(contradiction_clause,[status(thm)],[f11169]) ).
fof(f11171,plain,
( sQ616_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11164,f244]) ).
fof(f11172,plain,
sQ616_spl,
inference(contradiction_clause,[status(thm)],[f11171]) ).
fof(f11177,definition,
( sQ619_spl
<=> ssItem(skaf60(nil)) ),
introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition]) ).
fof(f11179,plain,
( sQ619_spl
| ~ ssItem(skaf60(nil)) ),
inference(component_clause,[status(thm)],[f11177]) ).
fof(f11180,definition,
( sQ620_spl
<=> ssList(skaf63(nil)) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f11182,plain,
( sQ620_spl
| ~ ssList(skaf63(nil)) ),
inference(component_clause,[status(thm)],[f11180]) ).
fof(f11184,plain,
( sQ620_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11182,f236]) ).
fof(f11185,plain,
sQ620_spl,
inference(contradiction_clause,[status(thm)],[f11184]) ).
fof(f11186,plain,
( sQ619_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11179,f239]) ).
fof(f11187,plain,
sQ619_spl,
inference(contradiction_clause,[status(thm)],[f11186]) ).
fof(f11192,definition,
( sQ622_spl
<=> ssItem(skaf65(nil)) ),
introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition]) ).
fof(f11194,plain,
( sQ622_spl
| ~ ssItem(skaf65(nil)) ),
inference(component_clause,[status(thm)],[f11192]) ).
fof(f11195,definition,
( sQ623_spl
<=> ssList(skaf68(nil)) ),
introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition]) ).
fof(f11197,plain,
( sQ623_spl
| ~ ssList(skaf68(nil)) ),
inference(component_clause,[status(thm)],[f11195]) ).
fof(f11199,plain,
( sQ623_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11197,f231]) ).
fof(f11200,plain,
sQ623_spl,
inference(contradiction_clause,[status(thm)],[f11199]) ).
fof(f11201,plain,
( sQ622_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11194,f234]) ).
fof(f11202,plain,
sQ622_spl,
inference(contradiction_clause,[status(thm)],[f11201]) ).
fof(f11219,plain,
! [X0] :
( ~ sQ176_spl
| ~ frontsegP(sk6,X0)
| sk6 = X0
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2932,f255]) ).
fof(f11224,plain,
! [X0] :
( ~ sQ189_spl
| ~ rearsegP(sk6,X0)
| sk6 = X0
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3129,f254]) ).
fof(f11261,plain,
( ~ sQ176_spl
| ~ ssList(sk6)
| sk6 = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f11219,f264]) ).
fof(f11263,plain,
( ~ sQ176_spl
| ~ sQ34_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f11261,f792,f1584,f1274,f2924]) ).
fof(f11265,plain,
( ~ sQ189_spl
| ~ ssList(sk6)
| sk6 = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f11224,f262]) ).
fof(f11267,plain,
( ~ sQ189_spl
| ~ sQ34_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f11265,f792,f1584,f1274,f3089]) ).
fof(f11302,definition,
( sQ625_spl
<=> ssItem(skaf70(nil)) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f11304,plain,
( sQ625_spl
| ~ ssItem(skaf70(nil)) ),
inference(component_clause,[status(thm)],[f11302]) ).
fof(f11305,definition,
( sQ626_spl
<=> ssList(skaf73(nil)) ),
introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition]) ).
fof(f11307,plain,
( sQ626_spl
| ~ ssList(skaf73(nil)) ),
inference(component_clause,[status(thm)],[f11305]) ).
fof(f11309,plain,
( sQ626_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11307,f226]) ).
fof(f11310,plain,
sQ626_spl,
inference(contradiction_clause,[status(thm)],[f11309]) ).
fof(f11311,plain,
( sQ625_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11304,f229]) ).
fof(f11312,plain,
sQ625_spl,
inference(contradiction_clause,[status(thm)],[f11311]) ).
fof(f11322,definition,
( sQ629_spl
<=> ssItem(skaf50(nil)) ),
introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition]) ).
fof(f11324,plain,
( sQ629_spl
| ~ ssItem(skaf50(nil)) ),
inference(component_clause,[status(thm)],[f11322]) ).
fof(f11325,definition,
( sQ630_spl
<=> ssList(skaf53(nil)) ),
introduced(definition,[new_symbols(definition,[sQ630_spl])],[split_symbol_definition]) ).
fof(f11327,plain,
( sQ630_spl
| ~ ssList(skaf53(nil)) ),
inference(component_clause,[status(thm)],[f11325]) ).
fof(f11329,plain,
( sQ630_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11327,f246]) ).
fof(f11330,plain,
sQ630_spl,
inference(contradiction_clause,[status(thm)],[f11329]) ).
fof(f11331,plain,
( sQ629_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11324,f249]) ).
fof(f11332,plain,
sQ629_spl,
inference(contradiction_clause,[status(thm)],[f11331]) ).
fof(f11384,definition,
( sQ631_spl
<=> memberP(nil,sk8) ),
introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition]) ).
fof(f11385,plain,
( ~ sQ631_spl
| memberP(nil,sk8) ),
inference(component_clause,[status(thm)],[f11384]) ).
fof(f11389,plain,
( ~ sQ631_spl
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f11385,f275]) ).
fof(f11390,plain,
( ~ sQ631_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f11389,f470,f11384]) ).
fof(f11391,plain,
( ~ sQ597_spl
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ rearsegP(sk6,sk6)
| skaf46(sk6,sk6) = sk6
| ~ ssList(skaf46(sk6,sk6)) ),
inference(resolution,[status(thm)],[f10637,f348]) ).
fof(f11392,plain,
( ~ sQ597_spl
| ~ ssList(sk6)
| nil = sk6
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f10637,f279]) ).
fof(f11393,definition,
( sQ632_spl
<=> ssList(skaf46(sk6,sk6)) ),
introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition]) ).
fof(f11395,plain,
( sQ632_spl
| ~ ssList(skaf46(sk6,sk6)) ),
inference(component_clause,[status(thm)],[f11393]) ).
fof(f11396,plain,
( ~ sQ597_spl
| ~ sQ34_spl
| ~ sQ594_spl
| sQ601_spl
| ~ sQ632_spl ),
inference(split_clause,[status(thm)],[f11391,f11393,f10654,f10624,f1274,f10636]) ).
fof(f11397,plain,
( ~ sQ597_spl
| ~ sQ34_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f11392,f792,f1584,f1274,f10636]) ).
fof(f11398,plain,
( sQ632_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11395,f254]) ).
fof(f11399,plain,
sQ632_spl,
inference(contradiction_clause,[status(thm)],[f11398]) ).
fof(f11400,plain,
( ~ sQ598_spl
| ~ ssList(sk6)
| nil = sk6
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f10642,f278]) ).
fof(f11402,plain,
( ~ sQ598_spl
| ~ sQ34_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f11400,f792,f1584,f1274,f10641]) ).
fof(f11696,plain,
( ~ sQ255_spl
| ~ sQ134_spl
| nil = sk7
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f2279,f5283]) ).
fof(f11699,plain,
( ~ sQ255_spl
| ~ sQ134_spl
| sQ43_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f11696,f792,f1317,f2278,f5282]) ).
fof(f11702,plain,
( ~ sQ103_spl
| ~ sQ130_spl
| ~ sQ7_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f9956,f2278,f481,f2177,f2022]) ).
fof(f11804,plain,
( ~ sQ90_spl
| ~ ssList(sk3)
| nil = sk6
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1770,f279]) ).
fof(f11806,plain,
( ~ sQ90_spl
| ~ sQ12_spl
| sQ61_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f11804,f792,f1584,f655,f1769]) ).
fof(f11812,plain,
( ~ sQ521_spl
| ~ ssList(sk3)
| frontsegP(sk6,sk3)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f8650,f265]) ).
fof(f11824,plain,
( ~ sQ521_spl
| sQ49_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f11812,f655,f1455,f8649]) ).
fof(f11829,plain,
! [X0] :
( ~ sQ139_spl
| ~ ssList(sk3)
| ~ ssList(X0)
| rearsegP(app(X0,sk3),sk6)
| ~ ssList(app(X0,sk3)) ),
inference(resolution,[status(thm)],[f2727,f511]) ).
fof(f11830,plain,
! [X0,X1] :
( ~ sQ139_spl
| ~ ssList(X1)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ rearsegP(X1,sk3)
| rearsegP(app(X0,X1),sk6)
| ~ ssList(app(X0,X1)) ),
inference(resolution,[status(thm)],[f2727,f355]) ).
fof(f11832,plain,
( ~ sQ139_spl
| ~ ssList(sk3)
| rearsegP(sk3,sk6)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f2727,f263]) ).
fof(f11833,definition,
! [X0] :
( sQ648_spl
<=> ( ~ ssList(X0)
| rearsegP(app(X0,sk3),sk6)
| ~ ssList(app(X0,sk3)) ) ),
introduced(definition,[new_symbols(definition,[sQ648_spl])],[split_symbol_definition]) ).
fof(f11836,plain,
( ~ sQ139_spl
| ~ sQ12_spl
| sQ648_spl ),
inference(split_clause,[status(thm)],[f11829,f11833,f655,f2726]) ).
fof(f11837,definition,
! [X0,X1] :
( sQ649_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,sk3)
| rearsegP(app(X0,X1),sk6)
| ~ ssList(app(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition]) ).
fof(f11840,plain,
( ~ sQ139_spl
| ~ sQ12_spl
| sQ649_spl ),
inference(split_clause,[status(thm)],[f11830,f11837,f655,f2726]) ).
fof(f11841,definition,
( sQ650_spl
<=> rearsegP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition]) ).
fof(f11845,plain,
( ~ sQ139_spl
| sQ650_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f11832,f655,f11841,f2726]) ).
fof(f11873,plain,
( ~ sQ7_spl
| hd(sk3) = sk8
| ~ ssList(nil)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f482,f302]) ).
fof(f11874,plain,
( ~ sQ7_spl
| sQ215_spl
| ~ sQ18_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f11873,f470,f792,f3347,f481]) ).
fof(f11910,plain,
( ~ sQ467_spl
| ~ sQ536_spl
| app(sk3,tl(sk6)) = sk6
| ~ ssList(tl(sk6)) ),
inference(paramodulation,[status(thm)],[f8134,f8892]) ).
fof(f11918,plain,
( ~ sQ467_spl
| ~ sQ536_spl
| sQ469_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f11910,f3333,f8183,f8891,f8133]) ).
fof(f12077,plain,
! [X0] :
( ~ sQ61_spl
| app(sk6,X0) = X0
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f279]) ).
fof(f12078,plain,
! [X0] :
( ~ sQ61_spl
| app(X0,sk6) = X0
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f278]) ).
fof(f12165,plain,
! [X0] :
( ~ sQ61_spl
| cons(skaf44(X0),sk6) = X0
| ~ ssList(X0)
| ~ singletonP(X0) ),
inference(backward_demodulation,[status(thm)],[f1585,f308]) ).
fof(f12294,plain,
( sQ2_spl
| ~ sQ5_spl
| ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ61_spl
| ~ memberP(sk7,sk5) ),
inference(backward_demodulation,[status(thm)],[f4405,f465]) ).
fof(f13210,plain,
( ~ sQ111_spl
| ~ sQ79_spl
| sQ593_spl ),
inference(split_clause,[status(thm)],[f3554,f10620,f1677,f2068]) ).
fof(f14369,plain,
( sQ2_spl
| ~ sQ5_spl
| ~ sQ35_spl
| ~ sQ43_spl
| ~ sQ6_spl
| ~ sQ61_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f12294,f466,f1584,f477,f1317,f1277,f473,f463]) ).
fof(f14933,plain,
( sQ594_spl
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f10626,f263]) ).
fof(f14934,plain,
( sQ594_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f14933,f1274,f10624]) ).
fof(f14937,plain,
( ~ sQ594_spl
| sk6 = sk6
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ rearsegP(sk6,sk6) ),
inference(resolution,[status(thm)],[f10625,f345]) ).
fof(f14938,plain,
! [X0] :
( ~ sQ594_spl
| rearsegP(X0,sk6)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ rearsegP(X0,sk6) ),
inference(resolution,[status(thm)],[f10625,f381]) ).
fof(f14939,plain,
( sQ138_spl
| ~ sQ34_spl
| ~ sQ594_spl ),
inference(split_clause,[status(thm)],[f14937,f10624,f1274,f2302]) ).
fof(f14940,plain,
( ~ sQ594_spl
| ~ sQ34_spl
| sQ588_spl ),
inference(split_clause,[status(thm)],[f14938,f10601,f1274,f10624]) ).
fof(f14942,plain,
! [X0] :
( ~ sQ592_spl
| frontsegP(X0,sk6)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ frontsegP(X0,sk6) ),
inference(resolution,[status(thm)],[f383,f10618]) ).
fof(f14947,definition,
! [X0] :
( sQ651_spl
<=> ( frontsegP(X0,sk6)
| ~ ssList(X0)
| ~ frontsegP(X0,sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f14950,plain,
( ~ sQ592_spl
| ~ sQ34_spl
| sQ651_spl ),
inference(split_clause,[status(thm)],[f14942,f14947,f1274,f10617]) ).
fof(f14964,plain,
! [X0,X1] :
( ~ sQ61_spl
| X1 = sk6
| ~ ssList(sk6)
| ~ ssList(X1)
| ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f12165,f408]) ).
fof(f14965,plain,
( ~ sQ61_spl
| ~ ssList(sk6)
| ~ ssItem(skaf44(sk6))
| ~ ssList(sk6)
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[f12165,f306]) ).
fof(f14967,definition,
! [X0,X1] :
( sQ652_spl
<=> ( X1 = sk6
| ~ ssList(X1)
| ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0)
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ652_spl])],[split_symbol_definition]) ).
fof(f14970,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ652_spl ),
inference(split_clause,[status(thm)],[f14964,f14967,f1274,f1584]) ).
fof(f14971,definition,
( sQ653_spl
<=> ssItem(skaf44(sk6)) ),
introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition]) ).
fof(f14973,plain,
( sQ653_spl
| ~ ssItem(skaf44(sk6)) ),
inference(component_clause,[status(thm)],[f14971]) ).
fof(f14974,plain,
( ~ sQ61_spl
| ~ sQ653_spl
| ~ sQ34_spl
| ~ sQ473_spl ),
inference(split_clause,[status(thm)],[f14965,f8199,f1274,f14971,f1584]) ).
fof(f14977,plain,
( sQ653_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14973,f251]) ).
fof(f14978,plain,
sQ653_spl,
inference(contradiction_clause,[status(thm)],[f14977]) ).
fof(f14994,plain,
( ~ sQ259_spl
| ~ sQ61_spl
| app(sk3,sk6) = sk3
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ rearsegP(sk3,sk6) ),
inference(paramodulation,[status(thm)],[f7133,f348]) ).
fof(f14997,definition,
( sQ654_spl
<=> app(sk3,sk6) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f15000,plain,
( ~ sQ259_spl
| ~ sQ61_spl
| sQ654_spl
| ~ sQ12_spl
| ~ sQ34_spl
| ~ sQ650_spl ),
inference(split_clause,[status(thm)],[f14994,f11841,f1274,f655,f14997,f1584,f5311]) ).
fof(f15005,plain,
! [X0,X1] :
( ~ sQ61_spl
| ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1))
| skaf44(cons(X0,X1)) = X0
| ~ ssList(sk6)
| ~ ssList(X1)
| ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f406,f12165]) ).
fof(f15010,definition,
! [X0,X1] :
( sQ655_spl
<=> ( ~ ssList(cons(X0,X1))
| ~ singletonP(cons(X0,X1))
| skaf44(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(skaf44(cons(X0,X1)))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition]) ).
fof(f15013,plain,
( ~ sQ61_spl
| ~ sQ34_spl
| sQ655_spl ),
inference(split_clause,[status(thm)],[f15005,f15010,f1274,f1584]) ).
fof(f15023,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ61_spl
| memberP(sk3,X0)
| memberP(sk6,X0)
| ~ ssItem(X0)
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f7130,f390]) ).
fof(f15030,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ61_spl
| rearsegP(sk3,X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ rearsegP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f7130,f355]) ).
fof(f15032,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ61_spl
| app(sk3,X0) = app(sk3,app(sk6,X0))
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f7130,f373]) ).
fof(f15033,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ61_spl
| X0 = sk6
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ ssList(X0)
| app(sk3,X0) != sk3 ),
inference(paramodulation,[status(thm)],[f7130,f375]) ).
fof(f15035,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ61_spl
| X0 = sk3
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ ssList(X0)
| app(X0,sk6) != sk3 ),
inference(paramodulation,[status(thm)],[f7130,f377]) ).
fof(f15037,plain,
! [X0,X1] :
( ~ sQ255_spl
| ~ sQ61_spl
| segmentP(app(sk3,X1),X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(X1)
| ~ segmentP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f7130,f409]) ).
fof(f15038,plain,
! [X0] :
( ~ sQ255_spl
| ~ sQ61_spl
| segmentP(app(sk3,X0),sk6)
| ~ ssList(app(app(sk3,sk6),X0))
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f7130,f516]) ).
fof(f15039,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ12_spl
| ~ sQ34_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f15023,f2091,f1274,f655,f1584,f5282]) ).
fof(f15046,definition,
! [X0] :
( sQ656_spl
<=> ( rearsegP(sk3,X0)
| ~ ssList(X0)
| ~ rearsegP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f15049,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ34_spl
| ~ sQ12_spl
| sQ656_spl ),
inference(split_clause,[status(thm)],[f15030,f15046,f655,f1274,f1584,f5282]) ).
fof(f15051,definition,
! [X0] :
( sQ657_spl
<=> ( app(sk3,X0) = app(sk3,app(sk6,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition]) ).
fof(f15054,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ12_spl
| ~ sQ34_spl
| sQ657_spl ),
inference(split_clause,[status(thm)],[f15032,f15051,f1274,f655,f1584,f5282]) ).
fof(f15055,definition,
! [X0] :
( sQ658_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| app(sk3,X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f15058,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ34_spl
| ~ sQ12_spl
| sQ658_spl ),
inference(split_clause,[status(thm)],[f15033,f15055,f655,f1274,f1584,f5282]) ).
fof(f15060,definition,
! [X0] :
( sQ659_spl
<=> ( X0 = sk3
| ~ ssList(X0)
| app(X0,sk6) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition]) ).
fof(f15063,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ12_spl
| ~ sQ34_spl
| sQ659_spl ),
inference(split_clause,[status(thm)],[f15035,f15060,f1274,f655,f1584,f5282]) ).
fof(f15065,definition,
! [X0,X1] :
( sQ660_spl
<=> ( segmentP(app(sk3,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ660_spl])],[split_symbol_definition]) ).
fof(f15068,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ34_spl
| ~ sQ12_spl
| sQ660_spl ),
inference(split_clause,[status(thm)],[f15037,f15065,f655,f1274,f1584,f5282]) ).
fof(f15069,definition,
! [X0] :
( sQ661_spl
<=> ( segmentP(app(sk3,X0),sk6)
| ~ ssList(app(app(sk3,sk6),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition]) ).
fof(f15072,plain,
( ~ sQ255_spl
| ~ sQ61_spl
| ~ sQ34_spl
| ~ sQ12_spl
| sQ661_spl ),
inference(split_clause,[status(thm)],[f15038,f15069,f655,f1274,f1584,f5282]) ).
fof(f15074,plain,
( sQ593_spl
| ~ sQ61_spl
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f12078,f10622]) ).
fof(f15078,plain,
( sQ593_spl
| ~ sQ61_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f15074,f1274,f1584,f10620]) ).
fof(f15341,plain,
! [X0] :
( ~ sQ593_spl
| frontsegP(sk6,X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ frontsegP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f10621,f356]) ).
fof(f15358,definition,
! [X0] :
( sQ666_spl
<=> ( frontsegP(sk6,X0)
| ~ ssList(X0)
| ~ frontsegP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ666_spl])],[split_symbol_definition]) ).
fof(f15361,plain,
( ~ sQ593_spl
| ~ sQ34_spl
| sQ666_spl ),
inference(split_clause,[status(thm)],[f15341,f15358,f1274,f10620]) ).
fof(f15391,plain,
( sQ370_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ61_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f12077,f9948]) ).
fof(f15395,plain,
( sQ370_spl
| ~ sQ130_spl
| ~ sQ7_spl
| ~ sQ61_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f15391,f655,f1584,f481,f2177,f6650]) ).
fof(f15619,plain,
( sQ2_spl
| ~ sQ130_spl
| ~ sQ61_spl
| ~ sQ43_spl
| ~ memberP(sk7,sk8) ),
inference(backward_demodulation,[status(thm)],[f4702,f7259]) ).
fof(f16082,plain,
( sQ2_spl
| ~ sQ130_spl
| ~ sQ61_spl
| ~ sQ43_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15619,f2557]) ).
fof(f16083,plain,
( sQ2_spl
| ~ sQ130_spl
| ~ sQ61_spl
| ~ sQ43_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f16082]) ).
fof(f16084,plain,
$false,
inference(sat_refutation,[status(thm)],[f462,f469,f476,f480,f484,f493,f494,f495,f640,f669,f796,f962,f974,f1246,f1254,f1280,f1287,f1292,f1297,f1301,f1305,f1308,f1320,f1407,f1409,f1427,f1430,f1471,f1473,f1492,f1496,f1500,f1504,f1505,f1531,f1535,f1550,f1554,f1587,f1595,f1599,f1603,f1607,f1612,f1617,f1622,f1630,f1638,f1660,f1669,f1675,f1680,f1687,f1691,f1695,f1700,f1702,f1710,f1717,f1719,f1872,f1908,f1917,f1921,f1940,f1945,f2025,f2063,f2071,f2078,f2098,f2105,f2109,f2113,f2121,f2125,f2136,f2140,f2148,f2152,f2158,f2162,f2169,f2174,f2180,f2181,f2294,f2311,f2729,f2749,f2753,f2761,f2765,f2773,f2777,f2783,f2854,f2858,f2927,f3038,f3049,f3092,f3096,f3121,f3128,f3167,f3169,f3171,f3179,f3181,f3183,f3191,f3193,f3195,f3203,f3205,f3207,f3215,f3217,f3219,f3387,f3432,f3645,f3985,f4977,f5093,f5129,f5145,f5301,f5306,f5310,f5314,f5316,f5328,f5329,f5391,f5677,f5759,f5792,f5887,f5957,f6356,f6680,f6691,f6872,f6918,f6941,f6961,f7027,f7040,f7385,f7860,f7864,f7891,f8038,f8136,f8327,f8354,f8652,f8702,f8843,f8845,f8884,f8894,f8900,f8902,f8904,f8906,f8908,f8928,f9021,f9080,f9161,f9187,f9195,f9233,f9453,f9458,f9503,f9587,f9984,f10627,f10765,f10769,f10835,f10836,f10837,f10838,f10841,f10842,f10843,f10846,f10847,f10848,f10850,f10852,f10853,f10855,f10861,f10934,f11155,f11157,f11170,f11172,f11185,f11187,f11200,f11202,f11263,f11267,f11310,f11312,f11330,f11332,f11390,f11396,f11397,f11399,f11402,f11699,f11702,f11806,f11824,f11836,f11840,f11845,f11874,f11918,f13210,f14369,f14934,f14939,f14940,f14950,f14970,f14974,f14978,f15000,f15013,f15039,f15049,f15054,f15058,f15063,f15068,f15072,f15078,f15361,f15395,f16083]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC183-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/15.40 % Computer : n002.cluster.edu
% 0.11/15.40 % Model : x86_64 x86_64
% 0.11/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/15.40 % Memory : 8046.5625MB
% 0.11/15.40 % OS : Linux 6.8.0-71-generic
% 0.11/15.41 % CPULimit : 300
% 0.11/15.41 % WCLimit : 300
% 0.11/15.41 % DateTime : Mon Sep 21 08:05:20 UTC 2026
% 0.11/15.41 % CPUTime :
% 0.11/15.43 % Drodi V4.1.1
% 33.38/19.80 % Refutation found
% 33.38/19.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 33.38/19.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 32.80/19.88 % Elapsed time: 4.455938 seconds
% 32.80/19.88 % CPU time: 34.586546 seconds
% 32.80/19.88 % Total memory used: 292.276 MB
% 32.80/19.88 % Net memory used: 276.177 MB
%------------------------------------------------------------------------------