%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR077+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 47.76s 6.77s
% Output : CNFRefutation 47.76s
% 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(f3247,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/sandbox/benchmark/theBenchmark.p') ).
fof(f3410,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/sandbox/benchmark/theBenchmark.p') ).
fof(f3412,axiom,
! [V__NUMBER] :
( s__instance(V__NUMBER,s__RealNumber)
=> ( s__instance(V__NUMBER,s__NegativeRealNumber)
=> s__SignumFn(V__NUMBER) = "-1" ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14788,axiom,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14789,conjecture,
~ s__instance(s__Number3_1,s__NegativeRealNumber),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14790,negated_conjecture,
~ ~ s__instance(s__Number3_1,s__NegativeRealNumber),
inference(negated_conjecture,[status(cth)],[f14789]) ).
fof(f20776,definition,
! [V__NUMBER2,V__NUMBER1] :
( sP9_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,[sP9_prd])],[]) ).
fof(f20777,plain,
! [V__NUMBER2,V__NUMBER1] :
( sP9_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)],[f3247,f20776]) ).
fof(f20778,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) ) )
| sP9_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) )
| ~ sP9_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(NNF_transformation,[status(thm)],[f20777]) ).
fof(f20779,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) ) )
| sP9_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) )
| ~ sP9_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(miniscoping,[status(thm)],[f20778]) ).
fof(f20784,plain,
! [X0,X1] :
( X0 != X1
| ~ s__instance(X0,s__NonnegativeRealNumber)
| sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20779]) ).
fof(f21063,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)],[f3410]) ).
fof(f21064,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)],[f21063]) ).
fof(f21067,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)],[f3412]) ).
fof(f21068,plain,
! [X0] :
( s__SignumFn(X0) = "-1"
| ~ s__instance(X0,s__NegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[status(thm)],[f21067]) ).
fof(f34360,plain,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
inference(cnf_transformation,[status(thm)],[f14788]) ).
fof(f34361,plain,
s__instance(s__Number3_1,s__NegativeRealNumber),
inference(cnf_transformation,[status(thm)],[f14790]) ).
fof(f34434,plain,
! [V__NUMBER2,V__NUMBER1] :
( ( ~ s__instance(V__NUMBER2,s__RealNumber)
| ~ s__instance(V__NUMBER1,s__RealNumber)
| s__AbsoluteValueFn(V__NUMBER1) != V__NUMBER2
| sP9_prd(V__NUMBER1,V__NUMBER2) )
& ( ( s__instance(V__NUMBER2,s__RealNumber)
& s__instance(V__NUMBER1,s__RealNumber)
& s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2 )
| ~ sP9_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(NNF_transformation,[status(thm)],[f20776]) ).
fof(f34435,plain,
( ! [V__NUMBER2,V__NUMBER1] :
( ~ s__instance(V__NUMBER2,s__RealNumber)
| ~ s__instance(V__NUMBER1,s__RealNumber)
| s__AbsoluteValueFn(V__NUMBER1) != V__NUMBER2
| sP9_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 )
| ~ sP9_prd(V__NUMBER1,V__NUMBER2) ) ),
inference(miniscoping,[status(thm)],[f34434]) ).
fof(f34438,plain,
! [X0,X1] :
( s__instance(X1,s__RealNumber)
| ~ sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f34435]) ).
fof(f34794,plain,
! [X0] :
( ~ s__instance(X0,s__NonnegativeRealNumber)
| sP9_prd(X0,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f20784]) ).
fof(f38029,plain,
( s__SignumFn(s__Number3_1) = "0"
| s__SignumFn(s__Number3_1) = "1"
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(resolution,[status(thm)],[f21064,f34360]) ).
fof(f38032,definition,
( sQ379_spl
<=> s__instance(s__Number3_1,s__RealNumber) ),
introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition]) ).
fof(f38034,plain,
( sQ379_spl
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(component_clause,[status(thm)],[f38032]) ).
fof(f38035,definition,
( sQ380_spl
<=> s__SignumFn(s__Number3_1) = "1" ),
introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition]) ).
fof(f38036,plain,
( ~ sQ380_spl
| s__SignumFn(s__Number3_1) = "1" ),
inference(component_clause,[status(thm)],[f38035]) ).
fof(f38038,definition,
( sQ381_spl
<=> s__SignumFn(s__Number3_1) = "0" ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f38039,plain,
( ~ sQ381_spl
| s__SignumFn(s__Number3_1) = "0" ),
inference(component_clause,[status(thm)],[f38038]) ).
fof(f38041,plain,
( sQ381_spl
| sQ380_spl
| ~ sQ379_spl ),
inference(split_clause,[status(thm)],[f38029,f38032,f38035,f38038]) ).
fof(f38056,plain,
! [X0] :
( sQ379_spl
| ~ sP9_prd(X0,s__Number3_1) ),
inference(resolution,[status(thm)],[f38034,f34438]) ).
fof(f38066,definition,
( sQ386_spl
<=> s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f38068,plain,
( sQ386_spl
| ~ s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
inference(component_clause,[status(thm)],[f38066]) ).
fof(f38070,definition,
( sQ387_spl
<=> s__instance(s__Number3_1,s__NegativeRealNumber) ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f38072,plain,
( sQ387_spl
| ~ s__instance(s__Number3_1,s__NegativeRealNumber) ),
inference(component_clause,[status(thm)],[f38070]) ).
fof(f38074,plain,
( sQ387_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38072,f34361]) ).
fof(f38075,plain,
sQ387_spl,
inference(contradiction_clause,[status(thm)],[f38074]) ).
fof(f38076,plain,
( sQ386_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38068,f34360]) ).
fof(f38077,plain,
sQ386_spl,
inference(contradiction_clause,[status(thm)],[f38076]) ).
fof(f38078,plain,
( ~ sQ381_spl
| "0" = "-1"
| ~ s__instance(s__Number3_1,s__NegativeRealNumber)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(paramodulation,[status(thm)],[f38039,f21068]) ).
fof(f38079,definition,
( sQ388_spl
<=> "0" = "-1" ),
introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition]) ).
fof(f38080,plain,
( ~ sQ388_spl
| "0" = "-1" ),
inference(component_clause,[status(thm)],[f38079]) ).
fof(f38082,plain,
( ~ sQ381_spl
| sQ388_spl
| ~ sQ387_spl
| ~ sQ379_spl ),
inference(split_clause,[status(thm)],[f38078,f38032,f38070,f38079,f38038]) ).
fof(f38083,plain,
( ~ sQ388_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f38080]) ).
fof(f38084,plain,
~ sQ388_spl,
inference(contradiction_clause,[status(thm)],[f38083]) ).
fof(f38085,plain,
( ~ sQ380_spl
| "1" = "-1"
| ~ s__instance(s__Number3_1,s__NegativeRealNumber)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(paramodulation,[status(thm)],[f38036,f21068]) ).
fof(f38086,definition,
( sQ389_spl
<=> "1" = "-1" ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f38087,plain,
( ~ sQ389_spl
| "1" = "-1" ),
inference(component_clause,[status(thm)],[f38086]) ).
fof(f38089,plain,
( ~ sQ380_spl
| sQ389_spl
| ~ sQ387_spl
| ~ sQ379_spl ),
inference(split_clause,[status(thm)],[f38085,f38032,f38070,f38086,f38035]) ).
fof(f38090,plain,
( ~ sQ389_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f38087]) ).
fof(f38091,plain,
~ sQ389_spl,
inference(contradiction_clause,[status(thm)],[f38090]) ).
fof(f38100,plain,
( sQ379_spl
| ~ s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
inference(resolution,[status(thm)],[f38056,f34794]) ).
fof(f38101,plain,
( sQ379_spl
| ~ sQ386_spl ),
inference(split_clause,[status(thm)],[f38100,f38066,f38032]) ).
fof(f38102,plain,
$false,
inference(sat_refutation,[status(thm)],[f38041,f38075,f38077,f38082,f38084,f38089,f38091,f38101]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR077+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 14:48:33 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.47/0.72 % Drodi V4.1.1
% 47.76/6.77 % Refutation found
% 47.76/6.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 47.76/6.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.85/7.10 % Elapsed time: 6.712325 seconds
% 4.85/7.10 % CPU time: 49.043143 seconds
% 4.85/7.10 % Total memory used: 927.823 MB
% 4.85/7.10 % Net memory used: 910.782 MB
%------------------------------------------------------------------------------