%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC184-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 : n009.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 8.79s 1.53s
% Output : CNFRefutation 8.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 92
% Number of leaves : 41
% Syntax : Number of formulae : 287 ( 40 unt; 0 def)
% Number of atoms : 912 ( 358 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1130 ( 505 ~; 625 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 233 ( 233 !; 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(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(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(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = 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(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(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(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [U,V] :
( app(V,skaf45(U,V)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [U,V] :
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(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(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(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(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(f178,axiom,
! [U,V,W,X] :
( frontsegP(cons(W,U),cons(X,V))
| ~ ssItem(W)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(V)
| W != X
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
ssList(sk3),
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(f198,negated_conjecture,
( nil = sk3
| ssItem(sk8) ),
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(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(f255,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f264,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f275,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
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(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(f301,plain,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
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(f311,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f316,plain,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
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(f346,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
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(f350,plain,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
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(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(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(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(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(f420,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(f437,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
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(f447,plain,
( nil = sk3
| ssItem(sk8) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f452,plain,
( nil = sk3
| cons(sk8,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f471,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f365]) ).
fof(f476,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)],[f420]) ).
fof(f477,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)],[f476]) ).
fof(f487,plain,
app(app(sk6,cons(sk5,nil)),sk7) = sk3,
inference(forward_demodulation,[status(thm)],[f440,f444]) ).
fof(f491,plain,
( nil = app(sk6,cons(sk5,nil))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f487,f332]) ).
fof(f492,plain,
( nil = app(sk6,cons(sk5,nil))
| ~ ssList(app(sk6,cons(sk5,nil)))
| sk3 != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f491,f443]) ).
fof(f516,plain,
! [X0] :
( nil = sk3
| app(sk3,X0) = cons(sk8,X0)
| ~ ssList(X0)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f452,f335]) ).
fof(f518,plain,
! [X0] :
( nil = sk3
| app(sk3,X0) = cons(sk8,X0)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f516,f447]) ).
fof(f522,plain,
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| nil = app(sk6,cons(sk5,nil))
| sk3 != nil ),
inference(resolution,[status(thm)],[f492,f290]) ).
fof(f523,plain,
( ~ ssList(cons(sk5,nil))
| nil = app(sk6,cons(sk5,nil))
| sk3 != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f522,f442]) ).
fof(f545,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)],[f487,f359]) ).
fof(f546,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f443]) ).
fof(f547,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(sk7,X0) ),
inference(paramodulation,[status(thm)],[f487,f360]) ).
fof(f548,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f547,f443]) ).
fof(f549,plain,
( sk3 = app(sk6,app(cons(sk5,nil),sk7))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f487,f373]) ).
fof(f551,plain,
( sk3 = app(sk6,app(cons(sk5,nil),sk7))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f549,f443]) ).
fof(f573,plain,
! [X0,X1] :
( nil = sk3
| sk8 = X0
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssItem(sk8)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(paramodulation,[status(thm)],[f452,f406]) ).
fof(f578,plain,
! [X0,X1] :
( nil = sk3
| sk8 = X0
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f447]) ).
fof(f582,plain,
! [X0,X1] :
( nil = sk3
| X1 = nil
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssItem(sk8)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(paramodulation,[status(thm)],[f452,f408]) ).
fof(f587,plain,
! [X0,X1] :
( nil = sk3
| X1 = nil
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f582,f447]) ).
fof(f605,plain,
! [X0,X1] :
( nil = sk3
| sk8 = X0
| ~ ssList(X1)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f212]) ).
fof(f625,plain,
! [X0,X1] :
( nil = sk3
| X1 = nil
| ~ ssList(X1)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f587,f212]) ).
fof(f635,plain,
( nil = cons(sk5,nil)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk5,nil))
| sk3 != nil ),
inference(resolution,[status(thm)],[f523,f334]) ).
fof(f637,plain,
( nil = cons(sk5,nil)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| sk3 != nil ),
inference(duplicate_literals_removal,[status(thm)],[f635]) ).
fof(f638,plain,
( nil = cons(sk5,nil)
| ~ ssList(cons(sk5,nil))
| sk3 != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f637,f442]) ).
fof(f667,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(resolution,[status(thm)],[f546,f359]) ).
fof(f672,plain,
! [X0] :
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(duplicate_literals_removal,[status(thm)],[f667]) ).
fof(f673,plain,
! [X0] :
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f290]) ).
fof(f675,plain,
! [X0] :
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(resolution,[status(thm)],[f548,f290]) ).
fof(f676,plain,
! [X0] :
( ~ ssList(cons(sk5,nil))
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f675,f442]) ).
fof(f677,plain,
( sk3 = app(sk6,app(cons(sk5,nil),sk7))
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f551,f442]) ).
fof(f686,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| nil = cons(sk5,nil)
| sk3 != nil ),
inference(resolution,[status(thm)],[f638,f291]) ).
fof(f687,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| sk3 != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f686,f304]) ).
fof(f688,plain,
( ~ ssList(nil)
| sk3 != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f687,f441]) ).
fof(f689,plain,
sk3 != nil,
inference(resolution,[status(thm)],[f688,f212]) ).
fof(f697,plain,
! [X0,X1] :
( X1 = nil
| ~ ssList(X1)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f625,f689]) ).
fof(f698,plain,
! [X0,X1] :
( sk8 = X0
| ~ ssList(X1)
| ~ ssItem(X0)
| sk3 != cons(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f605,f689]) ).
fof(f700,plain,
! [X0] :
( app(sk3,X0) = cons(sk8,X0)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f518,f689]) ).
fof(f702,plain,
cons(sk8,nil) = sk3,
inference(backward_subsumption_resolution,[status(thm)],[f452,f689]) ).
fof(f704,plain,
ssItem(sk8),
inference(backward_subsumption_resolution,[status(thm)],[f447,f689]) ).
fof(f720,plain,
! [X0] :
( cons(sk8,app(nil,X0)) = app(sk3,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f702,f388]) ).
fof(f725,plain,
! [X0] :
( X0 = sk8
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f702,f396]) ).
fof(f733,plain,
! [X0] :
( cons(sk8,app(nil,X0)) = app(sk3,X0)
| ~ ssList(X0)
| ~ ssItem(sk8) ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f212]) ).
fof(f738,plain,
! [X0] :
( X0 = sk8
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f725,f212]) ).
fof(f767,plain,
! [X0] :
( X0 = sk8
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f704]) ).
fof(f817,plain,
( hd(sk3) = sk8
| ~ ssList(nil)
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f702,f302]) ).
fof(f818,plain,
( hd(sk3) = sk8
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f704]) ).
fof(f819,plain,
hd(sk3) = sk8,
inference(forward_subsumption_resolution,[status(thm)],[f818,f212]) ).
fof(f833,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssItem(sk5)
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(resolution,[status(thm)],[f676,f291]) ).
fof(f834,plain,
! [X0] :
( ~ ssList(nil)
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f833,f441]) ).
fof(f835,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f834,f212]) ).
fof(f836,plain,
( memberP(sk6,sk5)
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f835,f445]) ).
fof(f837,plain,
( memberP(sk6,sk5)
| memberP(sk3,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f441]) ).
fof(f838,plain,
! [X0] :
( cons(sk8,app(nil,X0)) = app(sk3,X0)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f733,f704]) ).
fof(f885,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0)
| nil = cons(X0,X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f316,f406]) ).
fof(f887,plain,
( sk8 = skaf83(sk3)
| ~ ssList(skaf82(sk3))
| ~ ssItem(skaf83(sk3))
| nil = sk3
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f316,f698]) ).
fof(f892,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0)
| nil = cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f885,f291]) ).
fof(f893,plain,
( sk8 = skaf83(sk3)
| ~ ssList(skaf82(sk3))
| ~ ssItem(skaf83(sk3))
| nil = sk3 ),
inference(forward_subsumption_resolution,[status(thm)],[f887,f437]) ).
fof(f898,plain,
( sk8 = skaf83(sk3)
| ~ ssList(skaf82(sk3))
| ~ ssItem(skaf83(sk3)) ),
inference(forward_subsumption_resolution,[status(thm)],[f893,f689]) ).
fof(f899,plain,
( sk8 = skaf83(sk3)
| ~ ssList(skaf82(sk3)) ),
inference(resolution,[status(thm)],[f898,f216]) ).
fof(f901,plain,
sk8 = skaf83(sk3),
inference(forward_subsumption_resolution,[status(thm)],[f899,f217]) ).
fof(f904,plain,
( nil = sk3
| cons(sk8,skaf82(sk3)) = sk3
| ~ ssList(sk3) ),
inference(paramodulation,[status(thm)],[f901,f316]) ).
fof(f906,plain,
( nil = sk3
| cons(sk8,skaf82(sk3)) = sk3 ),
inference(forward_subsumption_resolution,[status(thm)],[f904,f437]) ).
fof(f908,plain,
cons(sk8,skaf82(sk3)) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[f906,f689]) ).
fof(f910,plain,
( skaf82(sk3) = nil
| ~ ssList(skaf82(sk3))
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f908,f697]) ).
fof(f927,plain,
( skaf82(sk3) = nil
| ~ ssList(skaf82(sk3)) ),
inference(forward_subsumption_resolution,[status(thm)],[f910,f704]) ).
fof(f940,plain,
skaf82(sk3) = nil,
inference(forward_subsumption_resolution,[status(thm)],[f927,f217]) ).
fof(f1022,plain,
! [X0] :
( ~ ssList(cons(sk5,nil))
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f442]) ).
fof(f1023,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1022,f291]) ).
fof(f1024,plain,
! [X0] :
( ~ ssList(nil)
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1023,f441]) ).
fof(f1025,plain,
! [X0] :
( ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1024,f212]) ).
fof(f1026,plain,
( memberP(sk3,sk5)
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1025,f837]) ).
fof(f1027,plain,
( memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f1026]) ).
fof(f1028,plain,
memberP(sk3,sk5),
inference(forward_subsumption_resolution,[status(thm)],[f1027,f441]) ).
fof(f1052,plain,
( sk5 = sk8
| memberP(nil,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1028,f767]) ).
fof(f1053,plain,
( sk5 = sk8
| memberP(nil,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f1052,f441]) ).
fof(f1054,plain,
( ~ ssItem(sk5)
| sk5 = sk8 ),
inference(resolution,[status(thm)],[f1053,f275]) ).
fof(f1055,plain,
sk5 = sk8,
inference(forward_subsumption_resolution,[status(thm)],[f1054,f441]) ).
fof(f1061,plain,
( sk3 = app(sk6,app(cons(sk8,nil),sk7))
| ~ ssList(cons(sk5,nil)) ),
inference(backward_demodulation,[status(thm)],[f1055,f677]) ).
fof(f1065,plain,
( memberP(sk7,sk8)
| memberP(sk6,sk5) ),
inference(backward_demodulation,[status(thm)],[f1055,f445]) ).
fof(f1079,plain,
( sk3 = app(sk6,app(cons(sk8,nil),sk7))
| ~ ssList(cons(sk8,nil)) ),
inference(forward_demodulation,[status(thm)],[f1055,f1061]) ).
fof(f1080,plain,
( sk3 = app(sk6,app(cons(sk8,nil),sk7))
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f702,f1079]) ).
fof(f1081,plain,
( sk3 = app(sk6,app(sk3,sk7))
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f702,f1080]) ).
fof(f1082,plain,
sk3 = app(sk6,app(sk3,sk7)),
inference(forward_subsumption_resolution,[status(thm)],[f1081,f437]) ).
fof(f1092,plain,
( memberP(sk7,sk8)
| memberP(sk6,sk8) ),
inference(forward_demodulation,[status(thm)],[f1055,f1065]) ).
fof(f1094,plain,
( hd(sk3) = hd(sk6)
| nil = sk6
| ~ ssList(sk6)
| ~ ssList(app(sk3,sk7)) ),
inference(paramodulation,[status(thm)],[f1082,f338]) ).
fof(f1106,plain,
( sk8 = hd(sk6)
| nil = sk6
| ~ ssList(sk6)
| ~ ssList(app(sk3,sk7)) ),
inference(forward_demodulation,[status(thm)],[f819,f1094]) ).
fof(f1107,plain,
( sk8 = hd(sk6)
| nil = sk6
| ~ ssList(app(sk3,sk7)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1106,f442]) ).
fof(f1151,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(f1155,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)],[f1151]) ).
fof(f1156,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1155,f290]) ).
fof(f1172,plain,
( ~ ssList(sk3)
| ~ ssList(sk7)
| sk8 = hd(sk6)
| nil = sk6 ),
inference(resolution,[status(thm)],[f1107,f290]) ).
fof(f1173,plain,
( ~ ssList(sk3)
| sk8 = hd(sk6)
| nil = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1172,f443]) ).
fof(f1174,plain,
( sk8 = hd(sk6)
| nil = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1173,f437]) ).
fof(f1175,plain,
( nil = sk6
| nil = sk6
| cons(sk8,tl(sk6)) = sk6
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1174,f311]) ).
fof(f1177,plain,
( nil = sk6
| cons(sk8,tl(sk6)) = sk6
| ~ ssList(sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1175]) ).
fof(f1178,plain,
( nil = sk6
| cons(sk8,tl(sk6)) = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1177,f442]) ).
fof(f1187,plain,
( nil = sk6
| tl(sk6) = nil
| ~ ssList(tl(sk6))
| ~ ssItem(sk8)
| sk3 != sk6 ),
inference(paramodulation,[status(thm)],[f1178,f697]) ).
fof(f1204,plain,
( nil = sk6
| tl(sk6) = nil
| ~ ssList(tl(sk6))
| sk3 != sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1187,f704]) ).
fof(f1219,plain,
( nil = sk6
| ~ ssList(sk6)
| nil = sk6
| tl(sk6) = nil
| sk3 != sk6 ),
inference(resolution,[status(thm)],[f1204,f280]) ).
fof(f1220,plain,
( ~ ssList(sk6)
| nil = sk6
| tl(sk6) = nil
| sk3 != sk6 ),
inference(duplicate_literals_removal,[status(thm)],[f1219]) ).
fof(f1221,plain,
( nil = sk6
| tl(sk6) = nil
| sk3 != sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1220,f442]) ).
fof(f1267,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f471,f290]) ).
fof(f1269,plain,
( frontsegP(sk3,sk6)
| ~ ssList(sk6)
| ~ ssList(app(sk3,sk7)) ),
inference(paramodulation,[status(thm)],[f1082,f1267]) ).
fof(f1273,plain,
( frontsegP(sk3,sk6)
| ~ ssList(app(sk3,sk7)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1269,f442]) ).
fof(f1275,plain,
( ~ ssList(sk3)
| ~ ssList(sk7)
| frontsegP(sk3,sk6) ),
inference(resolution,[status(thm)],[f1273,f290]) ).
fof(f1276,plain,
( ~ ssList(sk3)
| frontsegP(sk3,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1275,f443]) ).
fof(f1277,plain,
frontsegP(sk3,sk6),
inference(forward_subsumption_resolution,[status(thm)],[f1276,f437]) ).
fof(f1278,plain,
( sk3 = sk6
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ frontsegP(sk6,sk3) ),
inference(resolution,[status(thm)],[f1277,f346]) ).
fof(f1279,plain,
( sk3 = sk6
| ~ ssList(sk3)
| ~ frontsegP(sk6,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1278,f442]) ).
fof(f1298,plain,
( sk3 = sk6
| ~ frontsegP(sk6,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1279,f437]) ).
fof(f1771,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f892,f304]) ).
fof(f1772,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1771,f216]) ).
fof(f1776,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1772,f217]) ).
fof(f1786,plain,
( nil = sk6
| skaf83(sk6) = sk8
| ~ ssList(tl(sk6))
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f1178,f1776]) ).
fof(f1788,plain,
( nil = sk6
| skaf83(sk6) = sk8
| ~ ssList(tl(sk6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1786,f704]) ).
fof(f1789,plain,
( nil = sk6
| ~ ssList(sk6)
| nil = sk6
| skaf83(sk6) = sk8 ),
inference(resolution,[status(thm)],[f1788,f280]) ).
fof(f1790,plain,
( ~ ssList(sk6)
| nil = sk6
| skaf83(sk6) = sk8 ),
inference(duplicate_literals_removal,[status(thm)],[f1789]) ).
fof(f1791,plain,
( nil = sk6
| skaf83(sk6) = sk8 ),
inference(forward_subsumption_resolution,[status(thm)],[f1790,f442]) ).
fof(f1792,plain,
( nil = sk6
| nil = sk6
| cons(sk8,skaf82(sk6)) = sk6
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1791,f316]) ).
fof(f1794,plain,
( nil = sk6
| cons(sk8,skaf82(sk6)) = sk6
| ~ ssList(sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1792]) ).
fof(f1795,plain,
( nil = sk6
| cons(sk8,skaf82(sk6)) = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1794,f442]) ).
fof(f1807,plain,
( nil = sk6
| tl(sk6) = skaf82(sk6)
| ~ ssList(skaf82(sk6))
| ~ ssItem(sk8) ),
inference(paramodulation,[status(thm)],[f1795,f301]) ).
fof(f1830,plain,
( nil = sk6
| tl(sk6) = skaf82(sk6)
| ~ ssList(skaf82(sk6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1807,f704]) ).
fof(f1845,plain,
( nil = sk6
| tl(sk6) = skaf82(sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1830,f217]) ).
fof(f1848,plain,
( nil = sk6
| nil = sk6
| cons(skaf83(sk6),tl(sk6)) = sk6
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1845,f316]) ).
fof(f1849,plain,
( nil = sk6
| ssList(tl(sk6)) ),
inference(paramodulation,[status(thm)],[f1845,f217]) ).
fof(f1852,plain,
( nil = sk6
| cons(skaf83(sk6),tl(sk6)) = sk6
| ~ ssList(sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1848]) ).
fof(f1853,plain,
( nil = sk6
| cons(skaf83(sk6),tl(sk6)) = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1852,f442]) ).
fof(f1871,plain,
( nil = sk6
| hd(sk6) = skaf83(sk6)
| ~ ssList(tl(sk6))
| ~ ssItem(skaf83(sk6)) ),
inference(paramodulation,[status(thm)],[f1853,f302]) ).
fof(f1896,plain,
( nil = sk6
| hd(sk6) = skaf83(sk6)
| ~ ssList(tl(sk6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1871,f216]) ).
fof(f1906,plain,
( nil = sk6
| hd(sk6) = skaf83(sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1896,f1849]) ).
fof(f1910,plain,
( nil = sk6
| nil = sk6
| cons(hd(sk6),skaf82(sk6)) = sk6
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1906,f316]) ).
fof(f1911,plain,
( nil = sk6
| ssItem(hd(sk6)) ),
inference(paramodulation,[status(thm)],[f1906,f216]) ).
fof(f1915,plain,
( nil = sk6
| cons(hd(sk6),skaf82(sk6)) = sk6
| ~ ssList(sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1910]) ).
fof(f1916,plain,
( nil = sk6
| cons(hd(sk6),skaf82(sk6)) = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1915,f442]) ).
fof(f2408,plain,
! [X0] :
( frontsegP(cons(sk8,X0),sk3)
| ~ ssItem(sk8)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X0,nil) ),
inference(paramodulation,[status(thm)],[f702,f477]) ).
fof(f2422,plain,
! [X0] :
( frontsegP(cons(sk8,X0),sk3)
| ~ ssItem(sk8)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f2408,f264]) ).
fof(f2423,plain,
! [X0] :
( frontsegP(cons(sk8,X0),sk3)
| ~ ssItem(sk8)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2422,f212]) ).
fof(f2426,plain,
( nil = sk6
| frontsegP(sk6,sk3)
| ~ ssItem(sk8)
| ~ ssList(skaf82(sk6)) ),
inference(paramodulation,[status(thm)],[f1795,f2423]) ).
fof(f2431,plain,
( nil = sk6
| frontsegP(sk6,sk3)
| ~ ssItem(sk8) ),
inference(forward_subsumption_resolution,[status(thm)],[f2426,f217]) ).
fof(f2437,plain,
( nil = sk6
| frontsegP(sk6,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[f2431,f704]) ).
fof(f2438,plain,
( sk3 = sk6
| nil = sk6 ),
inference(resolution,[status(thm)],[f2437,f1298]) ).
fof(f2454,plain,
( nil = sk6
| tl(sk6) = nil ),
inference(backward_subsumption_resolution,[status(thm)],[f1221,f2438]) ).
fof(f2468,plain,
( nil = sk6
| nil = sk6
| cons(hd(sk6),skaf82(sk3)) = sk6 ),
inference(paramodulation,[status(thm)],[f2438,f1916]) ).
fof(f2517,plain,
( nil = sk6
| nil = sk6
| cons(hd(sk6),nil) = sk6 ),
inference(forward_demodulation,[status(thm)],[f940,f2468]) ).
fof(f2518,plain,
( nil = sk6
| cons(hd(sk6),nil) = sk6 ),
inference(duplicate_literals_removal,[status(thm)],[f2517]) ).
fof(f2595,plain,
! [X0] :
( nil = sk6
| app(sk6,X0) = cons(hd(sk6),X0)
| ~ ssList(X0)
| ~ ssItem(hd(sk6)) ),
inference(paramodulation,[status(thm)],[f2518,f335]) ).
fof(f2641,plain,
! [X0] :
( nil = sk6
| app(sk6,X0) = cons(hd(sk6),X0)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2595,f1911]) ).
fof(f3055,plain,
( nil = sk6
| nil = sk6
| app(sk6,nil) = sk6
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f2518,f2641]) ).
fof(f3060,plain,
( nil = sk6
| app(sk6,nil) = sk6
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f3055]) ).
fof(f3061,plain,
( nil = sk6
| app(sk6,nil) = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f3060,f212]) ).
fof(f3084,plain,
( nil = sk6
| tl(sk6) = app(tl(sk6),nil)
| nil = sk6
| ~ ssList(sk6)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f3061,f350]) ).
fof(f3102,plain,
( tl(sk6) = app(tl(sk6),nil)
| nil = sk6
| ~ ssList(sk6)
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f3084]) ).
fof(f3103,plain,
( tl(sk6) = app(tl(sk6),nil)
| nil = sk6
| ~ ssList(sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f3102,f212]) ).
fof(f3330,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)],[f1156,f1267]) ).
fof(f3331,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f3330,f255]) ).
fof(f3409,plain,
( nil = sk6
| skaf45(sk6,sk6) = nil
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f3061,f3331]) ).
fof(f3410,plain,
( skaf45(sk3,sk6) = app(sk3,sk7)
| ~ ssList(app(sk3,sk7))
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1082,f3331]) ).
fof(f3419,plain,
( nil = sk6
| skaf45(sk6,sk6) = nil
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f3409,f442]) ).
fof(f3420,plain,
( skaf45(sk3,sk6) = app(sk3,sk7)
| ~ ssList(app(sk3,sk7)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3410,f442]) ).
fof(f3450,plain,
( nil = sk6
| skaf45(sk6,sk6) = nil ),
inference(forward_subsumption_resolution,[status(thm)],[f3419,f212]) ).
fof(f3451,plain,
( nil = sk6
| nil = sk6
| skaf45(sk3,sk6) = nil ),
inference(paramodulation,[status(thm)],[f2438,f3450]) ).
fof(f3455,plain,
( nil = sk6
| skaf45(sk3,sk6) = nil ),
inference(duplicate_literals_removal,[status(thm)],[f3451]) ).
fof(f3912,plain,
( tl(sk6) = app(tl(sk6),nil)
| nil = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f3103,f442]) ).
fof(f3913,plain,
( nil = sk6
| tl(sk6) = app(nil,nil)
| nil = sk6 ),
inference(paramodulation,[status(thm)],[f2454,f3912]) ).
fof(f3947,plain,
( tl(sk6) = app(nil,nil)
| nil = sk6 ),
inference(duplicate_literals_removal,[status(thm)],[f3913]) ).
fof(f3964,plain,
( nil = sk6
| cons(sk8,tl(sk6)) = app(sk3,nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f3947,f838]) ).
fof(f3998,plain,
( nil = sk6
| cons(sk8,tl(sk6)) = app(sk3,nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f3964,f212]) ).
fof(f4303,plain,
( nil = sk6
| ~ ssList(tl(sk6))
| ~ ssItem(sk8)
| app(sk3,nil) != nil ),
inference(paramodulation,[status(thm)],[f3998,f304]) ).
fof(f4348,plain,
( nil = sk6
| ~ ssList(tl(sk6))
| app(sk3,nil) != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f4303,f704]) ).
fof(f4454,plain,
( nil = sk6
| app(sk3,nil) != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f4348,f1849]) ).
fof(f5181,plain,
( nil = sk6
| nil = app(sk3,sk7)
| ~ ssList(app(sk3,sk7)) ),
inference(paramodulation,[status(thm)],[f3455,f3420]) ).
fof(f5345,plain,
( ~ ssList(sk3)
| ~ ssList(sk7)
| nil = sk6
| nil = app(sk3,sk7) ),
inference(resolution,[status(thm)],[f5181,f290]) ).
fof(f5346,plain,
( ~ ssList(sk3)
| nil = sk6
| nil = app(sk3,sk7) ),
inference(forward_subsumption_resolution,[status(thm)],[f5345,f443]) ).
fof(f5477,plain,
( nil = sk6
| nil = app(sk3,sk7) ),
inference(forward_subsumption_resolution,[status(thm)],[f5346,f437]) ).
fof(f5478,plain,
( nil = sk7
| ~ ssList(sk3)
| ~ ssList(sk7)
| nil = sk6 ),
inference(resolution,[status(thm)],[f5477,f334]) ).
fof(f5520,plain,
( nil = sk7
| ~ ssList(sk3)
| nil = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f5478,f443]) ).
fof(f5558,plain,
( nil = sk7
| nil = sk6 ),
inference(forward_subsumption_resolution,[status(thm)],[f5520,f437]) ).
fof(f5559,plain,
( nil = sk6
| nil = sk6
| nil = app(sk3,nil) ),
inference(paramodulation,[status(thm)],[f5558,f5477]) ).
fof(f5584,plain,
( nil = sk6
| nil = app(sk3,nil) ),
inference(duplicate_literals_removal,[status(thm)],[f5559]) ).
fof(f5585,plain,
nil = sk6,
inference(forward_subsumption_resolution,[status(thm)],[f5584,f4454]) ).
fof(f5723,plain,
( memberP(sk7,sk8)
| memberP(nil,sk8) ),
inference(backward_demodulation,[status(thm)],[f5585,f1092]) ).
fof(f5724,plain,
sk3 = app(nil,app(sk3,sk7)),
inference(backward_demodulation,[status(thm)],[f5585,f1082]) ).
fof(f5940,plain,
( sk3 = app(sk3,sk7)
| ~ ssList(app(sk3,sk7)) ),
inference(paramodulation,[status(thm)],[f5724,f279]) ).
fof(f6008,plain,
( ~ ssList(sk3)
| ~ ssList(sk7)
| sk3 = app(sk3,sk7) ),
inference(resolution,[status(thm)],[f5940,f290]) ).
fof(f6009,plain,
( ~ ssList(sk3)
| sk3 = app(sk3,sk7) ),
inference(forward_subsumption_resolution,[status(thm)],[f6008,f443]) ).
fof(f6013,plain,
sk3 = app(sk3,sk7),
inference(forward_subsumption_resolution,[status(thm)],[f6009,f437]) ).
fof(f6015,plain,
( sk3 = cons(sk8,sk7)
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f6013,f700]) ).
fof(f6048,plain,
sk3 = cons(sk8,sk7),
inference(forward_subsumption_resolution,[status(thm)],[f6015,f443]) ).
fof(f6121,plain,
( sk7 = nil
| ~ ssList(sk7)
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f6048,f697]) ).
fof(f6181,plain,
( sk7 = nil
| ~ ssList(sk7) ),
inference(forward_subsumption_resolution,[status(thm)],[f6121,f704]) ).
fof(f6240,plain,
( memberP(nil,sk8)
| memberP(nil,sk8) ),
inference(backward_demodulation,[status(thm)],[f6253,f5723]) ).
fof(f6253,plain,
sk7 = nil,
inference(forward_subsumption_resolution,[status(thm)],[f6181,f443]) ).
fof(f6254,plain,
memberP(nil,sk8),
inference(duplicate_literals_removal,[status(thm)],[f6240]) ).
fof(f6260,plain,
~ ssItem(sk8),
inference(resolution,[status(thm)],[f6254,f275]) ).
fof(f6261,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6260,f704]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC184-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:02:43 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 8.79/1.53 % Refutation found
% 8.79/1.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 8.79/1.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.79/1.57 % Elapsed time: 1.200442 seconds
% 8.79/1.57 % CPU time: 9.188561 seconds
% 8.79/1.57 % Total memory used: 217.741 MB
% 8.79/1.57 % Net memory used: 210.033 MB
%------------------------------------------------------------------------------