%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC346-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 : n010.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:52 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.44s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 52
% Syntax : Number of formulae : 167 ( 25 unt; 27 def)
% Number of atoms : 426 ( 72 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 461 ( 202 ~; 232 |; 0 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 28 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 77 ( 77 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
strictorderedP(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(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(f80,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ segmentP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [U,V] :
( strictorderedP(cons(V,U))
| ~ ssItem(V)
| ~ ssList(U)
| nil != 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(f145,axiom,
! [U,V] :
( app(U,V) = nil
| ~ ssList(U)
| ~ ssList(V)
| nil != V
| nil != U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [U,V,W] :
( segmentP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [U,V,W,X] :
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,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,
( ~ strictorderedP(sk1)
| ~ segmentP(sk2,sk1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,plain,
strictorderedP(nil),
inference(cnf_transformation,[status(thm)],[f3]) ).
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(f282,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f283,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f287,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f323,plain,
! [X0,X1] :
( strictorderedP(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f112]) ).
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(f368,plain,
! [X0,X1] :
( app(X0,X1) = nil
| ~ ssList(X0)
| ~ ssList(X1)
| nil != X1
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f380,plain,
! [U,W] :
( segmentP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ) ),
inference(miniscoping,[status(thm)],[f152]) ).
fof(f381,plain,
! [X0,X1,X2] :
( segmentP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f411,plain,
! [X0,X1,X2,X3] :
( segmentP(app(app(X3,X0),X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
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,
( ~ strictorderedP(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(f470,plain,
( ~ sQ2_spl
| ssItem(sk5) ),
inference(component_clause,[status(thm)],[f469]) ).
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(f478,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(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
<=> strictorderedP(sk1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( sQ12_spl
| ~ strictorderedP(sk1) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f461,f510,f513]) ).
fof(f522,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f323]) ).
fof(f533,plain,
( app(nil,nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f368]) ).
fof(f534,plain,
( app(nil,nil) = nil
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f533]) ).
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(f546,plain,
segmentP(nil,nil),
inference(resolution,[status(thm)],[f262,f214]) ).
fof(f550,plain,
segmentP(sk2,sk2),
inference(resolution,[status(thm)],[f263,f438]) ).
fof(f551,plain,
segmentP(sk1,sk1),
inference(resolution,[status(thm)],[f263,f437]) ).
fof(f553,plain,
segmentP(sk3,nil),
inference(resolution,[status(thm)],[f439,f262]) ).
fof(f573,plain,
! [X0] :
( ~ sQ4_spl
| segmentP(X0,sk1)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f576,f262]) ).
fof(f575,plain,
( ~ sQ4_spl
| strictorderedP(sk1) ),
inference(backward_demodulation,[status(thm)],[f576,f209]) ).
fof(f576,plain,
( ~ sQ4_spl
| nil = sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f477]) ).
fof(f609,plain,
( ~ sQ8_spl
| app(app(sk6,sk3),sk7) = sk2 ),
inference(forward_demodulation,[status(thm)],[f441,f493]) ).
fof(f628,plain,
( ~ sQ4_spl
| sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f575,f515]) ).
fof(f629,plain,
( ~ sQ4_spl
| sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f628]) ).
fof(f634,plain,
( ~ sQ7_spl
| cons(sk5,nil) = sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f489]) ).
fof(f659,plain,
( sQ4_spl
| nil != sk1 ),
inference(forward_demodulation,[status(thm)],[f442,f478]) ).
fof(f660,plain,
( ~ sQ8_spl
| app(app(sk6,sk1),sk7) = sk2 ),
inference(forward_demodulation,[status(thm)],[f442,f609]) ).
fof(f661,plain,
( nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f546,f287]) ).
fof(f662,definition,
( sQ13_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f664,plain,
( sQ13_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f662]) ).
fof(f665,definition,
( sQ14_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f661,f662,f665]) ).
fof(f669,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f664,f214]) ).
fof(f670,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f669]) ).
fof(f686,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f522,f214]) ).
fof(f690,plain,
( ~ sQ2_spl
| strictorderedP(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f686,f470]) ).
fof(f696,plain,
( ~ sQ2_spl
| ~ sQ7_spl
| strictorderedP(sk1) ),
inference(forward_demodulation,[status(thm)],[f634,f690]) ).
fof(f731,plain,
! [X0] :
( nil = sk1
| ~ ssList(X0)
| app(X0,sk1) != nil ),
inference(resolution,[status(thm)],[f336,f437]) ).
fof(f747,definition,
! [X0] :
( sQ16_spl
<=> ( ~ ssList(X0)
| app(X0,sk1) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f750,definition,
( sQ17_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f751,plain,
( ~ sQ17_spl
| nil = sk1 ),
inference(component_clause,[status(thm)],[f750]) ).
fof(f753,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f731,f747,f750]) ).
fof(f853,plain,
( ~ sQ4_spl
| segmentP(sk2,sk1) ),
inference(resolution,[status(thm)],[f573,f438]) ).
fof(f854,plain,
( ~ sQ4_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f853,f512]) ).
fof(f855,plain,
( ~ sQ4_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f854]) ).
fof(f906,plain,
( sk2 = sk2
| ~ ssList(sk2)
| ~ ssList(sk2)
| ~ segmentP(sk2,sk2) ),
inference(resolution,[status(thm)],[f550,f346]) ).
fof(f907,definition,
( sQ26_spl
<=> segmentP(sk2,sk2) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f909,plain,
( sQ26_spl
| ~ segmentP(sk2,sk2) ),
inference(component_clause,[status(thm)],[f907]) ).
fof(f910,definition,
( sQ27_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( sQ27_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f910]) ).
fof(f913,definition,
( sQ28_spl
<=> sk2 = sk2 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f916,plain,
( sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f906,f907,f910,f913]) ).
fof(f917,plain,
( sk1 = sk1
| ~ ssList(sk1)
| ~ ssList(sk1)
| ~ segmentP(sk1,sk1) ),
inference(resolution,[status(thm)],[f551,f346]) ).
fof(f918,definition,
( sQ29_spl
<=> segmentP(sk1,sk1) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f920,plain,
( sQ29_spl
| ~ segmentP(sk1,sk1) ),
inference(component_clause,[status(thm)],[f918]) ).
fof(f921,definition,
( sQ30_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ30_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f924,definition,
( sQ31_spl
<=> sk1 = sk1 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f927,plain,
( sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f917,f918,f921,f924]) ).
fof(f928,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f437]) ).
fof(f929,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f928]) ).
fof(f930,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f920,f551]) ).
fof(f931,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f930]) ).
fof(f934,plain,
segmentP(sk1,nil),
inference(forward_demodulation,[status(thm)],[f442,f553]) ).
fof(f935,plain,
( nil = sk1
| ~ ssList(nil)
| ~ ssList(sk1)
| ~ segmentP(nil,sk1) ),
inference(resolution,[status(thm)],[f934,f346]) ).
fof(f936,definition,
( sQ32_spl
<=> segmentP(nil,sk1) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f939,plain,
( sQ17_spl
| ~ sQ13_spl
| ~ sQ30_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f935,f936,f921,f662,f750]) ).
fof(f940,plain,
( ~ sQ17_spl
| sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f751,f659]) ).
fof(f941,plain,
( ~ sQ17_spl
| sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f940]) ).
fof(f965,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f912,f438]) ).
fof(f966,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f965]) ).
fof(f967,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f909,f550]) ).
fof(f968,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f967]) ).
fof(f1266,plain,
( sQ12_spl
| ~ sQ2_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f696]) ).
fof(f1267,plain,
( sQ12_spl
| ~ sQ2_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f1266]) ).
fof(f1268,definition,
( sQ35_spl
<=> app(nil,nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
( sQ35_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f534,f662,f1268]) ).
fof(f1272,plain,
! [X0] :
( segmentP(sk1,X0)
| ~ ssList(sk1)
| ~ ssList(sk1)
| ~ ssList(X0)
| ~ segmentP(sk1,X0) ),
inference(resolution,[status(thm)],[f381,f551]) ).
fof(f1273,plain,
! [X0] :
( segmentP(sk2,X0)
| ~ ssList(sk2)
| ~ ssList(sk2)
| ~ ssList(X0)
| ~ segmentP(sk2,X0) ),
inference(resolution,[status(thm)],[f381,f550]) ).
fof(f1274,definition,
! [X0] :
( sQ36_spl
<=> ( segmentP(sk1,X0)
| ~ ssList(X0)
| ~ segmentP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1277,plain,
( ~ sQ30_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1272,f1274,f921]) ).
fof(f1278,definition,
! [X0] :
( sQ37_spl
<=> ( segmentP(sk2,X0)
| ~ ssList(X0)
| ~ segmentP(sk2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1281,plain,
( ~ sQ27_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1273,f1278,f910]) ).
fof(f1472,plain,
( nil = sk1
| ssList(tl(sk1)) ),
inference(resolution,[status(thm)],[f282,f437]) ).
fof(f1488,definition,
( sQ42_spl
<=> ssList(tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1491,plain,
( sQ17_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f1472,f1488,f750]) ).
fof(f1524,plain,
( nil = sk1
| ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f283,f437]) ).
fof(f1540,definition,
( sQ47_spl
<=> ssItem(hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1543,plain,
( sQ17_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1524,f1540,f750]) ).
fof(f1743,plain,
! [X0,X1] :
( segmentP(app(app(X1,sk1),X0),sk1)
| ~ ssList(sk1)
| ~ ssList(sk1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f411,f551]) ).
fof(f1744,plain,
! [X0,X1] :
( segmentP(app(app(X1,sk2),X0),sk2)
| ~ ssList(sk2)
| ~ ssList(sk2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f411,f550]) ).
fof(f1745,definition,
! [X0,X1] :
( sQ55_spl
<=> ( segmentP(app(app(X1,sk1),X0),sk1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1748,plain,
( ~ sQ30_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1743,f1745,f921]) ).
fof(f1749,definition,
! [X0,X1] :
( sQ56_spl
<=> ( segmentP(app(app(X1,sk2),X0),sk2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1752,plain,
( ~ sQ27_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1744,f1749,f910]) ).
fof(f1950,plain,
( ~ sQ8_spl
| segmentP(app(app(sk6,sk1),sk7),sk1)
| ~ ssList(sk2)
| ~ ssList(sk1)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f660,f535]) ).
fof(f1953,definition,
( sQ82_spl
<=> segmentP(app(app(sk6,sk1),sk7),sk1) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1954,plain,
( ~ sQ82_spl
| segmentP(app(app(sk6,sk1),sk7),sk1) ),
inference(component_clause,[status(thm)],[f1953]) ).
fof(f1956,plain,
( ~ sQ8_spl
| sQ82_spl
| ~ sQ27_spl
| ~ sQ30_spl
| ~ sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1950,f484,f480,f921,f910,f1953,f492]) ).
fof(f1962,plain,
( ~ sQ82_spl
| ~ sQ8_spl
| segmentP(sk2,sk1) ),
inference(forward_demodulation,[status(thm)],[f660,f1954]) ).
fof(f1963,plain,
( ~ sQ82_spl
| ~ sQ8_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1962,f512]) ).
fof(f1964,plain,
( ~ sQ82_spl
| ~ sQ8_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1963]) ).
fof(f1965,plain,
$false,
inference(sat_refutation,[status(thm)],[f479,f504,f505,f506,f507,f516,f629,f668,f670,f753,f855,f916,f927,f929,f931,f939,f941,f966,f968,f1267,f1271,f1277,f1281,f1491,f1543,f1748,f1752,f1956,f1964]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC346-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:18:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.44 % Refutation found
% 0.09/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.46 % Elapsed time: 0.087260 seconds
% 0.09/0.46 % CPU time: 0.437723 seconds
% 0.09/0.46 % Total memory used: 83.673 MB
% 0.09/0.46 % Net memory used: 83.229 MB
%------------------------------------------------------------------------------