%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC155-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 : n026.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:11 PM UTC 2026
% Result : Unsatisfiable 0.23s 0.59s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 49
% Syntax : Number of formulae : 165 ( 26 unt; 28 def)
% Number of atoms : 509 ( 27 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 655 ( 311 ~; 316 |; 0 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 29 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 87 ( 87 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
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(f130,axiom,
! [U,V] :
( V = U
| ~ ssItem(V)
| ~ ssItem(U)
| ~ leq(V,U)
| ~ leq(U,V) ),
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(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(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
! [A,B,C,D] :
( ~ memberP(C,D)
| leq(A,D)
| ~ ssItem(D)
| app(app(B,cons(A,nil)),C) != sk3
| ~ ssList(C)
| ~ ssList(B)
| ~ ssItem(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
! [A,B,C,D] :
( ~ memberP(B,D)
| leq(D,A)
| ~ ssItem(D)
| app(app(B,cons(A,nil)),C) != sk3
| ~ ssList(C)
| ~ ssList(B)
| ~ ssItem(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
leq(sk6,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
( ~ leq(sk5,sk6)
| ssItem(sk10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( ~ leq(sk5,sk6)
| memberP(sk8,sk10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
( ~ leq(sk5,sk6)
| ~ leq(sk10,sk6)
| ~ leq(sk5,sk10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f289,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f290,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f346,plain,
! [X0,X1] :
( X1 = X0
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f356,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f358,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(f359,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(f372,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(f439,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f440,plain,
! [C,D] :
( ~ memberP(C,D)
| ! [A] :
( leq(A,D)
| ~ ssItem(D)
| ! [B] :
( app(app(B,cons(A,nil)),C) != sk3
| ~ ssList(C)
| ~ ssList(B)
| ~ ssItem(A) ) ) ),
inference(miniscoping,[status(thm)],[f192]) ).
fof(f441,plain,
! [X0,X1,X2,X3] :
( ~ memberP(X2,X3)
| leq(X0,X3)
| ~ ssItem(X3)
| app(app(X1,cons(X0,nil)),X2) != sk3
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f440]) ).
fof(f442,plain,
! [B,D] :
( ~ memberP(B,D)
| ! [A] :
( leq(D,A)
| ~ ssItem(D)
| ! [C] :
( app(app(B,cons(A,nil)),C) != sk3
| ~ ssList(C)
| ~ ssList(B)
| ~ ssItem(A) ) ) ),
inference(miniscoping,[status(thm)],[f193]) ).
fof(f443,plain,
! [X0,X1,X2,X3] :
( ~ memberP(X1,X3)
| leq(X3,X0)
| ~ ssItem(X3)
| app(app(X1,cons(X0,nil)),X2) != sk3
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f445,plain,
ssItem(sk6),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f446,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f447,plain,
ssList(sk8),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f448,plain,
ssList(sk9),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f449,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f450,plain,
leq(sk6,sk5),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f451,plain,
( ~ leq(sk5,sk6)
| ssItem(sk10) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f452,plain,
( ~ leq(sk5,sk6)
| memberP(sk8,sk10) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f453,plain,
( ~ leq(sk5,sk6)
| ~ leq(sk10,sk6)
| ~ leq(sk5,sk10) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f461,definition,
( sQ2_spl
<=> ssItem(sk10) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f464,definition,
( sQ3_spl
<=> leq(sk5,sk6) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f451,f461,f464]) ).
fof(f468,definition,
( sQ4_spl
<=> memberP(sk8,sk10) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ4_spl
| memberP(sk8,sk10) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,plain,
( ~ sQ3_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f452,f468,f464]) ).
fof(f472,definition,
( sQ5_spl
<=> leq(sk5,sk10) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ5_spl
| ~ leq(sk5,sk10) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,definition,
( sQ6_spl
<=> leq(sk10,sk6) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f453,f472,f475,f464]) ).
fof(f491,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f356]) ).
fof(f492,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f491]) ).
fof(f510,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk3,
inference(forward_demodulation,[status(thm)],[f439,f449]) ).
fof(f513,definition,
( sQ7_spl
<=> ssItem(sk6) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( sQ7_spl
| ~ ssItem(sk6) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,definition,
( sQ8_spl
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ8_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,definition,
( sQ9_spl
<=> ssList(sk9) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f521,plain,
( sQ9_spl
| ~ ssList(sk9) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f530,plain,
! [X0] :
( ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| leq(X0,sk6)
| ~ ssItem(X0)
| ~ ssList(sk9)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f443,f510]) ).
fof(f532,definition,
! [X0] :
( sQ12_spl
<=> ( ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f533,plain,
! [X0] :
( ~ sQ12_spl
| ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f532]) ).
fof(f535,plain,
( sQ12_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f530,f513,f516,f519,f532]) ).
fof(f537,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f521,f448]) ).
fof(f538,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f537]) ).
fof(f539,plain,
( sQ8_spl
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8) ),
inference(resolution,[status(thm)],[f289,f518]) ).
fof(f541,definition,
( sQ13_spl
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( sQ13_spl
| ~ ssList(sk8) ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f544,definition,
( sQ14_spl
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f545,plain,
( ~ sQ14_spl
| ssList(app(sk7,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f546,plain,
( sQ14_spl
| ~ ssList(app(sk7,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f547,plain,
( sQ8_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f539,f541,f544,f516]) ).
fof(f555,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f445]) ).
fof(f556,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f555]) ).
fof(f557,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f447]) ).
fof(f558,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f557]) ).
fof(f559,plain,
( sQ14_spl
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f546,f289]) ).
fof(f560,definition,
( sQ17_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f562,plain,
( sQ17_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f563,definition,
( sQ18_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ18_spl
| ~ ssList(sk7) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f566,plain,
( sQ14_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f559,f560,f563,f544]) ).
fof(f567,plain,
( sQ17_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f562,f290]) ).
fof(f568,definition,
( sQ19_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f570,plain,
( sQ19_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f568]) ).
fof(f571,definition,
( sQ20_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( sQ20_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f574,plain,
( sQ17_spl
| ~ sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f567,f568,f571,f560]) ).
fof(f575,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f446]) ).
fof(f576,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f575]) ).
fof(f577,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f570,f444]) ).
fof(f578,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f577]) ).
fof(f579,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f211]) ).
fof(f580,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f579]) ).
fof(f606,definition,
( sQ25_spl
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( sQ25_spl
| ~ ssList(cons(sk6,nil)) ),
inference(component_clause,[status(thm)],[f606]) ).
fof(f610,plain,
( sk6 = sk5
| ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ leq(sk5,sk6) ),
inference(resolution,[status(thm)],[f346,f450]) ).
fof(f612,definition,
( sQ26_spl
<=> sk6 = sk5 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ26_spl
| sk6 = sk5 ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( sQ26_spl
| ~ sQ7_spl
| ~ sQ19_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f610,f464,f568,f513,f612]) ).
fof(f656,plain,
! [X0] :
( ~ sQ12_spl
| leq(X0,sk6)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ),
inference(resolution,[status(thm)],[f358,f533]) ).
fof(f658,definition,
! [X0] :
( sQ33_spl
<=> ( leq(X0,sk6)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f659,plain,
! [X0] :
( ~ sQ33_spl
| leq(X0,sk6)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ),
inference(component_clause,[status(thm)],[f658]) ).
fof(f661,plain,
( ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ13_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f656,f658,f541,f544,f532]) ).
fof(f666,plain,
! [X0] :
( ~ sQ33_spl
| leq(X0,sk6)
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f659]) ).
fof(f669,definition,
! [X0] :
( sQ35_spl
<=> ( leq(X0,sk6)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f670,plain,
! [X0] :
( ~ sQ35_spl
| leq(X0,sk6)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ),
inference(component_clause,[status(thm)],[f669]) ).
fof(f677,plain,
! [X0] :
( ~ sQ35_spl
| leq(X0,sk6)
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f670]) ).
fof(f689,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk9) ),
inference(paramodulation,[status(thm)],[f510,f372]) ).
fof(f691,definition,
( sQ39_spl
<=> sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( ~ sQ39_spl
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9)) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f694,plain,
( sQ39_spl
| ~ sQ8_spl
| ~ sQ25_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f689,f519,f606,f516,f691]) ).
fof(f704,plain,
( sQ25_spl
| ~ ssList(nil)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f608,f290]) ).
fof(f705,plain,
( sQ25_spl
| ~ sQ20_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f704,f513,f571,f606]) ).
fof(f706,plain,
! [X0] :
( ~ sQ33_spl
| ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f666,f359]) ).
fof(f708,definition,
! [X0] :
( sQ42_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f709,plain,
! [X0] :
( ~ sQ42_spl
| ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,plain,
( ~ sQ33_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f706,f708,f560,f563,f658]) ).
fof(f716,plain,
! [X0] :
( ~ sQ42_spl
| ~ memberP(cons(sk5,nil),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f709]) ).
fof(f719,plain,
( ~ sQ42_spl
| ~ ssItem(sk5)
| ~ ssList(nil)
| leq(sk5,sk6)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f716,f492]) ).
fof(f724,plain,
( ~ sQ42_spl
| ~ sQ20_spl
| sQ3_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f719,f568,f464,f571,f708]) ).
fof(f729,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ26_spl
| ~ memberP(app(app(sk7,cons(sk6,nil)),sk8),X0)
| leq(X0,sk6)
| ~ ssItem(X0) ),
inference(backward_demodulation,[status(thm)],[f613,f533]) ).
fof(f732,plain,
( ~ sQ14_spl
| ~ sQ26_spl
| ssList(app(sk7,cons(sk6,nil))) ),
inference(backward_demodulation,[status(thm)],[f613,f545]) ).
fof(f737,plain,
( ~ sQ35_spl
| ~ sQ4_spl
| leq(sk10,sk6)
| ~ ssItem(sk10) ),
inference(resolution,[status(thm)],[f469,f677]) ).
fof(f738,plain,
( ~ sQ35_spl
| ~ sQ4_spl
| sQ6_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f737,f461,f475,f468,f669]) ).
fof(f739,plain,
( sQ5_spl
| ~ sQ26_spl
| ~ leq(sk6,sk10) ),
inference(forward_demodulation,[status(thm)],[f613,f474]) ).
fof(f762,definition,
( sQ49_spl
<=> leq(sk6,sk10) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ49_spl
| leq(sk6,sk10) ),
inference(component_clause,[status(thm)],[f762]) ).
fof(f915,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ26_spl
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk6,nil)))
| ~ ssList(sk8)
| ~ memberP(sk8,X0)
| leq(X0,sk6)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f729,f359]) ).
fof(f917,definition,
( sQ67_spl
<=> ssList(app(sk7,cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f919,plain,
( sQ67_spl
| ~ ssList(app(sk7,cons(sk6,nil))) ),
inference(component_clause,[status(thm)],[f917]) ).
fof(f920,plain,
( ~ sQ12_spl
| ~ sQ26_spl
| ~ sQ67_spl
| ~ sQ13_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f915,f669,f541,f917,f612,f532]) ).
fof(f925,plain,
( sQ67_spl
| ~ sQ14_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f919,f732]) ).
fof(f926,plain,
( sQ67_spl
| ~ sQ14_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f925]) ).
fof(f932,plain,
( ~ sQ39_spl
| ~ sQ26_spl
| sk3 = app(app(app(sk7,cons(sk6,nil)),sk8),app(cons(sk6,nil),sk9)) ),
inference(forward_demodulation,[status(thm)],[f613,f692]) ).
fof(f933,plain,
( ~ sQ39_spl
| ~ sQ26_spl
| sk3 = app(app(sk7,cons(sk6,nil)),app(sk8,app(cons(sk6,nil),sk9)))
| ~ ssList(app(sk7,cons(sk6,nil)))
| ~ ssList(sk8)
| ~ ssList(app(cons(sk6,nil),sk9)) ),
inference(paramodulation,[status(thm)],[f932,f372]) ).
fof(f946,definition,
( sQ69_spl
<=> ssList(app(cons(sk6,nil),sk9)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f948,plain,
( sQ69_spl
| ~ ssList(app(cons(sk6,nil),sk9)) ),
inference(component_clause,[status(thm)],[f946]) ).
fof(f949,definition,
( sQ70_spl
<=> sk3 = app(app(sk7,cons(sk6,nil)),app(sk8,app(cons(sk6,nil),sk9))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( ~ sQ70_spl
| sk3 = app(app(sk7,cons(sk6,nil)),app(sk8,app(cons(sk6,nil),sk9))) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f952,plain,
( ~ sQ39_spl
| ~ sQ26_spl
| sQ70_spl
| ~ sQ67_spl
| ~ sQ13_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f933,f946,f541,f917,f949,f612,f691]) ).
fof(f992,plain,
( sQ69_spl
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk9) ),
inference(resolution,[status(thm)],[f948,f289]) ).
fof(f993,plain,
( sQ69_spl
| ~ sQ25_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f992,f519,f606,f946]) ).
fof(f1205,plain,
! [X0] :
( ~ sQ70_spl
| ~ memberP(app(sk8,app(cons(sk6,nil),sk9)),X0)
| leq(sk6,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk8,app(cons(sk6,nil),sk9)))
| ~ ssList(sk7)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f950,f441]) ).
fof(f1223,definition,
( sQ96_spl
<=> ssList(app(sk8,app(cons(sk6,nil),sk9))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1225,plain,
( sQ96_spl
| ~ ssList(app(sk8,app(cons(sk6,nil),sk9))) ),
inference(component_clause,[status(thm)],[f1223]) ).
fof(f1226,definition,
! [X0] :
( sQ97_spl
<=> ( ~ memberP(app(sk8,app(cons(sk6,nil),sk9)),X0)
| leq(sk6,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1227,plain,
! [X0] :
( ~ sQ97_spl
| ~ memberP(app(sk8,app(cons(sk6,nil),sk9)),X0)
| leq(sk6,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1226]) ).
fof(f1229,plain,
( ~ sQ70_spl
| sQ97_spl
| ~ sQ96_spl
| ~ sQ18_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1205,f513,f563,f1223,f1226,f949]) ).
fof(f1280,plain,
( sQ96_spl
| ~ ssList(sk8)
| ~ ssList(app(cons(sk6,nil),sk9)) ),
inference(resolution,[status(thm)],[f1225,f289]) ).
fof(f1281,plain,
( sQ96_spl
| ~ sQ13_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f1280,f946,f541,f1223]) ).
fof(f1326,plain,
! [X0] :
( ~ sQ97_spl
| ~ ssItem(X0)
| ~ ssList(sk8)
| ~ ssList(app(cons(sk6,nil),sk9))
| ~ memberP(sk8,X0)
| leq(sk6,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1227,f358]) ).
fof(f1328,definition,
! [X0] :
( sQ109_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk8,X0)
| leq(sk6,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1329,plain,
! [X0] :
( ~ sQ109_spl
| ~ ssItem(X0)
| ~ memberP(sk8,X0)
| leq(sk6,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1328]) ).
fof(f1331,plain,
( ~ sQ97_spl
| ~ sQ13_spl
| ~ sQ69_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f1326,f1328,f946,f541,f1226]) ).
fof(f1336,plain,
! [X0] :
( ~ sQ109_spl
| ~ memberP(sk8,X0)
| leq(sk6,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1329]) ).
fof(f1338,plain,
( ~ sQ4_spl
| ~ sQ109_spl
| leq(sk6,sk10)
| ~ ssItem(sk10) ),
inference(resolution,[status(thm)],[f1336,f469]) ).
fof(f1339,plain,
( ~ sQ4_spl
| ~ sQ109_spl
| sQ49_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1338,f461,f762,f1328,f468]) ).
fof(f1340,plain,
( ~ sQ49_spl
| sQ5_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f763,f739]) ).
fof(f1341,plain,
( ~ sQ49_spl
| sQ5_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f1340]) ).
fof(f1342,plain,
$false,
inference(sat_refutation,[status(thm)],[f467,f471,f478,f535,f538,f547,f556,f558,f566,f574,f576,f578,f580,f615,f661,f694,f705,f711,f724,f738,f920,f926,f952,f993,f1229,f1281,f1331,f1339,f1341]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC155-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.47 % Computer : n026.cluster.edu
% 0.18/0.47 % Model : x86_64 x86_64
% 0.18/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.47 % Memory : 8046.5625MB
% 0.18/0.47 % OS : Linux 6.8.0-71-generic
% 0.18/0.47 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 08:02:40 UTC 2026
% 0.18/0.48 % CPUTime :
% 0.18/0.53 % Drodi V4.1.1
% 0.23/0.59 % Refutation found
% 0.23/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.23/0.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/0.64 % Elapsed time: 0.143642 seconds
% 0.23/0.64 % CPU time: 0.465753 seconds
% 0.23/0.64 % Total memory used: 73.483 MB
% 0.23/0.64 % Net memory used: 73.245 MB
%------------------------------------------------------------------------------