%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC299-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 : n006.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 10.28s 1.80s
% Output : CNFRefutation 10.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 29
% Syntax : Number of formulae : 198 ( 30 unt; 0 def)
% Number of atoms : 681 ( 139 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 908 ( 425 ~; 483 |; 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 : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 107 ( 107 !; 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(f175,axiom,
! [U,V,W,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
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(f203,negated_conjecture,
( nil = sk4
| cons(sk10,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,negated_conjecture,
( nil = sk3
| ssList(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,negated_conjecture,
( nil = sk3
| ssList(sk12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,negated_conjecture,
( nil = sk3
| cons(sk10,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,negated_conjecture,
( nil = sk3
| app(app(sk11,sk3),sk12) = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f283,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f298,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f299,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f311,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f312,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f331,plain,
! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ) ),
inference(miniscoping,[status(thm)],[f114]) ).
fof(f332,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssItem(X0)
| ~ lt(X1,X0)
| ~ lt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f339,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f340,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f341,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f342,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f365,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f367,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(f368,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(f403,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(f404,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)],[f403]) ).
fof(f422,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(f423,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)],[f422]) ).
fof(f443,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f447,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f448,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f449,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f450,plain,
ssItem(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f451,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f452,plain,
ssList(sk8),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f453,plain,
ssList(sk9),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f454,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f455,plain,
lt(sk6,sk5),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f457,plain,
( nil = sk3
| ssItem(sk10) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f460,plain,
( nil = sk4
| cons(sk10,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f466,plain,
( nil = sk3
| ssList(sk11) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f467,plain,
( nil = sk3
| ssList(sk12) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f468,plain,
( nil = sk3
| cons(sk10,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f469,plain,
( nil = sk3
| app(app(sk11,sk3),sk12) = sk4 ),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f486,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f365]) ).
fof(f487,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f486]) ).
fof(f495,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)],[f423]) ).
fof(f508,plain,
( nil = sk1
| ssItem(sk10) ),
inference(forward_demodulation,[status(thm)],[f448,f457]) ).
fof(f511,plain,
( nil = sk4
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f448,f460]) ).
fof(f512,plain,
( nil = sk2
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f447,f511]) ).
fof(f518,plain,
( nil = sk1
| ssList(sk11) ),
inference(forward_demodulation,[status(thm)],[f448,f466]) ).
fof(f519,plain,
( nil = sk1
| ssList(sk12) ),
inference(forward_demodulation,[status(thm)],[f448,f467]) ).
fof(f520,plain,
( nil = sk3
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f448,f468]) ).
fof(f521,plain,
( nil = sk1
| cons(sk10,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f448,f520]) ).
fof(f522,plain,
( nil = sk3
| app(app(sk11,sk1),sk12) = sk4 ),
inference(forward_demodulation,[status(thm)],[f448,f469]) ).
fof(f523,plain,
( nil = sk3
| app(app(sk11,sk1),sk12) = sk2 ),
inference(forward_demodulation,[status(thm)],[f447,f522]) ).
fof(f524,plain,
( nil = sk1
| app(app(sk11,sk1),sk12) = sk2 ),
inference(forward_demodulation,[status(thm)],[f448,f523]) ).
fof(f548,plain,
! [X0] :
( nil = sk2
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ ssList(nil)
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f512,f404]) ).
fof(f549,plain,
! [X0] :
( nil = sk2
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f548,f220]) ).
fof(f554,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ ssList(nil)
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f521,f404]) ).
fof(f555,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f554,f220]) ).
fof(f1125,plain,
( ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ lt(sk5,sk6) ),
inference(resolution,[status(thm)],[f332,f455]) ).
fof(f1129,plain,
( ~ ssItem(sk6)
| ~ lt(sk5,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1125,f449]) ).
fof(f1139,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)],[f454,f340]) ).
fof(f1143,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)],[f1139,f453]) ).
fof(f1157,plain,
( nil = sk1
| memberP(sk1,sk10)
| ~ ssItem(sk10)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f521,f487]) ).
fof(f1159,plain,
( nil = sk1
| memberP(sk1,sk10)
| ~ ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1157,f220]) ).
fof(f1175,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)],[f342,f1143]) ).
fof(f1182,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)],[f1175,f298]) ).
fof(f1224,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| sk1 != nil
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil)) ),
inference(resolution,[status(thm)],[f1182,f312]) ).
fof(f1226,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| sk1 != nil
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1224,f299]) ).
fof(f1227,plain,
( ssList(sk12)
| ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(resolution,[status(thm)],[f1226,f519]) ).
fof(f1228,plain,
( ssList(sk11)
| ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(resolution,[status(thm)],[f1226,f518]) ).
fof(f1229,plain,
( ssItem(sk10)
| ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(resolution,[status(thm)],[f1226,f508]) ).
fof(f1233,plain,
( ssList(sk12)
| ~ ssList(nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1227,f450]) ).
fof(f1234,plain,
( ssList(sk11)
| ~ ssList(nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1228,f450]) ).
fof(f1235,plain,
( ssItem(sk10)
| ~ ssList(nil)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1229,f450]) ).
fof(f1239,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssList(sk12)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1233,f298]) ).
fof(f1240,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssList(sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f1239,f220]) ).
fof(f1241,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| ssList(sk12) ),
inference(resolution,[status(thm)],[f1240,f298]) ).
fof(f1242,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ssList(sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f1241,f452]) ).
fof(f1243,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ssList(sk12) ),
inference(resolution,[status(thm)],[f1242,f299]) ).
fof(f1244,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ssList(sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f1243,f451]) ).
fof(f1248,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssList(sk11)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1234,f298]) ).
fof(f1249,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssList(sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f1248,f220]) ).
fof(f1250,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssItem(sk10)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1235,f298]) ).
fof(f1251,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1250,f220]) ).
fof(f1261,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| ssList(sk11) ),
inference(resolution,[status(thm)],[f1249,f298]) ).
fof(f1262,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ssList(sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f1261,f452]) ).
fof(f1263,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1251,f298]) ).
fof(f1264,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1263,f452]) ).
fof(f1265,plain,
( ~ ssList(nil)
| ssList(sk12) ),
inference(resolution,[status(thm)],[f1244,f449]) ).
fof(f1273,plain,
ssList(sk12),
inference(forward_subsumption_resolution,[status(thm)],[f1265,f220]) ).
fof(f1285,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ssList(sk11) ),
inference(resolution,[status(thm)],[f1262,f299]) ).
fof(f1286,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ssList(sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f451]) ).
fof(f1287,plain,
( ~ ssList(nil)
| ssList(sk11) ),
inference(resolution,[status(thm)],[f1286,f449]) ).
fof(f1298,plain,
ssList(sk11),
inference(forward_subsumption_resolution,[status(thm)],[f1287,f220]) ).
fof(f1309,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1264,f299]) ).
fof(f1310,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ssItem(sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1309,f451]) ).
fof(f1311,plain,
( ~ ssList(nil)
| ssItem(sk10) ),
inference(resolution,[status(thm)],[f1310,f449]) ).
fof(f1320,plain,
( nil = sk1
| memberP(sk1,sk10) ),
inference(backward_subsumption_resolution,[status(thm)],[f1159,f1345]) ).
fof(f1343,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f555,f1345]) ).
fof(f1344,plain,
! [X0] :
( nil = sk2
| X0 = sk10
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f549,f1345]) ).
fof(f1345,plain,
ssItem(sk10),
inference(forward_subsumption_resolution,[status(thm)],[f1311,f220]) ).
fof(f1346,plain,
! [X0] :
( nil = sk1
| X0 = sk10
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1343,f283]) ).
fof(f1347,plain,
! [X0] :
( nil = sk2
| X0 = sk10
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1344,f283]) ).
fof(f1400,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)],[f454,f367]) ).
fof(f1401,plain,
! [X0] :
( nil = sk1
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk11,sk1))
| ~ ssList(sk12)
| ~ memberP(app(sk11,sk1),X0) ),
inference(paramodulation,[status(thm)],[f524,f367]) ).
fof(f1403,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)],[f1400,f453]) ).
fof(f1404,plain,
! [X0] :
( nil = sk1
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk11,sk1))
| ~ memberP(app(sk11,sk1),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1401,f1273]) ).
fof(f1453,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(sk11)
| ~ ssList(sk1)
| ~ memberP(sk1,X0)
| nil = sk1
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk11,sk1)) ),
inference(resolution,[status(thm)],[f1404,f368]) ).
fof(f1455,plain,
! [X0] :
( ~ ssList(sk11)
| ~ ssList(sk1)
| ~ memberP(sk1,X0)
| nil = sk1
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk11,sk1)) ),
inference(duplicate_literals_removal,[status(thm)],[f1453]) ).
fof(f1456,plain,
! [X0] :
( ~ ssList(sk11)
| ~ ssList(sk1)
| ~ memberP(sk1,X0)
| nil = sk1
| memberP(sk2,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1455,f298]) ).
fof(f1473,plain,
( nil = sk1
| ~ ssList(sk11)
| ~ ssList(sk1)
| nil = sk1
| memberP(sk2,sk10)
| ~ ssItem(sk10) ),
inference(resolution,[status(thm)],[f1456,f1320]) ).
fof(f1475,plain,
( ~ ssList(sk11)
| ~ ssList(sk1)
| nil = sk1
| memberP(sk2,sk10)
| ~ ssItem(sk10) ),
inference(duplicate_literals_removal,[status(thm)],[f1473]) ).
fof(f1476,plain,
( ~ ssList(sk11)
| ~ ssList(sk1)
| nil = sk1
| memberP(sk2,sk10) ),
inference(forward_subsumption_resolution,[status(thm)],[f1475,f1345]) ).
fof(f1546,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)],[f1403,f367]) ).
fof(f1549,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)],[f1546]) ).
fof(f1550,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)],[f1549,f298]) ).
fof(f1557,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)],[f1550,f367]) ).
fof(f1560,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)],[f1557]) ).
fof(f1561,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)],[f1560,f298]) ).
fof(f1573,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)],[f1561,f368]) ).
fof(f1575,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)],[f1573]) ).
fof(f1576,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)],[f1575,f452]) ).
fof(f1580,plain,
( memberP(sk1,sk6)
| ~ ssItem(sk6)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f495,f1403]) ).
fof(f1586,plain,
( memberP(sk1,sk6)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f1580]) ).
fof(f1587,plain,
( memberP(sk1,sk6)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1586,f220]) ).
fof(f1680,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(resolution,[status(thm)],[f1587,f298]) ).
fof(f1681,plain,
( ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(duplicate_literals_removal,[status(thm)],[f1680]) ).
fof(f1682,plain,
( ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1681,f450]) ).
fof(f1685,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6) ),
inference(resolution,[status(thm)],[f1682,f298]) ).
fof(f1686,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1685,f452]) ).
fof(f1699,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6) ),
inference(resolution,[status(thm)],[f1686,f298]) ).
fof(f1700,plain,
( ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1699,f451]) ).
fof(f1701,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6) ),
inference(resolution,[status(thm)],[f1700,f299]) ).
fof(f1702,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1701,f450]) ).
fof(f1703,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk1,sk6) ),
inference(resolution,[status(thm)],[f1702,f299]) ).
fof(f1704,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk1,sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1703]) ).
fof(f1705,plain,
( ~ ssItem(sk5)
| memberP(sk1,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1704,f220]) ).
fof(f1708,plain,
( nil = sk2
| sk6 = sk10
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1705,f1347]) ).
fof(f1709,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1705,f1346]) ).
fof(f1713,plain,
( nil = sk2
| sk6 = sk10
| ~ ssItem(sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1708,f449]) ).
fof(f1714,plain,
( nil = sk1
| sk6 = sk10
| ~ ssItem(sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1709,f449]) ).
fof(f1715,plain,
( nil = sk2
| sk6 = sk10 ),
inference(resolution,[status(thm)],[f1713,f450]) ).
fof(f1784,plain,
( nil = sk1
| sk6 = sk10 ),
inference(resolution,[status(thm)],[f1714,f450]) ).
fof(f1807,plain,
( nil = sk1
| ~ ssList(sk11)
| ~ ssList(sk1)
| nil = sk1
| memberP(sk2,sk6) ),
inference(paramodulation,[status(thm)],[f1784,f1476]) ).
fof(f1836,plain,
( ~ ssList(sk11)
| ~ ssList(sk1)
| nil = sk1
| memberP(sk2,sk6) ),
inference(duplicate_literals_removal,[status(thm)],[f1807]) ).
fof(f1837,plain,
( ~ ssList(sk11)
| nil = sk1
| memberP(sk2,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f1836,f443]) ).
fof(f2041,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)],[f1576,f298]) ).
fof(f2042,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)],[f2041]) ).
fof(f2043,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)],[f2042,f451]) ).
fof(f2046,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f2043,f487]) ).
fof(f2048,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f2046]) ).
fof(f2049,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(cons(sk6,nil))
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f2048,f449]) ).
fof(f2457,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f2049,f299]) ).
fof(f2460,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f2457]) ).
fof(f2461,plain,
( ~ ssItem(sk6)
| ~ ssList(cons(sk5,nil))
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f2460,f220]) ).
fof(f2479,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ ssItem(sk6)
| memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f2461,f299]) ).
fof(f2480,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| memberP(sk1,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f2479,f450]) ).
fof(f2485,plain,
( nil = sk2
| sk5 = sk10
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f2480,f1347]) ).
fof(f2496,plain,
( nil = sk2
| sk5 = sk10
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(duplicate_literals_removal,[status(thm)],[f2485]) ).
fof(f2497,plain,
( nil = sk2
| sk5 = sk10
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f2496,f449]) ).
fof(f2541,plain,
( nil = sk2
| sk5 = sk10 ),
inference(resolution,[status(thm)],[f2497,f220]) ).
fof(f2543,plain,
( nil = sk2
| nil = sk2
| sk5 = sk6 ),
inference(paramodulation,[status(thm)],[f1715,f2541]) ).
fof(f2585,plain,
( nil = sk2
| sk5 = sk6 ),
inference(duplicate_literals_removal,[status(thm)],[f2543]) ).
fof(f2668,plain,
( nil = sk2
| ~ ssItem(sk6)
| ~ lt(sk5,sk5) ),
inference(paramodulation,[status(thm)],[f2585,f1129]) ).
fof(f2674,plain,
( nil = sk2
| lt(sk5,sk5) ),
inference(paramodulation,[status(thm)],[f2585,f455]) ).
fof(f2702,plain,
( nil = sk2
| ~ lt(sk5,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f2668,f450]) ).
fof(f2726,plain,
( ~ ssList(sk11)
| nil = sk1
| memberP(nil,sk6) ),
inference(backward_demodulation,[status(thm)],[f2911,f1837]) ).
fof(f2911,plain,
nil = sk2,
inference(forward_subsumption_resolution,[status(thm)],[f2674,f2702]) ).
fof(f2912,plain,
( nil = sk1
| memberP(nil,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[f2726,f1298]) ).
fof(f2968,plain,
( ~ ssItem(sk6)
| nil = sk1 ),
inference(resolution,[status(thm)],[f2912,f283]) ).
fof(f3006,plain,
( ~ ssItem(sk5)
| memberP(nil,sk6) ),
inference(backward_demodulation,[status(thm)],[f3163,f1705]) ).
fof(f3163,plain,
nil = sk1,
inference(forward_subsumption_resolution,[status(thm)],[f2968,f450]) ).
fof(f3168,plain,
memberP(nil,sk6),
inference(forward_subsumption_resolution,[status(thm)],[f3006,f449]) ).
fof(f3218,plain,
~ ssItem(sk6),
inference(resolution,[status(thm)],[f3168,f283]) ).
fof(f3219,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3218,f450]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC299-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n006.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 08:13:12 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 10.28/1.80 % Refutation found
% 10.28/1.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.28/1.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.32/1.83 % Elapsed time: 1.472607 seconds
% 3.32/1.83 % CPU time: 11.291488 seconds
% 3.32/1.83 % Total memory used: 225.213 MB
% 3.32/1.83 % Net memory used: 216.829 MB
%------------------------------------------------------------------------------