%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG404-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 : n012.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:08 AM UTC 2026
% Result : Unsatisfiable 163.43s 30.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG404-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/10.31 % Computer : n012.cluster.edu
% 0.03/10.31 % Model : x86_64 x86_64
% 0.03/10.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/10.31 % Memory : 8046.5625MB
% 0.03/10.31 % OS : Linux 6.8.0-71-generic
% 0.03/10.31 % CPULimit : 300
% 0.03/10.31 % WCLimit : 300
% 0.03/10.31 % DateTime : Mon Sep 21 13:19:18 UTC 2026
% 0.03/10.31 % CPUTime :
% 0.03/10.35 % Drodi V4.1.1
% 163.43/30.93 % Refutation found
% 163.43/30.93 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 163.43/30.93 % SZS output start CNFRefutation for theBenchmark
% 163.43/30.93 fof(f28,axiom,(
% 163.43/30.93 (![T_a,V_b]: (( ~ class_OrderedGroup_Ogroup__add(T_a)| c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) = V_b ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f101,axiom,(
% 163.43/30.93 (![T_a,V_y,V_x]: (( ~ class_Orderings_Opreorder(T_a)| ~ c_lessequals(V_y,V_x,T_a)| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f102,axiom,(
% 163.43/30.93 (![T_a,V_x,V_y]: (( ~ class_Orderings_Olinorder(T_a)| c_HOL_Oord__class_Oless(V_x,V_y,T_a)| c_lessequals(V_y,V_x,T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f109,axiom,(
% 163.43/30.93 (![T_a,V_a,V_b]: (( ~ class_OrderedGroup_Opordered__ab__group__add(T_a)| c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a)| ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_b,T_a),V_a,T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f171,axiom,(
% 163.43/30.93 (![T_a,V_x,V_y]: (( ~ class_OrderedGroup_Oab__group__add(T_a)| c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f176,axiom,(
% 163.43/30.93 (![V_y]: (c_Transcendental_Oln(c_Transcendental_Oexp(V_y,tc_RealDef_Oreal)) = V_y ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f182,axiom,(
% 163.43/30.93 (![T_a,V_a]: (( ~ class_OrderedGroup_Opordered__ab__group__add(T_a)| c_lessequals(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)| ~ c_lessequals(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f252,axiom,(
% 163.43/30.93 (![T_a,V_a,V_b]: (( ~ class_OrderedGroup_Oab__group__add(T_a)| c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f283,axiom,(
% 163.43/30.93 (![V_x,V_y]: (( c_lessequals(c_Transcendental_Oln(V_x),c_Transcendental_Oln(V_y),tc_RealDef_Oreal)| ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f331,axiom,(
% 163.43/30.93 (![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) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f339,axiom,(
% 163.43/30.93 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f420,axiom,(
% 163.43/30.93 (![V_x]: (( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)| ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f548,axiom,(
% 163.43/30.93 (![T_a]: (( ~ class_Ring__and__Field_Oordered__semidom(T_a)| ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f588,axiom,(
% 163.43/30.93 (![V_x]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f609,axiom,(
% 163.43/30.93 (![V_n]: (c_Suc(V_n) = c_HOL_Oplus__class_Oplus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f645,axiom,(
% 163.43/30.93 (![V_x]: (( c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f746,axiom,(
% 163.43/30.93 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f819,axiom,(
% 163.43/30.93 (![T_a,V_a]: (( ~ class_Ring__and__Field_Oordered__semidom(T_a)| c_HOL_Oord__class_Oless(V_a,c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oone__class_Oone(T_a),T_a),T_a) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f881,axiom,(
% 163.43/30.93 (![V_t]: (( v_thesis____| ~ c_HOL_Oord__class_Oless(V_t,c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_t,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_t,tc_RealDef_Oreal) ) ))),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f919,negated_conjecture,(
% 163.43/30.93 ~ v_thesis____ ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f963,axiom,(
% 163.43/30.93 class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f972,axiom,(
% 163.43/30.93 class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f991,axiom,(
% 163.43/30.93 class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f1000,axiom,(
% 163.43/30.93 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f1007,axiom,(
% 163.43/30.93 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f1008,axiom,(
% 163.43/30.93 class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 163.43/30.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 163.43/30.93 fof(f1095,plain,(
% 163.43/30.93 ![T_a]: (~class_OrderedGroup_Ogroup__add(T_a)|(![V_b]: c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a)=V_b))),
% 163.43/30.93 inference(miniscoping,[status(thm)],[f28])).
% 163.43/30.93 fof(f1096,plain,(
% 163.43/30.93 ![X0,X1]: (~class_OrderedGroup_Ogroup__add(X0)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0)=X1)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1095])).
% 163.43/30.93 fof(f1211,plain,(
% 163.43/30.93 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|~c_lessequals(X1,X2,X0)|~c_HOL_Oord__class_Oless(X2,X1,X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f101])).
% 163.43/30.93 fof(f1212,plain,(
% 163.43/30.93 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|c_HOL_Oord__class_Oless(X1,X2,X0)|c_lessequals(X2,X1,X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f102])).
% 163.43/30.93 fof(f1219,plain,(
% 163.43/30.93 ![X0,X1,X2]: (~class_OrderedGroup_Opordered__ab__group__add(X0)|c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(X1,X0),X2,X0)|~c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(X2,X0),X1,X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f109])).
% 163.43/30.93 fof(f1311,plain,(
% 163.43/30.93 ![T_a]: (~class_OrderedGroup_Oab__group__add(T_a)|(![V_x,V_y]: c_HOL_Ominus__class_Ominus(V_x,V_y,T_a)=c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a)))),
% 163.43/30.93 inference(miniscoping,[status(thm)],[f171])).
% 163.43/30.93 fof(f1312,plain,(
% 163.43/30.93 ![X0,X1,X2]: (~class_OrderedGroup_Oab__group__add(X0)|c_HOL_Ominus__class_Ominus(X1,X2,X0)=c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X2,X0),X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1311])).
% 163.43/30.93 fof(f1321,plain,(
% 163.43/30.93 ![X0]: (c_Transcendental_Oln(c_Transcendental_Oexp(X0,tc_RealDef_Oreal))=X0)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f176])).
% 163.43/30.93 fof(f1329,plain,(
% 163.43/30.93 ![X0,X1]: (~class_OrderedGroup_Opordered__ab__group__add(X0)|c_lessequals(X1,c_HOL_Ozero__class_Ozero(X0),X0)|~c_lessequals(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ouminus__class_Ouminus(X1,X0),X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f182])).
% 163.43/30.93 fof(f1434,plain,(
% 163.43/30.93 ![T_a]: (~class_OrderedGroup_Oab__group__add(T_a)|(![V_a,V_b]: c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a)=c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a)))),
% 163.43/30.93 inference(miniscoping,[status(thm)],[f252])).
% 163.43/30.93 fof(f1435,plain,(
% 163.43/30.93 ![X0,X1,X2]: (~class_OrderedGroup_Oab__group__add(X0)|c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(X1,X2,X0),X0)=c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Ouminus__class_Ouminus(X2,X0),X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1434])).
% 163.43/30.93 fof(f1494,plain,(
% 163.43/30.93 ![V_x]: ((![V_y]: ((c_lessequals(c_Transcendental_Oln(V_x),c_Transcendental_Oln(V_y),tc_RealDef_Oreal)|~c_lessequals(V_x,V_y,tc_RealDef_Oreal))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal))),
% 163.43/30.93 inference(miniscoping,[status(thm)],[f283])).
% 163.43/30.93 fof(f1495,plain,(
% 163.43/30.93 ![X0,X1]: (c_lessequals(c_Transcendental_Oln(X0),c_Transcendental_Oln(X1),tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1494])).
% 163.43/30.93 fof(f1568,plain,(
% 163.43/30.93 ![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))),
% 163.43/30.93 inference(miniscoping,[status(thm)],[f331])).
% 163.43/30.93 fof(f1569,plain,(
% 163.43/30.93 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1568])).
% 163.43/30.93 fof(f1580,plain,(
% 163.43/30.93 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f339])).
% 163.43/30.93 fof(f1712,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f420])).
% 163.43/30.93 fof(f1908,plain,(
% 163.43/30.93 ![X0]: (~class_Ring__and__Field_Oordered__semidom(X0)|~c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f548])).
% 163.43/30.93 fof(f1978,plain,(
% 163.43/30.93 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f588])).
% 163.43/30.93 fof(f2009,plain,(
% 163.43/30.93 ![X0]: (c_Suc(X0)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f609])).
% 163.43/30.93 fof(f2062,plain,(
% 163.43/30.93 ![X0]: (c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f645])).
% 163.43/30.93 fof(f2218,plain,(
% 163.43/30.93 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f746])).
% 163.43/30.93 fof(f2336,plain,(
% 163.43/30.93 ![T_a]: (~class_Ring__and__Field_Oordered__semidom(T_a)|(![V_a]: c_HOL_Oord__class_Oless(V_a,c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oone__class_Oone(T_a),T_a),T_a)))),
% 163.43/30.93 inference(miniscoping,[status(thm)],[f819])).
% 163.43/30.93 fof(f2337,plain,(
% 163.43/30.93 ![X0,X1]: (~class_Ring__and__Field_Oordered__semidom(X0)|c_HOL_Oord__class_Oless(X1,c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(X0),X0),X0))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f2336])).
% 163.43/30.93 fof(f2442,plain,(
% 163.43/30.93 ![X0]: (v_thesis____|~c_HOL_Oord__class_Oless(X0,c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f881])).
% 163.43/30.93 fof(f2507,plain,(
% 163.43/30.93 ~v_thesis____),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f919])).
% 163.43/30.93 fof(f2551,plain,(
% 163.43/30.93 class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f963])).
% 163.43/30.93 fof(f2560,plain,(
% 163.43/30.93 class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f972])).
% 163.43/30.93 fof(f2579,plain,(
% 163.43/30.93 class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f991])).
% 163.43/30.93 fof(f2588,plain,(
% 163.43/30.93 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1000])).
% 163.43/30.93 fof(f2595,plain,(
% 163.43/30.93 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1007])).
% 163.43/30.93 fof(f2596,plain,(
% 163.43/30.93 class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 163.43/30.93 inference(cnf_transformation,[status(thm)],[f1008])).
% 163.43/30.93 fof(f2641,plain,(
% 163.43/30.93 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(forward_subsumption_resolution,[status(thm)],[f2442,f2507])).
% 163.43/30.93 fof(f2822,plain,(
% 163.43/30.93 ![X0]: (c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 163.43/30.93 inference(resolution,[status(thm)],[f2588,f1096])).
% 163.43/30.93 fof(f2845,plain,(
% 163.43/30.93 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f1312,f2579])).
% 163.43/30.93 fof(f2872,plain,(
% 163.43/30.93 ![X0,X1]: (~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f2595,f1211])).
% 163.43/30.93 fof(f2879,plain,(
% 163.43/30.93 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f2596,f1212])).
% 163.43/30.93 fof(f3068,plain,(
% 163.43/30.93 ![X0,X1]: (c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f1435,f2579])).
% 163.43/30.93 fof(f3938,plain,(
% 163.43/30.93 ~c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 163.43/30.93 inference(resolution,[status(thm)],[f1908,f2560])).
% 163.43/30.93 fof(f3976,plain,(
% 163.43/30.93 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(backward_demodulation,[status(thm)],[f2009,f2641])).
% 163.43/30.93 fof(f4487,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f2879,f3976])).
% 163.43/30.93 fof(f5252,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f1978,f4487])).
% 163.43/30.93 fof(f5257,plain,(
% 163.43/30.93 ![X0,X1]: (c_lessequals(c_Transcendental_Oln(X0),c_Transcendental_Oln(c_Transcendental_Oexp(X1,tc_RealDef_Oreal)),tc_RealDef_Oreal)|~c_lessequals(X0,c_Transcendental_Oexp(X1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f1978,f1495])).
% 163.43/30.93 fof(f5266,plain,(
% 163.43/30.93 ![X0,X1]: (c_lessequals(c_Transcendental_Oln(X0),X1,tc_RealDef_Oreal)|~c_lessequals(X0,c_Transcendental_Oexp(X1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(forward_demodulation,[status(thm)],[f1321,f5257])).
% 163.43/30.93 fof(f5302,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f5252,f2879])).
% 163.43/30.93 fof(f6692,plain,(
% 163.43/30.93 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f2062,f3976])).
% 163.43/30.93 fof(f6700,plain,(
% 163.43/30.93 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(forward_subsumption_resolution,[status(thm)],[f6692,f1978])).
% 163.43/30.93 fof(f6744,plain,(
% 163.43/30.93 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f6700,f2879])).
% 163.43/30.93 fof(f6793,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f6744,f2879])).
% 163.43/30.93 fof(f6835,plain,(
% 163.43/30.93 ![X0,X1]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_lessequals(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f6793,f1569])).
% 163.43/30.93 fof(f7289,plain,(
% 163.43/30.93 ![X0,X1]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|c_lessequals(X1,c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f6835,f1580])).
% 163.43/30.93 fof(f9278,plain,(
% 163.43/30.93 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 163.43/30.93 inference(forward_demodulation,[status(thm)],[f2009,f2218])).
% 163.43/30.93 fof(f10053,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f7289,f1712])).
% 163.43/30.93 fof(f10085,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(duplicate_literals_removal,[status(thm)],[f10053])).
% 163.43/30.93 fof(f10279,plain,(
% 163.43/30.93 ![X0]: (c_HOL_Oord__class_Oless(X0,c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f2337,f2560])).
% 163.43/30.93 fof(f11582,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|~class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)|c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(resolution,[status(thm)],[f10085,f1329])).
% 163.43/30.93 fof(f11629,plain,(
% 163.43/30.93 ![X0]: (c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)|c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 163.43/30.93 inference(forward_subsumption_resolution,[status(thm)],[f11582,f2551])).
% 163.43/30.93 fof(f11762,plain,(
% 163.43/30.93 c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 55.66/31.12 inference(resolution,[status(thm)],[f11629,f3938])).
% 55.66/31.12 fof(f12125,plain,(
% 55.66/31.12 ![X0]: (c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 55.66/31.12 inference(resolution,[status(thm)],[f11762,f1569])).
% 55.66/31.12 fof(f12741,plain,(
% 55.66/31.12 ![X0]: (c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 55.66/31.12 inference(backward_subsumption_resolution,[status(thm)],[f5302,f12125])).
% 55.66/31.12 fof(f30216,plain,(
% 55.66/31.12 ![X0,X1]: (c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 55.66/31.12 inference(forward_demodulation,[status(thm)],[f2845,f3068])).
% 55.66/31.12 fof(f42909,plain,(
% 55.66/31.12 ![X0]: (~class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 55.66/31.12 inference(resolution,[status(thm)],[f10279,f1219])).
% 55.66/31.12 fof(f42952,plain,(
% 55.66/31.12 ![X0]: (~class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 55.66/31.12 inference(forward_demodulation,[status(thm)],[f30216,f42909])).
% 55.66/31.12 fof(f42953,plain,(
% 55.66/31.12 ![X0]: (~class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 55.66/31.12 inference(forward_demodulation,[status(thm)],[f2822,f42952])).
% 55.66/31.12 fof(f42954,plain,(
% 55.66/31.12 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 55.66/31.12 inference(forward_subsumption_resolution,[status(thm)],[f42953,f2551])).
% 55.66/31.12 fof(f67577,plain,(
% 55.66/31.12 ![X0]: (~c_lessequals(X0,c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 55.66/31.12 inference(resolution,[status(thm)],[f42954,f2872])).
% 55.66/31.12 fof(f84235,plain,(
% 55.66/31.12 ![X0]: (c_lessequals(c_Transcendental_Oln(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)),X0,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 55.66/31.12 inference(resolution,[status(thm)],[f5266,f9278])).
% 55.66/31.12 fof(f84256,plain,(
% 55.66/31.12 ![X0]: (c_lessequals(c_Transcendental_Oln(c_HOL_Oinverse__class_Oinverse(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)),X0,tc_RealDef_Oreal))),
% 55.66/31.12 inference(forward_subsumption_resolution,[status(thm)],[f84235,f12741])).
% 55.66/31.12 fof(f84474,plain,(
% 55.66/31.12 $false),
% 55.66/31.12 inference(resolution,[status(thm)],[f84256,f67577])).
% 55.66/31.12 % SZS output end CNFRefutation for theBenchmark.p
% 73.07/31.18 % Elapsed time: 20.853587 seconds
% 73.07/31.18 % CPU time: 164.902818 seconds
% 73.07/31.18 % Total memory used: 1.462 GB
% 73.07/31.18 % Net memory used: 1.388 GB
%------------------------------------------------------------------------------