%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG406-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 : n016.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 6.49s 6.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG406-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.48 % Computer : n016.cluster.edu
% 0.16/5.48 % Model : x86_64 x86_64
% 0.16/5.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.48 % Memory : 8046.5625MB
% 0.16/5.48 % OS : Linux 6.8.0-71-generic
% 0.16/5.48 % CPULimit : 300
% 0.16/5.48 % WCLimit : 300
% 0.16/5.48 % DateTime : Mon Sep 21 13:23:58 UTC 2026
% 0.16/5.49 % CPUTime :
% 0.23/5.56 % Drodi V4.1.1
% 6.49/6.48 % Refutation found
% 6.49/6.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.49/6.48 % SZS output start CNFRefutation for theBenchmark
% 6.49/6.48 fof(f27,axiom,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f36,axiom,(
% 6.49/6.48 (![T_a,V_x]: (( ~ class_RealVector_Oreal__normed__vector(T_a)| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f75,axiom,(
% 6.49/6.48 (![V_x,V_y]: (( c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f90,axiom,(
% 6.49/6.48 (![V_z,V_x,V_y]: (( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_z,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f92,axiom,(
% 6.49/6.48 (![V_x,V_y,V_z]: (( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_x,V_z,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_z,tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f140,axiom,(
% 6.49/6.48 (![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) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f275,axiom,(
% 6.49/6.48 (![T_a,V_a]: (( ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a)| c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f334,axiom,(
% 6.49/6.48 (![V_x,V_y]: (( c_lessequals(V_x,V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f337,axiom,(
% 6.49/6.48 (![V_x,V_y]: (( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)| V_x = V_y| ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f347,axiom,(
% 6.49/6.48 c_NthRoot_Osqrt(c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f407,axiom,(
% 6.49/6.48 (![V_x]: (~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f420,axiom,(
% 6.49/6.48 (![T_a]: (( ~ class_Ring__and__Field_Oordered__semidom(T_a)| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oone__class_Oone(T_a),T_a) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f508,axiom,(
% 6.49/6.48 c_HOL_Oord__class_Oless(v_t____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f521,axiom,(
% 6.49/6.48 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f525,axiom,(
% 6.49/6.48 (![V_w]: (c_lessequals(V_w,V_w,tc_RealDef_Oreal) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f543,axiom,(
% 6.49/6.48 (![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) ) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f552,axiom,(
% 6.49/6.48 (![V_z]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f556,axiom,(
% 6.49/6.48 (![V_z,V_w]: (c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal) ))),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f559,negated_conjecture,(
% 6.49/6.48 ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f560,axiom,(
% 6.49/6.48 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f562,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f564,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oordered__semiring__strict(tc_nat) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f572,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oordered__semidom(tc_nat) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f587,axiom,(
% 6.49/6.48 class_Orderings_Olinorder(tc_nat) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f590,axiom,(
% 6.49/6.48 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f592,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f595,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f597,axiom,(
% 6.49/6.48 class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f600,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f602,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f605,axiom,(
% 6.49/6.48 class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f618,axiom,(
% 6.49/6.48 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f627,axiom,(
% 6.49/6.48 class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f630,axiom,(
% 6.49/6.48 class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f631,axiom,(
% 6.49/6.48 class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f639,axiom,(
% 6.49/6.48 class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f644,axiom,(
% 6.49/6.48 class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f659,axiom,(
% 6.49/6.48 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f664,axiom,(
% 6.49/6.48 class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f665,axiom,(
% 6.49/6.48 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f666,axiom,(
% 6.49/6.48 class_RealVector_Oreal__algebra__1(tc_Complex_Ocomplex) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f667,axiom,(
% 6.49/6.48 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f672,axiom,(
% 6.49/6.48 class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex) ),
% 6.49/6.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.49/6.48 fof(f726,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f27])).
% 6.49/6.48 fof(f737,plain,(
% 6.49/6.48 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(![V_x]: ~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 6.49/6.48 inference(miniscoping,[status(thm)],[f36])).
% 6.49/6.48 fof(f738,plain,(
% 6.49/6.48 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(X1,X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f737])).
% 6.49/6.48 fof(f794,plain,(
% 6.49/6.48 ![X0,X1]: (c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f75])).
% 6.49/6.48 fof(f822,plain,(
% 6.49/6.48 ![V_z]: ((![V_x,V_y]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_z,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal))),
% 6.49/6.48 inference(miniscoping,[status(thm)],[f90])).
% 6.49/6.48 fof(f823,plain,(
% 6.49/6.48 ![X0,X1,X2]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f822])).
% 6.49/6.48 fof(f826,plain,(
% 6.49/6.48 ![V_z]: ((![V_x,V_y]: (c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_x,V_z,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_z,tc_RealDef_Oreal),tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal))),
% 6.49/6.48 inference(miniscoping,[status(thm)],[f92])).
% 6.49/6.48 fof(f827,plain,(
% 6.49/6.48 ![X0,X1,X2]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f826])).
% 6.49/6.48 fof(f905,plain,(
% 6.49/6.48 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|c_HOL_Oord__class_Oless(X1,X2,X0)|c_lessequals(X2,X1,X0))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f140])).
% 6.49/6.48 fof(f1103,plain,(
% 6.49/6.48 ![T_a]: (~class_Ring__and__Field_Oring__no__zero__divisors(T_a)|(![V_a]: c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 6.49/6.48 inference(miniscoping,[status(thm)],[f275])).
% 6.49/6.48 fof(f1104,plain,(
% 6.49/6.48 ![X0,X1]: (~class_Ring__and__Field_Oring__no__zero__divisors(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(X0))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f1103])).
% 6.49/6.48 fof(f1210,plain,(
% 6.49/6.48 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f334])).
% 6.49/6.48 fof(f1213,plain,(
% 6.49/6.48 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f337])).
% 6.49/6.48 fof(f1229,plain,(
% 6.49/6.48 c_NthRoot_Osqrt(c_HOL_Oone__class_Oone(tc_RealDef_Oreal))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f347])).
% 6.49/6.48 fof(f1314,plain,(
% 6.49/6.48 ![X0]: (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f407])).
% 6.49/6.48 fof(f1334,plain,(
% 6.49/6.48 ![X0]: (~class_Ring__and__Field_Oordered__semidom(X0)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oone__class_Oone(X0),X0))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f420])).
% 6.49/6.48 fof(f1461,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(v_t____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f508])).
% 6.49/6.48 fof(f1486,plain,(
% 6.49/6.48 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f521])).
% 6.49/6.48 fof(f1492,plain,(
% 6.49/6.48 ![X0]: (c_lessequals(X0,X0,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f525])).
% 6.49/6.48 fof(f1522,plain,(
% 6.49/6.48 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f543])).
% 6.49/6.48 fof(f1539,plain,(
% 6.49/6.48 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=X0)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f552])).
% 6.49/6.48 fof(f1546,plain,(
% 6.49/6.48 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal))),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f556])).
% 6.49/6.48 fof(f1550,plain,(
% 6.49/6.48 ~c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f559])).
% 6.49/6.48 fof(f1551,plain,(
% 6.49/6.48 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f560])).
% 6.49/6.48 fof(f1553,plain,(
% 6.49/6.48 class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f562])).
% 6.49/6.48 fof(f1555,plain,(
% 6.49/6.48 class_Ring__and__Field_Oordered__semiring__strict(tc_nat)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f564])).
% 6.49/6.48 fof(f1563,plain,(
% 6.49/6.48 class_Ring__and__Field_Oordered__semidom(tc_nat)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f572])).
% 6.49/6.48 fof(f1578,plain,(
% 6.49/6.48 class_Orderings_Olinorder(tc_nat)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f587])).
% 6.49/6.48 fof(f1581,plain,(
% 6.49/6.48 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f590])).
% 6.49/6.48 fof(f1583,plain,(
% 6.49/6.48 class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f592])).
% 6.49/6.48 fof(f1586,plain,(
% 6.49/6.48 class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f595])).
% 6.49/6.48 fof(f1588,plain,(
% 6.49/6.48 class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f597])).
% 6.49/6.48 fof(f1591,plain,(
% 6.49/6.48 class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f600])).
% 6.49/6.48 fof(f1593,plain,(
% 6.49/6.48 class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f602])).
% 6.49/6.48 fof(f1596,plain,(
% 6.49/6.48 class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f605])).
% 6.49/6.48 fof(f1609,plain,(
% 6.49/6.48 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f618])).
% 6.49/6.48 fof(f1618,plain,(
% 6.49/6.48 class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f627])).
% 6.49/6.48 fof(f1621,plain,(
% 6.49/6.48 class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f630])).
% 6.49/6.48 fof(f1622,plain,(
% 6.49/6.48 class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f631])).
% 6.49/6.48 fof(f1630,plain,(
% 6.49/6.48 class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f639])).
% 6.49/6.48 fof(f1635,plain,(
% 6.49/6.48 class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f644])).
% 6.49/6.48 fof(f1650,plain,(
% 6.49/6.48 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f659])).
% 6.49/6.48 fof(f1655,plain,(
% 6.49/6.48 class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f664])).
% 6.49/6.48 fof(f1656,plain,(
% 6.49/6.48 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f665])).
% 6.49/6.48 fof(f1657,plain,(
% 6.49/6.48 class_RealVector_Oreal__algebra__1(tc_Complex_Ocomplex)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f666])).
% 6.49/6.48 fof(f1658,plain,(
% 6.49/6.48 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f667])).
% 6.49/6.48 fof(f1663,plain,(
% 6.49/6.48 class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex)),
% 6.49/6.48 inference(cnf_transformation,[status(thm)],[f672])).
% 6.49/6.48 fof(f1671,plain,(
% 6.49/6.48 ~c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 6.49/6.48 inference(backward_demodulation,[status(thm)],[f1539,f1550])).
% 6.49/6.48 fof(f1672,plain,(
% 6.49/6.48 c_lessequals(v_t____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 6.49/6.48 inference(resolution,[status(thm)],[f1210,f1461])).
% 6.49/6.48 fof(f1674,plain,(
% 6.49/6.48 ![X0]: (X0=c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 6.49/6.48 inference(paramodulation,[status(thm)],[f1539,f1546])).
% 6.49/6.48 fof(f1689,plain,(
% 6.49/6.48 ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_t____,X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 6.49/6.48 inference(resolution,[status(thm)],[f823,f726])).
% 6.49/6.48 fof(f1690,plain,(
% 6.49/6.48 c_lessequals(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 6.49/6.48 inference(resolution,[status(thm)],[f1671,f1486])).
% 6.49/6.48 fof(f1692,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 6.49/6.48 inference(resolution,[status(thm)],[f1213,f1690])).
% 6.49/6.48 fof(f1700,definition,(
% 6.49/6.48 sQ0_spl <=> (c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f1701,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ0_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f1700])).
% 6.49/6.48 fof(f1703,definition,(
% 6.49/6.48 sQ1_spl <=> (c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f1704,plain,(
% 6.49/6.48 c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)|~sQ1_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f1703])).
% 6.49/6.48 fof(f1705,plain,(
% 6.49/6.48 ~c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(v_t____,c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ1_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f1703])).
% 6.49/6.48 fof(f1706,plain,(
% 6.49/6.48 sQ0_spl|sQ1_spl),
% 6.49/6.48 inference(split_clause,[status(thm)],[f1692,f1700,f1703])).
% 6.49/6.48 fof(f1717,definition,(
% 6.49/6.48 sQ5_spl <=> (v_t____=c_HOL_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f1718,plain,(
% 6.49/6.48 v_t____=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|~sQ5_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f1717])).
% 6.49/6.48 fof(f1724,plain,(
% 6.49/6.48 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=v_t____|~c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)),
% 6.49/6.48 inference(resolution,[status(thm)],[f1522,f1672])).
% 6.49/6.48 fof(f1738,definition,(
% 6.49/6.48 sQ8_spl <=> (c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f1740,plain,(
% 6.49/6.48 ~c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)|sQ8_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f1738])).
% 6.49/6.48 fof(f1741,plain,(
% 6.49/6.48 sQ5_spl|~sQ8_spl),
% 6.49/6.48 inference(split_clause,[status(thm)],[f1724,f1717,f1738])).
% 6.49/6.48 fof(f1745,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(v_t____,v_t____,tc_RealDef_Oreal)|~sQ5_spl),
% 6.49/6.48 inference(backward_demodulation,[status(thm)],[f1718,f1461])).
% 6.49/6.48 fof(f1747,plain,(
% 6.49/6.48 $false|~sQ5_spl),
% 6.49/6.48 inference(forward_subsumption_resolution,[status(thm)],[f1745,f1314])).
% 6.49/6.48 fof(f1748,plain,(
% 6.49/6.48 ~sQ5_spl),
% 6.49/6.48 inference(contradiction_clause,[status(thm)],[f1747])).
% 6.49/6.48 fof(f1774,plain,(
% 6.49/6.48 ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 6.49/6.48 inference(paramodulation,[status(thm)],[f1539,f827])).
% 6.49/6.48 fof(f1807,plain,(
% 6.49/6.48 ~c_lessequals(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)|~sQ1_spl),
% 6.49/6.48 inference(backward_demodulation,[status(thm)],[f1704,f1671])).
% 6.49/6.48 fof(f1810,plain,(
% 6.49/6.48 $false|~sQ1_spl),
% 6.49/6.48 inference(forward_subsumption_resolution,[status(thm)],[f1807,f1492])).
% 6.49/6.48 fof(f1811,plain,(
% 6.49/6.48 ~sQ1_spl),
% 6.49/6.48 inference(contradiction_clause,[status(thm)],[f1810])).
% 6.49/6.48 fof(f2533,definition,(
% 6.49/6.48 sQ79_spl <=> (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f2535,plain,(
% 6.49/6.48 ~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ79_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f2533])).
% 6.49/6.48 fof(f2795,definition,(
% 6.49/6.48 sQ109_spl <=> (c_HOL_Otimes__class_Otimes(v_t____,v_t____,tc_RealDef_Oreal)=v_t____)),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f2796,plain,(
% 6.49/6.48 c_HOL_Otimes__class_Otimes(v_t____,v_t____,tc_RealDef_Oreal)=v_t____|~sQ109_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f2795])).
% 6.49/6.48 fof(f3474,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_t____,v_t____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 6.49/6.48 inference(resolution,[status(thm)],[f1689,f1461])).
% 6.49/6.48 fof(f3478,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_t____,v_t____,tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)),
% 6.49/6.48 inference(forward_demodulation,[status(thm)],[f1674,f3474])).
% 6.49/6.48 fof(f3490,plain,(
% 6.49/6.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat)),
% 6.49/6.48 inference(resolution,[status(thm)],[f1334,f1563])).
% 6.49/6.48 fof(f3930,definition,(
% 6.49/6.48 ![X0]: (sQ232_spl <=> (~X0=X0))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f3931,plain,(
% 6.49/6.48 ![X0]: (~X0=X0|~sQ232_spl)),
% 6.49/6.48 inference(component_clause,[status(thm)],[f3930])).
% 6.49/6.48 fof(f4149,definition,(
% 6.49/6.48 sQ246_spl <=> (class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f4151,plain,(
% 6.49/6.48 ~class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)|sQ246_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f4149])).
% 6.49/6.48 fof(f4157,plain,(
% 6.49/6.48 $false|sQ246_spl),
% 6.49/6.48 inference(forward_subsumption_resolution,[status(thm)],[f4151,f1650])).
% 6.49/6.48 fof(f4158,plain,(
% 6.49/6.48 sQ246_spl),
% 6.49/6.48 inference(contradiction_clause,[status(thm)],[f4157])).
% 6.49/6.48 fof(f4161,definition,(
% 6.49/6.48 sQ248_spl <=> (class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal))),
% 6.49/6.48 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 6.49/6.48 fof(f4163,plain,(
% 6.49/6.48 ~class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal)|sQ248_spl),
% 6.49/6.48 inference(component_clause,[status(thm)],[f4161])).
% 6.49/6.48 fof(f4166,plain,(
% 6.49/6.48 $false|sQ248_spl),
% 6.49/6.48 inference(forward_subsumption_resolution,[status(thm)],[f4163,f1630])).
% 6.49/6.49 fof(f4167,plain,(
% 6.49/6.49 sQ248_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f4166])).
% 6.49/6.49 fof(f4170,definition,(
% 6.49/6.49 sQ249_spl <=> (class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f4172,plain,(
% 6.49/6.49 ~class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)|sQ249_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f4170])).
% 6.49/6.49 fof(f4175,plain,(
% 6.49/6.49 $false|sQ249_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f4172,f1588])).
% 6.49/6.49 fof(f4176,plain,(
% 6.49/6.49 sQ249_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f4175])).
% 6.49/6.49 fof(f4193,definition,(
% 6.49/6.49 sQ251_spl <=> (class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f4195,plain,(
% 6.49/6.49 ~class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)|sQ251_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f4193])).
% 6.49/6.49 fof(f4341,plain,(
% 6.49/6.49 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 6.49/6.49 inference(resolution,[status(thm)],[f905,f1635])).
% 6.49/6.49 fof(f4497,definition,(
% 6.49/6.49 sQ282_spl <=> (class_Orderings_Olinorder(tc_nat))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f4499,plain,(
% 6.49/6.49 ~class_Orderings_Olinorder(tc_nat)|sQ282_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f4497])).
% 6.49/6.49 fof(f4540,plain,(
% 6.49/6.49 $false|sQ282_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f4499,f1578])).
% 6.49/6.49 fof(f4541,plain,(
% 6.49/6.49 sQ282_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f4540])).
% 6.49/6.49 fof(f4703,plain,(
% 6.49/6.49 $false|sQ79_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f2535,f1492])).
% 6.49/6.49 fof(f4704,plain,(
% 6.49/6.49 sQ79_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f4703])).
% 6.49/6.49 fof(f4747,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)|~sQ0_spl),
% 6.49/6.49 inference(resolution,[status(thm)],[f1701,f1774])).
% 6.49/6.49 fof(f4758,definition,(
% 6.49/6.49 sQ310_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f4759,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)|~sQ310_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f4758])).
% 6.49/6.49 fof(f4761,definition,(
% 6.49/6.49 sQ311_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f4763,plain,(
% 6.49/6.49 ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ311_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f4761])).
% 6.49/6.49 fof(f4764,plain,(
% 6.49/6.49 sQ310_spl|~sQ311_spl|~sQ0_spl),
% 6.49/6.49 inference(split_clause,[status(thm)],[f4747,f4758,f4761,f1700])).
% 6.49/6.49 fof(f4784,plain,(
% 6.49/6.49 c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)|~sQ310_spl),
% 6.49/6.49 inference(resolution,[status(thm)],[f4759,f1210])).
% 6.49/6.49 fof(f4794,plain,(
% 6.49/6.49 $false|sQ8_spl|~sQ310_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f4784,f1740])).
% 6.49/6.49 fof(f4795,plain,(
% 6.49/6.49 sQ8_spl|~sQ310_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f4794])).
% 6.49/6.49 fof(f4938,definition,(
% 6.49/6.49 ![X0]: (sQ321_spl <=> (~class_OrderedGroup_Ogroup__add(X0)))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f4939,plain,(
% 6.49/6.49 ![X0]: (~class_OrderedGroup_Ogroup__add(X0)|~sQ321_spl)),
% 6.49/6.49 inference(component_clause,[status(thm)],[f4938])).
% 6.49/6.49 fof(f4944,plain,(
% 6.49/6.49 $false|~sQ321_spl),
% 6.49/6.49 inference(backward_subsumption_resolution,[status(thm)],[f1663,f4939])).
% 6.49/6.49 fof(f4946,plain,(
% 6.49/6.49 ~sQ321_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f4944])).
% 6.49/6.49 fof(f5040,plain,(
% 6.49/6.49 $false|sQ251_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f4195,f1596])).
% 6.49/6.49 fof(f5041,plain,(
% 6.49/6.49 sQ251_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5040])).
% 6.49/6.49 fof(f5119,plain,(
% 6.49/6.49 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 6.49/6.49 inference(resolution,[status(thm)],[f1104,f1591])).
% 6.49/6.49 fof(f5157,definition,(
% 6.49/6.49 sQ334_spl <=> (class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5159,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal)|sQ334_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5157])).
% 6.49/6.49 fof(f5164,plain,(
% 6.49/6.49 $false|sQ334_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5159,f1593])).
% 6.49/6.49 fof(f5165,plain,(
% 6.49/6.49 sQ334_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5164])).
% 6.49/6.49 fof(f5173,definition,(
% 6.49/6.49 sQ336_spl <=> (class_Ring__and__Field_Oordered__semiring__strict(tc_nat))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5175,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Oordered__semiring__strict(tc_nat)|sQ336_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5173])).
% 6.49/6.49 fof(f5180,definition,(
% 6.49/6.49 sQ338_spl <=> (class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5182,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)|sQ338_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5180])).
% 6.49/6.49 fof(f5207,plain,(
% 6.49/6.49 $false|sQ338_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5182,f1586])).
% 6.49/6.49 fof(f5208,plain,(
% 6.49/6.49 sQ338_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5207])).
% 6.49/6.49 fof(f5209,plain,(
% 6.49/6.49 $false|sQ336_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5175,f1555])).
% 6.49/6.49 fof(f5210,plain,(
% 6.49/6.49 sQ336_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5209])).
% 6.49/6.49 fof(f5223,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(v_t____,v_t____,tc_RealDef_Oreal)|~sQ109_spl),
% 6.49/6.49 inference(backward_demodulation,[status(thm)],[f2796,f3478])).
% 6.49/6.49 fof(f5247,plain,(
% 6.49/6.49 $false|~sQ109_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5223,f1314])).
% 6.49/6.49 fof(f5248,plain,(
% 6.49/6.49 ~sQ109_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5247])).
% 6.49/6.49 fof(f5295,plain,(
% 6.49/6.49 $false|~sQ232_spl),
% 6.49/6.49 inference(trivial_equality_resolution,[status(thm)],[f3931])).
% 6.49/6.49 fof(f5296,plain,(
% 6.49/6.49 ~sQ232_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5295])).
% 6.49/6.49 fof(f5454,definition,(
% 6.49/6.49 sQ355_spl <=> (class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5456,plain,(
% 6.49/6.49 ~class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)|sQ355_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5454])).
% 6.49/6.49 fof(f5460,plain,(
% 6.49/6.49 $false|sQ355_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5456,f1609])).
% 6.49/6.49 fof(f5461,plain,(
% 6.49/6.49 sQ355_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5460])).
% 6.49/6.49 fof(f5537,definition,(
% 6.49/6.49 ![X0]: (sQ369_spl <=> (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5538,plain,(
% 6.49/6.49 ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ369_spl)),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5537])).
% 6.49/6.49 fof(f5554,plain,(
% 6.49/6.49 ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ369_spl)),
% 6.49/6.49 inference(duplicate_literals_removal,[status(thm)],[f5538])).
% 6.49/6.49 fof(f5644,plain,(
% 6.49/6.49 c_lessequals(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ311_spl),
% 6.49/6.49 inference(resolution,[status(thm)],[f4763,f4341])).
% 6.49/6.49 fof(f5757,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|sQ311_spl),
% 6.49/6.49 inference(resolution,[status(thm)],[f5644,f1213])).
% 6.49/6.49 fof(f5762,definition,(
% 6.49/6.49 sQ386_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5763,plain,(
% 6.49/6.49 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)|~sQ386_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5762])).
% 6.49/6.49 fof(f5769,definition,(
% 6.49/6.49 sQ388_spl <=> (c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5770,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ388_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5769])).
% 6.49/6.49 fof(f5772,plain,(
% 6.49/6.49 sQ388_spl|sQ386_spl|sQ311_spl),
% 6.49/6.49 inference(split_clause,[status(thm)],[f5757,f5769,f5762,f4761])).
% 6.49/6.49 fof(f5794,plain,(
% 6.49/6.49 $false|~sQ369_spl),
% 6.49/6.49 inference(backward_subsumption_resolution,[status(thm)],[f3490,f5554])).
% 6.49/6.49 fof(f5796,plain,(
% 6.49/6.49 ~sQ369_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5794])).
% 6.49/6.49 fof(f5798,plain,(
% 6.49/6.49 ~c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ386_spl|sQ1_spl),
% 6.49/6.49 inference(backward_demodulation,[status(thm)],[f5763,f1705])).
% 6.49/6.49 fof(f5819,plain,(
% 6.49/6.49 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ386_spl|sQ1_spl),
% 6.49/6.49 inference(forward_demodulation,[status(thm)],[f5763,f5798])).
% 6.49/6.49 fof(f5930,definition,(
% 6.49/6.49 sQ404_spl <=> (class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5932,plain,(
% 6.49/6.49 ~class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex)|sQ404_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5930])).
% 6.49/6.49 fof(f5971,definition,(
% 6.49/6.49 sQ415_spl <=> (class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f5973,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)|sQ415_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f5971])).
% 6.49/6.49 fof(f5998,plain,(
% 6.49/6.49 $false|sQ404_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5932,f1655])).
% 6.49/6.49 fof(f5999,plain,(
% 6.49/6.49 sQ404_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f5998])).
% 6.49/6.49 fof(f6000,plain,(
% 6.49/6.49 $false|sQ415_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f5973,f1656])).
% 6.49/6.49 fof(f6001,plain,(
% 6.49/6.49 sQ415_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f6000])).
% 6.49/6.49 fof(f6444,plain,(
% 6.49/6.49 ~class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)|~sQ388_spl),
% 6.49/6.49 inference(resolution,[status(thm)],[f5770,f738])).
% 6.49/6.49 fof(f6464,plain,(
% 6.49/6.49 ~sQ246_spl|~sQ388_spl),
% 6.49/6.49 inference(split_clause,[status(thm)],[f6444,f4149,f5769])).
% 6.49/6.49 fof(f7057,definition,(
% 6.49/6.49 sQ503_spl <=> (class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ503_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f7059,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal)|sQ503_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f7057])).
% 6.49/6.49 fof(f7104,plain,(
% 6.49/6.49 $false|sQ503_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f7059,f1618])).
% 6.49/6.49 fof(f7105,plain,(
% 6.49/6.49 sQ503_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f7104])).
% 6.49/6.49 fof(f7447,definition,(
% 6.49/6.49 sQ532_spl <=> (class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ532_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f7449,plain,(
% 6.49/6.49 ~class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)|sQ532_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f7447])).
% 6.49/6.49 fof(f7454,definition,(
% 6.49/6.49 sQ534_spl <=> (class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ534_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f7456,plain,(
% 6.49/6.49 ~class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)|sQ534_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f7454])).
% 6.49/6.49 fof(f7522,plain,(
% 6.49/6.49 $false|sQ534_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f7456,f1658])).
% 6.49/6.49 fof(f7523,plain,(
% 6.49/6.49 sQ534_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f7522])).
% 6.49/6.49 fof(f7524,plain,(
% 6.49/6.49 $false|sQ532_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f7449,f1622])).
% 6.49/6.49 fof(f7525,plain,(
% 6.49/6.49 sQ532_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f7524])).
% 6.49/6.49 fof(f7774,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(v_t____),c_NthRoot_Osqrt(c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),tc_RealDef_Oreal)),
% 6.49/6.49 inference(resolution,[status(thm)],[f794,f1461])).
% 6.49/6.49 fof(f7782,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(v_t____),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 6.49/6.49 inference(forward_demodulation,[status(thm)],[f1229,f7774])).
% 6.49/6.49 fof(f7827,definition,(
% 6.49/6.49 sQ572_spl <=> (class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f7829,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat)|sQ572_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f7827])).
% 6.49/6.49 fof(f7838,definition,(
% 6.49/6.49 sQ575_spl <=> (class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ575_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f7840,plain,(
% 6.49/6.49 ~class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal)|sQ575_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f7838])).
% 6.49/6.49 fof(f7856,plain,(
% 6.49/6.49 $false|sQ575_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f7840,f1583])).
% 6.49/6.49 fof(f7857,plain,(
% 6.49/6.49 sQ575_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f7856])).
% 6.49/6.49 fof(f7858,plain,(
% 6.49/6.49 $false|sQ572_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f7829,f1553])).
% 6.49/6.49 fof(f7859,plain,(
% 6.49/6.49 sQ572_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f7858])).
% 6.49/6.49 fof(f8024,definition,(
% 6.49/6.49 sQ592_spl <=> (c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_NthRoot_Osqrt(v_t____))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f8025,plain,(
% 6.49/6.49 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_NthRoot_Osqrt(v_t____)|~sQ592_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f8024])).
% 6.49/6.49 fof(f8033,plain,(
% 6.49/6.49 c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(v_t____),c_NthRoot_Osqrt(v_t____),tc_RealDef_Oreal)|~sQ592_spl),
% 6.49/6.49 inference(backward_demodulation,[status(thm)],[f8025,f7782])).
% 6.49/6.49 fof(f8078,plain,(
% 6.49/6.49 $false|~sQ592_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f8033,f1314])).
% 6.49/6.49 fof(f8079,plain,(
% 6.49/6.49 ~sQ592_spl),
% 6.49/6.49 inference(contradiction_clause,[status(thm)],[f8078])).
% 6.49/6.49 fof(f9401,definition,(
% 6.49/6.49 sQ673_spl <=> (class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ673_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f9403,plain,(
% 6.49/6.49 ~class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal)|sQ673_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f9401])).
% 6.49/6.49 fof(f9448,definition,(
% 6.49/6.49 sQ685_spl <=> (class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat))),
% 6.49/6.49 introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition])).
% 6.49/6.49 fof(f9450,plain,(
% 6.49/6.49 ~class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat)|sQ685_spl),
% 6.49/6.49 inference(component_clause,[status(thm)],[f9448])).
% 6.49/6.49 fof(f9463,plain,(
% 6.49/6.49 $false|sQ673_spl),
% 6.49/6.49 inference(forward_subsumption_resolution,[status(thm)],[f9403,f1581])).
% 6.49/6.51 fof(f9464,plain,(
% 6.49/6.51 sQ673_spl),
% 6.49/6.51 inference(contradiction_clause,[status(thm)],[f9463])).
% 6.49/6.51 fof(f9465,plain,(
% 6.49/6.51 $false|sQ685_spl),
% 6.49/6.51 inference(forward_subsumption_resolution,[status(thm)],[f9450,f1551])).
% 6.49/6.51 fof(f9466,plain,(
% 6.49/6.51 sQ685_spl),
% 6.49/6.51 inference(contradiction_clause,[status(thm)],[f9465])).
% 6.49/6.51 fof(f9868,definition,(
% 6.49/6.51 sQ737_spl <=> (class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal))),
% 6.49/6.51 introduced(definition,[new_symbols(definition,[sQ737_spl])],[split_symbol_definition])).
% 6.49/6.51 fof(f9870,plain,(
% 6.49/6.51 ~class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal)|sQ737_spl),
% 6.49/6.51 inference(component_clause,[status(thm)],[f9868])).
% 6.49/6.51 fof(f9875,definition,(
% 6.49/6.51 sQ739_spl <=> (class_RealVector_Oreal__algebra__1(tc_Complex_Ocomplex))),
% 6.49/6.51 introduced(definition,[new_symbols(definition,[sQ739_spl])],[split_symbol_definition])).
% 6.49/6.51 fof(f9877,plain,(
% 6.49/6.51 ~class_RealVector_Oreal__algebra__1(tc_Complex_Ocomplex)|sQ739_spl),
% 6.49/6.51 inference(component_clause,[status(thm)],[f9875])).
% 6.49/6.51 fof(f9895,plain,(
% 6.49/6.51 $false|sQ739_spl),
% 6.49/6.51 inference(forward_subsumption_resolution,[status(thm)],[f9877,f1657])).
% 6.49/6.51 fof(f9896,plain,(
% 6.49/6.51 sQ739_spl),
% 6.49/6.51 inference(contradiction_clause,[status(thm)],[f9895])).
% 6.49/6.51 fof(f9897,plain,(
% 6.49/6.51 $false|sQ737_spl),
% 6.49/6.51 inference(forward_subsumption_resolution,[status(thm)],[f9870,f1621])).
% 6.49/6.51 fof(f9898,plain,(
% 6.49/6.51 sQ737_spl),
% 6.49/6.51 inference(contradiction_clause,[status(thm)],[f9897])).
% 6.49/6.51 fof(f11037,plain,(
% 6.49/6.51 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ386_spl|sQ1_spl),
% 6.49/6.51 inference(forward_demodulation,[status(thm)],[f5119,f5819])).
% 6.49/6.51 fof(f11038,plain,(
% 6.49/6.51 $false|~sQ386_spl|sQ1_spl),
% 6.49/6.51 inference(trivial_equality_resolution,[status(thm)],[f11037])).
% 6.49/6.51 fof(f11039,plain,(
% 6.49/6.51 ~sQ386_spl|sQ1_spl),
% 6.49/6.51 inference(contradiction_clause,[status(thm)],[f11038])).
% 6.49/6.51 fof(f11040,plain,(
% 6.49/6.51 $false),
% 6.49/6.51 inference(sat_refutation,[status(thm)],[f1706,f1741,f1748,f1811,f4158,f4167,f4176,f4541,f4704,f4764,f4795,f4946,f5041,f5165,f5208,f5210,f5248,f5296,f5461,f5772,f5796,f5999,f6001,f6464,f7105,f7523,f7525,f7857,f7859,f8079,f9464,f9466,f9896,f9898,f11039])).
% 6.49/6.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.73/6.53 % Elapsed time: 1.022359 seconds
% 0.73/6.53 % CPU time: 7.248606 seconds
% 0.73/6.53 % Total memory used: 190.067 MB
% 0.73/6.53 % Net memory used: 186.351 MB
%------------------------------------------------------------------------------