%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR077+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 191.46s 30.09s
% Output : CNFRefutation 192.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 50 ( 11 unt; 6 def)
% Number of atoms : 143 ( 39 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 148 ( 55 ~; 59 |; 22 &)
% ( 8 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-2 aty)
% Number of functors : 12 ( 9 usr; 9 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f3368,axiom,
s__instance(s__NumberE,s__PositiveRealNumber),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f7218,axiom,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7219,conjecture,
~ s__instance(s__Number3_1,s__NegativeRealNumber),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7220,negated_conjecture,
~ ~ s__instance(s__Number3_1,s__NegativeRealNumber),
inference(negated_conjecture,[status(cth)],[f7219]) ).
fof(f13206,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(f13207,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,f13206]) ).
fof(f13208,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)],[f13207]) ).
fof(f13209,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)],[f13208]) ).
fof(f13214,plain,
! [X0,X1] :
( X0 != X1
| ~ s__instance(X0,s__NonnegativeRealNumber)
| sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f13209]) ).
fof(f13440,plain,
s__instance(s__NumberE,s__PositiveRealNumber),
inference(cnf_transformation,[status(thm)],[f3368]) ).
fof(f13493,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(f13494,plain,
! [X0] :
( "0" = s__SignumFn(X0)
| ~ s__instance(X0,s__NonnegativeRealNumber)
| s__SignumFn(X0) = "1"
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[status(thm)],[f13493]) ).
fof(f13497,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(f13498,plain,
! [X0] :
( ~ s__instance(X0,s__NegativeRealNumber)
| "-1" = s__SignumFn(X0)
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[status(thm)],[f13497]) ).
fof(f19220,plain,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
inference(cnf_transformation,[status(thm)],[f7218]) ).
fof(f19221,plain,
s__instance(s__Number3_1,s__NegativeRealNumber),
inference(cnf_transformation,[status(thm)],[f7220]) ).
fof(f19294,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)],[f13206]) ).
fof(f19295,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)],[f19294]) ).
fof(f19298,plain,
! [X0,X1] :
( s__instance(X1,s__RealNumber)
| ~ sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f19295]) ).
fof(f19721,plain,
! [X0] :
( ~ s__instance(X0,s__NonnegativeRealNumber)
| sP9_prd(X0,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f13214]) ).
fof(f25810,plain,
sP9_prd(s__Number3_1,s__Number3_1),
inference(resolution,[status(thm)],[f19721,f19220]) ).
fof(f25820,definition,
( sQ449_spl
<=> s__instance(s__Number3_1,s__RealNumber) ),
introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition]) ).
fof(f25822,plain,
( sQ449_spl
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(component_clause,[status(thm)],[f25820]) ).
fof(f25828,plain,
! [X0] :
( sQ449_spl
| ~ sP9_prd(X0,s__Number3_1) ),
inference(resolution,[status(thm)],[f25822,f19298]) ).
fof(f26818,plain,
( "0" = s__SignumFn(s__Number3_1)
| s__SignumFn(s__Number3_1) = "1"
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(resolution,[status(thm)],[f13494,f19220]) ).
fof(f26820,definition,
( sQ624_spl
<=> s__SignumFn(s__Number3_1) = "1" ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f26821,plain,
( ~ sQ624_spl
| "1" = s__SignumFn(s__Number3_1) ),
inference(component_clause,[status(thm)],[f26820]) ).
fof(f26823,definition,
( sQ625_spl
<=> "0" = s__SignumFn(s__Number3_1) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f26824,plain,
( ~ sQ625_spl
| "0" = s__SignumFn(s__Number3_1) ),
inference(component_clause,[status(thm)],[f26823]) ).
fof(f26826,plain,
( sQ625_spl
| sQ624_spl
| ~ sQ449_spl ),
inference(split_clause,[status(thm)],[f26818,f25820,f26820,f26823]) ).
fof(f26831,plain,
( sQ449_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f25810,f25828]) ).
fof(f26832,plain,
sQ449_spl,
inference(contradiction_clause,[status(thm)],[f26831]) ).
fof(f26899,plain,
( "-1" = s__SignumFn(s__Number3_1)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(resolution,[status(thm)],[f13498,f19221]) ).
fof(f26902,definition,
( sQ638_spl
<=> "-1" = s__SignumFn(s__Number3_1) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f26903,plain,
( ~ sQ638_spl
| s__SignumFn(s__Number3_1) = "-1" ),
inference(component_clause,[status(thm)],[f26902]) ).
fof(f26905,plain,
( sQ638_spl
| ~ sQ449_spl ),
inference(split_clause,[status(thm)],[f26899,f25820,f26902]) ).
fof(f26908,plain,
( ~ sQ638_spl
| ~ sQ624_spl
| "-1" = "1" ),
inference(forward_demodulation,[status(thm)],[f26821,f26903]) ).
fof(f26909,plain,
( ~ sQ638_spl
| ~ sQ624_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f26908]) ).
fof(f26910,plain,
( ~ sQ638_spl
| ~ sQ624_spl ),
inference(contradiction_clause,[status(thm)],[f26909]) ).
fof(f26953,definition,
( sQ647_spl
<=> s__instance(s__NumberE,s__PositiveRealNumber) ),
introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition]) ).
fof(f26955,plain,
( sQ647_spl
| ~ s__instance(s__NumberE,s__PositiveRealNumber) ),
inference(component_clause,[status(thm)],[f26953]) ).
fof(f26961,plain,
( sQ647_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26955,f13440]) ).
fof(f26962,plain,
sQ647_spl,
inference(contradiction_clause,[status(thm)],[f26961]) ).
fof(f26963,plain,
( ~ sQ638_spl
| ~ sQ625_spl
| "0" = "-1" ),
inference(backward_demodulation,[status(thm)],[f26824,f26903]) ).
fof(f26964,plain,
( ~ sQ638_spl
| ~ sQ625_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f26963]) ).
fof(f26965,plain,
( ~ sQ638_spl
| ~ sQ625_spl ),
inference(contradiction_clause,[status(thm)],[f26964]) ).
fof(f26966,plain,
$false,
inference(sat_refutation,[status(thm)],[f26826,f26832,f26905,f26910,f26962,f26965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR077+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.45 % Computer : n006.cluster.edu
% 0.17/5.45 % Model : x86_64 x86_64
% 0.17/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.45 % Memory : 8046.5625MB
% 0.17/5.45 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Mon Sep 21 14:48:02 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.21/5.89 % Drodi V4.1.1
% 191.46/30.09 % Refutation found
% 191.46/30.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 191.46/30.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.85/30.24 % Elapsed time: 24.760738 seconds
% 23.85/30.24 % CPU time: 192.704868 seconds
% 23.85/30.24 % Total memory used: 860.098 MB
% 23.85/30.24 % Net memory used: 822.670 MB
%------------------------------------------------------------------------------