%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC373-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 : n018.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:59 PM UTC 2026
% Result : Unsatisfiable 2.88s 0.84s
% Output : CNFRefutation 2.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 19
% Syntax : Number of formulae : 63 ( 25 unt; 7 def)
% Number of atoms : 142 ( 15 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 152 ( 73 ~; 72 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 41 ( 41 !; 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(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(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(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(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(f188,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
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,
rearsegP(sk4,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
~ segmentP(sk2,sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f243,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f267,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f279,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f337,plain,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f399,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(f400,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)],[f399]) ).
fof(f426,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f427,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f428,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f429,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f430,plain,
rearsegP(sk4,sk3),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f431,plain,
~ segmentP(sk2,sk1),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f457,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)],[f400]) ).
fof(f470,plain,
~ segmentP(sk4,sk1),
inference(forward_demodulation,[status(thm)],[f428,f431]) ).
fof(f471,plain,
~ segmentP(sk4,sk3),
inference(forward_demodulation,[status(thm)],[f429,f470]) ).
fof(f504,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f506,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f517,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f506,f201]) ).
fof(f518,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f517]) ).
fof(f526,definition,
( sQ11_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f528,plain,
( sQ11_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f526]) ).
fof(f529,definition,
( sQ12_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( sQ12_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f549,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f531,f427]) ).
fof(f550,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f549]) ).
fof(f589,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f528,f426]) ).
fof(f590,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f797,plain,
app(sk4,nil) = sk4,
inference(resolution,[status(thm)],[f267,f427]) ).
fof(f1920,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X1,X2))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f279,f457]) ).
fof(f1937,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(app(X1,X2))
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1920]) ).
fof(f1938,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1937,f279]) ).
fof(f6457,plain,
( app(skaf46(sk4,sk3),sk3) = sk4
| ~ ssList(sk4)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f337,f430]) ).
fof(f6496,definition,
( sQ714_spl
<=> app(skaf46(sk4,sk3),sk3) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition]) ).
fof(f6497,plain,
( ~ sQ714_spl
| app(skaf46(sk4,sk3),sk3) = sk4 ),
inference(component_clause,[status(thm)],[f6496]) ).
fof(f6499,plain,
( sQ714_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f6457,f526,f529,f6496]) ).
fof(f6702,plain,
! [X0] :
( ~ sQ714_spl
| segmentP(app(sk4,X0),sk3)
| ~ ssList(sk3)
| ~ ssList(skaf46(sk4,sk3))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f6497,f1938]) ).
fof(f6709,definition,
( sQ734_spl
<=> ssList(skaf46(sk4,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f6711,plain,
( sQ734_spl
| ~ ssList(skaf46(sk4,sk3)) ),
inference(component_clause,[status(thm)],[f6709]) ).
fof(f6717,definition,
! [X0] :
( sQ736_spl
<=> ( segmentP(app(sk4,X0),sk3)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ736_spl])],[split_symbol_definition]) ).
fof(f6718,plain,
! [X0] :
( ~ sQ736_spl
| segmentP(app(sk4,X0),sk3)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f6717]) ).
fof(f6720,plain,
( ~ sQ714_spl
| ~ sQ11_spl
| ~ sQ734_spl
| sQ736_spl ),
inference(split_clause,[status(thm)],[f6702,f6717,f6709,f526,f6496]) ).
fof(f6742,plain,
( sQ734_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6711,f243]) ).
fof(f6743,plain,
sQ734_spl,
inference(contradiction_clause,[status(thm)],[f6742]) ).
fof(f6809,plain,
( ~ sQ736_spl
| segmentP(sk4,sk3)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f797,f6718]) ).
fof(f6818,definition,
( sQ747_spl
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[sQ747_spl])],[split_symbol_definition]) ).
fof(f6819,plain,
( ~ sQ747_spl
| segmentP(sk4,sk3) ),
inference(component_clause,[status(thm)],[f6818]) ).
fof(f6821,plain,
( ~ sQ736_spl
| sQ747_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f6809,f504,f6818,f6717]) ).
fof(f6822,plain,
( ~ sQ747_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6819,f471]) ).
fof(f6823,plain,
~ sQ747_spl,
inference(contradiction_clause,[status(thm)],[f6822]) ).
fof(f6824,plain,
$false,
inference(sat_refutation,[status(thm)],[f518,f550,f590,f6499,f6720,f6743,f6821,f6823]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC373-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 08:21:14 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 2.88/0.84 % Refutation found
% 2.88/0.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.88/0.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.88/0.85 % Elapsed time: 0.469889 seconds
% 2.88/0.85 % CPU time: 3.339942 seconds
% 2.88/0.85 % Total memory used: 157.865 MB
% 2.88/0.85 % Net memory used: 152.902 MB
%------------------------------------------------------------------------------