%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG377-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 11:50:06 AM UTC 2026
% Result : Unsatisfiable 0.15s 5.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG377-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n017.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 13:13:33 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 0.15/5.58 % Refutation found
% 0.15/5.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.58 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.58 fof(f443,axiom,(
% 0.15/5.58 (![V_m,V_n]: (c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat)) ))),
% 0.15/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.58 fof(f470,axiom,(
% 0.15/5.58 (![V_z,V_x,V_y]: (( c_lessequals(c_HOL_Oplus__class_Oplus(V_z,V_x,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 0.15/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.58 fof(f506,axiom,(
% 0.15/5.58 c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 0.15/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.58 fof(f507,negated_conjecture,(
% 0.15/5.58 ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 0.15/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.58 fof(f1195,plain,(
% 0.15/5.58 ![X0,X1]: (c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat)=c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)))),
% 0.15/5.58 inference(cnf_transformation,[status(thm)],[f443])).
% 0.15/5.58 fof(f1242,plain,(
% 0.15/5.58 ![V_x,V_y]: ((![V_z]: c_lessequals(c_HOL_Oplus__class_Oplus(V_z,V_x,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal))|~c_lessequals(V_x,V_y,tc_RealDef_Oreal))),
% 0.15/5.58 inference(miniscoping,[status(thm)],[f470])).
% 0.15/5.58 fof(f1243,plain,(
% 0.15/5.58 ![X0,X1,X2]: (c_lessequals(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(X1,X2,tc_RealDef_Oreal))),
% 0.15/5.58 inference(cnf_transformation,[status(thm)],[f1242])).
% 0.15/5.58 fof(f1300,plain,(
% 0.15/5.58 c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.15/5.58 inference(cnf_transformation,[status(thm)],[f506])).
% 0.15/5.58 fof(f1301,plain,(
% 0.15/5.58 ~c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.15/5.58 inference(cnf_transformation,[status(thm)],[f507])).
% 0.15/5.58 fof(f2316,plain,(
% 0.15/5.58 ~c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_HOL_Oplus__class_Oplus(v_N1____,c_Suc(v_N2____),tc_nat),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.15/5.59 inference(backward_demodulation,[status(thm)],[f1195,f1301])).
% 0.15/5.59 fof(f2502,plain,(
% 0.15/5.59 ~c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_HOL_Oplus__class_Oplus(v_N1____,c_Suc(v_N2____),tc_nat),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.15/5.59 inference(resolution,[status(thm)],[f1243,f2316])).
% 0.15/5.59 fof(f2740,plain,(
% 0.15/5.59 c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_f____(c_HOL_Oplus__class_Oplus(v_N1____,v_N2____,tc_nat))),tc_nat),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_HOL_Oplus__class_Oplus(v_N1____,c_Suc(v_N2____),tc_nat),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.15/5.59 inference(forward_demodulation,[status(thm)],[f1195,f1300])).
% 0.15/5.59 fof(f2741,plain,(
% 0.15/5.59 $false),
% 0.15/5.59 inference(forward_subsumption_resolution,[status(thm)],[f2740,f2502])).
% 0.15/5.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.59 % Elapsed time: 0.222852 seconds
% 0.15/5.59 % CPU time: 1.338326 seconds
% 0.15/5.59 % Total memory used: 147.627 MB
% 0.15/5.59 % Net memory used: 146.282 MB
%------------------------------------------------------------------------------