%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR077+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 12:13:28 PM UTC 2026
% Result : Theorem 84.98s 11.89s
% Output : CNFRefutation 86.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 13
% Syntax : Number of formulae : 53 ( 10 unt; 8 def)
% Number of atoms : 154 ( 40 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 162 ( 61 ~; 65 |; 22 &)
% ( 10 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 10 ( 7 usr; 7 con; 0-2 aty)
% Number of variables : 30 ( 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4433,axiom,
! [V__NUMBER2,V__NUMBER1] :
( ( s__instance(V__NUMBER2,s__RealNumber)
& s__instance(V__NUMBER1,s__RealNumber)
& s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2 )
<=> ( ( V__NUMBER2 = minus("0",V__NUMBER1)
& s__instance(V__NUMBER1,s__NegativeRealNumber) )
| ( V__NUMBER1 = V__NUMBER2
& s__instance(V__NUMBER1,s__NonnegativeRealNumber) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4596,axiom,
! [V__NUMBER] :
( s__instance(V__NUMBER,s__RealNumber)
=> ( s__instance(V__NUMBER,s__NonnegativeRealNumber)
=> ( s__SignumFn(V__NUMBER) = "0"
| s__SignumFn(V__NUMBER) = "1" ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4598,axiom,
! [V__NUMBER] :
( s__instance(V__NUMBER,s__RealNumber)
=> ( s__instance(V__NUMBER,s__NegativeRealNumber)
=> s__SignumFn(V__NUMBER) = "-1" ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37982,axiom,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37983,conjecture,
~ s__instance(s__Number3_1,s__NegativeRealNumber),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37984,negated_conjecture,
~ ~ s__instance(s__Number3_1,s__NegativeRealNumber),
inference(negated_conjecture,[status(cth)],[f37983]) ).
fof(f46397,definition,
! [V__NUMBER2,V__NUMBER1] :
( sP14_prd(V__NUMBER1,V__NUMBER2)
<=> ( s__instance(V__NUMBER2,s__RealNumber)
& s__instance(V__NUMBER1,s__RealNumber)
& s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2 ) ),
introduced(definition,[new_symbols(definition,[sP14_prd])],[]) ).
fof(f46398,plain,
! [V__NUMBER2,V__NUMBER1] :
( sP14_prd(V__NUMBER1,V__NUMBER2)
<=> ( ( V__NUMBER2 = minus("0",V__NUMBER1)
& s__instance(V__NUMBER1,s__NegativeRealNumber) )
| ( V__NUMBER1 = V__NUMBER2
& s__instance(V__NUMBER1,s__NonnegativeRealNumber) ) ) ),
inference(formula_renaming,[status(thm)],[f4433,f46397]) ).
fof(f46399,plain,
! [V__NUMBER2,V__NUMBER1] :
( ( ( ( V__NUMBER2 != minus("0",V__NUMBER1)
| ~ s__instance(V__NUMBER1,s__NegativeRealNumber) )
& ( V__NUMBER1 != V__NUMBER2
| ~ s__instance(V__NUMBER1,s__NonnegativeRealNumber) ) )
| sP14_prd(V__NUMBER1,V__NUMBER2) )
& ( ( V__NUMBER2 = minus("0",V__NUMBER1)
& s__instance(V__NUMBER1,s__NegativeRealNumber) )
| ( V__NUMBER1 = V__NUMBER2
& s__instance(V__NUMBER1,s__NonnegativeRealNumber) )
| ~ sP14_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(NNF_transformation,[status(thm)],[f46398]) ).
fof(f46400,plain,
( ! [V__NUMBER2,V__NUMBER1] :
( ( ( V__NUMBER2 != minus("0",V__NUMBER1)
| ~ s__instance(V__NUMBER1,s__NegativeRealNumber) )
& ( V__NUMBER1 != V__NUMBER2
| ~ s__instance(V__NUMBER1,s__NonnegativeRealNumber) ) )
| sP14_prd(V__NUMBER1,V__NUMBER2) )
& ! [V__NUMBER2,V__NUMBER1] :
( ( V__NUMBER2 = minus("0",V__NUMBER1)
& s__instance(V__NUMBER1,s__NegativeRealNumber) )
| ( V__NUMBER1 = V__NUMBER2
& s__instance(V__NUMBER1,s__NonnegativeRealNumber) )
| ~ sP14_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(miniscoping,[status(thm)],[f46399]) ).
fof(f46405,plain,
! [X0,X1] :
( X0 != X1
| ~ s__instance(X0,s__NonnegativeRealNumber)
| sP14_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f46400]) ).
fof(f46684,plain,
! [V__NUMBER] :
( s__SignumFn(V__NUMBER) = "0"
| s__SignumFn(V__NUMBER) = "1"
| ~ s__instance(V__NUMBER,s__NonnegativeRealNumber)
| ~ s__instance(V__NUMBER,s__RealNumber) ),
inference(pre_NNF_transformation,[status(thm)],[f4596]) ).
fof(f46685,plain,
! [X0] :
( s__SignumFn(X0) = "0"
| s__SignumFn(X0) = "1"
| ~ s__instance(X0,s__NonnegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[status(thm)],[f46684]) ).
fof(f46688,plain,
! [V__NUMBER] :
( s__SignumFn(V__NUMBER) = "-1"
| ~ s__instance(V__NUMBER,s__NegativeRealNumber)
| ~ s__instance(V__NUMBER,s__RealNumber) ),
inference(pre_NNF_transformation,[status(thm)],[f4598]) ).
fof(f46689,plain,
! [X0] :
( s__SignumFn(X0) = "-1"
| ~ s__instance(X0,s__NegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[status(thm)],[f46688]) ).
fof(f86670,plain,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
inference(cnf_transformation,[status(thm)],[f37982]) ).
fof(f86671,plain,
s__instance(s__Number3_1,s__NegativeRealNumber),
inference(cnf_transformation,[status(thm)],[f37984]) ).
fof(f86784,plain,
! [V__NUMBER2,V__NUMBER1] :
( ( ~ s__instance(V__NUMBER2,s__RealNumber)
| ~ s__instance(V__NUMBER1,s__RealNumber)
| s__AbsoluteValueFn(V__NUMBER1) != V__NUMBER2
| sP14_prd(V__NUMBER1,V__NUMBER2) )
& ( ( s__instance(V__NUMBER2,s__RealNumber)
& s__instance(V__NUMBER1,s__RealNumber)
& s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2 )
| ~ sP14_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(NNF_transformation,[status(thm)],[f46397]) ).
fof(f86785,plain,
( ! [V__NUMBER2,V__NUMBER1] :
( ~ s__instance(V__NUMBER2,s__RealNumber)
| ~ s__instance(V__NUMBER1,s__RealNumber)
| s__AbsoluteValueFn(V__NUMBER1) != V__NUMBER2
| sP14_prd(V__NUMBER1,V__NUMBER2) )
& ! [V__NUMBER2,V__NUMBER1] :
( ( s__instance(V__NUMBER2,s__RealNumber)
& s__instance(V__NUMBER1,s__RealNumber)
& s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2 )
| ~ sP14_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(miniscoping,[status(thm)],[f86784]) ).
fof(f86788,plain,
! [X0,X1] :
( s__instance(X1,s__RealNumber)
| ~ sP14_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f86785]) ).
fof(f87787,plain,
! [X0] :
( ~ s__instance(X0,s__NonnegativeRealNumber)
| sP14_prd(X0,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f46405]) ).
fof(f91755,plain,
( s__SignumFn(s__Number3_1) = "0"
| s__SignumFn(s__Number3_1) = "1"
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(resolution,[status(thm)],[f46685,f86670]) ).
fof(f91758,definition,
( sQ607_spl
<=> s__instance(s__Number3_1,s__RealNumber) ),
introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition]) ).
fof(f91760,plain,
( sQ607_spl
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(component_clause,[status(thm)],[f91758]) ).
fof(f91761,definition,
( sQ608_spl
<=> s__SignumFn(s__Number3_1) = "1" ),
introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition]) ).
fof(f91762,plain,
( ~ sQ608_spl
| s__SignumFn(s__Number3_1) = "1" ),
inference(component_clause,[status(thm)],[f91761]) ).
fof(f91764,definition,
( sQ609_spl
<=> s__SignumFn(s__Number3_1) = "0" ),
introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition]) ).
fof(f91765,plain,
( ~ sQ609_spl
| s__SignumFn(s__Number3_1) = "0" ),
inference(component_clause,[status(thm)],[f91764]) ).
fof(f91767,plain,
( sQ609_spl
| sQ608_spl
| ~ sQ607_spl ),
inference(split_clause,[status(thm)],[f91755,f91758,f91761,f91764]) ).
fof(f91772,plain,
! [X0] :
( sQ607_spl
| ~ sP14_prd(X0,s__Number3_1) ),
inference(resolution,[status(thm)],[f91760,f86788]) ).
fof(f91782,definition,
( sQ612_spl
<=> s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f91784,plain,
( sQ612_spl
| ~ s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
inference(component_clause,[status(thm)],[f91782]) ).
fof(f91786,definition,
( sQ613_spl
<=> s__instance(s__Number3_1,s__NegativeRealNumber) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f91788,plain,
( sQ613_spl
| ~ s__instance(s__Number3_1,s__NegativeRealNumber) ),
inference(component_clause,[status(thm)],[f91786]) ).
fof(f91790,plain,
( sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91788,f86671]) ).
fof(f91791,plain,
sQ613_spl,
inference(contradiction_clause,[status(thm)],[f91790]) ).
fof(f91792,plain,
( sQ612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91784,f86670]) ).
fof(f91793,plain,
sQ612_spl,
inference(contradiction_clause,[status(thm)],[f91792]) ).
fof(f91805,plain,
( sQ607_spl
| ~ s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
inference(resolution,[status(thm)],[f91772,f87787]) ).
fof(f91806,plain,
( sQ607_spl
| ~ sQ612_spl ),
inference(split_clause,[status(thm)],[f91805,f91782,f91758]) ).
fof(f91821,plain,
( ~ sQ608_spl
| "1" = "-1"
| ~ s__instance(s__Number3_1,s__NegativeRealNumber)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(paramodulation,[status(thm)],[f91762,f46689]) ).
fof(f91822,definition,
( sQ616_spl
<=> "1" = "-1" ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f91823,plain,
( ~ sQ616_spl
| "1" = "-1" ),
inference(component_clause,[status(thm)],[f91822]) ).
fof(f91825,plain,
( ~ sQ608_spl
| sQ616_spl
| ~ sQ613_spl
| ~ sQ607_spl ),
inference(split_clause,[status(thm)],[f91821,f91758,f91786,f91822,f91761]) ).
fof(f91826,plain,
( ~ sQ616_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f91823]) ).
fof(f91827,plain,
~ sQ616_spl,
inference(contradiction_clause,[status(thm)],[f91826]) ).
fof(f91829,plain,
( ~ sQ609_spl
| "0" = "-1"
| ~ s__instance(s__Number3_1,s__NegativeRealNumber)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(paramodulation,[status(thm)],[f91765,f46689]) ).
fof(f91830,definition,
( sQ617_spl
<=> "0" = "-1" ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f91831,plain,
( ~ sQ617_spl
| "0" = "-1" ),
inference(component_clause,[status(thm)],[f91830]) ).
fof(f91833,plain,
( ~ sQ609_spl
| sQ617_spl
| ~ sQ613_spl
| ~ sQ607_spl ),
inference(split_clause,[status(thm)],[f91829,f91758,f91786,f91830,f91764]) ).
fof(f91834,plain,
( ~ sQ617_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f91831]) ).
fof(f91835,plain,
~ sQ617_spl,
inference(contradiction_clause,[status(thm)],[f91834]) ).
fof(f91836,plain,
$false,
inference(sat_refutation,[status(thm)],[f91767,f91791,f91793,f91806,f91825,f91827,f91833,f91835]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR077+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n020.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 14:49:03 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.89/1.18 % Drodi V4.1.1
% 84.98/11.89 % Refutation found
% 84.98/11.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 84.98/11.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.61/12.21 % Elapsed time: 11.812282 seconds
% 3.61/12.21 % CPU time: 86.446110 seconds
% 3.61/12.21 % Total memory used: 1.950 GB
% 3.61/12.21 % Net memory used: 1.940 GB
%------------------------------------------------------------------------------