%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC336-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:50 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.39s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 64
% Syntax : Number of formulae : 199 ( 26 unt; 35 def)
% Number of atoms : 554 ( 130 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 654 ( 299 ~; 320 |; 0 &)
% ( 35 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 36 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 100 ( 100 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
totalorderedP(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [U] :
( totalorderedP(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(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ segmentP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(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(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ segmentP(V,U)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,axiom,
! [U,V,W] :
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
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(f188,negated_conjecture,
ssList(sk3),
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(f193,negated_conjecture,
( nil = sk3
| ssItem(sk5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
( nil = sk3
| ssList(sk6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
( nil = sk3
| ssList(sk7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( nil = sk3
| cons(sk5,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
( nil = sk3
| app(app(sk6,sk3),sk7) = sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,negated_conjecture,
( ~ totalorderedP(sk1)
| ~ segmentP(sk2,sk1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,plain,
totalorderedP(nil),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f214,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f262,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f263,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f273,plain,
! [X0] :
( totalorderedP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f280,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f281,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f287,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
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(f313,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f318,plain,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
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(f346,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f376,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f377,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f379,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f412,plain,
! [V,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(app(U,V),W) != X ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f413,plain,
! [X0,X1,X2,X3] :
( segmentP(X3,X1)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(app(X0,X1),X2) != X3 ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f437,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f438,plain,
ssList(sk2),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f439,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f441,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f442,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f444,plain,
( nil = sk3
| ssItem(sk5) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f453,plain,
( nil = sk3
| ssList(sk6) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f454,plain,
( nil = sk3
| ssList(sk7) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f455,plain,
( nil = sk3
| cons(sk5,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f456,plain,
( nil = sk3
| app(app(sk6,sk3),sk7) = sk4 ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f461,plain,
( ~ totalorderedP(sk1)
| ~ segmentP(sk2,sk1) ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f469,definition,
( sQ2_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f476,definition,
( sQ4_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( ~ sQ4_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f479,plain,
( sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f444,f469,f476]) ).
fof(f480,definition,
( sQ5_spl
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( ~ sQ5_spl
| ssList(sk6) ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f484,definition,
( sQ6_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f488,definition,
( sQ7_spl
<=> cons(sk5,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( ~ sQ7_spl
| cons(sk5,nil) = sk3 ),
inference(component_clause,[status(thm)],[f488]) ).
fof(f492,definition,
( sQ8_spl
<=> app(app(sk6,sk3),sk7) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( ~ sQ8_spl
| app(app(sk6,sk3),sk7) = sk4 ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f504,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f453,f480,f476]) ).
fof(f505,plain,
( sQ4_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f454,f484,f476]) ).
fof(f506,plain,
( sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f455,f488,f476]) ).
fof(f507,plain,
( sQ4_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f456,f492,f476]) ).
fof(f510,definition,
( sQ11_spl
<=> segmentP(sk2,sk1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f512,plain,
( sQ11_spl
| ~ segmentP(sk2,sk1) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,definition,
( sQ12_spl
<=> totalorderedP(sk1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( sQ12_spl
| ~ totalorderedP(sk1) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f461,f510,f513]) ).
fof(f535,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(app(app(X1,X2),X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f413]) ).
fof(f547,plain,
segmentP(nil,nil),
inference(resolution,[status(thm)],[f263,f214]) ).
fof(f548,plain,
segmentP(sk3,sk3),
inference(resolution,[status(thm)],[f263,f439]) ).
fof(f549,plain,
segmentP(sk2,sk2),
inference(resolution,[status(thm)],[f263,f438]) ).
fof(f554,plain,
( ~ sQ4_spl
| nil = sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f477]) ).
fof(f565,plain,
( sQ12_spl
| ~ sQ4_spl
| ~ totalorderedP(nil) ),
inference(forward_demodulation,[status(thm)],[f554,f515]) ).
fof(f566,plain,
( sQ12_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f210]) ).
fof(f567,plain,
( sQ12_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f566]) ).
fof(f579,plain,
segmentP(sk1,sk3),
inference(forward_demodulation,[status(thm)],[f442,f548]) ).
fof(f580,plain,
segmentP(sk1,sk1),
inference(forward_demodulation,[status(thm)],[f442,f579]) ).
fof(f581,plain,
app(sk1,nil) = sk1,
inference(resolution,[status(thm)],[f280,f437]) ).
fof(f586,plain,
( ~ sQ5_spl
| app(sk6,nil) = sk6 ),
inference(resolution,[status(thm)],[f280,f481]) ).
fof(f587,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f280,f214]) ).
fof(f609,plain,
app(nil,sk1) = sk1,
inference(resolution,[status(thm)],[f281,f437]) ).
fof(f614,plain,
( ~ sQ5_spl
| app(nil,sk6) = sk6 ),
inference(resolution,[status(thm)],[f281,f481]) ).
fof(f635,plain,
( ~ sQ8_spl
| app(app(sk6,sk1),sk7) = sk4 ),
inference(forward_demodulation,[status(thm)],[f442,f493]) ).
fof(f636,plain,
( ~ sQ8_spl
| app(app(sk6,sk1),sk7) = sk2 ),
inference(forward_demodulation,[status(thm)],[f441,f635]) ).
fof(f637,plain,
( ~ sQ7_spl
| cons(sk5,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f489]) ).
fof(f638,plain,
( ~ sQ7_spl
| totalorderedP(sk1)
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f637,f273]) ).
fof(f639,plain,
( ~ sQ7_spl
| sQ12_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f638,f469,f513,f488]) ).
fof(f646,plain,
( sQ11_spl
| ~ sQ4_spl
| ~ segmentP(sk2,nil) ),
inference(backward_demodulation,[status(thm)],[f554,f512]) ).
fof(f651,plain,
( nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f287,f547]) ).
fof(f653,definition,
( sQ13_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f655,plain,
( sQ13_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f653]) ).
fof(f656,definition,
( sQ14_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f651,f653,f656]) ).
fof(f661,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f655,f214]) ).
fof(f662,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f661]) ).
fof(f678,plain,
( sQ11_spl
| ~ sQ4_spl
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f646,f262]) ).
fof(f679,plain,
( sQ11_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f678,f438]) ).
fof(f680,plain,
( sQ11_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f679]) ).
fof(f689,plain,
( ~ sQ7_spl
| ssList(sk1)
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f637,f293]) ).
fof(f690,definition,
( sQ15_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f693,plain,
( ~ sQ7_spl
| sQ15_spl
| ~ sQ13_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f689,f469,f653,f690,f488]) ).
fof(f694,plain,
( ~ sQ7_spl
| ~ ssList(nil)
| ~ ssItem(sk5)
| sk1 != nil ),
inference(paramodulation,[status(thm)],[f637,f306]) ).
fof(f695,definition,
( sQ16_spl
<=> sk1 = nil ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( ~ sQ7_spl
| ~ sQ13_spl
| ~ sQ2_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f694,f695,f469,f653,f488]) ).
fof(f718,plain,
( ~ sQ8_spl
| ssList(sk2)
| ~ ssList(app(sk6,sk1))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f636,f292]) ).
fof(f719,definition,
( sQ17_spl
<=> ssList(app(sk6,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f721,plain,
( sQ17_spl
| ~ ssList(app(sk6,sk1)) ),
inference(component_clause,[status(thm)],[f719]) ).
fof(f722,definition,
( sQ18_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f725,plain,
( ~ sQ8_spl
| sQ18_spl
| ~ sQ17_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f718,f484,f719,f722,f492]) ).
fof(f831,definition,
( sQ22_spl
<=> nil = app(sk6,sk1) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f832,plain,
( ~ sQ22_spl
| nil = app(sk6,sk1) ),
inference(component_clause,[status(thm)],[f831]) ).
fof(f1032,plain,
! [X0] :
( sk1 = X0
| ~ ssList(X0)
| ~ segmentP(sk1,X0)
| ~ segmentP(X0,sk1) ),
inference(resolution,[status(thm)],[f346,f437]) ).
fof(f1205,plain,
( sQ17_spl
| ~ ssList(sk6)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f721,f292]) ).
fof(f1206,plain,
( sQ17_spl
| ~ sQ5_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1205,f690,f480,f719]) ).
fof(f1423,plain,
! [X0] :
( ~ sQ5_spl
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sk6)
| sk6 != app(nil,X0) ),
inference(paramodulation,[status(thm)],[f614,f377]) ).
fof(f1426,plain,
! [X0] :
( sk1 = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sk1)
| sk1 != app(nil,X0) ),
inference(paramodulation,[status(thm)],[f609,f377]) ).
fof(f1427,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| nil != app(nil,X0) ),
inference(paramodulation,[status(thm)],[f587,f377]) ).
fof(f1428,plain,
! [X0] :
( ~ sQ5_spl
| nil = X0
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(nil)
| sk6 != app(sk6,X0) ),
inference(paramodulation,[status(thm)],[f586,f377]) ).
fof(f1431,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(sk1)
| ~ ssList(nil)
| sk1 != app(sk1,X0) ),
inference(paramodulation,[status(thm)],[f581,f377]) ).
fof(f1444,definition,
! [X0] :
( sQ33_spl
<=> ( sk6 = X0
| ~ ssList(X0)
| sk6 != app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1447,plain,
( ~ sQ13_spl
| ~ sQ5_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1423,f1444,f480,f653]) ).
fof(f1456,definition,
! [X0] :
( sQ36_spl
<=> ( sk1 = X0
| ~ ssList(X0)
| sk1 != app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1459,plain,
( ~ sQ13_spl
| ~ sQ15_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1426,f1456,f690,f653]) ).
fof(f1460,definition,
! [X0] :
( sQ37_spl
<=> ( nil = X0
| ~ ssList(X0)
| nil != app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1463,plain,
( ~ sQ13_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1427,f1460,f653]) ).
fof(f1464,definition,
! [X0] :
( sQ38_spl
<=> ( nil = X0
| ~ ssList(X0)
| sk6 != app(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1467,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1428,f1464,f653,f480]) ).
fof(f1476,definition,
! [X0] :
( sQ41_spl
<=> ( nil = X0
| ~ ssList(X0)
| sk1 != app(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1479,plain,
( ~ sQ15_spl
| ~ sQ13_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1431,f1476,f653,f690]) ).
fof(f1574,plain,
! [X0] :
( ~ sQ5_spl
| nil = X0
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(nil)
| sk6 != app(X0,sk6) ),
inference(paramodulation,[status(thm)],[f614,f379]) ).
fof(f1577,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(sk1)
| ~ ssList(nil)
| sk1 != app(X0,sk1) ),
inference(paramodulation,[status(thm)],[f609,f379]) ).
fof(f1578,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| nil != app(X0,nil) ),
inference(paramodulation,[status(thm)],[f587,f379]) ).
fof(f1579,plain,
! [X0] :
( ~ sQ5_spl
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sk6)
| sk6 != app(X0,nil) ),
inference(paramodulation,[status(thm)],[f586,f379]) ).
fof(f1582,plain,
! [X0] :
( sk1 = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sk1)
| sk1 != app(X0,nil) ),
inference(paramodulation,[status(thm)],[f581,f379]) ).
fof(f1595,definition,
! [X0] :
( sQ45_spl
<=> ( nil = X0
| ~ ssList(X0)
| sk6 != app(X0,sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1598,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f1574,f1595,f653,f480]) ).
fof(f1607,definition,
! [X0] :
( sQ48_spl
<=> ( nil = X0
| ~ ssList(X0)
| sk1 != app(X0,sk1) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1610,plain,
( ~ sQ15_spl
| ~ sQ13_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1577,f1607,f653,f690]) ).
fof(f1611,definition,
! [X0] :
( sQ49_spl
<=> ( nil = X0
| ~ ssList(X0)
| nil != app(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1614,plain,
( ~ sQ13_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1578,f1611,f653]) ).
fof(f1615,definition,
! [X0] :
( sQ50_spl
<=> ( sk6 = X0
| ~ ssList(X0)
| sk6 != app(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1618,plain,
( ~ sQ13_spl
| ~ sQ5_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1579,f1615,f480,f653]) ).
fof(f1627,definition,
! [X0] :
( sQ53_spl
<=> ( sk1 = X0
| ~ ssList(X0)
| sk1 != app(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1630,plain,
( ~ sQ13_spl
| ~ sQ15_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1582,f1627,f690,f653]) ).
fof(f1701,plain,
( sk1 = sk1
| ~ ssList(sk1)
| ~ segmentP(sk1,sk1) ),
inference(resolution,[status(thm)],[f1032,f580]) ).
fof(f1702,plain,
( ~ ssList(sk1)
| sk1 = nil
| ~ ssList(nil)
| ~ segmentP(nil,sk1) ),
inference(resolution,[status(thm)],[f1032,f262]) ).
fof(f1703,definition,
( sQ55_spl
<=> segmentP(sk1,sk1) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1705,plain,
( sQ55_spl
| ~ segmentP(sk1,sk1) ),
inference(component_clause,[status(thm)],[f1703]) ).
fof(f1706,definition,
( sQ56_spl
<=> sk1 = sk1 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1709,plain,
( sQ56_spl
| ~ sQ15_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f1701,f1703,f690,f1706]) ).
fof(f1710,definition,
( sQ57_spl
<=> segmentP(nil,sk1) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1713,plain,
( ~ sQ15_spl
| sQ16_spl
| ~ sQ13_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f1702,f1710,f653,f695,f690]) ).
fof(f1714,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1705,f580]) ).
fof(f1715,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f1714]) ).
fof(f1756,definition,
( sQ58_spl
<=> segmentP(sk2,sk2) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1758,plain,
( sQ58_spl
| ~ segmentP(sk2,sk2) ),
inference(component_clause,[status(thm)],[f1756]) ).
fof(f1767,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1758,f549]) ).
fof(f1768,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f1767]) ).
fof(f1907,plain,
( ~ sQ22_spl
| nil = sk1
| ~ ssList(sk6)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f832,f336]) ).
fof(f1916,plain,
( ~ sQ22_spl
| sQ16_spl
| ~ sQ5_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1907,f690,f480,f695,f831]) ).
fof(f2169,plain,
( nil = sk1
| cons(hd(sk1),tl(sk1)) = sk1 ),
inference(resolution,[status(thm)],[f313,f437]) ).
fof(f2198,definition,
( sQ75_spl
<=> cons(hd(sk1),tl(sk1)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f2201,plain,
( sQ16_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f2169,f2198,f695]) ).
fof(f2320,plain,
! [X0] :
( segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f609,f535]) ).
fof(f2321,plain,
! [X0] :
( segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0))
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f587,f535]) ).
fof(f2322,plain,
! [X0] :
( segmentP(app(app(sk1,nil),X0),nil)
| ~ ssList(app(sk1,X0))
| ~ ssList(nil)
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f581,f535]) ).
fof(f2325,definition,
! [X0] :
( sQ80_spl
<=> ( segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f2328,plain,
( ~ sQ15_spl
| ~ sQ13_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f2320,f2325,f653,f690]) ).
fof(f2329,definition,
! [X0] :
( sQ81_spl
<=> ( segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f2332,plain,
( ~ sQ13_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f2321,f2329,f653]) ).
fof(f2333,definition,
! [X0] :
( sQ82_spl
<=> ( segmentP(app(app(sk1,nil),X0),nil)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f2336,plain,
( ~ sQ13_spl
| ~ sQ15_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f2322,f2333,f690,f653]) ).
fof(f2402,plain,
( nil = sk1
| cons(skaf83(sk1),skaf82(sk1)) = sk1 ),
inference(resolution,[status(thm)],[f318,f437]) ).
fof(f2430,definition,
( sQ86_spl
<=> cons(skaf83(sk1),skaf82(sk1)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2433,plain,
( sQ16_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f2402,f2430,f695]) ).
fof(f2546,plain,
( ~ sQ8_spl
| segmentP(app(app(sk6,sk1),sk7),sk1)
| ~ ssList(sk2)
| ~ ssList(sk1)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f636,f535]) ).
fof(f2555,definition,
( sQ98_spl
<=> segmentP(app(app(sk6,sk1),sk7),sk1) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2556,plain,
( ~ sQ98_spl
| segmentP(app(app(sk6,sk1),sk7),sk1) ),
inference(component_clause,[status(thm)],[f2555]) ).
fof(f2558,plain,
( ~ sQ8_spl
| sQ98_spl
| ~ sQ18_spl
| ~ sQ15_spl
| ~ sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2546,f484,f480,f690,f722,f2555,f492]) ).
fof(f2570,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| segmentP(sk2,sk1) ),
inference(forward_demodulation,[status(thm)],[f636,f2556]) ).
fof(f2571,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2570,f512]) ).
fof(f2572,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2571]) ).
fof(f2573,plain,
$false,
inference(sat_refutation,[status(thm)],[f479,f504,f505,f506,f507,f516,f567,f639,f659,f662,f680,f693,f698,f725,f1206,f1447,f1459,f1463,f1467,f1479,f1598,f1610,f1614,f1618,f1630,f1709,f1713,f1715,f1768,f1916,f2201,f2328,f2332,f2336,f2433,f2558,f2572]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC336-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n002.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 08:19:16 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.42 % Elapsed time: 0.063903 seconds
% 0.12/0.42 % CPU time: 0.271908 seconds
% 0.12/0.42 % Total memory used: 112.826 MB
% 0.12/0.42 % Net memory used: 112.578 MB
%------------------------------------------------------------------------------