%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG373-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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:50:06 AM UTC 2026
% Result : Unsatisfiable 22.51s 18.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG373-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/15.43 % Computer : n008.cluster.edu
% 0.15/15.43 % Model : x86_64 x86_64
% 0.15/15.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/15.43 % Memory : 8046.5625MB
% 0.15/15.43 % OS : Linux 6.8.0-71-generic
% 0.15/15.43 % CPULimit : 300
% 0.15/15.43 % WCLimit : 300
% 0.15/15.43 % DateTime : Mon Sep 21 13:19:11 UTC 2026
% 0.15/15.43 % CPUTime :
% 0.15/15.48 % Drodi V4.1.1
% 22.51/18.36 % Refutation found
% 22.51/18.36 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.51/18.36 % SZS output start CNFRefutation for theBenchmark
% 22.51/18.36 fof(f94,axiom,(
% 22.51/18.36 (![T_a,V_a]: (( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a)| c_lessequals(V_a,c_HOL_Oabs__class_Oabs(V_a,T_a),T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f105,axiom,(
% 22.51/18.36 (![T_a,V_a]: (( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a)| c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) = c_HOL_Oabs__class_Oabs(V_a,T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f112,axiom,(
% 22.51/18.36 (![T_a,V_a]: (( ~ class_OrderedGroup_Oordered__ab__group__add(T_a)| c_HOL_Ouminus__class_Ouminus(V_a,T_a) != V_a| V_a = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f132,axiom,(
% 22.51/18.36 (![T_a,V_a]: (( ~ class_RealVector_Oreal__normed__vector(T_a)| c_HOL_Oabs__class_Oabs(c_RealVector_Onorm__class_Onorm(V_a,T_a),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(V_a,T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f142,axiom,(
% 22.51/18.36 (![T_a,V_a]: (( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a)| c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Oabs__class_Oabs(V_a,T_a),T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f188,axiom,(
% 22.51/18.36 (![V_p,V_r]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(V_p,V_r),tc_RealDef_Oreal) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f232,axiom,(
% 22.51/18.36 (![V_r]: (( c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r| c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f250,axiom,(
% 22.51/18.36 (![T_a,V_a]: (( ~ class_OrderedGroup_Olordered__ab__group__add(T_a)| c_lessequals(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)| ~ c_lessequals(V_a,c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f266,axiom,(
% 22.51/18.36 (![V_r,V_x]: (( c_lessequals(c_HOL_Ouminus__class_Ouminus(V_r,tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)| ~ c_lessequals(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),V_r,tc_RealDef_Oreal) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f270,axiom,(
% 22.51/18.36 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f275,axiom,(
% 22.51/18.36 (![T_a,V_a,V_b]: (( ~ class_Orderings_Oorder(T_a)| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f277,axiom,(
% 22.51/18.36 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f288,axiom,(
% 22.51/18.36 (![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) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f292,axiom,(
% 22.51/18.36 (![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) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f300,axiom,(
% 22.51/18.36 (![V_x]: (c_lessequals(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(V_x,tc_Complex_Ocomplex),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(V_x,tc_Complex_Ocomplex),tc_RealDef_Oreal) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f307,axiom,(
% 22.51/18.36 (![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) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f318,axiom,(
% 22.51/18.36 (![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) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f327,axiom,(
% 22.51/18.36 (![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) ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f335,axiom,(
% 22.51/18.36 (![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 ) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f350,negated_conjecture,(
% 22.51/18.36 (![V_xb]: (c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_xa(V_xb),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ouminus__class_Ouminus(v_x(V_xb),tc_RealDef_Oreal) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f351,negated_conjecture,(
% 22.51/18.36 (![V_xb]: (~ c_HOL_Oord__class_Oless(v_x(V_xb),V_xb,tc_RealDef_Oreal) ))),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f370,axiom,(
% 22.51/18.36 class_Ring__and__Field_Oordered__ring__strict(tc_Int_Oint) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f391,axiom,(
% 22.51/18.36 class_Orderings_Opreorder(tc_Int_Oint) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f400,axiom,(
% 22.51/18.36 class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f406,axiom,(
% 22.51/18.36 class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f407,axiom,(
% 22.51/18.36 class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f416,axiom,(
% 22.51/18.36 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f427,axiom,(
% 22.51/18.36 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f431,axiom,(
% 22.51/18.36 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f433,axiom,(
% 22.51/18.36 class_Orderings_Oorder(tc_RealDef_Oreal) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f444,axiom,(
% 22.51/18.36 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 22.51/18.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.51/18.36 fof(f651,plain,(
% 22.51/18.36 ![T_a]: (~class_OrderedGroup_Opordered__ab__group__add__abs(T_a)|(![V_a]: c_lessequals(V_a,c_HOL_Oabs__class_Oabs(V_a,T_a),T_a)))),
% 22.51/18.36 inference(miniscoping,[status(thm)],[f94])).
% 22.51/18.36 fof(f652,plain,(
% 22.51/18.36 ![X0,X1]: (~class_OrderedGroup_Opordered__ab__group__add__abs(X0)|c_lessequals(X1,c_HOL_Oabs__class_Oabs(X1,X0),X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f651])).
% 22.51/18.36 fof(f665,plain,(
% 22.51/18.36 ![T_a]: (~class_OrderedGroup_Opordered__ab__group__add__abs(T_a)|(![V_a]: c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a)=c_HOL_Oabs__class_Oabs(V_a,T_a)))),
% 22.51/18.36 inference(miniscoping,[status(thm)],[f105])).
% 22.51/18.36 fof(f666,plain,(
% 22.51/18.36 ![X0,X1]: (~class_OrderedGroup_Opordered__ab__group__add__abs(X0)|c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(X1,X0),X0)=c_HOL_Oabs__class_Oabs(X1,X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f665])).
% 22.51/18.36 fof(f679,plain,(
% 22.51/18.36 ![X0,X1]: (~class_OrderedGroup_Oordered__ab__group__add(X0)|~c_HOL_Ouminus__class_Ouminus(X1,X0)=X1|X1=c_HOL_Ozero__class_Ozero(X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f112])).
% 22.51/18.36 fof(f710,plain,(
% 22.51/18.36 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(![V_a]: c_HOL_Oabs__class_Oabs(c_RealVector_Onorm__class_Onorm(V_a,T_a),tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(V_a,T_a)))),
% 22.51/18.36 inference(miniscoping,[status(thm)],[f132])).
% 22.51/18.36 fof(f711,plain,(
% 22.51/18.36 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_HOL_Oabs__class_Oabs(c_RealVector_Onorm__class_Onorm(X1,X0),tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(X1,X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f710])).
% 22.51/18.36 fof(f721,plain,(
% 22.51/18.36 ![T_a]: (~class_OrderedGroup_Opordered__ab__group__add__abs(T_a)|(![V_a]: c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Oabs__class_Oabs(V_a,T_a),T_a)))),
% 22.51/18.36 inference(miniscoping,[status(thm)],[f142])).
% 22.51/18.36 fof(f722,plain,(
% 22.51/18.36 ![X0,X1]: (~class_OrderedGroup_Opordered__ab__group__add__abs(X0)|c_lessequals(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Oabs__class_Oabs(X1,X0),X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f721])).
% 22.51/18.36 fof(f803,plain,(
% 22.51/18.36 ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f188])).
% 22.51/18.36 fof(f886,plain,(
% 22.51/18.36 ![X0]: (c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)=X0|c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f232])).
% 22.51/18.36 fof(f910,plain,(
% 22.51/18.36 ![X0,X1]: (~class_OrderedGroup_Olordered__ab__group__add(X0)|c_lessequals(X1,c_HOL_Ozero__class_Ozero(X0),X0)|~c_lessequals(X1,c_HOL_Ouminus__class_Ouminus(X1,X0),X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f250])).
% 22.51/18.36 fof(f933,plain,(
% 22.51/18.36 ![X0,X1]: (c_lessequals(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f266])).
% 22.51/18.36 fof(f938,plain,(
% 22.51/18.36 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f270])).
% 22.51/18.36 fof(f945,plain,(
% 22.51/18.36 ![X0,X1,X2]: (~class_Orderings_Oorder(X0)|~c_HOL_Oord__class_Oless(X1,X2,X0)|~c_HOL_Oord__class_Oless(X2,X1,X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f275])).
% 22.51/18.36 fof(f947,plain,(
% 22.51/18.36 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f277])).
% 22.51/18.36 fof(f964,plain,(
% 22.51/18.36 ![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))),
% 22.51/18.36 inference(miniscoping,[status(thm)],[f288])).
% 22.51/18.36 fof(f965,plain,(
% 22.51/18.36 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f964])).
% 22.51/18.36 fof(f971,plain,(
% 22.51/18.36 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f292])).
% 22.51/18.36 fof(f983,plain,(
% 22.51/18.36 ![X0]: (c_lessequals(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f300])).
% 22.51/18.36 fof(f992,plain,(
% 22.51/18.36 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f307])).
% 22.51/18.36 fof(f1005,plain,(
% 22.51/18.36 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f318])).
% 22.51/18.36 fof(f1018,plain,(
% 22.51/18.36 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|~c_lessequals(X1,X2,X0)|~c_HOL_Oord__class_Oless(X2,X1,X0))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f327])).
% 22.51/18.36 fof(f1026,plain,(
% 22.51/18.36 ![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))),
% 22.51/18.36 inference(miniscoping,[status(thm)],[f335])).
% 22.51/18.36 fof(f1027,plain,(
% 22.51/18.36 ![X0,X1]: (~class_OrderedGroup_Ogroup__add(X0)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0)=X1)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f1026])).
% 22.51/18.36 fof(f1047,plain,(
% 22.51/18.36 ![X0]: (c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_xa(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f350])).
% 22.51/18.36 fof(f1048,plain,(
% 22.51/18.36 ![X0]: (~c_HOL_Oord__class_Oless(v_x(X0),X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f351])).
% 22.51/18.36 fof(f1067,plain,(
% 22.51/18.36 class_Ring__and__Field_Oordered__ring__strict(tc_Int_Oint)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f370])).
% 22.51/18.36 fof(f1088,plain,(
% 22.51/18.36 class_Orderings_Opreorder(tc_Int_Oint)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f391])).
% 22.51/18.36 fof(f1097,plain,(
% 22.51/18.36 class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f400])).
% 22.51/18.36 fof(f1103,plain,(
% 22.51/18.36 class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f406])).
% 22.51/18.36 fof(f1104,plain,(
% 22.51/18.36 class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f407])).
% 22.51/18.36 fof(f1113,plain,(
% 22.51/18.36 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f416])).
% 22.51/18.36 fof(f1124,plain,(
% 22.51/18.36 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f427])).
% 22.51/18.36 fof(f1128,plain,(
% 22.51/18.36 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f431])).
% 22.51/18.36 fof(f1130,plain,(
% 22.51/18.36 class_Orderings_Oorder(tc_RealDef_Oreal)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f433])).
% 22.51/18.36 fof(f1141,plain,(
% 22.51/18.36 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 22.51/18.36 inference(cnf_transformation,[status(thm)],[f444])).
% 22.51/18.36 fof(f1198,plain,(
% 22.51/18.36 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r),
% 22.51/18.36 inference(resolution,[status(thm)],[f992,f938])).
% 22.51/18.36 fof(f1202,plain,(
% 22.51/18.36 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(resolution,[status(thm)],[f992,f947])).
% 22.51/18.36 fof(f1206,definition,(
% 22.51/18.36 sQ2_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal))),
% 22.51/18.36 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 22.51/18.36 fof(f1207,plain,(
% 22.51/18.36 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)|~sQ2_spl),
% 22.51/18.36 inference(component_clause,[status(thm)],[f1206])).
% 22.51/18.36 fof(f1209,definition,(
% 22.51/18.36 sQ3_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r)),
% 22.51/18.36 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 22.51/18.36 fof(f1210,plain,(
% 22.51/18.36 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|~sQ3_spl),
% 22.51/18.36 inference(component_clause,[status(thm)],[f1209])).
% 22.51/18.36 fof(f1212,plain,(
% 22.51/18.36 sQ2_spl|sQ3_spl),
% 22.51/18.36 inference(split_clause,[status(thm)],[f1198,f1206,f1209])).
% 22.51/18.36 fof(f1217,plain,(
% 22.51/18.36 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)),
% 22.51/18.36 inference(resolution,[status(thm)],[f1005,f938])).
% 22.51/18.36 fof(f1219,plain,(
% 22.51/18.36 ![X0,X1]: (X0=X1|~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(resolution,[status(thm)],[f1005,f971])).
% 22.51/18.36 fof(f1225,definition,(
% 22.51/18.36 sQ4_spl <=> (c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.36 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 22.51/18.36 fof(f1227,plain,(
% 22.51/18.36 ~c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ4_spl),
% 22.51/18.36 inference(component_clause,[status(thm)],[f1225])).
% 22.51/18.36 fof(f1228,plain,(
% 22.51/18.36 sQ3_spl|~sQ4_spl),
% 22.51/18.36 inference(split_clause,[status(thm)],[f1217,f1209,f1225])).
% 22.51/18.36 fof(f1240,plain,(
% 22.51/18.36 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|X1=X0)),
% 22.51/18.36 inference(resolution,[status(thm)],[f1202,f992])).
% 22.51/18.36 fof(f1242,plain,(
% 22.51/18.36 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(duplicate_literals_removal,[status(thm)],[f1240])).
% 22.51/18.36 fof(f1271,plain,(
% 22.51/18.36 ![X0]: (v_x(X0)=X0|c_HOL_Oord__class_Oless(X0,v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.36 inference(resolution,[status(thm)],[f1242,f1048])).
% 22.51/18.36 fof(f1306,plain,(
% 22.51/18.36 ~c_HOL_Oord__class_Oless(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ4_spl),
% 22.51/18.36 inference(resolution,[status(thm)],[f1227,f971])).
% 22.51/18.36 fof(f1333,plain,(
% 22.51/18.36 ![X0]: (v_x(X0)=X0|v_x(X0)=X0|~c_lessequals(v_x(X0),X0,tc_RealDef_Oreal))),
% 22.51/18.36 inference(resolution,[status(thm)],[f1271,f1219])).
% 22.51/18.36 fof(f1334,definition,(
% 22.51/18.36 sQ10_spl <=> (v_x(v_r)=v_r)),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f1335,plain,(
% 22.51/18.37 v_x(v_r)=v_r|~sQ10_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f1334])).
% 22.51/18.37 fof(f1341,plain,(
% 22.51/18.37 ![X0]: (v_x(X0)=X0|~c_lessequals(v_x(X0),X0,tc_RealDef_Oreal))),
% 22.51/18.37 inference(duplicate_literals_removal,[status(thm)],[f1333])).
% 22.51/18.37 fof(f1350,plain,(
% 22.51/18.37 ![X0]: (v_x(X0)=X0|c_lessequals(X0,v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f1341,f947])).
% 22.51/18.37 fof(f1498,plain,(
% 22.51/18.37 ![X0,X1]: (~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(v_x(X1),X0,tc_RealDef_Oreal)|v_x(X1)=X1)),
% 22.51/18.37 inference(resolution,[status(thm)],[f965,f1341])).
% 22.51/18.37 fof(f1499,plain,(
% 22.51/18.37 ![X0]: (~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(v_r,X0,tc_RealDef_Oreal)|sQ4_spl)),
% 22.51/18.37 inference(resolution,[status(thm)],[f965,f1227])).
% 22.51/18.37 fof(f1552,plain,(
% 22.51/18.37 ![X0]: (c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_xa(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 22.51/18.37 inference(paramodulation,[status(thm)],[f1047,f983])).
% 22.51/18.37 fof(f1554,plain,(
% 22.51/18.37 ![X0]: (c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f1047,f1552])).
% 22.51/18.37 fof(f1599,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f1554,f992])).
% 22.51/18.37 fof(f1604,plain,(
% 22.51/18.37 ![X0]: (~c_lessequals(v_r,X0,tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|sQ4_spl)),
% 22.51/18.37 inference(resolution,[status(thm)],[f1499,f947])).
% 22.51/18.37 fof(f2000,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|~sQ10_spl),
% 22.51/18.37 inference(paramodulation,[status(thm)],[f1335,f1599])).
% 22.51/18.37 fof(f2017,definition,(
% 22.51/18.37 sQ74_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f2018,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ74_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2017])).
% 22.51/18.37 fof(f2020,definition,(
% 22.51/18.37 sQ75_spl <=> (c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f2021,plain,(
% 22.51/18.37 c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|~sQ75_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2020])).
% 22.51/18.37 fof(f2022,plain,(
% 22.51/18.37 ~c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|sQ75_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2020])).
% 22.51/18.37 fof(f2023,plain,(
% 22.51/18.37 sQ74_spl|sQ75_spl|~sQ10_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f2000,f2017,f2020,f1334])).
% 22.51/18.37 fof(f2032,definition,(
% 22.51/18.37 sQ78_spl <=> (c_HOL_Oord__class_Oless(v_x(v_r),v_r,tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f2033,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(v_x(v_r),v_r,tc_RealDef_Oreal)|~sQ78_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2032])).
% 22.51/18.37 fof(f2040,definition,(
% 22.51/18.37 sQ80_spl <=> (c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f2041,plain,(
% 22.51/18.37 c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ80_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2040])).
% 22.51/18.37 fof(f2042,plain,(
% 22.51/18.37 ~c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ80_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2040])).
% 22.51/18.37 fof(f2852,plain,(
% 22.51/18.37 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|v_x(v_r)=v_r|sQ4_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f1604,f1350])).
% 22.51/18.37 fof(f2865,definition,(
% 22.51/18.37 sQ139_spl <=> (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f2866,plain,(
% 22.51/18.37 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|~sQ139_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f2865])).
% 22.51/18.37 fof(f2868,plain,(
% 22.51/18.37 sQ139_spl|sQ10_spl|sQ4_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f2852,f2865,f1334,f1225])).
% 22.51/18.37 fof(f2996,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_x(v_r)|~sQ139_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f2866,f992])).
% 22.51/18.37 fof(f3000,definition,(
% 22.51/18.37 sQ147_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_x(v_r))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f3001,plain,(
% 22.51/18.37 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_x(v_r)|~sQ147_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f3000])).
% 22.51/18.37 fof(f3008,definition,(
% 22.51/18.37 sQ149_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f3009,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|~sQ149_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f3008])).
% 22.51/18.37 fof(f3011,plain,(
% 22.51/18.37 sQ149_spl|sQ147_spl|~sQ139_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f2996,f3008,f3000,f2865])).
% 22.51/18.37 fof(f3024,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(v_x(v_r),v_r,tc_RealDef_Oreal)|~sQ147_spl|~sQ2_spl),
% 22.51/18.37 inference(backward_demodulation,[status(thm)],[f3001,f1207])).
% 22.51/18.37 fof(f3038,plain,(
% 22.51/18.37 $false|~sQ147_spl|~sQ2_spl),
% 22.51/18.37 inference(forward_subsumption_resolution,[status(thm)],[f3024,f1048])).
% 22.51/18.37 fof(f3039,plain,(
% 22.51/18.37 ~sQ147_spl|~sQ2_spl),
% 22.51/18.37 inference(contradiction_clause,[status(thm)],[f3038])).
% 22.51/18.37 fof(f3221,plain,(
% 22.51/18.37 ![X0]: (c_lessequals(X0,c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f652,f1097])).
% 22.51/18.37 fof(f3226,plain,(
% 22.51/18.37 ![X0]: (~c_lessequals(c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|v_x(X0)=X0)),
% 22.51/18.37 inference(resolution,[status(thm)],[f3221,f1498])).
% 22.51/18.37 fof(f3356,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 22.51/18.37 inference(resolution,[status(thm)],[f1027,f1124])).
% 22.51/18.37 fof(f3362,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)|v_x(X0)=c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.37 inference(backward_demodulation,[status(thm)],[f3356,f1599])).
% 22.51/18.37 fof(f3369,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Oord__class_Oless(v_x(X0),c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)|v_x(X0)=c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f3356,f3362])).
% 22.51/18.37 fof(f3521,plain,(
% 22.51/18.37 ![X0]: (~c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)=X0|X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f679,f1104])).
% 22.51/18.37 fof(f3601,plain,(
% 22.51/18.37 v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|~sQ75_spl),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f3356,f2021])).
% 22.51/18.37 fof(f3609,plain,(
% 22.51/18.37 v_x(v_r)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ75_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f3601,f3521])).
% 22.51/18.37 fof(f3616,plain,(
% 22.51/18.37 sQ147_spl|~sQ75_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f3609,f3000,f2020])).
% 22.51/18.37 fof(f3622,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(v_x(v_r),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ74_spl),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f3356,f2018])).
% 22.51/18.37 fof(f3625,plain,(
% 22.51/18.37 ~c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|sQ80_spl),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f3356,f2042])).
% 22.51/18.37 fof(f3627,plain,(
% 22.51/18.37 ~v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|sQ75_spl),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f3356,f2022])).
% 22.51/18.37 fof(f3725,plain,(
% 22.51/18.37 c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal)=v_x(v_r)|~c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|~sQ74_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f3622,f1219])).
% 22.51/18.37 fof(f3730,definition,(
% 22.51/18.37 sQ173_spl <=> (c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_r,tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f3734,definition,(
% 22.51/18.37 sQ174_spl <=> (c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal)=v_x(v_r))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f3735,plain,(
% 22.51/18.37 c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal)=v_x(v_r)|~sQ174_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f3734])).
% 22.51/18.37 fof(f3737,definition,(
% 22.51/18.37 sQ175_spl <=> (c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f3739,plain,(
% 22.51/18.37 ~c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|sQ175_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f3737])).
% 22.51/18.37 fof(f3740,plain,(
% 22.51/18.37 sQ174_spl|~sQ175_spl|~sQ74_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f3725,f3734,f3737,f2017])).
% 22.51/18.37 fof(f3818,definition,(
% 22.51/18.37 sQ178_spl <=> (v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f3819,plain,(
% 22.51/18.37 v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|~sQ178_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f3818])).
% 22.51/18.37 fof(f3820,plain,(
% 22.51/18.37 ~v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|sQ178_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f3818])).
% 22.51/18.37 fof(f4257,definition,(
% 22.51/18.37 sQ195_spl <=> (c_HOL_Oord__class_Oless(v_x(v_r),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f4588,definition,(
% 22.51/18.37 sQ218_spl <=> (c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)=v_r)),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f4589,plain,(
% 22.51/18.37 c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)=v_r|~sQ218_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f4588])).
% 22.51/18.37 fof(f4598,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(v_x(v_r),v_r,tc_RealDef_Oreal)|v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)|~sQ218_spl),
% 22.51/18.37 inference(paramodulation,[status(thm)],[f4589,f3369])).
% 22.51/18.37 fof(f4860,plain,(
% 22.51/18.37 $false|sQ75_spl|~sQ178_spl),
% 22.51/18.37 inference(forward_subsumption_resolution,[status(thm)],[f3819,f3627])).
% 22.51/18.37 fof(f4861,plain,(
% 22.51/18.37 sQ75_spl|~sQ178_spl),
% 22.51/18.37 inference(contradiction_clause,[status(thm)],[f4860])).
% 22.51/18.37 fof(f4862,plain,(
% 22.51/18.37 ~c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)|~sQ10_spl|sQ80_spl),
% 22.51/18.37 inference(backward_demodulation,[status(thm)],[f1335,f3625])).
% 22.51/18.37 fof(f5030,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(v_x(v_r),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)|v_x(v_r)=c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal)|sQ175_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f3739,f1202])).
% 22.51/18.37 fof(f5036,plain,(
% 22.51/18.37 sQ195_spl|sQ174_spl|sQ175_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f5030,f4257,f3734,f3737])).
% 22.51/18.37 fof(f5372,plain,(
% 22.51/18.37 c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|~sQ80_spl),
% 22.51/18.37 inference(forward_demodulation,[status(thm)],[f3356,f2041])).
% 22.51/18.37 fof(f5484,plain,(
% 22.51/18.37 ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f945,f1130])).
% 22.51/18.37 fof(f5490,plain,(
% 22.51/18.37 ~c_HOL_Oord__class_Oless(v_x(v_r),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ149_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f5484,f3009])).
% 22.51/18.37 fof(f5491,plain,(
% 22.51/18.37 ![X0,X1]: (~c_HOL_Oord__class_Oless(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f5484,f803])).
% 22.51/18.37 fof(f5517,definition,(
% 22.51/18.37 sQ255_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal))),
% 22.51/18.37 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 22.51/18.37 fof(f5518,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|~sQ255_spl),
% 22.51/18.37 inference(component_clause,[status(thm)],[f5517])).
% 22.51/18.37 fof(f5522,plain,(
% 22.51/18.37 ~sQ173_spl|~sQ10_spl|sQ80_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f4862,f3730,f1334,f2040])).
% 22.51/18.37 fof(f5554,plain,(
% 22.51/18.37 c_HOL_Ouminus__class_Ouminus(v_x(v_r),tc_RealDef_Oreal)=v_r|~sQ174_spl),
% 22.51/18.37 inference(paramodulation,[status(thm)],[f3735,f3356])).
% 22.51/18.37 fof(f5841,plain,(
% 22.51/18.37 c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_x(v_r),tc_RealDef_Oreal)|c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal)=v_x(v_r)|~sQ80_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f5372,f992])).
% 22.51/18.37 fof(f5850,plain,(
% 22.51/18.37 sQ255_spl|sQ174_spl|~sQ80_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f5841,f5517,f3734,f2040])).
% 22.51/18.37 fof(f5914,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f666,f1097])).
% 22.51/18.37 fof(f6231,plain,(
% 22.51/18.37 ![X0,X1]: (~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f1018,f1128])).
% 22.51/18.37 fof(f6246,plain,(
% 22.51/18.37 ![X0,X1]: (~c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f6231,f803])).
% 22.51/18.37 fof(f6726,plain,(
% 22.51/18.37 ~c_HOL_Oord__class_Oless(v_x(v_r),c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ255_spl),
% 22.51/18.37 inference(resolution,[status(thm)],[f5518,f5484])).
% 22.51/18.37 fof(f7002,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Oabs__class_Oabs(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex))),
% 22.51/18.37 inference(resolution,[status(thm)],[f711,f1141])).
% 22.51/18.37 fof(f7385,plain,(
% 22.51/18.37 ![X0]: (c_lessequals(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.37 inference(resolution,[status(thm)],[f722,f1097])).
% 22.51/18.37 fof(f7465,plain,(
% 22.51/18.37 sQ78_spl|sQ178_spl|~sQ218_spl),
% 22.51/18.37 inference(split_clause,[status(thm)],[f4598,f2032,f3818,f4588])).
% 22.51/18.37 fof(f7969,plain,(
% 22.51/18.37 ![X0]: (c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_xa(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 22.51/18.38 inference(paramodulation,[status(thm)],[f1047,f7002])).
% 22.51/18.38 fof(f7980,plain,(
% 22.51/18.38 ![X0]: (c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_xa(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 22.51/18.38 inference(forward_demodulation,[status(thm)],[f5914,f7969])).
% 22.51/18.38 fof(f8470,plain,(
% 22.51/18.38 ![X0]: (c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal)=c_HOL_Ouminus__class_Ouminus(v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.38 inference(backward_demodulation,[status(thm)],[f7980,f1047])).
% 22.51/18.38 fof(f8893,plain,(
% 22.51/18.38 sQ218_spl|~sQ174_spl),
% 22.51/18.38 inference(split_clause,[status(thm)],[f5554,f4588,f3734])).
% 22.51/18.38 fof(f8906,plain,(
% 22.51/18.38 ~v_x(v_r)=c_HOL_Oabs__class_Oabs(v_x(v_r),tc_RealDef_Oreal)|sQ178_spl),
% 22.51/18.38 inference(forward_demodulation,[status(thm)],[f8470,f3820])).
% 22.51/18.38 fof(f8911,plain,(
% 22.51/18.38 ~sQ195_spl|~sQ255_spl),
% 22.51/18.38 inference(split_clause,[status(thm)],[f6726,f4257,f5517])).
% 22.51/18.38 fof(f10368,plain,(
% 22.51/18.38 $false|~sQ78_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f2033,f1048])).
% 22.51/18.38 fof(f10369,plain,(
% 22.51/18.38 ~sQ78_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f10368])).
% 22.51/18.38 fof(f11643,plain,(
% 22.51/18.38 ![X0,X1]: (c_HOL_Oabs__class_Oabs(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),tc_RealDef_Oreal)=v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1))),
% 22.51/18.38 inference(resolution,[status(thm)],[f886,f5491])).
% 22.51/18.38 fof(f11663,plain,(
% 22.51/18.38 c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)=v_r|sQ4_spl),
% 22.51/18.38 inference(resolution,[status(thm)],[f886,f1306])).
% 22.51/18.38 fof(f11664,plain,(
% 22.51/18.38 c_HOL_Oabs__class_Oabs(v_x(v_r),tc_RealDef_Oreal)=v_x(v_r)|~sQ149_spl),
% 22.51/18.38 inference(resolution,[status(thm)],[f886,f5490])).
% 22.51/18.38 fof(f11708,plain,(
% 22.51/18.38 $false|sQ178_spl|~sQ149_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f11664,f8906])).
% 22.51/18.38 fof(f11709,plain,(
% 22.51/18.38 sQ178_spl|~sQ149_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f11708])).
% 22.51/18.38 fof(f11844,plain,(
% 22.51/18.38 c_lessequals(c_HOL_Ouminus__class_Ouminus(v_r,tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)|sQ4_spl),
% 22.51/18.38 inference(paramodulation,[status(thm)],[f11663,f7385])).
% 22.51/18.38 fof(f11850,plain,(
% 22.51/18.38 sQ173_spl|sQ4_spl),
% 22.51/18.38 inference(split_clause,[status(thm)],[f11844,f3730,f1225])).
% 22.51/18.38 fof(f11895,plain,(
% 22.51/18.38 ![X0,X1]: (~c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),v_r,tc_RealDef_Oreal)|~sQ3_spl)),
% 22.51/18.38 inference(backward_demodulation,[status(thm)],[f1210,f6246])).
% 22.51/18.38 fof(f12483,definition,(
% 22.51/18.38 sQ538_spl <=> (class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f12485,plain,(
% 22.51/18.38 ~class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)|sQ538_spl),
% 22.51/18.38 inference(component_clause,[status(thm)],[f12483])).
% 22.51/18.38 fof(f12806,plain,(
% 22.51/18.38 $false|sQ538_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f12485,f1103])).
% 22.51/18.38 fof(f12807,plain,(
% 22.51/18.38 sQ538_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f12806])).
% 22.51/18.38 fof(f12861,definition,(
% 22.51/18.38 sQ564_spl <=> (class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f12863,plain,(
% 22.51/18.38 ~class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)|sQ564_spl),
% 22.51/18.38 inference(component_clause,[status(thm)],[f12861])).
% 22.51/18.38 fof(f12980,definition,(
% 22.51/18.38 sQ576_spl <=> (class_Orderings_Opreorder(tc_RealDef_Oreal))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ576_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f12982,plain,(
% 22.51/18.38 ~class_Orderings_Opreorder(tc_RealDef_Oreal)|sQ576_spl),
% 22.51/18.38 inference(component_clause,[status(thm)],[f12980])).
% 22.51/18.38 fof(f13009,definition,(
% 22.51/18.38 sQ578_spl <=> (class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f13011,plain,(
% 22.51/18.38 ~class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)|sQ578_spl),
% 22.51/18.38 inference(component_clause,[status(thm)],[f13009])).
% 22.51/18.38 fof(f13238,plain,(
% 22.51/18.38 $false|sQ564_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f12863,f1141])).
% 22.51/18.38 fof(f13239,plain,(
% 22.51/18.38 sQ564_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f13238])).
% 22.51/18.38 fof(f13527,plain,(
% 22.51/18.38 ![X0,X1]: (c_lessequals(c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),v_x(X0),tc_RealDef_Oreal))),
% 22.51/18.38 inference(paramodulation,[status(thm)],[f8470,f933])).
% 22.51/18.38 fof(f13531,plain,(
% 22.51/18.38 ![X0]: (~class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)|c_lessequals(v_x(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(v_x(X0),c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 22.51/18.38 inference(paramodulation,[status(thm)],[f8470,f910])).
% 22.51/18.38 fof(f13536,definition,(
% 22.51/18.38 ![X0]: (sQ615_spl <=> (c_lessequals(v_x(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(v_x(X0),c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f13537,plain,(
% 22.51/18.38 ![X0]: (c_lessequals(v_x(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(v_x(X0),c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ615_spl)),
% 22.51/18.38 inference(component_clause,[status(thm)],[f13536])).
% 22.51/18.38 fof(f13539,plain,(
% 22.51/18.38 ~sQ538_spl|sQ615_spl),
% 22.51/18.38 inference(split_clause,[status(thm)],[f13531,f12483,f13536])).
% 22.51/18.38 fof(f13548,plain,(
% 22.51/18.38 ![X0]: (c_lessequals(v_x(X0),v_r,tc_RealDef_Oreal)|~c_lessequals(v_x(X0),c_HOL_Oabs__class_Oabs(v_x(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ3_spl|~sQ615_spl)),
% 22.51/18.38 inference(forward_demodulation,[status(thm)],[f1210,f13537])).
% 22.51/18.38 fof(f13549,plain,(
% 22.51/18.38 ![X0]: (c_lessequals(v_x(X0),v_r,tc_RealDef_Oreal)|~sQ3_spl|~sQ615_spl)),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f13548,f3221])).
% 22.51/18.38 fof(f13755,definition,(
% 22.51/18.38 sQ627_spl <=> (class_Ring__and__Field_Oordered__ring__strict(tc_Int_Oint))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f13757,plain,(
% 22.51/18.38 ~class_Ring__and__Field_Oordered__ring__strict(tc_Int_Oint)|sQ627_spl),
% 22.51/18.38 inference(component_clause,[status(thm)],[f13755])).
% 22.51/18.38 fof(f13782,plain,(
% 22.51/18.38 $false|sQ627_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f13757,f1067])).
% 22.51/18.38 fof(f13783,plain,(
% 22.51/18.38 sQ627_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f13782])).
% 22.51/18.38 fof(f14560,plain,(
% 22.51/18.38 $false|sQ576_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f12982,f1128])).
% 22.51/18.38 fof(f14561,plain,(
% 22.51/18.38 sQ576_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f14560])).
% 22.51/18.38 fof(f15418,plain,(
% 22.51/18.38 $false|sQ578_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f13011,f1113])).
% 22.51/18.38 fof(f15419,plain,(
% 22.51/18.38 sQ578_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f15418])).
% 22.51/18.38 fof(f15577,definition,(
% 22.51/18.38 sQ719_spl <=> (class_Orderings_Opreorder(tc_Int_Oint))),
% 22.51/18.38 introduced(definition,[new_symbols(definition,[sQ719_spl])],[split_symbol_definition])).
% 22.51/18.38 fof(f15579,plain,(
% 22.51/18.38 ~class_Orderings_Opreorder(tc_Int_Oint)|sQ719_spl),
% 22.51/18.38 inference(component_clause,[status(thm)],[f15577])).
% 22.51/18.38 fof(f15826,plain,(
% 22.51/18.38 $false|sQ719_spl),
% 22.51/18.38 inference(forward_subsumption_resolution,[status(thm)],[f15579,f1088])).
% 22.51/18.38 fof(f15827,plain,(
% 22.51/18.38 sQ719_spl),
% 22.51/18.38 inference(contradiction_clause,[status(thm)],[f15826])).
% 22.51/18.38 fof(f16013,plain,(
% 22.51/18.38 ![X0]: (~c_lessequals(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),v_x(X0),tc_RealDef_Oreal)|v_x(X0)=X0)),
% 22.51/18.38 inference(resolution,[status(thm)],[f13527,f3226])).
% 22.51/18.38 fof(f16509,plain,(
% 22.51/18.38 ![X0,X1]: (~c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),v_x(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1)),tc_RealDef_Oreal)|v_x(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1))=v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1))),
% 22.51/18.38 inference(paramodulation,[status(thm)],[f11643,f16013])).
% 22.51/18.38 fof(f16522,plain,(
% 22.51/18.38 ![X0,X1]: (v_x(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1))=v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1))),
% 22.51/18.40 inference(forward_subsumption_resolution,[status(thm)],[f16509,f1350])).
% 22.51/18.40 fof(f16548,plain,(
% 22.51/18.40 ![X0,X1]: (c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),v_r,tc_RealDef_Oreal)|~sQ3_spl|~sQ615_spl)),
% 22.51/18.40 inference(paramodulation,[status(thm)],[f16522,f13549])).
% 22.51/18.40 fof(f16583,plain,(
% 22.51/18.40 $false|~sQ3_spl|~sQ615_spl),
% 22.51/18.40 inference(forward_subsumption_resolution,[status(thm)],[f16548,f11895])).
% 22.51/18.40 fof(f16584,plain,(
% 22.51/18.40 ~sQ3_spl|~sQ615_spl),
% 22.51/18.40 inference(contradiction_clause,[status(thm)],[f16583])).
% 22.51/18.40 fof(f16585,plain,(
% 22.51/18.40 $false),
% 22.51/18.40 inference(sat_refutation,[status(thm)],[f1212,f1228,f2023,f2868,f3011,f3039,f3616,f3740,f4861,f5036,f5522,f5850,f7465,f8893,f8911,f10369,f11709,f11850,f12807,f13239,f13539,f13783,f14561,f15419,f15827,f16584])).
% 22.51/18.40 % SZS output end CNFRefutation for theBenchmark.p
% 1.69/18.42 % Elapsed time: 2.970085 seconds
% 1.69/18.42 % CPU time: 23.063395 seconds
% 1.69/18.42 % Total memory used: 275.180 MB
% 1.69/18.42 % Net memory used: 261.893 MB
%------------------------------------------------------------------------------