%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC298-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 : n020.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:42 PM UTC 2026
% Result : Unsatisfiable 30.41s 9.30s
% Output : CNFRefutation 30.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 22
% Syntax : Number of formulae : 131 ( 22 unt; 0 def)
% Number of atoms : 478 ( 78 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 679 ( 332 ~; 347 |; 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ 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(f114,axiom,
! [U,V] :
( ~ ssItem(V)
| ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [U,V,W] :
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W] :
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(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,
ssItem(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,
ssList(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
lt(sk6,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
( nil = sk3
| ssItem(sk10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,negated_conjecture,
( nil = sk3
| cons(sk10,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f214,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f277,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f292,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f293,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f305,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f306,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f325,plain,
! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ) ),
inference(miniscoping,[status(thm)],[f114]) ).
fof(f326,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssItem(X0)
| ~ lt(X1,X0)
| ~ lt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f333,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f334,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f335,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f336,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f359,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f361,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(f362,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(f397,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(f398,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)],[f397]) ).
fof(f442,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f443,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f444,plain,
ssItem(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f445,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f446,plain,
ssList(sk8),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f447,plain,
ssList(sk9),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f448,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f449,plain,
lt(sk6,sk5),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f451,plain,
( nil = sk3
| ssItem(sk10) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f456,plain,
( nil = sk3
| cons(sk10,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f472,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f359]) ).
fof(f473,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f472]) ).
fof(f494,plain,
( nil = sk1
| ssItem(sk10) ),
inference(forward_demodulation,[status(thm)],[f442,f451]) ).
fof(f501,plain,
( nil = sk3
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f456]) ).
fof(f502,plain,
( nil = sk1
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f501]) ).
fof(f520,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ ssList(nil)
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f502,f398]) ).
fof(f522,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f214]) ).
fof(f834,plain,
( ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ lt(sk5,sk6) ),
inference(resolution,[status(thm)],[f326,f449]) ).
fof(f837,plain,
( ~ ssItem(sk6)
| ~ lt(sk5,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f834,f443]) ).
fof(f965,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)],[f448,f334]) ).
fof(f967,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)],[f965,f447]) ).
fof(f985,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)],[f336,f967]) ).
fof(f989,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)],[f985,f292]) ).
fof(f991,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| sk1 != nil
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil)) ),
inference(resolution,[status(thm)],[f989,f306]) ).
fof(f993,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| sk1 != nil
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f991,f293]) ).
fof(f994,plain,
( ssItem(sk10)
| ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(resolution,[status(thm)],[f993,f494]) ).
fof(f996,plain,
( ssItem(sk10)
| ~ ssList(nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f994,f444]) ).
fof(f1001,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssItem(sk10)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f996,f292]) ).
fof(f1002,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1001,f214]) ).
fof(f1010,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)],[f448,f361]) ).
fof(f1011,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)],[f1010,f447]) ).
fof(f1024,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
inference(resolution,[status(thm)],[f1011,f362]) ).
fof(f1025,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)],[f1011,f361]) ).
fof(f1026,plain,
! [X0] :
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
inference(duplicate_literals_removal,[status(thm)],[f1024]) ).
fof(f1027,plain,
! [X0] :
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1026,f292]) ).
fof(f1028,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)],[f1025]) ).
fof(f1029,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)],[f1028,f292]) ).
fof(f1031,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1027,f292]) ).
fof(f1032,plain,
! [X0] :
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1031,f446]) ).
fof(f1035,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)],[f1029,f361]) ).
fof(f1038,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)],[f1035]) ).
fof(f1039,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)],[f1038,f292]) ).
fof(f1040,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1002,f292]) ).
fof(f1041,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1040,f446]) ).
fof(f1042,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1041,f293]) ).
fof(f1043,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1042,f445]) ).
fof(f1044,plain,
( ~ ssList(nil)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1043,f443]) ).
fof(f1075,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f522,f1076]) ).
fof(f1076,plain,
ssItem(sk10),
inference(forward_subsumption_resolution,[status(thm)],[f1044,f214]) ).
fof(f1078,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1075,f277]) ).
fof(f1197,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1032,f292]) ).
fof(f1198,plain,
! [X0] :
( ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1197,f445]) ).
fof(f1202,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1039,f362]) ).
fof(f1204,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1202]) ).
fof(f1205,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1204,f446]) ).
fof(f1212,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f1198,f473]) ).
fof(f1214,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1212]) ).
fof(f1215,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1214,f444]) ).
fof(f1218,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1205,f292]) ).
fof(f1219,plain,
! [X0] :
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1218]) ).
fof(f1220,plain,
! [X0] :
( ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1219,f445]) ).
fof(f1226,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6) ),
inference(resolution,[status(thm)],[f1215,f293]) ).
fof(f1227,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1226]) ).
fof(f1228,plain,
( ~ ssItem(sk6)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1227,f214]) ).
fof(f1232,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssItem(sk6)
| memberP(sk1,sk6) ),
inference(resolution,[status(thm)],[f1228,f293]) ).
fof(f1233,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1232,f444]) ).
fof(f1234,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1233,f1078]) ).
fof(f1237,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f1234,f443]) ).
fof(f1248,plain,
( nil = sk1
| sk6 = sk10
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1237,f444]) ).
fof(f1254,plain,
( nil = sk1
| sk6 = sk10 ),
inference(forward_subsumption_resolution,[status(thm)],[f1248,f214]) ).
fof(f3183,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1220,f473]) ).
fof(f3185,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f3183]) ).
fof(f3186,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f3185,f443]) ).
fof(f4180,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f3186,f293]) ).
fof(f4184,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f4180]) ).
fof(f4185,plain,
( ~ ssItem(sk6)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f4184,f214]) ).
fof(f4205,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssItem(sk6)
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f4185,f293]) ).
fof(f4206,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f4205,f444]) ).
fof(f4209,plain,
( nil = sk1
| sk5 = sk10
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f4206,f1078]) ).
fof(f4216,plain,
( nil = sk1
| sk5 = sk10
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f4209]) ).
fof(f4217,plain,
( nil = sk1
| sk5 = sk10
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f4216,f443]) ).
fof(f4246,plain,
( nil = sk1
| sk5 = sk10 ),
inference(resolution,[status(thm)],[f4217,f214]) ).
fof(f4248,plain,
( nil = sk1
| nil = sk1
| sk5 = sk6 ),
inference(paramodulation,[status(thm)],[f1254,f4246]) ).
fof(f4311,plain,
( nil = sk1
| sk5 = sk6 ),
inference(duplicate_literals_removal,[status(thm)],[f4248]) ).
fof(f4465,plain,
( nil = sk1
| ~ ssItem(sk6)
| ~ lt(sk5,sk5) ),
inference(paramodulation,[status(thm)],[f4311,f837]) ).
fof(f4472,plain,
( nil = sk1
| lt(sk5,sk5) ),
inference(paramodulation,[status(thm)],[f4311,f449]) ).
fof(f4547,plain,
( nil = sk1
| ~ lt(sk5,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f4465,f444]) ).
fof(f4554,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f5220,f4206]) ).
fof(f5220,plain,
nil = sk1,
inference(forward_subsumption_resolution,[status(thm)],[f4472,f4547]) ).
fof(f5221,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f4554,f277]) ).
fof(f5660,plain,
~ ssList(nil),
inference(resolution,[status(thm)],[f5221,f443]) ).
fof(f5664,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5660,f214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC298-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/5.34 % Computer : n020.cluster.edu
% 0.09/5.34 % Model : x86_64 x86_64
% 0.09/5.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.34 % Memory : 8046.5625MB
% 0.09/5.34 % OS : Linux 6.8.0-71-generic
% 0.09/5.34 % CPULimit : 300
% 0.09/5.34 % WCLimit : 300
% 0.09/5.34 % DateTime : Mon Sep 21 08:13:53 UTC 2026
% 0.09/5.34 % CPUTime :
% 0.09/5.36 % Drodi V4.1.1
% 30.41/9.30 % Refutation found
% 30.41/9.30 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 30.41/9.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 30.41/9.36 % Elapsed time: 4.005826 seconds
% 30.41/9.36 % CPU time: 31.525279 seconds
% 30.41/9.36 % Total memory used: 363.269 MB
% 30.41/9.36 % Net memory used: 342.113 MB
%------------------------------------------------------------------------------