%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC306-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:40:44 PM UTC 2026
% Result : Unsatisfiable 28.46s 9.38s
% Output : CNFRefutation 28.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 22
% Syntax : Number of formulae : 129 ( 22 unt; 0 def)
% Number of atoms : 480 ( 80 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 686 ( 335 ~; 351 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 90 ( 90 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(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(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [U,V] :
( ~ ssItem(V)
| ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
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(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| 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(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(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,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
lt(sk6,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
( nil = sk3
| ssItem(sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
( nil = sk3
| cons(sk10,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f212,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f275,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
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(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(f323,plain,
! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ) ),
inference(miniscoping,[status(thm)],[f114]) ).
fof(f324,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssItem(X0)
| ~ lt(X1,X0)
| ~ lt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
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(f357,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f359,plain,
! [X0,X1,X2] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f360,plain,
! [X0,X1,X2] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(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(f440,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f441,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f442,plain,
ssItem(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f443,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f444,plain,
ssList(sk8),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f445,plain,
ssList(sk9),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f446,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f447,plain,
lt(sk6,sk5),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f449,plain,
( nil = sk3
| ssItem(sk10) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f452,plain,
( nil = sk3
| cons(sk10,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f466,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f357]) ).
fof(f467,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f466]) ).
fof(f488,plain,
( nil = sk1
| ssItem(sk10) ),
inference(forward_demodulation,[status(thm)],[f440,f449]) ).
fof(f493,plain,
( nil = sk3
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f440,f452]) ).
fof(f494,plain,
( nil = sk1
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f440,f493]) ).
fof(f503,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ ssList(nil)
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f494,f396]) ).
fof(f505,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f503,f212]) ).
fof(f830,plain,
( ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ lt(sk5,sk6) ),
inference(resolution,[status(thm)],[f324,f447]) ).
fof(f833,plain,
( ~ ssItem(sk6)
| ~ lt(sk5,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f830,f441]) ).
fof(f931,plain,
! [X0] :
( memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(sk9)
| ~ memberP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0) ),
inference(paramodulation,[status(thm)],[f446,f359]) ).
fof(f932,plain,
! [X0] :
( memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ memberP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f931,f445]) ).
fof(f934,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
inference(resolution,[status(thm)],[f932,f359]) ).
fof(f935,plain,
! [X0] :
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
inference(duplicate_literals_removal,[status(thm)],[f934]) ).
fof(f936,plain,
! [X0] :
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f935,f290]) ).
fof(f938,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ memberP(app(sk7,cons(sk5,nil)),X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f936,f359]) ).
fof(f939,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ memberP(app(sk7,cons(sk5,nil)),X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f938]) ).
fof(f940,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ memberP(app(sk7,cons(sk5,nil)),X0)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f939,f290]) ).
fof(f962,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(sk9)
| sk1 != nil ),
inference(paramodulation,[status(thm)],[f446,f332]) ).
fof(f964,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| sk1 != nil ),
inference(forward_subsumption_resolution,[status(thm)],[f962,f445]) ).
fof(f982,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| sk1 != nil
| nil = cons(sk6,nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil)) ),
inference(resolution,[status(thm)],[f334,f964]) ).
fof(f986,plain,
( sk1 != nil
| nil = cons(sk6,nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f290]) ).
fof(f988,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| sk1 != nil
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil)) ),
inference(resolution,[status(thm)],[f986,f304]) ).
fof(f990,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| sk1 != nil
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f988,f291]) ).
fof(f991,plain,
( ssItem(sk10)
| ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(resolution,[status(thm)],[f990,f488]) ).
fof(f993,plain,
( ssItem(sk10)
| ~ ssList(nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f991,f442]) ).
fof(f995,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(resolution,[status(thm)],[f360,f940]) ).
fof(f997,plain,
! [X0] :
( memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(resolution,[status(thm)],[f360,f932]) ).
fof(f1000,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f995]) ).
fof(f1001,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1000,f443]) ).
fof(f1004,plain,
! [X0] :
( memberP(sk1,X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f997]) ).
fof(f1005,plain,
! [X0] :
( memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1004,f290]) ).
fof(f1025,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(resolution,[status(thm)],[f1005,f290]) ).
fof(f1026,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1025,f444]) ).
fof(f1027,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssItem(sk10)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f993,f290]) ).
fof(f1028,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1027,f212]) ).
fof(f1029,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1028,f290]) ).
fof(f1030,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1029,f444]) ).
fof(f1031,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1030,f291]) ).
fof(f1032,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1031,f443]) ).
fof(f1033,plain,
( ~ ssList(nil)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1032,f441]) ).
fof(f1062,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f505,f1063]) ).
fof(f1063,plain,
ssItem(sk10),
inference(forward_subsumption_resolution,[status(thm)],[f1033,f212]) ).
fof(f1065,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1062,f275]) ).
fof(f1183,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(resolution,[status(thm)],[f1026,f290]) ).
fof(f1184,plain,
! [X0] :
( ~ ssList(cons(sk5,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1183,f443]) ).
fof(f1192,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(resolution,[status(thm)],[f1001,f290]) ).
fof(f1193,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1192]) ).
fof(f1194,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1193,f444]) ).
fof(f1199,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6)
| ~ ssList(cons(sk6,nil)) ),
inference(resolution,[status(thm)],[f1184,f467]) ).
fof(f1201,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6)
| ~ ssList(cons(sk6,nil)) ),
inference(duplicate_literals_removal,[status(thm)],[f1199]) ).
fof(f1202,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1201,f291]) ).
fof(f1229,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk1,sk6)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f1202,f291]) ).
fof(f1230,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk1,sk6)
| ~ ssItem(sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1229]) ).
fof(f1231,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1230,f442]) ).
fof(f1232,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1231,f1065]) ).
fof(f1235,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f1232,f212]) ).
fof(f1237,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1235,f442]) ).
fof(f1243,plain,
( nil = sk1
| sk6 = sk10 ),
inference(forward_subsumption_resolution,[status(thm)],[f1237,f441]) ).
fof(f3525,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f1194,f467]) ).
fof(f3527,plain,
( ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5)
| ~ ssList(cons(sk5,nil)) ),
inference(duplicate_literals_removal,[status(thm)],[f3525]) ).
fof(f3528,plain,
( ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f3527,f291]) ).
fof(f3535,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(sk7)
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f3528,f291]) ).
fof(f3539,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(sk7)
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f3535]) ).
fof(f3540,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(sk7)
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f3539,f441]) ).
fof(f3546,plain,
( nil = sk1
| sk5 = sk10
| ~ ssItem(sk5)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f3540,f1065]) ).
fof(f3553,plain,
( nil = sk1
| sk5 = sk10
| ~ ssItem(sk5)
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f3546,f443]) ).
fof(f3616,plain,
( nil = sk1
| sk5 = sk10
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f3553,f442]) ).
fof(f3628,plain,
( nil = sk1
| sk5 = sk10
| ~ ssItem(sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f3616,f212]) ).
fof(f3630,plain,
( nil = sk1
| sk5 = sk10 ),
inference(resolution,[status(thm)],[f3628,f441]) ).
fof(f3637,plain,
( nil = sk1
| nil = sk1
| sk5 = sk6 ),
inference(paramodulation,[status(thm)],[f1243,f3630]) ).
fof(f3700,plain,
( nil = sk1
| sk5 = sk6 ),
inference(duplicate_literals_removal,[status(thm)],[f3637]) ).
fof(f3833,plain,
( nil = sk1
| ~ ssItem(sk6)
| ~ lt(sk5,sk5) ),
inference(paramodulation,[status(thm)],[f3700,f833]) ).
fof(f3840,plain,
( nil = sk1
| lt(sk5,sk5) ),
inference(paramodulation,[status(thm)],[f3700,f447]) ).
fof(f3883,plain,
( nil = sk1
| ~ lt(sk5,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f3833,f442]) ).
fof(f4048,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(nil,sk6) ),
inference(backward_demodulation,[status(thm)],[f4466,f1231]) ).
fof(f4466,plain,
nil = sk1,
inference(forward_subsumption_resolution,[status(thm)],[f3840,f3883]) ).
fof(f4521,plain,
( ~ ssItem(sk5)
| memberP(nil,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f4048,f212]) ).
fof(f4781,plain,
( ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f4521,f275]) ).
fof(f4783,plain,
~ ssItem(sk6),
inference(forward_subsumption_resolution,[status(thm)],[f4781,f441]) ).
fof(f4784,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f442,f4783]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC306-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.63 % Computer : n002.cluster.edu
% 0.14/5.63 % Model : x86_64 x86_64
% 0.14/5.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.63 % Memory : 8046.5625MB
% 0.14/5.63 % OS : Linux 6.8.0-71-generic
% 0.14/5.63 % CPULimit : 300
% 0.14/5.63 % WCLimit : 300
% 0.14/5.63 % DateTime : Mon Sep 21 08:16:38 UTC 2026
% 0.14/5.63 % CPUTime :
% 0.14/5.66 % Drodi V4.1.1
% 28.46/9.38 % Refutation found
% 28.46/9.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.46/9.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.54/9.42 % Elapsed time: 3.770130 seconds
% 7.54/9.42 % CPU time: 29.256885 seconds
% 7.54/9.42 % Total memory used: 319.405 MB
% 7.54/9.42 % Net memory used: 302.647 MB
%------------------------------------------------------------------------------