%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC122-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 : n007.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:03 PM UTC 2026
% Result : Unsatisfiable 4.63s 1.07s
% Output : CNFRefutation 4.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 32
% Syntax : Number of formulae : 104 ( 25 unt; 17 def)
% Number of atoms : 244 ( 16 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 258 ( 118 ~; 123 |; 0 &)
% ( 17 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 18 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 40 ( 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U,V] : ssList(skaf46(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ ssList(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(f131,axiom,
! [U,V] :
( app(skaf46(U,V),V) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ rearsegP(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(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(f194,negated_conjecture,
( ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( rearsegP(sk4,sk3)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f246,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f253,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f270,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f271,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f340,plain,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f401,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(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(f435,plain,
( ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f436,plain,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f437,plain,
( rearsegP(sk4,sk3)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f452,definition,
( sQ4_spl
<=> neq(sk1,nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( sQ4_spl
| ~ neq(sk1,nil) ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f455,definition,
( sQ5_spl
<=> segmentP(sk2,sk1) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ5_spl
| ~ segmentP(sk2,sk1) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,plain,
( ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f435,f452,f455]) ).
fof(f459,definition,
( sQ6_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ6_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
( sQ7_spl
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ7_spl
| neq(sk3,nil) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f436,f459,f462]) ).
fof(f466,definition,
( sQ8_spl
<=> rearsegP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ8_spl
| rearsegP(sk4,sk3) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,plain,
( sQ8_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f437,f459,f466]) ).
fof(f503,plain,
( sQ6_spl
| ~ neq(sk2,nil) ),
inference(forward_demodulation,[status(thm)],[f431,f461]) ).
fof(f504,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f503,f433]) ).
fof(f505,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f504]) ).
fof(f554,plain,
( ~ sQ7_spl
| neq(sk1,nil) ),
inference(forward_demodulation,[status(thm)],[f432,f463]) ).
fof(f556,plain,
( ~ sQ8_spl
| rearsegP(sk2,sk3) ),
inference(forward_demodulation,[status(thm)],[f431,f467]) ).
fof(f557,plain,
( ~ sQ8_spl
| rearsegP(sk2,sk1) ),
inference(forward_demodulation,[status(thm)],[f432,f556]) ).
fof(f596,definition,
( sQ14_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( sQ14_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f611,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f204]) ).
fof(f612,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f611]) ).
fof(f649,definition,
( sQ19_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f651,plain,
( sQ19_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,definition,
( sQ20_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f654,plain,
( sQ20_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f652]) ).
fof(f703,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f428,f654]) ).
fof(f704,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f703]) ).
fof(f705,plain,
( sQ4_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f454,f554]) ).
fof(f706,plain,
( sQ4_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f705]) ).
fof(f774,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f427]) ).
fof(f775,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f774]) ).
fof(f1002,plain,
app(nil,sk1) = sk1,
inference(resolution,[status(thm)],[f271,f427]) ).
fof(f1057,plain,
! [X0,X1] :
( segmentP(app(sk1,X1),X0)
| ~ ssList(sk1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ segmentP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f1002,f401]) ).
fof(f1061,definition,
! [X0,X1] :
( sQ54_spl
<=> ( segmentP(app(sk1,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
! [X0,X1] :
( ~ sQ54_spl
| segmentP(app(sk1,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk1,X0) ),
inference(component_clause,[status(thm)],[f1061]) ).
fof(f1064,plain,
( ~ sQ19_spl
| ~ sQ14_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1057,f1061,f596,f649]) ).
fof(f1104,plain,
app(sk2,nil) = sk2,
inference(resolution,[status(thm)],[f270,f428]) ).
fof(f1121,plain,
app(sk1,nil) = sk1,
inference(resolution,[status(thm)],[f270,f427]) ).
fof(f1616,plain,
! [X0] :
( ~ sQ54_spl
| ~ ssList(sk1)
| segmentP(app(sk1,X0),sk1)
| ~ ssList(sk1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1062,f253]) ).
fof(f1621,definition,
! [X0] :
( sQ80_spl
<=> ( segmentP(app(sk1,X0),sk1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1622,plain,
! [X0] :
( ~ sQ80_spl
| segmentP(app(sk1,X0),sk1)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1621]) ).
fof(f1624,plain,
( ~ sQ54_spl
| ~ sQ19_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1616,f1621,f649,f1061]) ).
fof(f1783,plain,
( ~ sQ80_spl
| segmentP(sk1,sk1)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1121,f1622]) ).
fof(f1792,definition,
( sQ93_spl
<=> segmentP(sk1,sk1) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1795,plain,
( ~ sQ80_spl
| sQ93_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1783,f596,f1792,f1621]) ).
fof(f3630,plain,
( ~ sQ8_spl
| app(skaf46(sk2,sk1),sk1) = sk2
| ~ ssList(sk2)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f340,f557]) ).
fof(f3657,definition,
( sQ361_spl
<=> app(skaf46(sk2,sk1),sk1) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f3658,plain,
( ~ sQ361_spl
| app(skaf46(sk2,sk1),sk1) = sk2 ),
inference(component_clause,[status(thm)],[f3657]) ).
fof(f3660,plain,
( ~ sQ8_spl
| sQ361_spl
| ~ sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f3630,f649,f652,f3657,f466]) ).
fof(f3692,plain,
! [X0,X1] :
( ~ sQ361_spl
| segmentP(app(sk2,X1),X0)
| ~ ssList(sk1)
| ~ ssList(X0)
| ~ ssList(skaf46(sk2,sk1))
| ~ ssList(X1)
| ~ segmentP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f3658,f401]) ).
fof(f3695,definition,
( sQ364_spl
<=> ssList(skaf46(sk2,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ364_spl])],[split_symbol_definition]) ).
fof(f3697,plain,
( sQ364_spl
| ~ ssList(skaf46(sk2,sk1)) ),
inference(component_clause,[status(thm)],[f3695]) ).
fof(f3707,definition,
! [X0,X1] :
( sQ367_spl
<=> ( segmentP(app(sk2,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ367_spl])],[split_symbol_definition]) ).
fof(f3708,plain,
! [X0,X1] :
( ~ sQ367_spl
| segmentP(app(sk2,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk1,X0) ),
inference(component_clause,[status(thm)],[f3707]) ).
fof(f3710,plain,
( ~ sQ361_spl
| ~ sQ19_spl
| ~ sQ364_spl
| sQ367_spl ),
inference(split_clause,[status(thm)],[f3692,f3707,f3695,f649,f3657]) ).
fof(f3719,plain,
( sQ364_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3697,f246]) ).
fof(f3720,plain,
sQ364_spl,
inference(contradiction_clause,[status(thm)],[f3719]) ).
fof(f3729,definition,
( sQ370_spl
<=> ssList(skaf46(sk2,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition]) ).
fof(f3731,plain,
( sQ370_spl
| ~ ssList(skaf46(sk2,sk2)) ),
inference(component_clause,[status(thm)],[f3729]) ).
fof(f3742,plain,
( sQ370_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3731,f246]) ).
fof(f3743,plain,
sQ370_spl,
inference(contradiction_clause,[status(thm)],[f3742]) ).
fof(f3747,plain,
! [X0] :
( ~ sQ367_spl
| segmentP(sk2,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f1104,f3708]) ).
fof(f3750,definition,
! [X0] :
( sQ372_spl
<=> ( segmentP(sk2,X0)
| ~ ssList(X0)
| ~ segmentP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f3751,plain,
! [X0] :
( ~ sQ372_spl
| segmentP(sk2,X0)
| ~ ssList(X0)
| ~ segmentP(sk1,X0) ),
inference(component_clause,[status(thm)],[f3750]) ).
fof(f3753,plain,
( ~ sQ367_spl
| ~ sQ14_spl
| sQ372_spl ),
inference(split_clause,[status(thm)],[f3747,f3750,f596,f3707]) ).
fof(f3973,definition,
( sQ375_spl
<=> ssList(skaf46(sk1,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition]) ).
fof(f3975,plain,
( sQ375_spl
| ~ ssList(skaf46(sk1,sk1)) ),
inference(component_clause,[status(thm)],[f3973]) ).
fof(f3985,plain,
( sQ375_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3975,f246]) ).
fof(f3986,plain,
sQ375_spl,
inference(contradiction_clause,[status(thm)],[f3985]) ).
fof(f4002,plain,
( sQ5_spl
| ~ sQ372_spl
| ~ ssList(sk1)
| ~ segmentP(sk1,sk1) ),
inference(resolution,[status(thm)],[f3751,f457]) ).
fof(f4006,plain,
( sQ5_spl
| ~ sQ372_spl
| ~ sQ19_spl
| ~ sQ93_spl ),
inference(split_clause,[status(thm)],[f4002,f1792,f649,f3750,f455]) ).
fof(f4016,plain,
$false,
inference(sat_refutation,[status(thm)],[f458,f465,f469,f505,f612,f704,f706,f775,f1064,f1624,f1795,f3660,f3710,f3720,f3743,f3753,f3986,f4006]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC122-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:55:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 4.63/1.07 % Refutation found
% 4.63/1.07 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.63/1.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.63/1.10 % Elapsed time: 0.735384 seconds
% 4.63/1.10 % CPU time: 5.462170 seconds
% 4.63/1.10 % Total memory used: 181.015 MB
% 4.63/1.10 % Net memory used: 175.491 MB
%------------------------------------------------------------------------------