%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR077+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:15:02 PM UTC 2026
% Result : Theorem 161.45s 21.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR077+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.57 % Computer : n026.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Mon Sep 21 14:50:52 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.14/0.86 % Drodi V4.1.1
% 161.45/21.31 % Refutation found
% 161.45/21.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 161.45/21.31 % SZS output start CNFRefutation for theBenchmark
% 161.45/21.31 fof(f3247,axiom,(
% 161.45/21.31 (! [V__NUMBER2,V__NUMBER1] :( ( s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2& s__instance(V__NUMBER1,s__RealNumber)& s__instance(V__NUMBER2,s__RealNumber) )<=> ( ( s__instance(V__NUMBER1,s__NonnegativeRealNumber)& V__NUMBER1 = V__NUMBER2 )| ( s__instance(V__NUMBER1,s__NegativeRealNumber)& V__NUMBER2 = minus("0",V__NUMBER1) ) ) ) )),
% 161.45/21.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 161.45/21.31 fof(f3410,axiom,(
% 161.45/21.31 (! [V__NUMBER] :( s__instance(V__NUMBER,s__RealNumber)=> ( s__instance(V__NUMBER,s__NonnegativeRealNumber)=> ( s__SignumFn(V__NUMBER) = "1"| s__SignumFn(V__NUMBER) = "0" ) ) ) )),
% 161.45/21.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 161.45/21.31 fof(f3412,axiom,(
% 161.45/21.31 (! [V__NUMBER] :( s__instance(V__NUMBER,s__RealNumber)=> ( s__instance(V__NUMBER,s__NegativeRealNumber)=> s__SignumFn(V__NUMBER) = "-1" ) ) )),
% 161.45/21.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 161.45/21.31 fof(f7218,axiom,(
% 161.45/21.31 s__instance(s__Number3_1,s__NonnegativeRealNumber) ),
% 161.45/21.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 161.45/21.31 fof(f7219,conjecture,(
% 161.45/21.31 ~ s__instance(s__Number3_1,s__NegativeRealNumber) ),
% 161.45/21.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 161.45/21.31 fof(f7220,negated_conjecture,(
% 161.45/21.31 ~(~ s__instance(s__Number3_1,s__NegativeRealNumber) )),
% 161.45/21.31 inference(negated_conjecture,[status(cth)],[f7219])).
% 161.45/21.31 fof(f13206,definition,(
% 161.45/21.31 ![V__NUMBER2,V__NUMBER1]: (sP9_prd(V__NUMBER1,V__NUMBER2)<=>((s__AbsoluteValueFn(V__NUMBER1)=V__NUMBER2&s__instance(V__NUMBER1,s__RealNumber))&s__instance(V__NUMBER2,s__RealNumber)))),
% 161.45/21.31 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 161.45/21.31 fof(f13207,plain,(
% 161.45/21.31 ![V__NUMBER2,V__NUMBER1]: (sP9_prd(V__NUMBER1,V__NUMBER2)<=>((s__instance(V__NUMBER1,s__NonnegativeRealNumber)&V__NUMBER1=V__NUMBER2)|(s__instance(V__NUMBER1,s__NegativeRealNumber)&V__NUMBER2=minus("0",V__NUMBER1))))),
% 161.45/21.31 inference(formula_renaming,[status(thm)],[f3247,f13206])).
% 161.45/21.31 fof(f13208,plain,(
% 161.45/21.31 ![V__NUMBER2,V__NUMBER1]: ((~sP9_prd(V__NUMBER1,V__NUMBER2)|((s__instance(V__NUMBER1,s__NonnegativeRealNumber)&V__NUMBER1=V__NUMBER2)|(s__instance(V__NUMBER1,s__NegativeRealNumber)&V__NUMBER2=minus("0",V__NUMBER1))))&(sP9_prd(V__NUMBER1,V__NUMBER2)|((~s__instance(V__NUMBER1,s__NonnegativeRealNumber)|~V__NUMBER1=V__NUMBER2)&(~s__instance(V__NUMBER1,s__NegativeRealNumber)|~V__NUMBER2=minus("0",V__NUMBER1)))))),
% 161.45/21.31 inference(NNF_transformation,[status(thm)],[f13207])).
% 161.45/21.31 fof(f13209,plain,(
% 161.45/21.31 (![V__NUMBER2,V__NUMBER1]: (~sP9_prd(V__NUMBER1,V__NUMBER2)|((s__instance(V__NUMBER1,s__NonnegativeRealNumber)&V__NUMBER1=V__NUMBER2)|(s__instance(V__NUMBER1,s__NegativeRealNumber)&V__NUMBER2=minus("0",V__NUMBER1)))))&(![V__NUMBER2,V__NUMBER1]: (sP9_prd(V__NUMBER1,V__NUMBER2)|((~s__instance(V__NUMBER1,s__NonnegativeRealNumber)|~V__NUMBER1=V__NUMBER2)&(~s__instance(V__NUMBER1,s__NegativeRealNumber)|~V__NUMBER2=minus("0",V__NUMBER1)))))),
% 161.45/21.31 inference(miniscoping,[status(thm)],[f13208])).
% 161.45/21.31 fof(f13215,plain,(
% 161.45/21.31 ![X0,X1]: (sP9_prd(X0,X1)|~s__instance(X0,s__NegativeRealNumber)|~X1=minus("0",X0))),
% 161.45/21.31 inference(cnf_transformation,[status(thm)],[f13209])).
% 161.45/21.31 fof(f13493,plain,(
% 161.45/21.31 ![V__NUMBER]: (~s__instance(V__NUMBER,s__RealNumber)|(~s__instance(V__NUMBER,s__NonnegativeRealNumber)|(s__SignumFn(V__NUMBER)="1"|s__SignumFn(V__NUMBER)="0")))),
% 161.45/21.31 inference(pre_NNF_transformation,[status(thm)],[f3410])).
% 161.45/21.31 fof(f13494,plain,(
% 161.45/21.31 ![X0]: (~s__instance(X0,s__RealNumber)|~s__instance(X0,s__NonnegativeRealNumber)|s__SignumFn(X0)="1"|s__SignumFn(X0)="0")),
% 161.45/21.31 inference(cnf_transformation,[status(thm)],[f13493])).
% 161.45/21.31 fof(f13497,plain,(
% 161.45/21.31 ![V__NUMBER]: (~s__instance(V__NUMBER,s__RealNumber)|(~s__instance(V__NUMBER,s__NegativeRealNumber)|s__SignumFn(V__NUMBER)="-1"))),
% 161.45/21.31 inference(pre_NNF_transformation,[status(thm)],[f3412])).
% 161.45/21.31 fof(f13498,plain,(
% 161.45/21.31 ![X0]: (~s__instance(X0,s__RealNumber)|~s__instance(X0,s__NegativeRealNumber)|s__SignumFn(X0)="-1")),
% 161.45/21.31 inference(cnf_transformation,[status(thm)],[f13497])).
% 161.45/21.31 fof(f19220,plain,(
% 161.45/21.31 s__instance(s__Number3_1,s__NonnegativeRealNumber)),
% 88.08/21.43 inference(cnf_transformation,[status(thm)],[f7218])).
% 88.08/21.43 fof(f19221,plain,(
% 88.08/21.43 s__instance(s__Number3_1,s__NegativeRealNumber)),
% 88.08/21.43 inference(cnf_transformation,[status(thm)],[f7220])).
% 88.08/21.43 fof(f19294,plain,(
% 88.08/21.43 ![V__NUMBER2,V__NUMBER1]: ((~sP9_prd(V__NUMBER1,V__NUMBER2)|((s__AbsoluteValueFn(V__NUMBER1)=V__NUMBER2&s__instance(V__NUMBER1,s__RealNumber))&s__instance(V__NUMBER2,s__RealNumber)))&(sP9_prd(V__NUMBER1,V__NUMBER2)|((~s__AbsoluteValueFn(V__NUMBER1)=V__NUMBER2|~s__instance(V__NUMBER1,s__RealNumber))|~s__instance(V__NUMBER2,s__RealNumber))))),
% 88.08/21.43 inference(NNF_transformation,[status(thm)],[f13206])).
% 88.08/21.43 fof(f19295,plain,(
% 88.08/21.43 (![V__NUMBER2,V__NUMBER1]: (~sP9_prd(V__NUMBER1,V__NUMBER2)|((s__AbsoluteValueFn(V__NUMBER1)=V__NUMBER2&s__instance(V__NUMBER1,s__RealNumber))&s__instance(V__NUMBER2,s__RealNumber))))&(![V__NUMBER2,V__NUMBER1]: (sP9_prd(V__NUMBER1,V__NUMBER2)|((~s__AbsoluteValueFn(V__NUMBER1)=V__NUMBER2|~s__instance(V__NUMBER1,s__RealNumber))|~s__instance(V__NUMBER2,s__RealNumber))))),
% 88.08/21.43 inference(miniscoping,[status(thm)],[f19294])).
% 88.08/21.43 fof(f19297,plain,(
% 88.08/21.43 ![X0,X1]: (~sP9_prd(X0,X1)|s__instance(X0,s__RealNumber))),
% 88.08/21.43 inference(cnf_transformation,[status(thm)],[f19295])).
% 88.08/21.43 fof(f20119,plain,(
% 88.08/21.43 ![X0]: (sP9_prd(X0,minus("0",X0))|~s__instance(X0,s__NegativeRealNumber))),
% 88.08/21.43 inference(destructive_equality_resolution,[status(thm)],[f13215])).
% 88.08/21.43 fof(f22953,plain,(
% 88.08/21.43 sP9_prd(s__Number3_1,minus("0",s__Number3_1))),
% 88.08/21.43 inference(resolution,[status(thm)],[f20119,f19221])).
% 88.08/21.43 fof(f22962,plain,(
% 88.08/21.43 s__instance(s__Number3_1,s__RealNumber)),
% 88.08/21.43 inference(resolution,[status(thm)],[f22953,f19297])).
% 88.08/21.43 fof(f23059,plain,(
% 88.08/21.43 ~s__instance(s__Number3_1,s__RealNumber)|s__SignumFn(s__Number3_1)="1"|s__SignumFn(s__Number3_1)="0"),
% 88.08/21.43 inference(resolution,[status(thm)],[f13494,f19220])).
% 88.08/21.43 fof(f23061,plain,(
% 88.08/21.43 s__SignumFn(s__Number3_1)="1"|s__SignumFn(s__Number3_1)="0"),
% 88.08/21.43 inference(forward_subsumption_resolution,[status(thm)],[f23059,f22962])).
% 88.08/21.43 fof(f23068,plain,(
% 88.08/21.43 ~s__instance(s__Number3_1,s__RealNumber)|s__SignumFn(s__Number3_1)="-1"),
% 88.08/21.43 inference(resolution,[status(thm)],[f13498,f19221])).
% 88.08/21.43 fof(f23069,plain,(
% 88.08/21.43 s__SignumFn(s__Number3_1)="1"|"-1"="0"),
% 88.08/21.43 inference(backward_demodulation,[status(thm)],[f23070,f23061])).
% 88.08/21.43 fof(f23070,plain,(
% 88.08/21.43 s__SignumFn(s__Number3_1)="-1"),
% 88.08/21.43 inference(forward_subsumption_resolution,[status(thm)],[f23068,f22962])).
% 88.08/21.43 fof(f23071,plain,(
% 88.08/21.43 "-1"="1"|"-1"="0"),
% 88.08/21.43 inference(forward_demodulation,[status(thm)],[f23070,f23069])).
% 88.08/21.43 fof(f23072,plain,(
% 88.08/21.43 $false),
% 88.08/21.43 inference(trivial_equality_resolution,[status(thm)],[f23071])).
% 88.08/21.43 % SZS output end CNFRefutation for theBenchmark.p
% 88.08/21.48 % Elapsed time: 20.882084 seconds
% 88.08/21.48 % CPU time: 163.078219 seconds
% 88.08/21.48 % Total memory used: 1.016 GB
% 88.08/21.48 % Net memory used: 987.836 MB
%------------------------------------------------------------------------------