%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC165-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:13 PM UTC 2026
% Result : Unsatisfiable 142.02s 18.36s
% Output : CNFRefutation 53.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 167
% Syntax : Number of formulae : 603 ( 132 unt; 106 def)
% Number of atoms : 1519 ( 166 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1642 ( 726 ~; 810 |; 0 &)
% ( 106 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 114 ( 112 usr; 107 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 11 con; 0-2 aty)
% Number of variables : 245 ( 245 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] : ssList(skaf80(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [U] : ssItem(skaf78(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] : ssList(skaf73(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U] : ssList(skaf71(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] : ssItem(skaf70(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [U] : ssList(skaf68(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [U] : ssList(skaf66(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U] : ssItem(skaf65(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [U] : ssList(skaf63(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [U] : ssList(skaf61(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [U] : ssItem(skaf60(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] : ssList(skaf58(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [U] : ssList(skaf56(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [U] : ssItem(skaf55(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] : ssList(skaf53(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [U] : ssList(skaf51(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U] : ssItem(skaf50(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U] : ssItem(skaf44(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U,V] : ssList(skaf46(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [U] :
( rearsegP(nil,U)
| ~ ssList(U)
| nil != U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [U] :
( frontsegP(nil,U)
| ~ ssList(U)
| nil != U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = V
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [U,V] :
( hd(cons(U,V)) = U
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssItem(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [U,V] :
( app(cons(U,nil),V) = cons(U,V)
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [U,V] :
( hd(app(V,U)) = hd(V)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [U,V] :
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [U,V,W] :
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W] :
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [U,V,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,axiom,
! [U,V,W] :
( frontsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [U,V,W] :
( W = U
| memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [U,V,W,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,axiom,
! [U,V,W,X] :
( frontsegP(cons(W,U),cons(X,V))
| ~ ssItem(W)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(V)
| W != X
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
~ neq(sk5,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
( nil = sk3
| ssItem(sk9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,negated_conjecture,
( nil = sk3
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f219,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f223,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f224,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f226,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f228,plain,
! [X0] : ssItem(skaf78(X0)),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f233,plain,
! [X0] : ssList(skaf73(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f235,plain,
! [X0] : ssList(skaf71(X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f236,plain,
! [X0] : ssItem(skaf70(X0)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f238,plain,
! [X0] : ssList(skaf68(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f240,plain,
! [X0] : ssList(skaf66(X0)),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f241,plain,
! [X0] : ssItem(skaf65(X0)),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f243,plain,
! [X0] : ssList(skaf63(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f245,plain,
! [X0] : ssList(skaf61(X0)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f246,plain,
! [X0] : ssItem(skaf60(X0)),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f248,plain,
! [X0] : ssList(skaf58(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f250,plain,
! [X0] : ssList(skaf56(X0)),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f251,plain,
! [X0] : ssItem(skaf55(X0)),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f253,plain,
! [X0] : ssList(skaf53(X0)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f255,plain,
! [X0] : ssList(skaf51(X0)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f256,plain,
! [X0] : ssItem(skaf50(X0)),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f258,plain,
! [X0] : ssItem(skaf44(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f261,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f262,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f271,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f282,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f286,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f287,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f293,plain,
! [X0] :
( rearsegP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f295,plain,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f297,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f298,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f308,plain,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f309,plain,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f312,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f313,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f316,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f318,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f340,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f341,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f342,plain,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f345,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f353,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f357,plain,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f363,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(f366,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(f367,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(f371,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f372,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f383,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f384,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f389,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(f390,plain,
! [X0,X1,X2] :
( frontsegP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f389]) ).
fof(f402,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(f403,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)],[f402]) ).
fof(f421,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(f422,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)],[f421]) ).
fof(f427,plain,
! [X0,X1,X2,X3] :
( frontsegP(cons(X2,X0),cons(X3,X1))
| ~ ssItem(X2)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| X2 != X3
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f444,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f445,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f447,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f448,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f449,plain,
ssItem(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f450,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f451,plain,
ssList(sk8),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f452,plain,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f453,plain,
~ neq(sk5,sk6),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f455,plain,
( nil = sk3
| ssItem(sk9) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f466,plain,
( nil = sk3
| cons(sk9,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f479,definition,
( sQ2_spl
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f486,definition,
( sQ4_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f487,plain,
( ~ sQ4_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,plain,
( sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f455,f479,f486]) ).
fof(f498,definition,
( sQ7_spl
<=> cons(sk9,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( ~ sQ7_spl
| cons(sk9,nil) = sk3 ),
inference(component_clause,[status(thm)],[f498]) ).
fof(f516,plain,
( sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f466,f498,f486]) ).
fof(f521,plain,
( rearsegP(nil,nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f293]) ).
fof(f522,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f295]) ).
fof(f535,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f372]) ).
fof(f539,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)],[f422]) ).
fof(f540,plain,
! [X0,X1,X3] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssItem(X3)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f427]) ).
fof(f541,plain,
! [X0,X1,X2] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f540]) ).
fof(f557,definition,
( sQ11_spl
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f559,plain,
( sQ11_spl
| ~ ssList(sk8) ),
inference(component_clause,[status(thm)],[f557]) ).
fof(f560,definition,
( sQ12_spl
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( ~ sQ12_spl
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f562,plain,
( sQ12_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f563,definition,
( sQ13_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ13_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f581,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f559,f451]) ).
fof(f582,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f581]) ).
fof(f583,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f219]) ).
fof(f584,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f583]) ).
fof(f594,definition,
( sQ17_spl
<=> sk5 = sk6 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f595,plain,
( ~ sQ17_spl
| sk5 = sk6 ),
inference(component_clause,[status(thm)],[f594]) ).
fof(f598,plain,
( sk5 = sk6
| ~ ssItem(sk5)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f316,f453]) ).
fof(f601,definition,
( sQ18_spl
<=> ssItem(sk6) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( sQ18_spl
| ~ ssItem(sk6) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,definition,
( sQ19_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( sQ19_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f607,plain,
( sQ17_spl
| ~ sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f598,f601,f604,f594]) ).
fof(f618,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f606,f448]) ).
fof(f619,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f618]) ).
fof(f622,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f603,f449]) ).
fof(f623,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f622]) ).
fof(f644,definition,
( sQ21_spl
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f646,plain,
( sQ21_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f644]) ).
fof(f686,plain,
( sQ21_spl
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f646,f297]) ).
fof(f687,definition,
( sQ29_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f689,plain,
( sQ29_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f690,definition,
( sQ30_spl
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( ~ sQ30_spl
| ssList(app(sk7,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f692,plain,
( sQ30_spl
| ~ ssList(app(sk7,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,plain,
( sQ21_spl
| ~ sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f686,f687,f690,f644]) ).
fof(f694,plain,
( sQ29_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f689,f298]) ).
fof(f695,plain,
( sQ29_spl
| ~ sQ13_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f694,f604,f563,f687]) ).
fof(f696,plain,
( ~ sQ17_spl
| app(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),sk8) = sk1 ),
inference(forward_demodulation,[status(thm)],[f595,f452]) ).
fof(f697,plain,
! [X0] :
( ~ sQ7_spl
| app(sk3,X0) = cons(sk9,X0)
| ~ ssList(X0)
| ~ ssItem(sk9) ),
inference(paramodulation,[status(thm)],[f499,f342]) ).
fof(f703,definition,
! [X0] :
( sQ31_spl
<=> ( app(sk3,X0) = cons(sk9,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f704,plain,
! [X0] :
( ~ sQ31_spl
| app(sk3,X0) = cons(sk9,X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,plain,
( ~ sQ7_spl
| sQ31_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f697,f479,f703,f498]) ).
fof(f717,definition,
( sQ34_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( sQ34_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f757,definition,
( sQ42_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f759,plain,
( sQ42_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f757]) ).
fof(f847,plain,
( ~ sQ17_spl
| app(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f447,f696]) ).
fof(f849,plain,
! [X0] :
( ~ sQ17_spl
| X0 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(X0)
| app(X0,sk8) != sk3 ),
inference(paramodulation,[status(thm)],[f847,f384]) ).
fof(f853,plain,
! [X0] :
( ~ sQ17_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(sk8)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0) ),
inference(paramodulation,[status(thm)],[f847,f366]) ).
fof(f863,definition,
! [X0] :
( sQ57_spl
<=> ( X0 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ ssList(X0)
| app(X0,sk8) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f864,plain,
! [X0] :
( ~ sQ57_spl
| X0 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ ssList(X0)
| app(X0,sk8) != sk3 ),
inference(component_clause,[status(thm)],[f863]) ).
fof(f866,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ11_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f849,f863,f557,f644,f594]) ).
fof(f876,definition,
! [X0] :
( sQ60_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f877,plain,
! [X0] :
( ~ sQ60_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0) ),
inference(component_clause,[status(thm)],[f876]) ).
fof(f879,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ11_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f853,f876,f557,f644,f594]) ).
fof(f888,plain,
( sQ12_spl
| ~ sQ17_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(forward_demodulation,[status(thm)],[f595,f562]) ).
fof(f891,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f719,f444]) ).
fof(f892,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f891]) ).
fof(f991,plain,
rearsegP(nil,nil),
inference(forward_subsumption_resolution,[status(thm)],[f521,f219]) ).
fof(f994,plain,
frontsegP(nil,nil),
inference(forward_subsumption_resolution,[status(thm)],[f522,f219]) ).
fof(f1097,definition,
( sQ75_spl
<=> ssItem(skaf44(nil)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1099,plain,
( sQ75_spl
| ~ ssItem(skaf44(nil)) ),
inference(component_clause,[status(thm)],[f1097]) ).
fof(f1116,plain,
( sQ30_spl
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f297,f692]) ).
fof(f1118,definition,
( sQ78_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( sQ78_spl
| ~ ssList(sk7) ),
inference(component_clause,[status(thm)],[f1118]) ).
fof(f1121,plain,
( sQ30_spl
| ~ sQ78_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f1116,f687,f1118,f690]) ).
fof(f1123,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1120,f450]) ).
fof(f1124,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1123]) ).
fof(f1175,definition,
( sQ80_spl
<=> ssItem(skaf83(nil)) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( sQ80_spl
| ~ ssItem(skaf83(nil)) ),
inference(component_clause,[status(thm)],[f1175]) ).
fof(f1178,definition,
( sQ81_spl
<=> ssList(skaf82(nil)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1180,plain,
( sQ81_spl
| ~ ssList(skaf82(nil)) ),
inference(component_clause,[status(thm)],[f1178]) ).
fof(f1186,plain,
! [X0] :
( ~ sQ7_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f499,f403]) ).
fof(f1193,plain,
( ~ sQ7_spl
| hd(sk3) = sk9
| ~ ssList(nil)
| ~ ssItem(sk9) ),
inference(paramodulation,[status(thm)],[f499,f309]) ).
fof(f1194,plain,
( ~ sQ7_spl
| tl(sk3) = nil
| ~ ssList(nil)
| ~ ssItem(sk9) ),
inference(paramodulation,[status(thm)],[f499,f308]) ).
fof(f1198,definition,
! [X0] :
( sQ82_spl
<=> ( X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1199,plain,
! [X0] :
( ~ sQ82_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(component_clause,[status(thm)],[f1198]) ).
fof(f1201,plain,
( ~ sQ7_spl
| ~ sQ2_spl
| ~ sQ13_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1186,f1198,f563,f479,f498]) ).
fof(f1211,definition,
( sQ84_spl
<=> hd(sk3) = sk9 ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1212,plain,
( ~ sQ84_spl
| hd(sk3) = sk9 ),
inference(component_clause,[status(thm)],[f1211]) ).
fof(f1214,plain,
( ~ sQ7_spl
| sQ84_spl
| ~ sQ13_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1193,f479,f563,f1211,f498]) ).
fof(f1215,definition,
( sQ85_spl
<=> tl(sk3) = nil ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1216,plain,
( ~ sQ85_spl
| tl(sk3) = nil ),
inference(component_clause,[status(thm)],[f1215]) ).
fof(f1218,plain,
( ~ sQ7_spl
| sQ85_spl
| ~ sQ13_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1194,f479,f563,f1215,f498]) ).
fof(f1221,plain,
! [X0] :
( ~ sQ82_spl
| X0 = sk9
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1199,f282]) ).
fof(f1377,definition,
! [X0] :
( sQ100_spl
<=> ( memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1378,plain,
! [X0] :
( ~ sQ100_spl
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(component_clause,[status(thm)],[f1377]) ).
fof(f1651,definition,
( sQ138_spl
<=> rearsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1653,plain,
( sQ138_spl
| ~ rearsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f1651]) ).
fof(f1657,definition,
( sQ139_spl
<=> frontsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1659,plain,
( sQ139_spl
| ~ frontsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f1657]) ).
fof(f1681,definition,
( sQ141_spl
<=> sk4 = sk4 ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1683,plain,
( sQ141_spl
| sk4 != sk4 ),
inference(component_clause,[status(thm)],[f1681]) ).
fof(f1829,plain,
( ~ sQ57_spl
| nil = cons(sk5,nil)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ ssList(nil)
| app(nil,sk8) != sk3 ),
inference(resolution,[status(thm)],[f864,f341]) ).
fof(f1844,definition,
( sQ170_spl
<=> app(nil,sk8) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1846,plain,
( sQ170_spl
| app(nil,sk8) != sk3 ),
inference(component_clause,[status(thm)],[f1844]) ).
fof(f1851,definition,
( sQ172_spl
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1852,plain,
( ~ sQ172_spl
| nil = cons(sk5,nil) ),
inference(component_clause,[status(thm)],[f1851]) ).
fof(f1854,plain,
( ~ sQ57_spl
| sQ172_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ13_spl
| ~ sQ170_spl ),
inference(split_clause,[status(thm)],[f1829,f1844,f563,f687,f690,f1851,f863]) ).
fof(f2000,plain,
( ~ sQ60_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssItem(sk5)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(nil)
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f877,f539]) ).
fof(f2003,definition,
( sQ192_spl
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2004,plain,
( ~ sQ192_spl
| memberP(sk3,sk5) ),
inference(component_clause,[status(thm)],[f2003]) ).
fof(f2006,plain,
( ~ sQ60_spl
| ~ sQ21_spl
| ~ sQ30_spl
| ~ sQ13_spl
| sQ192_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f2000,f604,f2003,f563,f690,f644,f876]) ).
fof(f2034,definition,
( sQ199_spl
<=> sk3 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f2036,plain,
( sQ199_spl
| sk3 != sk3 ),
inference(component_clause,[status(thm)],[f2034]) ).
fof(f2039,plain,
( sQ12_spl
| ~ sQ17_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f888,f644,f594,f560]) ).
fof(f2040,plain,
( sQ199_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2036]) ).
fof(f2041,plain,
sQ199_spl,
inference(contradiction_clause,[status(thm)],[f2040]) ).
fof(f2042,plain,
( ~ sQ12_spl
| ~ sQ17_spl
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(forward_demodulation,[status(thm)],[f595,f561]) ).
fof(f2043,plain,
( ~ sQ82_spl
| ~ sQ192_spl
| sk5 = sk9
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f2004,f1221]) ).
fof(f2044,definition,
( sQ200_spl
<=> sk5 = sk9 ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f2045,plain,
( ~ sQ200_spl
| sk5 = sk9 ),
inference(component_clause,[status(thm)],[f2044]) ).
fof(f2047,plain,
( ~ sQ82_spl
| ~ sQ192_spl
| sQ200_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f2043,f604,f2044,f2003,f1198]) ).
fof(f2048,plain,
( ~ sQ192_spl
| ~ sQ200_spl
| memberP(sk3,sk9) ),
inference(backward_demodulation,[status(thm)],[f2045,f2004]) ).
fof(f2055,plain,
( ~ sQ30_spl
| ~ sQ200_spl
| ssList(app(sk7,cons(sk9,nil))) ),
inference(backward_demodulation,[status(thm)],[f2045,f691]) ).
fof(f2056,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| app(app(app(sk7,cons(sk5,nil)),cons(sk9,nil)),sk8) = sk3 ),
inference(backward_demodulation,[status(thm)],[f2045,f847]) ).
fof(f2076,plain,
( ~ sQ30_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ssList(app(sk7,sk3)) ),
inference(forward_demodulation,[status(thm)],[f499,f2055]) ).
fof(f2077,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| app(app(app(sk7,cons(sk9,nil)),cons(sk9,nil)),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f2045,f2056]) ).
fof(f2078,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| app(app(app(sk7,sk3),cons(sk9,nil)),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f499,f2077]) ).
fof(f2079,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| app(app(app(sk7,sk3),sk3),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f499,f2078]) ).
fof(f2143,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| hd(sk3) = hd(app(app(sk7,sk3),sk3))
| nil = app(app(sk7,sk3),sk3)
| ~ ssList(app(app(sk7,sk3),sk3))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f2079,f345]) ).
fof(f2155,definition,
( sQ212_spl
<=> ssList(app(app(sk7,sk3),sk3)) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f2157,plain,
( sQ212_spl
| ~ ssList(app(app(sk7,sk3),sk3)) ),
inference(component_clause,[status(thm)],[f2155]) ).
fof(f2158,definition,
( sQ213_spl
<=> nil = app(app(sk7,sk3),sk3) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2159,plain,
( ~ sQ213_spl
| nil = app(app(sk7,sk3),sk3) ),
inference(component_clause,[status(thm)],[f2158]) ).
fof(f2165,definition,
( sQ215_spl
<=> hd(sk3) = hd(app(app(sk7,sk3),sk3)) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2166,plain,
( ~ sQ215_spl
| hd(sk3) = hd(app(app(sk7,sk3),sk3)) ),
inference(component_clause,[status(thm)],[f2165]) ).
fof(f2168,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| sQ215_spl
| sQ213_spl
| ~ sQ212_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2143,f557,f2155,f2158,f2165,f498,f2044,f594]) ).
fof(f2248,plain,
( ~ sQ172_spl
| ~ sQ200_spl
| nil = cons(sk9,nil) ),
inference(forward_demodulation,[status(thm)],[f2045,f1852]) ).
fof(f2250,plain,
( sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1659,f994]) ).
fof(f2251,plain,
sQ139_spl,
inference(contradiction_clause,[status(thm)],[f2250]) ).
fof(f2252,plain,
( sQ138_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1653,f991]) ).
fof(f2253,plain,
sQ138_spl,
inference(contradiction_clause,[status(thm)],[f2252]) ).
fof(f2254,plain,
! [X0] :
( ~ sQ100_spl
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1378,f282]) ).
fof(f2258,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1099,f258]) ).
fof(f2259,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f2258]) ).
fof(f2338,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)],[f363,f353]) ).
fof(f2339,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)],[f2338]) ).
fof(f2340,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)],[f2339,f297]) ).
fof(f2349,definition,
( sQ225_spl
<=> ssList(skaf80(nil)) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f2351,plain,
( sQ225_spl
| ~ ssList(skaf80(nil)) ),
inference(component_clause,[status(thm)],[f2349]) ).
fof(f2360,plain,
( sQ225_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2351,f226]) ).
fof(f2361,plain,
sQ225_spl,
inference(contradiction_clause,[status(thm)],[f2360]) ).
fof(f2362,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f445]) ).
fof(f2363,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f2362]) ).
fof(f2467,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f535,f297]) ).
fof(f2468,plain,
! [X0,X1] :
( app(X1,X0) = X1
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2467,f353]) ).
fof(f2470,plain,
! [X0,X1] :
( app(X1,X0) = X1
| ~ ssList(app(X1,X0))
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2468]) ).
fof(f2471,plain,
! [X0,X1] :
( app(X1,X0) = X1
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2470,f297]) ).
fof(f2557,plain,
! [X0,X1,X2] :
( ~ ssList(X1)
| ~ ssList(X2)
| frontsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(app(X1,X2))
| ~ ssList(X1)
| ~ frontsegP(X0,app(X1,X2)) ),
inference(resolution,[status(thm)],[f390,f2467]) ).
fof(f2566,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| frontsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(app(X1,X2))
| ~ ssList(X1)
| ~ frontsegP(X0,app(X1,X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f2557]) ).
fof(f2567,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| frontsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,app(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2566,f297]) ).
fof(f2751,plain,
( ~ sQ7_spl
| ~ sQ172_spl
| ~ sQ200_spl
| nil = sk3 ),
inference(backward_demodulation,[status(thm)],[f2248,f499]) ).
fof(f2759,plain,
( ~ sQ7_spl
| ~ sQ172_spl
| ~ sQ200_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f2751,f486,f2044,f1851,f498]) ).
fof(f2833,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| frontsegP(sk3,app(app(sk7,sk3),sk3))
| ~ ssList(app(app(sk7,sk3),sk3))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f2079,f2467]) ).
fof(f2847,definition,
( sQ285_spl
<=> frontsegP(sk3,app(app(sk7,sk3),sk3)) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f2848,plain,
( ~ sQ285_spl
| frontsegP(sk3,app(app(sk7,sk3),sk3)) ),
inference(component_clause,[status(thm)],[f2847]) ).
fof(f2850,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| sQ285_spl
| ~ sQ212_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2833,f557,f2155,f2847,f498,f2044,f594]) ).
fof(f3001,plain,
( ~ sQ192_spl
| ~ sQ4_spl
| memberP(nil,sk5) ),
inference(forward_demodulation,[status(thm)],[f487,f2004]) ).
fof(f3037,definition,
! [X2] :
( sQ302_spl
<=> ( ~ ssItem(X2)
| ~ ssItem(X2)
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f3038,plain,
! [X0] :
( ~ sQ302_spl
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f3037]) ).
fof(f3044,plain,
! [X0] :
( ~ sQ302_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3038]) ).
fof(f3140,plain,
( sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1180,f224]) ).
fof(f3141,plain,
sQ81_spl,
inference(contradiction_clause,[status(thm)],[f3140]) ).
fof(f3142,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1177,f223]) ).
fof(f3143,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f3142]) ).
fof(f3146,plain,
( ~ sQ302_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f448,f3044]) ).
fof(f3164,plain,
~ sQ302_spl,
inference(contradiction_clause,[status(thm)],[f3146]) ).
fof(f3196,plain,
( ~ sQ192_spl
| ~ sQ4_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f282,f3001]) ).
fof(f3197,plain,
( ~ sQ192_spl
| ~ sQ4_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f3196,f604,f486,f2003]) ).
fof(f3507,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| app(app(app(sk7,sk3),cons(sk9,nil)),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f499,f2077]) ).
fof(f3508,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| app(app(app(sk7,sk3),sk3),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f499,f3507]) ).
fof(f3530,definition,
( sQ343_spl
<=> ssList(app(sk7,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition]) ).
fof(f3532,plain,
( sQ343_spl
| ~ ssList(app(sk7,sk3)) ),
inference(component_clause,[status(thm)],[f3530]) ).
fof(f3677,definition,
( sQ354_spl
<=> sk3 = app(nil,sk3) ),
introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition]) ).
fof(f3678,plain,
( ~ sQ354_spl
| sk3 = app(nil,sk3) ),
inference(component_clause,[status(thm)],[f3677]) ).
fof(f3679,plain,
( sQ354_spl
| sk3 != app(nil,sk3) ),
inference(component_clause,[status(thm)],[f3677]) ).
fof(f4072,plain,
! [X0] :
( ~ sQ7_spl
| frontsegP(cons(sk9,X0),sk3)
| ~ ssItem(sk9)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X0,nil) ),
inference(paramodulation,[status(thm)],[f499,f541]) ).
fof(f4079,definition,
! [X0] :
( sQ404_spl
<=> ( frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f4080,plain,
! [X0] :
( ~ sQ404_spl
| frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(component_clause,[status(thm)],[f4079]) ).
fof(f4082,plain,
( ~ sQ7_spl
| ~ sQ2_spl
| ~ sQ13_spl
| sQ404_spl ),
inference(split_clause,[status(thm)],[f4072,f4079,f563,f479,f498]) ).
fof(f4083,plain,
! [X0] :
( ~ sQ404_spl
| frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4080,f271]) ).
fof(f4128,definition,
( sQ407_spl
<=> ssList(app(app(nil,sk3),sk3)) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f4129,plain,
( ~ sQ407_spl
| ssList(app(app(nil,sk3),sk3)) ),
inference(component_clause,[status(thm)],[f4128]) ).
fof(f4130,plain,
( sQ407_spl
| ~ ssList(app(app(nil,sk3),sk3)) ),
inference(component_clause,[status(thm)],[f4128]) ).
fof(f4366,definition,
( sQ432_spl
<=> ssList(skaf45(sk4,app(nil,sk3))) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f4368,plain,
( sQ432_spl
| ~ ssList(skaf45(sk4,app(nil,sk3))) ),
inference(component_clause,[status(thm)],[f4366]) ).
fof(f4374,plain,
( sQ432_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4368,f262]) ).
fof(f4375,plain,
sQ432_spl,
inference(contradiction_clause,[status(thm)],[f4374]) ).
fof(f4460,definition,
( sQ440_spl
<=> ssList(skaf46(sk4,sk11)) ),
introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition]) ).
fof(f4462,plain,
( sQ440_spl
| ~ ssList(skaf46(sk4,sk11)) ),
inference(component_clause,[status(thm)],[f4460]) ).
fof(f4472,plain,
( sQ440_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4462,f261]) ).
fof(f4473,plain,
sQ440_spl,
inference(contradiction_clause,[status(thm)],[f4472]) ).
fof(f4631,definition,
( sQ458_spl
<=> ssItem(skaf83(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ458_spl])],[split_symbol_definition]) ).
fof(f4633,plain,
( sQ458_spl
| ~ ssItem(skaf83(sk3)) ),
inference(component_clause,[status(thm)],[f4631]) ).
fof(f4645,plain,
( sQ458_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4633,f223]) ).
fof(f4646,plain,
sQ458_spl,
inference(contradiction_clause,[status(thm)],[f4645]) ).
fof(f4742,definition,
( sQ468_spl
<=> ssList(skaf82(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition]) ).
fof(f4744,plain,
( sQ468_spl
| ~ ssList(skaf82(sk3)) ),
inference(component_clause,[status(thm)],[f4742]) ).
fof(f4761,plain,
( sQ468_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4744,f224]) ).
fof(f4762,plain,
sQ468_spl,
inference(contradiction_clause,[status(thm)],[f4761]) ).
fof(f4834,plain,
( sQ343_spl
| ~ sQ30_spl
| ~ sQ200_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3532,f2076]) ).
fof(f4835,plain,
( sQ343_spl
| ~ sQ30_spl
| ~ sQ200_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f4834]) ).
fof(f5028,definition,
( sQ486_spl
<=> ssItem(skaf83(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition]) ).
fof(f5030,plain,
( sQ486_spl
| ~ ssItem(skaf83(sk4)) ),
inference(component_clause,[status(thm)],[f5028]) ).
fof(f5185,plain,
( sQ486_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5030,f223]) ).
fof(f5186,plain,
sQ486_spl,
inference(contradiction_clause,[status(thm)],[f5185]) ).
fof(f5332,plain,
( sQ141_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1683]) ).
fof(f5333,plain,
sQ141_spl,
inference(contradiction_clause,[status(thm)],[f5332]) ).
fof(f5960,plain,
( sQ354_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f3679,f286]) ).
fof(f5961,plain,
( sQ354_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f5960,f717,f3677]) ).
fof(f6936,plain,
( ~ sQ192_spl
| ~ sQ200_spl
| ~ sQ100_spl
| ~ ssItem(sk9) ),
inference(resolution,[status(thm)],[f2254,f2048]) ).
fof(f6937,plain,
( ~ sQ192_spl
| ~ sQ200_spl
| ~ sQ100_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f6936,f479,f1377,f2044,f2003]) ).
fof(f6968,definition,
( sQ642_spl
<=> ssList(skaf46(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ642_spl])],[split_symbol_definition]) ).
fof(f6970,plain,
( sQ642_spl
| ~ ssList(skaf46(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f6968]) ).
fof(f6975,definition,
( sQ644_spl
<=> ssList(skaf46(sk3,sk8)) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f6977,plain,
( sQ644_spl
| ~ ssList(skaf46(sk3,sk8)) ),
inference(component_clause,[status(thm)],[f6975]) ).
fof(f6987,plain,
( sQ642_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6970,f261]) ).
fof(f6988,plain,
sQ642_spl,
inference(contradiction_clause,[status(thm)],[f6987]) ).
fof(f6990,plain,
( sQ644_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6977,f261]) ).
fof(f6991,plain,
sQ644_spl,
inference(contradiction_clause,[status(thm)],[f6990]) ).
fof(f7140,plain,
( ~ sQ12_spl
| ~ sQ17_spl
| ~ sQ200_spl
| ssList(app(app(sk7,cons(sk9,nil)),cons(sk5,nil))) ),
inference(forward_demodulation,[status(thm)],[f2045,f2042]) ).
fof(f7141,plain,
( ~ sQ12_spl
| ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ssList(app(app(sk7,sk3),cons(sk5,nil))) ),
inference(forward_demodulation,[status(thm)],[f499,f7140]) ).
fof(f7142,plain,
( ~ sQ12_spl
| ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ssList(app(app(sk7,sk3),cons(sk9,nil))) ),
inference(forward_demodulation,[status(thm)],[f2045,f7141]) ).
fof(f7143,plain,
( ~ sQ12_spl
| ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ssList(app(app(sk7,sk3),sk3)) ),
inference(forward_demodulation,[status(thm)],[f499,f7142]) ).
fof(f7215,definition,
( sQ675_spl
<=> ssList(skaf46(tl(sk4),sk11)) ),
introduced(definition,[new_symbols(definition,[sQ675_spl])],[split_symbol_definition]) ).
fof(f7217,plain,
( sQ675_spl
| ~ ssList(skaf46(tl(sk4),sk11)) ),
inference(component_clause,[status(thm)],[f7215]) ).
fof(f7241,plain,
( sQ675_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7217,f261]) ).
fof(f7242,plain,
sQ675_spl,
inference(contradiction_clause,[status(thm)],[f7241]) ).
fof(f7286,definition,
( sQ683_spl
<=> ssList(skaf45(sk3,nil)) ),
introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition]) ).
fof(f7288,plain,
( sQ683_spl
| ~ ssList(skaf45(sk3,nil)) ),
inference(component_clause,[status(thm)],[f7286]) ).
fof(f7293,definition,
( sQ685_spl
<=> ssList(skaf45(sk3,app(app(sk7,sk3),sk3))) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f7295,plain,
( sQ685_spl
| ~ ssList(skaf45(sk3,app(app(sk7,sk3),sk3))) ),
inference(component_clause,[status(thm)],[f7293]) ).
fof(f7300,definition,
( sQ687_spl
<=> ssList(skaf45(sk4,app(sk10,sk3))) ),
introduced(definition,[new_symbols(definition,[sQ687_spl])],[split_symbol_definition]) ).
fof(f7302,plain,
( sQ687_spl
| ~ ssList(skaf45(sk4,app(sk10,sk3))) ),
inference(component_clause,[status(thm)],[f7300]) ).
fof(f7307,plain,
( sQ683_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7288,f262]) ).
fof(f7308,plain,
sQ683_spl,
inference(contradiction_clause,[status(thm)],[f7307]) ).
fof(f7309,plain,
( sQ687_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7302,f262]) ).
fof(f7310,plain,
sQ687_spl,
inference(contradiction_clause,[status(thm)],[f7309]) ).
fof(f7313,plain,
( sQ685_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7295,f262]) ).
fof(f7314,plain,
sQ685_spl,
inference(contradiction_clause,[status(thm)],[f7313]) ).
fof(f7373,definition,
( sQ692_spl
<=> ssList(skaf45(nil,tl(nil))) ),
introduced(definition,[new_symbols(definition,[sQ692_spl])],[split_symbol_definition]) ).
fof(f7375,plain,
( sQ692_spl
| ~ ssList(skaf45(nil,tl(nil))) ),
inference(component_clause,[status(thm)],[f7373]) ).
fof(f7380,definition,
( sQ694_spl
<=> ssList(skaf46(nil,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ694_spl])],[split_symbol_definition]) ).
fof(f7382,plain,
( sQ694_spl
| ~ ssList(skaf46(nil,sk3)) ),
inference(component_clause,[status(thm)],[f7380]) ).
fof(f7433,plain,
( sQ694_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7382,f261]) ).
fof(f7434,plain,
sQ694_spl,
inference(contradiction_clause,[status(thm)],[f7433]) ).
fof(f7435,plain,
( sQ692_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7375,f262]) ).
fof(f7436,plain,
sQ692_spl,
inference(contradiction_clause,[status(thm)],[f7435]) ).
fof(f7453,plain,
( sQ212_spl
| ~ sQ12_spl
| ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2157,f7143]) ).
fof(f7454,plain,
( sQ212_spl
| ~ sQ12_spl
| ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f7453]) ).
fof(f7571,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ213_spl
| app(nil,sk8) = sk3 ),
inference(backward_demodulation,[status(thm)],[f2159,f3508]) ).
fof(f7597,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ213_spl
| sQ170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7571,f1846]) ).
fof(f7598,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ213_spl
| sQ170_spl ),
inference(contradiction_clause,[status(thm)],[f7597]) ).
fof(f7878,definition,
( sQ738_spl
<=> ssList(skaf45(sk4,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ738_spl])],[split_symbol_definition]) ).
fof(f7880,plain,
( sQ738_spl
| ~ ssList(skaf45(sk4,sk3)) ),
inference(component_clause,[status(thm)],[f7878]) ).
fof(f7890,plain,
( sQ738_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7880,f262]) ).
fof(f7891,plain,
sQ738_spl,
inference(contradiction_clause,[status(thm)],[f7890]) ).
fof(f7930,definition,
( sQ742_spl
<=> ssList(skaf45(sk4,sk10)) ),
introduced(definition,[new_symbols(definition,[sQ742_spl])],[split_symbol_definition]) ).
fof(f7932,plain,
( sQ742_spl
| ~ ssList(skaf45(sk4,sk10)) ),
inference(component_clause,[status(thm)],[f7930]) ).
fof(f7937,definition,
( sQ744_spl
<=> ssList(skaf46(sk4,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition]) ).
fof(f7939,plain,
( sQ744_spl
| ~ ssList(skaf46(sk4,sk4)) ),
inference(component_clause,[status(thm)],[f7937]) ).
fof(f7980,plain,
( sQ744_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7939,f261]) ).
fof(f7981,plain,
sQ744_spl,
inference(contradiction_clause,[status(thm)],[f7980]) ).
fof(f7982,plain,
( sQ742_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7932,f262]) ).
fof(f7983,plain,
sQ742_spl,
inference(contradiction_clause,[status(thm)],[f7982]) ).
fof(f8820,definition,
( sQ859_spl
<=> ssItem(skaf78(nil)) ),
introduced(definition,[new_symbols(definition,[sQ859_spl])],[split_symbol_definition]) ).
fof(f8822,plain,
( sQ859_spl
| ~ ssItem(skaf78(nil)) ),
inference(component_clause,[status(thm)],[f8820]) ).
fof(f8827,plain,
( sQ859_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8822,f228]) ).
fof(f8828,plain,
sQ859_spl,
inference(contradiction_clause,[status(thm)],[f8827]) ).
fof(f9532,definition,
( sQ945_spl
<=> ssItem(skaf83(sk10)) ),
introduced(definition,[new_symbols(definition,[sQ945_spl])],[split_symbol_definition]) ).
fof(f9534,plain,
( sQ945_spl
| ~ ssItem(skaf83(sk10)) ),
inference(component_clause,[status(thm)],[f9532]) ).
fof(f9669,plain,
( sQ945_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9534,f223]) ).
fof(f9670,plain,
sQ945_spl,
inference(contradiction_clause,[status(thm)],[f9669]) ).
fof(f10476,definition,
( sQ1058_spl
<=> ssItem(skaf70(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1058_spl])],[split_symbol_definition]) ).
fof(f10478,plain,
( sQ1058_spl
| ~ ssItem(skaf70(nil)) ),
inference(component_clause,[status(thm)],[f10476]) ).
fof(f10479,definition,
( sQ1059_spl
<=> ssList(skaf73(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1059_spl])],[split_symbol_definition]) ).
fof(f10481,plain,
( sQ1059_spl
| ~ ssList(skaf73(nil)) ),
inference(component_clause,[status(thm)],[f10479]) ).
fof(f10483,plain,
( sQ1059_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10481,f233]) ).
fof(f10484,plain,
sQ1059_spl,
inference(contradiction_clause,[status(thm)],[f10483]) ).
fof(f10485,plain,
( sQ1058_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10478,f236]) ).
fof(f10486,plain,
sQ1058_spl,
inference(contradiction_clause,[status(thm)],[f10485]) ).
fof(f10488,definition,
( sQ1060_spl
<=> ssItem(skaf65(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1060_spl])],[split_symbol_definition]) ).
fof(f10490,plain,
( sQ1060_spl
| ~ ssItem(skaf65(nil)) ),
inference(component_clause,[status(thm)],[f10488]) ).
fof(f10491,definition,
( sQ1061_spl
<=> ssList(skaf68(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1061_spl])],[split_symbol_definition]) ).
fof(f10493,plain,
( sQ1061_spl
| ~ ssList(skaf68(nil)) ),
inference(component_clause,[status(thm)],[f10491]) ).
fof(f10495,plain,
( sQ1061_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10493,f238]) ).
fof(f10496,plain,
sQ1061_spl,
inference(contradiction_clause,[status(thm)],[f10495]) ).
fof(f10497,plain,
( sQ1060_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10490,f241]) ).
fof(f10498,plain,
sQ1060_spl,
inference(contradiction_clause,[status(thm)],[f10497]) ).
fof(f10500,definition,
( sQ1062_spl
<=> ssItem(skaf60(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1062_spl])],[split_symbol_definition]) ).
fof(f10502,plain,
( sQ1062_spl
| ~ ssItem(skaf60(nil)) ),
inference(component_clause,[status(thm)],[f10500]) ).
fof(f10503,definition,
( sQ1063_spl
<=> ssList(skaf63(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1063_spl])],[split_symbol_definition]) ).
fof(f10505,plain,
( sQ1063_spl
| ~ ssList(skaf63(nil)) ),
inference(component_clause,[status(thm)],[f10503]) ).
fof(f10507,plain,
( sQ1063_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10505,f243]) ).
fof(f10508,plain,
sQ1063_spl,
inference(contradiction_clause,[status(thm)],[f10507]) ).
fof(f10509,plain,
( sQ1062_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10502,f246]) ).
fof(f10510,plain,
sQ1062_spl,
inference(contradiction_clause,[status(thm)],[f10509]) ).
fof(f10512,definition,
( sQ1064_spl
<=> ssItem(skaf55(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1064_spl])],[split_symbol_definition]) ).
fof(f10514,plain,
( sQ1064_spl
| ~ ssItem(skaf55(nil)) ),
inference(component_clause,[status(thm)],[f10512]) ).
fof(f10515,definition,
( sQ1065_spl
<=> ssList(skaf58(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1065_spl])],[split_symbol_definition]) ).
fof(f10517,plain,
( sQ1065_spl
| ~ ssList(skaf58(nil)) ),
inference(component_clause,[status(thm)],[f10515]) ).
fof(f10519,plain,
( sQ1065_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10517,f248]) ).
fof(f10520,plain,
sQ1065_spl,
inference(contradiction_clause,[status(thm)],[f10519]) ).
fof(f10521,plain,
( sQ1064_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10514,f251]) ).
fof(f10522,plain,
sQ1064_spl,
inference(contradiction_clause,[status(thm)],[f10521]) ).
fof(f10552,definition,
( sQ1068_spl
<=> ssItem(skaf50(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1068_spl])],[split_symbol_definition]) ).
fof(f10554,plain,
( sQ1068_spl
| ~ ssItem(skaf50(nil)) ),
inference(component_clause,[status(thm)],[f10552]) ).
fof(f10555,definition,
( sQ1069_spl
<=> ssList(skaf53(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1069_spl])],[split_symbol_definition]) ).
fof(f10557,plain,
( sQ1069_spl
| ~ ssList(skaf53(nil)) ),
inference(component_clause,[status(thm)],[f10555]) ).
fof(f10559,plain,
( sQ1069_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10557,f253]) ).
fof(f10560,plain,
sQ1069_spl,
inference(contradiction_clause,[status(thm)],[f10559]) ).
fof(f10561,plain,
( sQ1068_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10554,f256]) ).
fof(f10562,plain,
sQ1068_spl,
inference(contradiction_clause,[status(thm)],[f10561]) ).
fof(f10880,definition,
( sQ1105_spl
<=> ssList(skaf71(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1105_spl])],[split_symbol_definition]) ).
fof(f10882,plain,
( sQ1105_spl
| ~ ssList(skaf71(nil)) ),
inference(component_clause,[status(thm)],[f10880]) ).
fof(f10884,plain,
( sQ1105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10882,f235]) ).
fof(f10885,plain,
sQ1105_spl,
inference(contradiction_clause,[status(thm)],[f10884]) ).
fof(f10906,plain,
( sQ407_spl
| ~ sQ354_spl
| ~ ssList(app(sk3,sk3)) ),
inference(forward_demodulation,[status(thm)],[f3678,f4130]) ).
fof(f10995,definition,
( sQ1107_spl
<=> ssList(skaf66(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1107_spl])],[split_symbol_definition]) ).
fof(f10997,plain,
( sQ1107_spl
| ~ ssList(skaf66(nil)) ),
inference(component_clause,[status(thm)],[f10995]) ).
fof(f10999,plain,
( sQ1107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10997,f240]) ).
fof(f11000,plain,
sQ1107_spl,
inference(contradiction_clause,[status(thm)],[f10999]) ).
fof(f11260,definition,
( sQ1136_spl
<=> nil = app(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[sQ1136_spl])],[split_symbol_definition]) ).
fof(f11261,plain,
( ~ sQ1136_spl
| nil = app(sk7,sk3) ),
inference(component_clause,[status(thm)],[f11260]) ).
fof(f11267,plain,
( sQ407_spl
| ~ sQ354_spl
| ~ ssList(sk3)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f10906,f297]) ).
fof(f11268,plain,
( sQ407_spl
| ~ sQ354_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f11267,f717,f3677,f4128]) ).
fof(f11269,plain,
( ~ sQ407_spl
| ~ sQ354_spl
| ssList(app(sk3,sk3)) ),
inference(forward_demodulation,[status(thm)],[f3678,f4129]) ).
fof(f11333,definition,
( sQ1143_spl
<=> ssList(skaf45(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1143_spl])],[split_symbol_definition]) ).
fof(f11335,plain,
( sQ1143_spl
| ~ ssList(skaf45(nil,nil)) ),
inference(component_clause,[status(thm)],[f11333]) ).
fof(f11340,definition,
( sQ1145_spl
<=> ssList(skaf46(nil,sk11)) ),
introduced(definition,[new_symbols(definition,[sQ1145_spl])],[split_symbol_definition]) ).
fof(f11342,plain,
( sQ1145_spl
| ~ ssList(skaf46(nil,sk11)) ),
inference(component_clause,[status(thm)],[f11340]) ).
fof(f11387,plain,
( sQ1145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11342,f261]) ).
fof(f11388,plain,
sQ1145_spl,
inference(contradiction_clause,[status(thm)],[f11387]) ).
fof(f11389,plain,
( sQ1143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11335,f262]) ).
fof(f11390,plain,
sQ1143_spl,
inference(contradiction_clause,[status(thm)],[f11389]) ).
fof(f11457,definition,
( sQ1158_spl
<=> ssList(skaf46(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1158_spl])],[split_symbol_definition]) ).
fof(f11459,plain,
( sQ1158_spl
| ~ ssList(skaf46(nil,nil)) ),
inference(component_clause,[status(thm)],[f11457]) ).
fof(f11504,plain,
( sQ1158_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11459,f261]) ).
fof(f11505,plain,
sQ1158_spl,
inference(contradiction_clause,[status(thm)],[f11504]) ).
fof(f11518,definition,
( sQ1168_spl
<=> ssList(skaf61(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1168_spl])],[split_symbol_definition]) ).
fof(f11520,plain,
( sQ1168_spl
| ~ ssList(skaf61(nil)) ),
inference(component_clause,[status(thm)],[f11518]) ).
fof(f11522,plain,
( sQ1168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11520,f245]) ).
fof(f11523,plain,
sQ1168_spl,
inference(contradiction_clause,[status(thm)],[f11522]) ).
fof(f11528,definition,
( sQ1170_spl
<=> ssList(skaf56(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1170_spl])],[split_symbol_definition]) ).
fof(f11530,plain,
( sQ1170_spl
| ~ ssList(skaf56(nil)) ),
inference(component_clause,[status(thm)],[f11528]) ).
fof(f11532,plain,
( sQ1170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11530,f250]) ).
fof(f11533,plain,
sQ1170_spl,
inference(contradiction_clause,[status(thm)],[f11532]) ).
fof(f11559,plain,
! [X0] :
( ~ sQ1136_spl
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(sk3)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f11261,f367]) ).
fof(f11580,definition,
( sQ1171_spl
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[sQ1171_spl])],[split_symbol_definition]) ).
fof(f11581,plain,
( ~ sQ1171_spl
| nil = sk7 ),
inference(component_clause,[status(thm)],[f11580]) ).
fof(f11609,definition,
( sQ1178_spl
<=> app(sk7,sk3) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ1178_spl])],[split_symbol_definition]) ).
fof(f11610,plain,
( ~ sQ1178_spl
| app(sk7,sk3) = sk3 ),
inference(component_clause,[status(thm)],[f11609]) ).
fof(f11625,definition,
( sQ1182_spl
<=> ssList(skaf45(nil,sk7)) ),
introduced(definition,[new_symbols(definition,[sQ1182_spl])],[split_symbol_definition]) ).
fof(f11627,plain,
( sQ1182_spl
| ~ ssList(skaf45(nil,sk7)) ),
inference(component_clause,[status(thm)],[f11625]) ).
fof(f11640,plain,
( ~ sQ1136_spl
| ~ sQ78_spl
| ~ sQ34_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f11559,f1377,f717,f1118,f11260]) ).
fof(f11682,plain,
( sQ1182_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11627,f262]) ).
fof(f11683,plain,
sQ1182_spl,
inference(contradiction_clause,[status(thm)],[f11682]) ).
fof(f11792,definition,
( sQ1199_spl
<=> ssList(skaf51(nil)) ),
introduced(definition,[new_symbols(definition,[sQ1199_spl])],[split_symbol_definition]) ).
fof(f11794,plain,
( sQ1199_spl
| ~ ssList(skaf51(nil)) ),
inference(component_clause,[status(thm)],[f11792]) ).
fof(f11796,plain,
( sQ1199_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11794,f255]) ).
fof(f11797,plain,
sQ1199_spl,
inference(contradiction_clause,[status(thm)],[f11796]) ).
fof(f11869,definition,
( sQ1209_spl
<=> ssList(skaf45(sk11,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1209_spl])],[split_symbol_definition]) ).
fof(f11871,plain,
( sQ1209_spl
| ~ ssList(skaf45(sk11,nil)) ),
inference(component_clause,[status(thm)],[f11869]) ).
fof(f11873,definition,
( sQ1210_spl
<=> ssList(skaf46(sk11,sk11)) ),
introduced(definition,[new_symbols(definition,[sQ1210_spl])],[split_symbol_definition]) ).
fof(f11875,plain,
( sQ1210_spl
| ~ ssList(skaf46(sk11,sk11)) ),
inference(component_clause,[status(thm)],[f11873]) ).
fof(f11935,plain,
( sQ1210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11875,f261]) ).
fof(f11936,plain,
sQ1210_spl,
inference(contradiction_clause,[status(thm)],[f11935]) ).
fof(f11937,plain,
( sQ1209_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11871,f262]) ).
fof(f11938,plain,
sQ1209_spl,
inference(contradiction_clause,[status(thm)],[f11937]) ).
fof(f12355,plain,
( ~ sQ1178_spl
| tl(sk3) = app(tl(sk7),sk3)
| nil = sk7
| ~ ssList(sk7)
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f11610,f357]) ).
fof(f12376,definition,
( sQ1250_spl
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[sQ1250_spl])],[split_symbol_definition]) ).
fof(f12393,definition,
( sQ1254_spl
<=> ssList(skaf45(sk3,sk7)) ),
introduced(definition,[new_symbols(definition,[sQ1254_spl])],[split_symbol_definition]) ).
fof(f12395,plain,
( sQ1254_spl
| ~ ssList(skaf45(sk3,sk7)) ),
inference(component_clause,[status(thm)],[f12393]) ).
fof(f12418,definition,
( sQ1259_spl
<=> tl(sk3) = app(tl(sk7),sk3) ),
introduced(definition,[new_symbols(definition,[sQ1259_spl])],[split_symbol_definition]) ).
fof(f12419,plain,
( ~ sQ1259_spl
| tl(sk3) = app(tl(sk7),sk3) ),
inference(component_clause,[status(thm)],[f12418]) ).
fof(f12421,plain,
( ~ sQ1178_spl
| sQ1259_spl
| sQ1171_spl
| ~ sQ78_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f12355,f717,f1118,f11580,f12418,f11609]) ).
fof(f12444,plain,
( ~ sQ1259_spl
| ~ sQ85_spl
| nil = app(tl(sk7),sk3) ),
inference(forward_demodulation,[status(thm)],[f1216,f12419]) ).
fof(f12445,plain,
( sQ1254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12395,f262]) ).
fof(f12446,plain,
sQ1254_spl,
inference(contradiction_clause,[status(thm)],[f12445]) ).
fof(f12450,definition,
( sQ1264_spl
<=> cons(sk9,tl(sk7)) = sk7 ),
introduced(definition,[new_symbols(definition,[sQ1264_spl])],[split_symbol_definition]) ).
fof(f12451,plain,
( ~ sQ1264_spl
| cons(sk9,tl(sk7)) = sk7 ),
inference(component_clause,[status(thm)],[f12450]) ).
fof(f12787,definition,
( sQ1281_spl
<=> ssList(skaf45(sk7,sk7)) ),
introduced(definition,[new_symbols(definition,[sQ1281_spl])],[split_symbol_definition]) ).
fof(f12789,plain,
( sQ1281_spl
| ~ ssList(skaf45(sk7,sk7)) ),
inference(component_clause,[status(thm)],[f12787]) ).
fof(f12791,definition,
( sQ1282_spl
<=> ssList(skaf46(sk7,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1282_spl])],[split_symbol_definition]) ).
fof(f12793,plain,
( sQ1282_spl
| ~ ssList(skaf46(sk7,sk3)) ),
inference(component_clause,[status(thm)],[f12791]) ).
fof(f12849,plain,
( sQ1282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12793,f261]) ).
fof(f12850,plain,
sQ1282_spl,
inference(contradiction_clause,[status(thm)],[f12849]) ).
fof(f12851,plain,
( sQ1281_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12789,f262]) ).
fof(f12852,plain,
sQ1281_spl,
inference(contradiction_clause,[status(thm)],[f12851]) ).
fof(f13828,plain,
( ~ sQ1259_spl
| ~ sQ85_spl
| nil = sk3
| ~ ssList(tl(sk7))
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f12444,f341]) ).
fof(f13860,definition,
( sQ1381_spl
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ1381_spl])],[split_symbol_definition]) ).
fof(f13862,plain,
( sQ1381_spl
| ~ ssList(tl(sk7)) ),
inference(component_clause,[status(thm)],[f13860]) ).
fof(f13867,plain,
( ~ sQ1259_spl
| ~ sQ85_spl
| sQ4_spl
| ~ sQ1381_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f13828,f717,f13860,f486,f1215,f12418]) ).
fof(f13906,definition,
( sQ1392_spl
<=> ssList(skaf45(nil,tl(sk7))) ),
introduced(definition,[new_symbols(definition,[sQ1392_spl])],[split_symbol_definition]) ).
fof(f13908,plain,
( sQ1392_spl
| ~ ssList(skaf45(nil,tl(sk7))) ),
inference(component_clause,[status(thm)],[f13906]) ).
fof(f13963,plain,
( sQ1392_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13908,f262]) ).
fof(f13964,plain,
sQ1392_spl,
inference(contradiction_clause,[status(thm)],[f13963]) ).
fof(f13969,plain,
( sQ1381_spl
| nil = sk7
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f13862,f287]) ).
fof(f13970,plain,
( sQ1381_spl
| sQ1171_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f13969,f1118,f11580,f13860]) ).
fof(f13981,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ1171_spl
| app(app(app(nil,sk3),sk3),sk8) = sk3 ),
inference(backward_demodulation,[status(thm)],[f11581,f3508]) ).
fof(f13995,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ1171_spl
| ~ sQ354_spl
| app(app(sk3,sk3),sk8) = sk3 ),
inference(forward_demodulation,[status(thm)],[f3678,f13981]) ).
fof(f14031,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ1171_spl
| ~ sQ354_spl
| frontsegP(sk3,app(sk3,sk3))
| ~ ssList(app(sk3,sk3))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f13995,f2467]) ).
fof(f14053,definition,
( sQ1406_spl
<=> ssList(app(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1406_spl])],[split_symbol_definition]) ).
fof(f14055,plain,
( sQ1406_spl
| ~ ssList(app(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f14053]) ).
fof(f14090,definition,
( sQ1415_spl
<=> ssList(skaf45(sk3,app(sk3,sk3))) ),
introduced(definition,[new_symbols(definition,[sQ1415_spl])],[split_symbol_definition]) ).
fof(f14092,plain,
( sQ1415_spl
| ~ ssList(skaf45(sk3,app(sk3,sk3))) ),
inference(component_clause,[status(thm)],[f14090]) ).
fof(f14115,definition,
( sQ1421_spl
<=> frontsegP(sk3,app(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1421_spl])],[split_symbol_definition]) ).
fof(f14116,plain,
( ~ sQ1421_spl
| frontsegP(sk3,app(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f14115]) ).
fof(f14118,plain,
( ~ sQ17_spl
| ~ sQ200_spl
| ~ sQ7_spl
| ~ sQ1171_spl
| ~ sQ354_spl
| sQ1421_spl
| ~ sQ1406_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f14031,f557,f14053,f14115,f3677,f11580,f498,f2044,f594]) ).
fof(f14149,plain,
( sQ1406_spl
| ~ sQ407_spl
| ~ sQ354_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14055,f11269]) ).
fof(f14150,plain,
( sQ1406_spl
| ~ sQ407_spl
| ~ sQ354_spl ),
inference(contradiction_clause,[status(thm)],[f14149]) ).
fof(f14153,plain,
( sQ1415_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14092,f262]) ).
fof(f14154,plain,
sQ1415_spl,
inference(contradiction_clause,[status(thm)],[f14153]) ).
fof(f14350,definition,
( sQ1435_spl
<=> app(sk3,sk3) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ1435_spl])],[split_symbol_definition]) ).
fof(f14351,plain,
( ~ sQ1435_spl
| app(sk3,sk3) = sk3 ),
inference(component_clause,[status(thm)],[f14350]) ).
fof(f14364,definition,
( sQ1438_spl
<=> ssList(skaf45(nil,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1438_spl])],[split_symbol_definition]) ).
fof(f14366,plain,
( sQ1438_spl
| ~ ssList(skaf45(nil,sk3)) ),
inference(component_clause,[status(thm)],[f14364]) ).
fof(f14412,plain,
( sQ1438_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14366,f262]) ).
fof(f14413,plain,
sQ1438_spl,
inference(contradiction_clause,[status(thm)],[f14412]) ).
fof(f14684,plain,
( ~ sQ1435_spl
| ~ sQ31_spl
| sk3 = cons(sk9,sk3)
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f14351,f704]) ).
fof(f14719,definition,
( sQ1478_spl
<=> sk3 = cons(sk9,sk3) ),
introduced(definition,[new_symbols(definition,[sQ1478_spl])],[split_symbol_definition]) ).
fof(f14720,plain,
( ~ sQ1478_spl
| sk3 = cons(sk9,sk3) ),
inference(component_clause,[status(thm)],[f14719]) ).
fof(f14722,plain,
( ~ sQ1435_spl
| ~ sQ31_spl
| sQ1478_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f14684,f717,f14719,f703,f14350]) ).
fof(f14758,definition,
( sQ1486_spl
<=> ssList(skaf45(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1486_spl])],[split_symbol_definition]) ).
fof(f14760,plain,
( sQ1486_spl
| ~ ssList(skaf45(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f14758]) ).
fof(f14804,plain,
( sQ1486_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14760,f262]) ).
fof(f14805,plain,
sQ1486_spl,
inference(contradiction_clause,[status(thm)],[f14804]) ).
fof(f15003,plain,
( ~ sQ1478_spl
| ~ ssList(sk3)
| ~ ssItem(sk9) ),
inference(resolution,[status(thm)],[f14720,f313]) ).
fof(f15052,plain,
( ~ sQ1478_spl
| ~ sQ34_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f15003,f479,f717,f14719]) ).
fof(f15360,definition,
( sQ1553_spl
<=> frontsegP(sk3,app(sk7,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1553_spl])],[split_symbol_definition]) ).
fof(f15361,plain,
( ~ sQ1553_spl
| frontsegP(sk3,app(sk7,sk3)) ),
inference(component_clause,[status(thm)],[f15360]) ).
fof(f15383,plain,
( ~ sQ285_spl
| ~ ssList(sk3)
| frontsegP(sk3,app(sk7,sk3))
| ~ ssList(sk3)
| ~ ssList(app(sk7,sk3)) ),
inference(resolution,[status(thm)],[f2848,f2567]) ).
fof(f15395,plain,
( ~ sQ285_spl
| sQ1553_spl
| ~ sQ34_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f15383,f3530,f717,f15360,f2847]) ).
fof(f15501,definition,
( sQ1572_spl
<=> ssList(skaf46(sk3,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1572_spl])],[split_symbol_definition]) ).
fof(f15503,plain,
( sQ1572_spl
| ~ ssList(skaf46(sk3,nil)) ),
inference(component_clause,[status(thm)],[f15501]) ).
fof(f15553,plain,
( sQ1572_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15503,f261]) ).
fof(f15554,plain,
sQ1572_spl,
inference(contradiction_clause,[status(thm)],[f15553]) ).
fof(f15901,plain,
( ~ sQ215_spl
| ~ sQ84_spl
| sk9 = hd(app(app(sk7,sk3),sk3)) ),
inference(forward_demodulation,[status(thm)],[f1212,f2166]) ).
fof(f15902,plain,
( ~ sQ215_spl
| ~ sQ84_spl
| sk9 = hd(app(sk7,sk3))
| nil = app(sk7,sk3)
| ~ ssList(app(sk7,sk3))
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f15901,f345]) ).
fof(f15905,definition,
( sQ1591_spl
<=> sk9 = hd(app(sk7,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1591_spl])],[split_symbol_definition]) ).
fof(f15906,plain,
( ~ sQ1591_spl
| sk9 = hd(app(sk7,sk3)) ),
inference(component_clause,[status(thm)],[f15905]) ).
fof(f15908,plain,
( ~ sQ215_spl
| ~ sQ84_spl
| sQ1591_spl
| sQ1136_spl
| ~ sQ343_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f15902,f717,f3530,f11260,f15905,f1211,f2165]) ).
fof(f16026,definition,
( sQ1610_spl
<=> ssList(skaf45(nil,tl(app(app(sk7,sk3),sk3)))) ),
introduced(definition,[new_symbols(definition,[sQ1610_spl])],[split_symbol_definition]) ).
fof(f16028,plain,
( sQ1610_spl
| ~ ssList(skaf45(nil,tl(app(app(sk7,sk3),sk3)))) ),
inference(component_clause,[status(thm)],[f16026]) ).
fof(f16033,definition,
( sQ1612_spl
<=> ssList(skaf46(nil,sk8)) ),
introduced(definition,[new_symbols(definition,[sQ1612_spl])],[split_symbol_definition]) ).
fof(f16035,plain,
( sQ1612_spl
| ~ ssList(skaf46(nil,sk8)) ),
inference(component_clause,[status(thm)],[f16033]) ).
fof(f16097,plain,
( sQ1612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16035,f261]) ).
fof(f16098,plain,
sQ1612_spl,
inference(contradiction_clause,[status(thm)],[f16097]) ).
fof(f16100,plain,
( sQ1610_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16028,f262]) ).
fof(f16101,plain,
sQ1610_spl,
inference(contradiction_clause,[status(thm)],[f16100]) ).
fof(f16882,plain,
( ~ sQ1264_spl
| ~ sQ404_spl
| frontsegP(sk7,sk3)
| ~ ssList(tl(sk7)) ),
inference(paramodulation,[status(thm)],[f12451,f4083]) ).
fof(f16931,plain,
( ~ sQ1264_spl
| ~ sQ404_spl
| sQ1250_spl
| ~ sQ1381_spl ),
inference(split_clause,[status(thm)],[f16882,f13860,f12376,f4079,f12450]) ).
fof(f17068,definition,
( sQ1707_spl
<=> hd(sk7) = sk9 ),
introduced(definition,[new_symbols(definition,[sQ1707_spl])],[split_symbol_definition]) ).
fof(f17069,plain,
( ~ sQ1707_spl
| hd(sk7) = sk9 ),
inference(component_clause,[status(thm)],[f17068]) ).
fof(f17984,plain,
( ~ sQ1421_spl
| app(sk3,sk3) = sk3
| ~ ssList(sk3)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f14116,f2471]) ).
fof(f17994,plain,
( ~ sQ1421_spl
| sQ1435_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f17984,f717,f14350,f14115]) ).
fof(f18153,plain,
( ~ sQ1707_spl
| nil = sk7
| cons(sk9,tl(sk7)) = sk7
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f17069,f318]) ).
fof(f18155,plain,
( ~ sQ1707_spl
| sQ1171_spl
| sQ1264_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f18153,f1118,f12450,f11580,f17068]) ).
fof(f18755,plain,
( ~ sQ1553_spl
| app(sk7,sk3) = sk3
| ~ ssList(sk7)
| ~ ssList(sk3)
| ~ ssList(sk3)
| ~ frontsegP(sk7,sk3) ),
inference(resolution,[status(thm)],[f15361,f2340]) ).
fof(f18764,plain,
( ~ sQ1553_spl
| sQ1178_spl
| ~ sQ78_spl
| ~ sQ34_spl
| ~ sQ1250_spl ),
inference(split_clause,[status(thm)],[f18755,f12376,f717,f1118,f11609,f15360]) ).
fof(f18886,plain,
( ~ sQ1591_spl
| sk9 = hd(sk7)
| nil = sk7
| ~ ssList(sk7)
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f15906,f345]) ).
fof(f18889,plain,
( ~ sQ1591_spl
| sQ1707_spl
| sQ1171_spl
| ~ sQ78_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f18886,f717,f1118,f11580,f17068,f15905]) ).
fof(f18895,plain,
$false,
inference(sat_refutation,[status(thm)],[f489,f516,f582,f584,f607,f619,f623,f693,f695,f706,f866,f879,f892,f1121,f1124,f1201,f1214,f1218,f1854,f2006,f2039,f2041,f2047,f2168,f2251,f2253,f2259,f2361,f2363,f2759,f2850,f3141,f3143,f3164,f3197,f4082,f4375,f4473,f4646,f4762,f4835,f5186,f5333,f5961,f6937,f6988,f6991,f7242,f7308,f7310,f7314,f7434,f7436,f7454,f7598,f7891,f7981,f7983,f8828,f9670,f10484,f10486,f10496,f10498,f10508,f10510,f10520,f10522,f10560,f10562,f10885,f11000,f11268,f11388,f11390,f11505,f11523,f11533,f11640,f11683,f11797,f11936,f11938,f12421,f12446,f12850,f12852,f13867,f13964,f13970,f14118,f14150,f14154,f14413,f14722,f14805,f15052,f15395,f15554,f15908,f16098,f16101,f16931,f17994,f18155,f18764,f18889]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC165-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n013.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 07:59:54 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 142.02/18.36 % Refutation found
% 142.02/18.36 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 142.02/18.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 53.72/18.50 % Elapsed time: 18.107168 seconds
% 53.72/18.50 % CPU time: 143.097719 seconds
% 53.72/18.50 % Total memory used: 611.046 MB
% 53.72/18.50 % Net memory used: 562.248 MB
%------------------------------------------------------------------------------