%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG341-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:03 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG341-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 13:16:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.46 % Refutation found
% 0.13/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.46 fof(f460,axiom,(
% 0.13/0.46 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f464,axiom,(
% 0.13/0.46 (![V_w]: (c_lessequals(V_w,V_w,tc_RealDef_Oreal) ))),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f465,axiom,(
% 0.13/0.46 (![V_i,V_k,V_j]: (( c_lessequals(V_i,V_k,tc_RealDef_Oreal)| ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)| ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal) ) ))),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f471,axiom,(
% 0.13/0.46 (![V_z,V_w]: (( V_z = V_w| ~ c_lessequals(V_w,V_z,tc_RealDef_Oreal)| ~ c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f472,axiom,(
% 0.13/0.46 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f473,axiom,(
% 0.13/0.46 c_lessequals(c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f474,negated_conjecture,(
% 0.13/0.46 ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
% 0.13/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f1392,plain,(
% 0.13/0.46 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f460])).
% 0.13/0.46 fof(f1398,plain,(
% 0.13/0.46 ![X0]: (c_lessequals(X0,X0,tc_RealDef_Oreal))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f464])).
% 0.13/0.46 fof(f1399,plain,(
% 0.13/0.46 ![V_i,V_j]: ((![V_k]: (c_lessequals(V_i,V_k,tc_RealDef_Oreal)|~c_lessequals(V_j,V_k,tc_RealDef_Oreal)))|~c_lessequals(V_i,V_j,tc_RealDef_Oreal))),
% 0.13/0.46 inference(miniscoping,[status(thm)],[f465])).
% 0.13/0.46 fof(f1400,plain,(
% 0.13/0.46 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f1399])).
% 0.13/0.46 fof(f1408,plain,(
% 0.13/0.46 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f471])).
% 0.13/0.46 fof(f1409,plain,(
% 0.13/0.46 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f472])).
% 0.13/0.46 fof(f1410,plain,(
% 0.13/0.46 c_lessequals(c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f473])).
% 0.13/0.46 fof(f1411,plain,(
% 0.13/0.46 ~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f474])).
% 0.13/0.46 fof(f1534,plain,(
% 0.13/0.46 c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.13/0.46 inference(resolution,[status(thm)],[f1392,f1411])).
% 0.13/0.46 fof(f1537,plain,(
% 0.13/0.46 v_r=c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex)|~c_lessequals(v_r,c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 0.13/0.46 inference(resolution,[status(thm)],[f1408,f1410])).
% 0.13/0.46 fof(f1544,plain,(
% 0.13/0.46 ![X0]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 0.13/0.46 inference(resolution,[status(thm)],[f1400,f1411])).
% 0.13/0.46 fof(f1549,plain,(
% 0.13/0.46 ![X0,X1]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 0.13/0.46 inference(resolution,[status(thm)],[f1544,f1400])).
% 0.13/0.46 fof(f1561,plain,(
% 0.13/0.46 ![X0,X1]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(X1,X0,tc_RealDef_Oreal)|c_lessequals(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.13/0.46 inference(resolution,[status(thm)],[f1549,f1392])).
% 0.13/0.46 fof(f1594,plain,(
% 0.13/0.46 ![X0]: (~c_lessequals(X0,c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),tc_RealDef_Oreal)|c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.13/0.46 inference(resolution,[status(thm)],[f1561,f1410])).
% 0.13/0.46 fof(f1602,plain,(
% 0.13/0.46 c_lessequals(c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.13/0.46 inference(resolution,[status(thm)],[f1594,f1392])).
% 0.13/0.46 fof(f1609,plain,(
% 0.13/0.46 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 0.13/0.46 inference(resolution,[status(thm)],[f1602,f1408])).
% 0.13/0.46 fof(f1612,plain,(
% 0.13/0.46 v_r=c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex)|~c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1621,f1537])).
% 0.13/0.46 fof(f1621,plain,(
% 0.13/0.46 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(v_z____,tc_Complex_Ocomplex)),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1609,f1409])).
% 0.13/0.46 fof(f1622,plain,(
% 0.13/0.46 v_r=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1621,f1612])).
% 0.13/0.46 fof(f1629,plain,(
% 0.13/0.46 ~c_lessequals(v_r,v_r,tc_RealDef_Oreal)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1684,f1411])).
% 0.13/0.46 fof(f1684,plain,(
% 0.13/0.46 v_r=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1622,f1534])).
% 0.13/0.46 fof(f1700,plain,(
% 0.13/0.46 $false),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1629,f1398])).
% 0.13/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.48 % Elapsed time: 0.123044 seconds
% 0.13/0.48 % CPU time: 0.646284 seconds
% 0.13/0.48 % Total memory used: 135.468 MB
% 0.13/0.48 % Net memory used: 134.646 MB
%------------------------------------------------------------------------------