%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC214-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:25 PM UTC 2026
% Result : Unsatisfiable 32.86s 19.88s
% Output : CNFRefutation 5.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 52
% Syntax : Number of formulae : 182 ( 27 unt; 26 def)
% Number of atoms : 575 ( 70 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 751 ( 358 ~; 367 |; 0 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 27 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 126 ( 126 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [U] :
( strictorderedP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ 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(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [U,V,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [U,V,W,X] :
( frontsegP(V,X)
| ~ ssItem(U)
| ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,axiom,
! [U,V,W,X] :
( U = W
| ~ ssItem(U)
| ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,axiom,
! [U,V,W,X] :
( frontsegP(cons(W,U),cons(X,V))
| ~ ssItem(W)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(V)
| W != X
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
neq(sk2,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
! [A] :
( ~ strictorderedP(A)
| ~ segmentP(A,sk3)
| ~ frontsegP(sk4,A)
| ~ neq(sk3,A)
| ~ ssList(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
~ neq(sk1,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f208,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f209,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f252,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f256,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f262,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f270,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f272,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f273,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f283,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f295,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f296,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f299,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f303,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f308,plain,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f338,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f356,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f357,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f404,plain,
! [V,X] :
( frontsegP(V,X)
| ! [U] :
( ~ ssItem(U)
| ! [W] :
( ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ) ) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f405,plain,
! [X0,X1,X2,X3] :
( frontsegP(X1,X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ frontsegP(cons(X0,X1),cons(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f408,plain,
! [U,W] :
( U = W
| ~ ssItem(U)
| ~ ssItem(W)
| ! [V] :
( ~ ssList(V)
| ! [X] :
( ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f409,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| ~ ssItem(X0)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ frontsegP(cons(X0,X1),cons(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f412,plain,
! [X0,X1,X2,X3] :
( frontsegP(cons(X2,X0),cons(X3,X1))
| ~ ssItem(X2)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| X2 != X3
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f427,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f428,plain,
ssList(sk2),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f431,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f432,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f433,plain,
neq(sk2,nil),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f436,plain,
! [X0] :
( ~ strictorderedP(X0)
| ~ segmentP(X0,sk3)
| ~ frontsegP(sk4,X0)
| ~ neq(sk3,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f437,plain,
~ neq(sk1,nil),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f460,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f357]) ).
fof(f465,plain,
! [X0,X1,X3] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssItem(X3)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f412]) ).
fof(f466,plain,
! [X0,X1,X2] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f465]) ).
fof(f479,plain,
! [X0] :
( ~ strictorderedP(X0)
| ~ segmentP(X0,sk3)
| ~ frontsegP(sk4,X0)
| ~ neq(sk1,X0)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f436]) ).
fof(f480,plain,
! [X0] :
( ~ strictorderedP(X0)
| ~ segmentP(X0,sk3)
| ~ frontsegP(sk2,X0)
| ~ neq(sk1,X0)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f431,f479]) ).
fof(f481,plain,
! [X0] :
( ~ strictorderedP(X0)
| ~ segmentP(X0,sk1)
| ~ frontsegP(sk2,X0)
| ~ neq(sk1,X0)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f480]) ).
fof(f484,definition,
( sQ2_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( sQ2_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f492,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f486,f204]) ).
fof(f493,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f492]) ).
fof(f502,plain,
! [X0,X1] :
( ~ ssList(X1)
| cons(skaf83(X0),X1) != nil ),
inference(resolution,[status(thm)],[f296,f208]) ).
fof(f517,plain,
( sk1 = nil
| ~ ssList(sk1)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f299,f437]) ).
fof(f518,plain,
! [X0] :
( ~ strictorderedP(X0)
| ~ segmentP(X0,sk1)
| ~ frontsegP(sk2,X0)
| ~ ssList(X0)
| sk1 = X0
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f299,f481]) ).
fof(f521,definition,
( sQ4_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ4_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,definition,
( sQ5_spl
<=> sk1 = nil ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( ~ sQ5_spl
| sk1 = nil ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f517,f484,f521,f524]) ).
fof(f528,definition,
! [X0] :
( sQ6_spl
<=> ( ~ strictorderedP(X0)
| ~ segmentP(X0,sk1)
| ~ frontsegP(sk2,X0)
| ~ ssList(X0)
| sk1 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f529,plain,
! [X0] :
( ~ sQ6_spl
| ~ strictorderedP(X0)
| ~ segmentP(X0,sk1)
| ~ frontsegP(sk2,X0)
| ~ ssList(X0)
| sk1 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f531,plain,
( ~ sQ4_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f518,f528,f521]) ).
fof(f532,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f427]) ).
fof(f533,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f532]) ).
fof(f534,plain,
! [X0] :
( ~ sQ6_spl
| ~ strictorderedP(X0)
| ~ segmentP(X0,sk1)
| ~ frontsegP(sk2,X0)
| sk1 = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f529]) ).
fof(f552,plain,
( ~ sQ5_spl
| ~ neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f525,f437]) ).
fof(f584,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ5_spl
| ~ strictorderedP(X0)
| ~ segmentP(X0,sk1)
| ~ frontsegP(sk2,X0)
| nil = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f525,f534]) ).
fof(f585,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ5_spl
| ~ strictorderedP(X0)
| ~ segmentP(X0,nil)
| ~ frontsegP(sk2,X0)
| nil = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f525,f584]) ).
fof(f586,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ5_spl
| ~ strictorderedP(X0)
| ~ frontsegP(sk2,X0)
| nil = X0
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f585,f252]) ).
fof(f626,definition,
( sQ17_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f628,plain,
( sQ17_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f626]) ).
fof(f629,definition,
( sQ18_spl
<=> sk2 = nil ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( ~ sQ18_spl
| sk2 = nil ),
inference(component_clause,[status(thm)],[f629]) ).
fof(f645,plain,
( ~ sQ18_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f630,f433]) ).
fof(f648,plain,
( ~ sQ18_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f645,f552]) ).
fof(f649,plain,
( ~ sQ18_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f648]) ).
fof(f689,plain,
app(sk2,nil) = sk2,
inference(resolution,[status(thm)],[f270,f428]) ).
fof(f712,plain,
( frontsegP(app(sk2,nil),sk2)
| ~ ssList(sk2)
| ~ ssList(sk2)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f689,f460]) ).
fof(f714,definition,
( sQ22_spl
<=> frontsegP(app(sk2,nil),sk2) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f715,plain,
( ~ sQ22_spl
| frontsegP(app(sk2,nil),sk2) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,plain,
( sQ22_spl
| ~ sQ17_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f712,f484,f626,f714]) ).
fof(f722,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f628,f428]) ).
fof(f723,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f722]) ).
fof(f724,plain,
( ~ sQ22_spl
| frontsegP(sk2,sk2) ),
inference(forward_demodulation,[status(thm)],[f689,f715]) ).
fof(f726,definition,
( sQ24_spl
<=> frontsegP(sk2,sk2) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f728,plain,
( sQ24_spl
| ~ frontsegP(sk2,sk2) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f733,plain,
( sQ24_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f724]) ).
fof(f734,plain,
( sQ24_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f733]) ).
fof(f2503,plain,
( nil = sk2
| cons(hd(sk2),tl(sk2)) = sk2 ),
inference(resolution,[status(thm)],[f303,f428]) ).
fof(f2527,definition,
( sQ249_spl
<=> cons(hd(sk2),tl(sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f2528,plain,
( ~ sQ249_spl
| cons(hd(sk2),tl(sk2)) = sk2 ),
inference(component_clause,[status(thm)],[f2527]) ).
fof(f2530,plain,
( sQ18_spl
| sQ249_spl ),
inference(split_clause,[status(thm)],[f2503,f2527,f629]) ).
fof(f2535,plain,
! [X0,X1] :
( ~ sQ249_spl
| frontsegP(X1,tl(sk2))
| ~ ssItem(X0)
| ~ ssItem(hd(sk2))
| ~ ssList(X1)
| ~ ssList(tl(sk2))
| ~ frontsegP(cons(X0,X1),sk2) ),
inference(paramodulation,[status(thm)],[f2528,f405]) ).
fof(f2536,plain,
! [X0,X1] :
( ~ sQ249_spl
| frontsegP(tl(sk2),X1)
| ~ ssItem(hd(sk2))
| ~ ssItem(X0)
| ~ ssList(tl(sk2))
| ~ ssList(X1)
| ~ frontsegP(sk2,cons(X0,X1)) ),
inference(paramodulation,[status(thm)],[f2528,f405]) ).
fof(f2538,plain,
! [X0] :
( ~ sQ249_spl
| frontsegP(sk2,cons(hd(sk2),X0))
| ~ ssItem(hd(sk2))
| ~ ssList(tl(sk2))
| ~ ssList(X0)
| ~ frontsegP(tl(sk2),X0) ),
inference(paramodulation,[status(thm)],[f2528,f466]) ).
fof(f2542,plain,
! [X0,X1] :
( ~ sQ249_spl
| X0 = hd(sk2)
| ~ ssItem(X0)
| ~ ssItem(hd(sk2))
| ~ ssList(X1)
| ~ ssList(tl(sk2))
| ~ frontsegP(cons(X0,X1),sk2) ),
inference(paramodulation,[status(thm)],[f2528,f409]) ).
fof(f2545,definition,
! [X0,X1] :
( sQ251_spl
<=> ( frontsegP(X1,tl(sk2))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ frontsegP(cons(X0,X1),sk2) ) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f2546,plain,
! [X0,X1] :
( ~ sQ251_spl
| frontsegP(X1,tl(sk2))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ frontsegP(cons(X0,X1),sk2) ),
inference(component_clause,[status(thm)],[f2545]) ).
fof(f2548,definition,
( sQ252_spl
<=> ssList(tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f2551,definition,
( sQ253_spl
<=> ssItem(hd(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f2552,plain,
( ~ sQ253_spl
| ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f2551]) ).
fof(f2553,plain,
( sQ253_spl
| ~ ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f2551]) ).
fof(f2554,plain,
( ~ sQ249_spl
| ~ sQ253_spl
| ~ sQ252_spl
| sQ251_spl ),
inference(split_clause,[status(thm)],[f2535,f2545,f2548,f2551,f2527]) ).
fof(f2555,definition,
! [X0,X1] :
( sQ254_spl
<=> ( frontsegP(tl(sk2),X1)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ frontsegP(sk2,cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f2556,plain,
! [X0,X1] :
( ~ sQ254_spl
| frontsegP(tl(sk2),X1)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ frontsegP(sk2,cons(X0,X1)) ),
inference(component_clause,[status(thm)],[f2555]) ).
fof(f2558,plain,
( ~ sQ249_spl
| ~ sQ253_spl
| ~ sQ252_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f2536,f2555,f2548,f2551,f2527]) ).
fof(f2563,definition,
! [X0] :
( sQ256_spl
<=> ( frontsegP(sk2,cons(hd(sk2),X0))
| ~ ssList(X0)
| ~ frontsegP(tl(sk2),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f2564,plain,
! [X0] :
( ~ sQ256_spl
| frontsegP(sk2,cons(hd(sk2),X0))
| ~ ssList(X0)
| ~ frontsegP(tl(sk2),X0) ),
inference(component_clause,[status(thm)],[f2563]) ).
fof(f2566,plain,
( ~ sQ249_spl
| ~ sQ253_spl
| ~ sQ252_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f2538,f2563,f2548,f2551,f2527]) ).
fof(f2576,definition,
! [X0,X1] :
( sQ259_spl
<=> ( X0 = hd(sk2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ frontsegP(cons(X0,X1),sk2) ) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f2577,plain,
! [X0,X1] :
( ~ sQ259_spl
| X0 = hd(sk2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ frontsegP(cons(X0,X1),sk2) ),
inference(component_clause,[status(thm)],[f2576]) ).
fof(f2579,plain,
( ~ sQ249_spl
| ~ sQ253_spl
| ~ sQ252_spl
| sQ259_spl ),
inference(split_clause,[status(thm)],[f2542,f2576,f2548,f2551,f2527]) ).
fof(f2594,plain,
( sQ253_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f2553,f273]) ).
fof(f2595,plain,
( sQ253_spl
| sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f2594,f626,f629,f2551]) ).
fof(f2660,plain,
! [X0] : cons(skaf83(X0),nil) != nil,
inference(resolution,[status(thm)],[f502,f204]) ).
fof(f2705,plain,
( nil = sk2
| cons(skaf83(sk2),skaf82(sk2)) = sk2 ),
inference(resolution,[status(thm)],[f308,f428]) ).
fof(f2729,definition,
( sQ266_spl
<=> cons(skaf83(sk2),skaf82(sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f2730,plain,
( ~ sQ266_spl
| cons(skaf83(sk2),skaf82(sk2)) = sk2 ),
inference(component_clause,[status(thm)],[f2729]) ).
fof(f2732,plain,
( sQ18_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f2705,f2729,f629]) ).
fof(f2981,definition,
( sQ286_spl
<=> ssList(skaf82(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition]) ).
fof(f2983,plain,
( sQ286_spl
| ~ ssList(skaf82(sk2)) ),
inference(component_clause,[status(thm)],[f2981]) ).
fof(f2984,definition,
( sQ287_spl
<=> ssItem(skaf83(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition]) ).
fof(f2986,plain,
( sQ287_spl
| ~ ssItem(skaf83(sk2)) ),
inference(component_clause,[status(thm)],[f2984]) ).
fof(f3024,plain,
( sQ287_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2986,f208]) ).
fof(f3025,plain,
sQ287_spl,
inference(contradiction_clause,[status(thm)],[f3024]) ).
fof(f3026,plain,
( sQ286_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2983,f209]) ).
fof(f3027,plain,
sQ286_spl,
inference(contradiction_clause,[status(thm)],[f3026]) ).
fof(f3368,plain,
( ~ sQ266_spl
| ~ sQ251_spl
| frontsegP(skaf82(sk2),tl(sk2))
| ~ ssItem(skaf83(sk2))
| ~ ssList(skaf82(sk2))
| ~ frontsegP(sk2,sk2) ),
inference(paramodulation,[status(thm)],[f2730,f2546]) ).
fof(f3374,definition,
( sQ301_spl
<=> frontsegP(skaf82(sk2),tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).
fof(f3375,plain,
( ~ sQ301_spl
| frontsegP(skaf82(sk2),tl(sk2)) ),
inference(component_clause,[status(thm)],[f3374]) ).
fof(f3377,plain,
( ~ sQ266_spl
| ~ sQ251_spl
| sQ301_spl
| ~ sQ287_spl
| ~ sQ286_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f3368,f726,f2981,f2984,f3374,f2545,f2729]) ).
fof(f3803,plain,
( ~ sQ266_spl
| ~ sQ254_spl
| frontsegP(tl(sk2),skaf82(sk2))
| ~ ssItem(skaf83(sk2))
| ~ ssList(skaf82(sk2))
| ~ frontsegP(sk2,sk2) ),
inference(paramodulation,[status(thm)],[f2730,f2556]) ).
fof(f3810,definition,
( sQ317_spl
<=> frontsegP(tl(sk2),skaf82(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition]) ).
fof(f3813,plain,
( ~ sQ266_spl
| ~ sQ254_spl
| sQ317_spl
| ~ sQ287_spl
| ~ sQ286_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f3803,f726,f2981,f2984,f3810,f2555,f2729]) ).
fof(f4303,plain,
( ~ sQ301_spl
| skaf82(sk2) = tl(sk2)
| ~ ssList(skaf82(sk2))
| ~ ssList(tl(sk2))
| ~ frontsegP(tl(sk2),skaf82(sk2)) ),
inference(resolution,[status(thm)],[f3375,f338]) ).
fof(f4314,definition,
( sQ353_spl
<=> skaf82(sk2) = tl(sk2) ),
introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition]) ).
fof(f4315,plain,
( ~ sQ353_spl
| skaf82(sk2) = tl(sk2) ),
inference(component_clause,[status(thm)],[f4314]) ).
fof(f4317,plain,
( ~ sQ301_spl
| sQ353_spl
| ~ sQ286_spl
| ~ sQ252_spl
| ~ sQ317_spl ),
inference(split_clause,[status(thm)],[f4303,f3810,f2548,f2981,f4314,f3374]) ).
fof(f6359,plain,
! [X0] :
( ~ sQ256_spl
| ~ sQ353_spl
| frontsegP(sk2,cons(hd(sk2),X0))
| ~ ssList(X0)
| ~ frontsegP(skaf82(sk2),X0) ),
inference(forward_demodulation,[status(thm)],[f4315,f2564]) ).
fof(f6361,plain,
( ~ sQ256_spl
| ~ sQ353_spl
| ~ ssList(skaf82(sk2))
| frontsegP(sk2,cons(hd(sk2),nil))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f6359,f256]) ).
fof(f6369,definition,
( sQ496_spl
<=> frontsegP(sk2,cons(hd(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ496_spl])],[split_symbol_definition]) ).
fof(f6370,plain,
( ~ sQ496_spl
| frontsegP(sk2,cons(hd(sk2),nil)) ),
inference(component_clause,[status(thm)],[f6369]) ).
fof(f6372,plain,
( ~ sQ256_spl
| ~ sQ353_spl
| ~ sQ286_spl
| sQ496_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f6361,f484,f6369,f2981,f4314,f2563]) ).
fof(f7659,plain,
! [X0] :
( ~ sQ253_spl
| ssList(cons(hd(sk2),X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f283,f2552]) ).
fof(f12216,plain,
( ~ sQ266_spl
| ~ sQ259_spl
| skaf83(sk2) = hd(sk2)
| ~ ssItem(skaf83(sk2))
| ~ ssList(skaf82(sk2))
| ~ frontsegP(sk2,sk2) ),
inference(paramodulation,[status(thm)],[f2730,f2577]) ).
fof(f12222,definition,
( sQ660_spl
<=> skaf83(sk2) = hd(sk2) ),
introduced(definition,[new_symbols(definition,[sQ660_spl])],[split_symbol_definition]) ).
fof(f12223,plain,
( ~ sQ660_spl
| skaf83(sk2) = hd(sk2) ),
inference(component_clause,[status(thm)],[f12222]) ).
fof(f12225,plain,
( ~ sQ266_spl
| ~ sQ259_spl
| sQ660_spl
| ~ sQ287_spl
| ~ sQ286_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f12216,f726,f2981,f2984,f12222,f2576,f2729]) ).
fof(f14630,plain,
( nil = sk2
| ssList(tl(sk2)) ),
inference(resolution,[status(thm)],[f272,f428]) ).
fof(f14675,plain,
( sQ18_spl
| sQ252_spl ),
inference(split_clause,[status(thm)],[f14630,f2548,f629]) ).
fof(f26748,plain,
( ~ sQ496_spl
| ~ sQ660_spl
| frontsegP(sk2,cons(skaf83(sk2),nil)) ),
inference(forward_demodulation,[status(thm)],[f12223,f6370]) ).
fof(f26752,definition,
( sQ1201_spl
<=> ssList(cons(skaf83(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ1201_spl])],[split_symbol_definition]) ).
fof(f26754,plain,
( sQ1201_spl
| ~ ssList(cons(skaf83(sk2),nil)) ),
inference(component_clause,[status(thm)],[f26752]) ).
fof(f26770,plain,
( ~ sQ496_spl
| ~ sQ660_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ strictorderedP(cons(skaf83(sk2),nil))
| nil = cons(skaf83(sk2),nil)
| ~ ssList(cons(skaf83(sk2),nil)) ),
inference(resolution,[status(thm)],[f586,f26748]) ).
fof(f26776,definition,
( sQ1206_spl
<=> nil = cons(skaf83(sk2),nil) ),
introduced(definition,[new_symbols(definition,[sQ1206_spl])],[split_symbol_definition]) ).
fof(f26777,plain,
( ~ sQ1206_spl
| nil = cons(skaf83(sk2),nil) ),
inference(component_clause,[status(thm)],[f26776]) ).
fof(f26779,definition,
( sQ1207_spl
<=> strictorderedP(cons(skaf83(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ1207_spl])],[split_symbol_definition]) ).
fof(f26781,plain,
( sQ1207_spl
| ~ strictorderedP(cons(skaf83(sk2),nil)) ),
inference(component_clause,[status(thm)],[f26779]) ).
fof(f26782,plain,
( ~ sQ496_spl
| ~ sQ660_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ1207_spl
| sQ1206_spl
| ~ sQ1201_spl ),
inference(split_clause,[status(thm)],[f26770,f26752,f26776,f26779,f524,f528,f12222,f6369]) ).
fof(f31100,plain,
! [X0] :
( ~ sQ253_spl
| ~ sQ660_spl
| ssList(cons(skaf83(sk2),X0))
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f12223,f7659]) ).
fof(f31101,plain,
( sQ1201_spl
| ~ sQ253_spl
| ~ sQ660_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f31100,f26754]) ).
fof(f31159,plain,
( sQ1201_spl
| ~ sQ253_spl
| ~ sQ660_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f31101,f484,f12222,f2551,f26752]) ).
fof(f31162,plain,
( ~ sQ1206_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26777,f2660]) ).
fof(f31163,plain,
~ sQ1206_spl,
inference(contradiction_clause,[status(thm)],[f31162]) ).
fof(f31230,plain,
( sQ1207_spl
| ~ ssItem(skaf83(sk2)) ),
inference(resolution,[status(thm)],[f26781,f262]) ).
fof(f31234,plain,
( sQ1207_spl
| ~ sQ287_spl ),
inference(split_clause,[status(thm)],[f31230,f2984,f26779]) ).
fof(f31247,plain,
$false,
inference(sat_refutation,[status(thm)],[f493,f527,f531,f533,f649,f717,f723,f734,f2530,f2554,f2558,f2566,f2579,f2595,f2732,f3025,f3027,f3377,f3813,f4317,f6372,f12225,f14675,f26782,f31159,f31163,f31234]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC214-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/15.60 % Computer : n002.cluster.edu
% 0.11/15.60 % Model : x86_64 x86_64
% 0.11/15.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/15.60 % Memory : 8046.5625MB
% 0.11/15.60 % OS : Linux 6.8.0-71-generic
% 0.11/15.60 % CPULimit : 300
% 0.11/15.60 % WCLimit : 300
% 0.11/15.60 % DateTime : Mon Sep 21 08:08:19 UTC 2026
% 0.11/15.60 % CPUTime :
% 0.11/15.62 % Drodi V4.1.1
% 32.86/19.88 % Refutation found
% 32.86/19.88 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 32.86/19.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.31/20.00 % Elapsed time: 4.374637 seconds
% 5.31/20.00 % CPU time: 33.865484 seconds
% 5.31/20.00 % Total memory used: 344.465 MB
% 5.31/20.00 % Net memory used: 316.934 MB
%------------------------------------------------------------------------------