Drodi-SAT---4.1.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : ALG339-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 : n005.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 11:50:03 AM UTC 2026

% Result   : Unsatisfiable 98.30s 12.91s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ALG339-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36  % Computer : n005.cluster.edu
% 0.11/0.36  % Model    : x86_64 x86_64
% 0.11/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36  % Memory   : 8046.5625MB
% 0.11/0.36  % OS       : Linux 6.8.0-71-generic
% 0.11/0.36  % CPULimit : 300
% 0.11/0.36  % WCLimit  : 300
% 0.11/0.36  % DateTime : Mon Sep 21 13:16:47 UTC 2026
% 0.14/0.36  % CPUTime  : 
% 0.14/0.40  % Drodi V4.1.1
% 98.30/12.91  % Refutation found
% 98.30/12.91  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 98.30/12.91  % SZS output start CNFRefutation for theBenchmark
% 98.30/12.91  fof(f5,axiom,(
% 98.30/12.91    (![T_a,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(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) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f6,axiom,(
% 98.30/12.91    (![T_a,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f37,axiom,(
% 98.30/12.91    (![T_a,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a) = V_x ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f118,axiom,(
% 98.30/12.91    (![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) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f175,axiom,(
% 98.30/12.91    (![T_a,V_a,V_c,V_b,V_d]: (( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a)| c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_d,T_a),T_a)| ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a)| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f191,axiom,(
% 98.30/12.91    c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f192,axiom,(
% 98.30/12.91    c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f196,axiom,(
% 98.30/12.91    (![V_x]: (( c_Transcendental_Oexp(c_Transcendental_Oln(V_x),tc_RealDef_Oreal) = V_x| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f201,axiom,(
% 98.30/12.91    (![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) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f217,axiom,(
% 98.30/12.91    (![T_a,V_a]: (( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a)| ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f273,axiom,(
% 98.30/12.91    (![V_z1,V_z2,V_z3]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_z1,V_z2,tc_RealDef_Oreal),V_z3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_z1,c_HOL_Otimes__class_Otimes(V_z2,V_z3,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f400,axiom,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f404,axiom,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f408,axiom,(
% 98.30/12.91    (![V_m]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(V_m),tc_RealDef_Oreal) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f412,axiom,(
% 98.30/12.91    (![V_d1,V_d2]: (( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f421,axiom,(
% 98.30/12.91    (![V_x]: (( c_HOL_Oord__class_Oless(c_Transcendental_Oln(V_x),V_x,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f428,axiom,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f429,axiom,(
% 98.30/12.91    (![V_x]: (( c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f431,axiom,(
% 98.30/12.91    (![V_x,V_y]: (( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f432,axiom,(
% 98.30/12.91    (![V_d1,V_d2]: (( c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d2,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f433,axiom,(
% 98.30/12.91    (![V_d1,V_d2]: (( c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d1,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f440,axiom,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f445,axiom,(
% 98.30/12.91    (![V_x]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f449,axiom,(
% 98.30/12.91    (![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) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f454,axiom,(
% 98.30/12.91    (![V_x]: (~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f464,negated_conjecture,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f465,negated_conjecture,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f466,negated_conjecture,(
% 98.30/12.91    (![V_x]: (( ~ c_HOL_Oord__class_Oless(V_x,v_d2,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,v_d1,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f470,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oordered__semiring__strict(tc_nat) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f474,axiom,(
% 98.30/12.91    class_Ring__and__Field_Ono__zero__divisors(tc_nat) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f482,axiom,(
% 98.30/12.91    class_Ring__and__Field_Ozero__neq__one(tc_nat) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f483,axiom,(
% 98.30/12.91    class_Ring__and__Field_Omult__zero(tc_nat) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f491,axiom,(
% 98.30/12.91    class_Power_Opower(tc_nat) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f492,axiom,(
% 98.30/12.91    class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f496,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f497,axiom,(
% 98.30/12.91    class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f498,axiom,(
% 98.30/12.91    class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f499,axiom,(
% 98.30/12.91    class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f502,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f505,axiom,(
% 98.30/12.91    class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f509,axiom,(
% 98.30/12.91    class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f510,axiom,(
% 98.30/12.91    class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f511,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f512,axiom,(
% 98.30/12.91    class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f515,axiom,(
% 98.30/12.91    class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f518,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f519,axiom,(
% 98.30/12.91    class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f521,axiom,(
% 98.30/12.91    class_RealVector_Oreal__normed__field(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f523,axiom,(
% 98.30/12.91    class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f524,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f527,axiom,(
% 98.30/12.91    class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f531,axiom,(
% 98.30/12.91    class_RealVector_Ometric__space(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f536,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f537,axiom,(
% 98.30/12.91    class_Ring__and__Field_Ofield(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f539,axiom,(
% 98.30/12.91    class_Ring__and__Field_Oidom(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f540,axiom,(
% 98.30/12.91    class_Nat_Osemiring__char__0(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f542,axiom,(
% 98.30/12.91    class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f543,axiom,(
% 98.30/12.91    class_Orderings_Oorder(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f545,axiom,(
% 98.30/12.91    class_Power_Opower(tc_RealDef_Oreal) ),
% 98.30/12.91    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.30/12.91  fof(f555,plain,(
% 98.30/12.91    ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(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)))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f5])).
% 98.30/12.91  fof(f556,plain,(
% 98.30/12.91    ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(X0))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f555])).
% 98.30/12.91  fof(f557,plain,(
% 98.30/12.91    ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a]: c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f6])).
% 98.30/12.91  fof(f558,plain,(
% 98.30/12.91    ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f557])).
% 98.30/12.91  fof(f607,plain,(
% 98.30/12.91    ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_x]: c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a)=V_x))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f37])).
% 98.30/12.91  fof(f608,plain,(
% 98.30/12.91    ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(X0),X1,X0)=X1)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f607])).
% 98.30/12.91  fof(f746,plain,(
% 98.30/12.91    ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f118])).
% 98.30/12.91  fof(f850,plain,(
% 98.30/12.91    ![T_a,V_a,V_b]: ((![V_c,V_d]: ((~class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a)|c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_d,T_a),T_a))|~c_HOL_Oord__class_Oless(V_c,V_d,T_a)))|~c_HOL_Oord__class_Oless(V_a,V_b,T_a))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f175])).
% 98.30/12.91  fof(f851,plain,(
% 98.30/12.91    ![X0,X1,X2,X3,X4]: (~class_OrderedGroup_Opordered__cancel__ab__semigroup__add(X0)|c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X1,X2,X0),c_HOL_Oplus__class_Oplus(X3,X4,X0),X0)|~c_HOL_Oord__class_Oless(X2,X4,X0)|~c_HOL_Oord__class_Oless(X1,X3,X0))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f850])).
% 98.30/12.91  fof(f873,plain,(
% 98.30/12.91    ~c_Transcendental_Opi=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f191])).
% 98.30/12.91  fof(f874,plain,(
% 98.30/12.91    c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f192])).
% 98.30/12.91  fof(f880,plain,(
% 98.30/12.91    ![X0]: (c_Transcendental_Oexp(c_Transcendental_Oln(X0),tc_RealDef_Oreal)=X0|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f196])).
% 98.30/12.91  fof(f885,plain,(
% 98.30/12.91    ![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))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f201])).
% 98.30/12.91  fof(f905,plain,(
% 98.30/12.91    ![T_a]: (~class_OrderedGroup_Opordered__ab__group__add__abs(T_a)|(![V_a]: ~c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f217])).
% 98.30/12.91  fof(f906,plain,(
% 98.30/12.91    ![X0,X1]: (~class_OrderedGroup_Opordered__ab__group__add__abs(X0)|~c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f905])).
% 98.30/12.91  fof(f994,plain,(
% 98.30/12.91    ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f273])).
% 98.30/12.91  fof(f1222,plain,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f400])).
% 98.30/12.91  fof(f1227,plain,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f404])).
% 98.30/12.91  fof(f1233,plain,(
% 98.30/12.91    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f408])).
% 98.30/12.91  fof(f1238,plain,(
% 98.30/12.91    ![V_d1]: ((![V_d2]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f412])).
% 98.30/12.91  fof(f1239,plain,(
% 98.30/12.91    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X0,X1),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f1238])).
% 98.30/12.91  fof(f1252,plain,(
% 98.30/12.91    ![X0]: (c_HOL_Oord__class_Oless(c_Transcendental_Oln(X0),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f421])).
% 98.30/12.91  fof(f1265,plain,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f428])).
% 98.30/12.91  fof(f1266,plain,(
% 98.30/12.91    ![X0]: (~c_NthRoot_Osqrt(X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f429])).
% 98.30/12.91  fof(f1268,plain,(
% 98.30/12.91    ![V_x]: ((![V_y]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f431])).
% 98.30/12.91  fof(f1269,plain,(
% 98.30/12.91    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),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)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f1268])).
% 98.30/12.91  fof(f1270,plain,(
% 98.30/12.91    ![V_d1]: ((![V_d2]: (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d2,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f432])).
% 98.30/12.91  fof(f1271,plain,(
% 98.30/12.91    ![X0,X1]: (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X0,X1),X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f1270])).
% 98.30/12.91  fof(f1272,plain,(
% 98.30/12.91    ![V_d1]: ((![V_d2]: (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)))|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal))),
% 98.30/12.91    inference(miniscoping,[status(thm)],[f433])).
% 98.30/12.91  fof(f1273,plain,(
% 98.30/12.91    ![X0,X1]: (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X0,X1),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f1272])).
% 98.30/12.91  fof(f1282,plain,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f440])).
% 98.30/12.91  fof(f1291,plain,(
% 98.30/12.91    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f445])).
% 98.30/12.91  fof(f1296,plain,(
% 98.30/12.91    ![X0,X1,X2]: (~class_Orderings_Oorder(X0)|~c_HOL_Oord__class_Oless(X1,X2,X0)|~c_HOL_Oord__class_Oless(X2,X1,X0))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f449])).
% 98.30/12.91  fof(f1302,plain,(
% 98.30/12.91    ![X0]: (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f454])).
% 98.30/12.91  fof(f1318,plain,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f464])).
% 98.30/12.91  fof(f1319,plain,(
% 98.30/12.91    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f465])).
% 98.30/12.91  fof(f1320,plain,(
% 98.30/12.91    ![X0]: (~c_HOL_Oord__class_Oless(X0,v_d2,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,v_d1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f466])).
% 98.30/12.91  fof(f1324,plain,(
% 98.30/12.91    class_Ring__and__Field_Oordered__semiring__strict(tc_nat)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f470])).
% 98.30/12.91  fof(f1328,plain,(
% 98.30/12.91    class_Ring__and__Field_Ono__zero__divisors(tc_nat)),
% 98.30/12.91    inference(cnf_transformation,[status(thm)],[f474])).
% 98.30/12.92  fof(f1336,plain,(
% 98.30/12.92    class_Ring__and__Field_Ozero__neq__one(tc_nat)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f482])).
% 98.30/12.92  fof(f1337,plain,(
% 98.30/12.92    class_Ring__and__Field_Omult__zero(tc_nat)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f483])).
% 98.30/12.92  fof(f1345,plain,(
% 98.30/12.92    class_Power_Opower(tc_nat)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f491])).
% 98.30/12.92  fof(f1346,plain,(
% 98.30/12.92    class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f492])).
% 98.30/12.92  fof(f1350,plain,(
% 98.30/12.92    class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f496])).
% 98.30/12.92  fof(f1351,plain,(
% 98.30/12.92    class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f497])).
% 98.30/12.92  fof(f1352,plain,(
% 98.30/12.92    class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f498])).
% 98.30/12.92  fof(f1353,plain,(
% 98.30/12.92    class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f499])).
% 98.30/12.92  fof(f1356,plain,(
% 98.30/12.92    class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f502])).
% 98.30/12.92  fof(f1359,plain,(
% 98.30/12.92    class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f505])).
% 98.30/12.92  fof(f1363,plain,(
% 98.30/12.92    class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f509])).
% 98.30/12.92  fof(f1364,plain,(
% 98.30/12.92    class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f510])).
% 98.30/12.92  fof(f1365,plain,(
% 98.30/12.92    class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f511])).
% 98.30/12.92  fof(f1366,plain,(
% 98.30/12.92    class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f512])).
% 98.30/12.92  fof(f1369,plain,(
% 98.30/12.92    class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f515])).
% 98.30/12.92  fof(f1372,plain,(
% 98.30/12.92    class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f518])).
% 98.30/12.92  fof(f1373,plain,(
% 98.30/12.92    class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f519])).
% 98.30/12.92  fof(f1375,plain,(
% 98.30/12.92    class_RealVector_Oreal__normed__field(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f521])).
% 98.30/12.92  fof(f1377,plain,(
% 98.30/12.92    class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f523])).
% 98.30/12.92  fof(f1378,plain,(
% 98.30/12.92    class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f524])).
% 98.30/12.92  fof(f1381,plain,(
% 98.30/12.92    class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f527])).
% 98.30/12.92  fof(f1385,plain,(
% 98.30/12.92    class_RealVector_Ometric__space(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f531])).
% 98.30/12.92  fof(f1390,plain,(
% 98.30/12.92    class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f536])).
% 98.30/12.92  fof(f1391,plain,(
% 98.30/12.92    class_Ring__and__Field_Ofield(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f537])).
% 98.30/12.92  fof(f1393,plain,(
% 98.30/12.92    class_Ring__and__Field_Oidom(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f539])).
% 98.30/12.92  fof(f1394,plain,(
% 98.30/12.92    class_Nat_Osemiring__char__0(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f540])).
% 98.30/12.92  fof(f1396,plain,(
% 98.30/12.92    class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f542])).
% 98.30/12.92  fof(f1397,plain,(
% 98.30/12.92    class_Orderings_Oorder(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f543])).
% 98.30/12.92  fof(f1399,plain,(
% 98.30/12.92    class_Power_Opower(tc_RealDef_Oreal)),
% 98.30/12.92    inference(cnf_transformation,[status(thm)],[f545])).
% 98.30/12.92  fof(f1402,definition,(
% 98.30/12.92    sQ0_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1404,plain,(
% 98.30/12.92    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)|sQ0_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f1402])).
% 98.30/12.92  fof(f1409,plain,(
% 98.30/12.92    $false|sQ0_spl),
% 98.30/12.92    inference(forward_subsumption_resolution,[status(thm)],[f1404,f1318])).
% 98.30/12.92  fof(f1410,plain,(
% 98.30/12.92    sQ0_spl),
% 98.30/12.92    inference(contradiction_clause,[status(thm)],[f1409])).
% 98.30/12.92  fof(f1437,plain,(
% 98.30/12.92    ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 98.30/12.92    inference(paramodulation,[status(thm)],[f746,f994])).
% 98.30/12.92  fof(f1476,plain,(
% 98.30/12.92    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.92    inference(resolution,[status(thm)],[f1269,f1319])).
% 98.30/12.92  fof(f1477,plain,(
% 98.30/12.92    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 98.30/12.92    inference(resolution,[status(thm)],[f1269,f1318])).
% 98.30/12.92  fof(f1484,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d2,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(resolution,[status(thm)],[f1476,f1319])).
% 98.30/12.92  fof(f1487,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_d2,v_d2,tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(resolution,[status(thm)],[f1484,f1476])).
% 98.30/12.92  fof(f1490,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d2,c_HOL_Otimes__class_Otimes(v_d2,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f994,f1487])).
% 98.30/12.92  fof(f1495,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d2,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(resolution,[status(thm)],[f1477,f1319])).
% 98.30/12.92  fof(f1496,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(resolution,[status(thm)],[f1477,f1318])).
% 98.30/12.92  fof(f1518,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(resolution,[status(thm)],[f1496,f1476])).
% 98.30/12.92  fof(f1522,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Otimes__class_Otimes(v_d1,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f994,f1518])).
% 98.30/12.92  fof(f1532,definition,(
% 98.30/12.92    ![X0]: (sQ4_spl <=> (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal)))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1535,definition,(
% 98.30/12.92    ![X1]: (sQ5_spl <=> (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1536,plain,(
% 98.30/12.92    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ5_spl)),
% 98.30/12.92    inference(component_clause,[status(thm)],[f1535])).
% 98.30/12.92  fof(f1638,plain,(
% 98.30/12.92    ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 98.30/12.92    inference(paramodulation,[status(thm)],[f746,f1437])).
% 98.30/12.92  fof(f1893,definition,(
% 98.30/12.92    ![X0,X1]: (sQ11_spl <=> (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1894,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ11_spl)),
% 98.30/12.92    inference(component_clause,[status(thm)],[f1893])).
% 98.30/12.92  fof(f1898,definition,(
% 98.30/12.92    sQ12_spl <=> (class_Ring__and__Field_Ozero__neq__one(tc_nat))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1900,plain,(
% 98.30/12.92    ~class_Ring__and__Field_Ozero__neq__one(tc_nat)|sQ12_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f1898])).
% 98.30/12.92  fof(f1901,definition,(
% 98.30/12.92    sQ13_spl <=> (class_Ring__and__Field_Ono__zero__divisors(tc_nat))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1903,plain,(
% 98.30/12.92    ~class_Ring__and__Field_Ono__zero__divisors(tc_nat)|sQ13_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f1901])).
% 98.30/12.92  fof(f1904,definition,(
% 98.30/12.92    sQ14_spl <=> (class_Ring__and__Field_Omult__zero(tc_nat))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f1906,plain,(
% 98.30/12.92    ~class_Ring__and__Field_Omult__zero(tc_nat)|sQ14_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f1904])).
% 98.30/12.92  fof(f2276,definition,(
% 98.30/12.92    sQ19_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f2278,plain,(
% 98.30/12.92    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)|sQ19_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f2276])).
% 98.30/12.92  fof(f2280,plain,(
% 98.30/12.92    $false|sQ19_spl),
% 98.30/12.92    inference(forward_subsumption_resolution,[status(thm)],[f2278,f1319])).
% 98.30/12.92  fof(f2281,plain,(
% 98.30/12.92    sQ19_spl),
% 98.30/12.92    inference(contradiction_clause,[status(thm)],[f2280])).
% 98.30/12.92  fof(f2414,definition,(
% 98.30/12.92    ![X0]: (sQ20_spl <=> (c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f2415,plain,(
% 98.30/12.92    ![X0]: (c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ20_spl)),
% 98.30/12.92    inference(component_clause,[status(thm)],[f2414])).
% 98.30/12.92  fof(f2495,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ20_spl),
% 98.30/12.92    inference(backward_demodulation,[status(thm)],[f2415,f1496])).
% 98.30/12.92  fof(f2553,plain,(
% 98.30/12.92    $false|~sQ20_spl),
% 98.30/12.92    inference(forward_subsumption_resolution,[status(thm)],[f2495,f1302])).
% 98.30/12.92  fof(f2554,plain,(
% 98.30/12.92    ~sQ20_spl),
% 98.30/12.92    inference(contradiction_clause,[status(thm)],[f2553])).
% 98.30/12.92  fof(f2746,definition,(
% 98.30/12.92    sQ21_spl <=> (class_Ring__and__Field_Ofield(tc_RealDef_Oreal))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f2748,plain,(
% 98.30/12.92    ~class_Ring__and__Field_Ofield(tc_RealDef_Oreal)|sQ21_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f2746])).
% 98.30/12.92  fof(f2755,definition,(
% 98.30/12.92    sQ23_spl <=> (class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f2757,plain,(
% 98.30/12.92    ~class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal)|sQ23_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f2755])).
% 98.30/12.92  fof(f2767,plain,(
% 98.30/12.92    ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 98.30/12.92    inference(resolution,[status(thm)],[f1366,f558])).
% 98.30/12.92  fof(f2768,plain,(
% 98.30/12.92    ![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))),
% 98.30/12.92    inference(resolution,[status(thm)],[f1366,f556])).
% 98.30/12.92  fof(f2822,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 98.30/12.92    inference(paramodulation,[status(thm)],[f1638,f2767])).
% 98.30/12.92  fof(f2850,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 98.30/12.92    inference(paramodulation,[status(thm)],[f2767,f1638])).
% 98.30/12.92  fof(f2873,plain,(
% 98.30/12.92    ![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))),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f2767,f2822])).
% 98.30/12.92  fof(f2876,definition,(
% 98.30/12.92    sQ27_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f2877,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ27_spl),
% 98.30/12.92    inference(component_clause,[status(thm)],[f2876])).
% 98.30/12.92  fof(f2895,plain,(
% 98.30/12.92    ![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))),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f2767,f2850])).
% 98.30/12.92  fof(f2918,plain,(
% 98.30/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ27_spl),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f2767,f2877])).
% 98.30/12.92  fof(f2919,plain,(
% 98.30/12.92    $false|~sQ27_spl),
% 98.30/12.92    inference(forward_subsumption_resolution,[status(thm)],[f2918,f1302])).
% 98.30/12.92  fof(f2920,plain,(
% 98.30/12.92    ~sQ27_spl),
% 98.30/12.92    inference(contradiction_clause,[status(thm)],[f2919])).
% 98.30/12.92  fof(f3003,definition,(
% 98.30/12.92    ![X0,X1]: (sQ35_spl <=> (c_HOL_Oord__class_Oless(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),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f3004,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(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),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ35_spl)),
% 98.30/12.92    inference(component_clause,[status(thm)],[f3003])).
% 98.30/12.92  fof(f3007,definition,(
% 98.30/12.92    ![X0,X1]: (sQ36_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)))),
% 98.30/12.92    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 98.30/12.92  fof(f3008,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ36_spl)),
% 98.30/12.92    inference(component_clause,[status(thm)],[f3007])).
% 98.30/12.92  fof(f3014,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ36_spl)),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f2768,f3008])).
% 98.30/12.92  fof(f3015,plain,(
% 98.30/12.92    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ36_spl)),
% 98.30/12.92    inference(forward_subsumption_resolution,[status(thm)],[f3014,f1302])).
% 98.30/12.92  fof(f3016,plain,(
% 98.30/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ35_spl)),
% 98.30/12.92    inference(forward_demodulation,[status(thm)],[f2768,f3004])).
% 98.30/12.92  fof(f3017,plain,(
% 98.30/12.92    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ35_spl)),
% 98.30/12.92    inference(forward_subsumption_resolution,[status(thm)],[f3016,f1302])).
% 98.30/12.92  fof(f3065,definition,(
% 98.30/12.92    ![X0]: (sQ38_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f3066,plain,(
% 99.18/12.92    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ38_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f3065])).
% 99.18/12.92  fof(f3110,plain,(
% 99.18/12.92    $false|~sQ38_spl),
% 99.18/12.92    inference(resolution,[status(thm)],[f3066,f1302])).
% 99.18/12.92  fof(f3111,plain,(
% 99.18/12.92    ~sQ38_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3110])).
% 99.18/12.92  fof(f3137,plain,(
% 99.18/12.92    ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.92    inference(paramodulation,[status(thm)],[f746,f2873])).
% 99.18/12.92  fof(f3252,plain,(
% 99.18/12.92    ![X0]: (c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=X0)),
% 99.18/12.92    inference(resolution,[status(thm)],[f608,f1366])).
% 99.18/12.92  fof(f3409,definition,(
% 99.18/12.92    ![X1]: (sQ39_spl <=> (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(X1,X1,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f3410,plain,(
% 99.18/12.92    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal)|~sQ39_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f3409])).
% 99.18/12.92  fof(f3414,definition,(
% 99.18/12.92    ![X0,X1]: (sQ40_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f3415,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ40_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f3414])).
% 99.18/12.92  fof(f3418,definition,(
% 99.18/12.92    ![X0,X1]: (sQ41_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f3419,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ41_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f3418])).
% 99.18/12.92  fof(f3422,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ41_spl)),
% 99.18/12.92    inference(forward_demodulation,[status(thm)],[f3137,f3419])).
% 99.18/12.92  fof(f3423,plain,(
% 99.18/12.92    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ41_spl)),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f3422,f1302])).
% 99.18/12.92  fof(f3424,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ40_spl)),
% 99.18/12.92    inference(forward_demodulation,[status(thm)],[f3137,f3415])).
% 99.18/12.92  fof(f3425,plain,(
% 99.18/12.92    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ40_spl)),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f3424,f1302])).
% 99.18/12.92  fof(f3426,plain,(
% 99.18/12.92    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ39_spl)),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f3410,f1302])).
% 99.18/12.92  fof(f3493,plain,(
% 99.18/12.92    $false|~sQ36_spl),
% 99.18/12.92    inference(backward_subsumption_resolution,[status(thm)],[f1490,f3015])).
% 99.18/12.92  fof(f3503,plain,(
% 99.18/12.92    ~sQ36_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3493])).
% 99.18/12.92  fof(f3532,definition,(
% 99.18/12.92    sQ42_spl <=> (class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f3534,plain,(
% 99.18/12.92    ~class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)|sQ42_spl),
% 99.18/12.92    inference(component_clause,[status(thm)],[f3532])).
% 99.18/12.92  fof(f3547,plain,(
% 99.18/12.92    $false|sQ42_spl),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f3534,f1364])).
% 99.18/12.92  fof(f3548,plain,(
% 99.18/12.92    sQ42_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3547])).
% 99.18/12.92  fof(f3559,plain,(
% 99.18/12.92    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 99.18/12.92    inference(paramodulation,[status(thm)],[f746,f1495])).
% 99.18/12.92  fof(f3563,plain,(
% 99.18/12.92    $false|~sQ35_spl),
% 99.18/12.92    inference(backward_subsumption_resolution,[status(thm)],[f1319,f3017])).
% 99.18/12.92  fof(f3568,plain,(
% 99.18/12.92    ~sQ35_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3563])).
% 99.18/12.92  fof(f3569,plain,(
% 99.18/12.92    $false|~sQ41_spl),
% 99.18/12.92    inference(backward_subsumption_resolution,[status(thm)],[f1318,f3423])).
% 99.18/12.92  fof(f3571,plain,(
% 99.18/12.92    ~sQ41_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3569])).
% 99.18/12.92  fof(f3598,plain,(
% 99.18/12.92    $false|~sQ40_spl),
% 99.18/12.92    inference(backward_subsumption_resolution,[status(thm)],[f1496,f3425])).
% 99.18/12.92  fof(f3602,plain,(
% 99.18/12.92    ~sQ40_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3598])).
% 99.18/12.92  fof(f3617,plain,(
% 99.18/12.92    $false|~sQ39_spl),
% 99.18/12.92    inference(backward_subsumption_resolution,[status(thm)],[f3559,f3426])).
% 99.18/12.92  fof(f3620,plain,(
% 99.18/12.92    ~sQ39_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3617])).
% 99.18/12.92  fof(f3845,plain,(
% 99.18/12.92    $false|sQ21_spl),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f2748,f1391])).
% 99.18/12.92  fof(f3846,plain,(
% 99.18/12.92    sQ21_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3845])).
% 99.18/12.92  fof(f3847,plain,(
% 99.18/12.92    $false|sQ23_spl),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f2757,f1373])).
% 99.18/12.92  fof(f3848,plain,(
% 99.18/12.92    sQ23_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f3847])).
% 99.18/12.92  fof(f4267,definition,(
% 99.18/12.92    sQ61_spl <=> (class_RealVector_Oreal__normed__field(tc_RealDef_Oreal))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f4269,plain,(
% 99.18/12.92    ~class_RealVector_Oreal__normed__field(tc_RealDef_Oreal)|sQ61_spl),
% 99.18/12.92    inference(component_clause,[status(thm)],[f4267])).
% 99.18/12.92  fof(f4274,plain,(
% 99.18/12.92    $false|sQ61_spl),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f4269,f1375])).
% 99.18/12.92  fof(f4275,plain,(
% 99.18/12.92    sQ61_spl),
% 99.18/12.92    inference(contradiction_clause,[status(thm)],[f4274])).
% 99.18/12.92  fof(f4718,definition,(
% 99.18/12.92    ![X0,X1]: (sQ68_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f4719,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ68_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f4718])).
% 99.18/12.92  fof(f4723,definition,(
% 99.18/12.92    ![X0,X1]: (sQ69_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f4724,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ69_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f4723])).
% 99.18/12.92  fof(f4728,definition,(
% 99.18/12.92    ![X0,X1]: (sQ70_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f4729,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ70_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f4728])).
% 99.18/12.92  fof(f4733,definition,(
% 99.18/12.92    ![X0,X1]: (sQ71_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)))),
% 99.18/12.92    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 99.18/12.92  fof(f4734,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ71_spl)),
% 99.18/12.92    inference(component_clause,[status(thm)],[f4733])).
% 99.18/12.92  fof(f4737,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ71_spl)),
% 99.18/12.92    inference(forward_demodulation,[status(thm)],[f3137,f4734])).
% 99.18/12.92  fof(f4738,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ71_spl)),
% 99.18/12.92    inference(forward_demodulation,[status(thm)],[f3137,f4737])).
% 99.18/12.92  fof(f4739,plain,(
% 99.18/12.92    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ71_spl)),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f4738,f1302])).
% 99.18/12.92  fof(f4740,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ70_spl)),
% 99.18/12.92    inference(forward_demodulation,[status(thm)],[f3137,f4729])).
% 99.18/12.92  fof(f4741,plain,(
% 99.18/12.92    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ70_spl)),
% 99.18/12.92    inference(forward_subsumption_resolution,[status(thm)],[f4740,f1302])).
% 99.18/12.92  fof(f4742,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ69_spl)),
% 99.18/12.92    inference(forward_demodulation,[status(thm)],[f3137,f4724])).
% 99.18/12.92  fof(f4743,plain,(
% 99.18/12.92    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ69_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f3137,f4742])).
% 99.18/12.93  fof(f4744,plain,(
% 99.18/12.93    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ69_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f4743,f1302])).
% 99.18/12.93  fof(f4745,plain,(
% 99.18/12.93    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ68_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f3137,f4719])).
% 99.18/12.93  fof(f4746,plain,(
% 99.18/12.93    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ68_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f4745,f1302])).
% 99.18/12.93  fof(f4764,definition,(
% 99.18/12.93    ![X0]: (sQ72_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f4765,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ72_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f4764])).
% 99.18/12.93  fof(f4769,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ72_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f4765])).
% 99.18/12.93  fof(f4770,plain,(
% 99.18/12.93    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ72_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f4769,f1302])).
% 99.18/12.93  fof(f4771,plain,(
% 99.18/12.93    $false|~sQ71_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1233,f4739])).
% 99.18/12.93  fof(f4791,plain,(
% 99.18/12.93    ~sQ71_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f4771])).
% 99.18/12.93  fof(f4792,plain,(
% 99.18/12.93    $false|~sQ70_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1318,f4741])).
% 99.18/12.93  fof(f4794,plain,(
% 99.18/12.93    ~sQ70_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f4792])).
% 99.18/12.93  fof(f4816,plain,(
% 99.18/12.93    $false|~sQ69_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1496,f4744])).
% 99.18/12.93  fof(f4820,plain,(
% 99.18/12.93    ~sQ69_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f4816])).
% 99.18/12.93  fof(f4821,plain,(
% 99.18/12.93    $false|~sQ68_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1318,f4746])).
% 99.18/12.93  fof(f4823,plain,(
% 99.18/12.93    ~sQ68_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f4821])).
% 99.18/12.93  fof(f4828,plain,(
% 99.18/12.93    $false|~sQ72_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1319,f4770])).
% 99.18/12.93  fof(f4830,plain,(
% 99.18/12.93    ~sQ72_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f4828])).
% 99.18/12.93  fof(f5250,definition,(
% 99.18/12.93    ![X0]: (sQ74_spl <=> (~class_Nat_Osemiring__char__0(X0)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f5251,plain,(
% 99.18/12.93    ![X0]: (~class_Nat_Osemiring__char__0(X0)|~sQ74_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f5250])).
% 99.18/12.93  fof(f5254,plain,(
% 99.18/12.93    $false|~sQ74_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1394,f5251])).
% 99.18/12.93  fof(f5256,plain,(
% 99.18/12.93    ~sQ74_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f5254])).
% 99.18/12.93  fof(f5438,plain,(
% 99.18/12.93    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.93    inference(resolution,[status(thm)],[f906,f1351])).
% 99.18/12.93  fof(f5603,definition,(
% 99.18/12.93    sQ76_spl <=> (class_Ring__and__Field_Oidom(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f5605,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oidom(tc_RealDef_Oreal)|sQ76_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f5603])).
% 99.18/12.93  fof(f5610,plain,(
% 99.18/12.93    $false|sQ76_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f5605,f1393])).
% 99.18/12.93  fof(f5611,plain,(
% 99.18/12.93    sQ76_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f5610])).
% 99.18/12.93  fof(f5752,plain,(
% 99.18/12.93    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 99.18/12.93    inference(resolution,[status(thm)],[f1296,f1397])).
% 99.18/12.93  fof(f6111,definition,(
% 99.18/12.93    sQ83_spl <=> (class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f6113,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)|sQ83_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f6111])).
% 99.18/12.93  fof(f6122,plain,(
% 99.18/12.93    $false|sQ83_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f6113,f1372])).
% 99.18/12.93  fof(f6123,plain,(
% 99.18/12.93    sQ83_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f6122])).
% 99.18/12.93  fof(f6166,definition,(
% 99.18/12.93    ![X0]: (sQ87_spl <=> (c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f6167,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ87_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f6166])).
% 99.18/12.93  fof(f6175,plain,(
% 99.18/12.93    $false|~sQ87_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f5438,f6167])).
% 99.18/12.93  fof(f6215,plain,(
% 99.18/12.93    ~sQ87_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f6175])).
% 99.18/12.93  fof(f6220,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ11_spl),
% 99.18/12.93    inference(backward_demodulation,[status(thm)],[f1894,f1522])).
% 99.18/12.93  fof(f6274,plain,(
% 99.18/12.93    $false|~sQ11_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f6220,f1302])).
% 99.18/12.93  fof(f6275,plain,(
% 99.18/12.93    ~sQ11_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f6274])).
% 99.18/12.93  fof(f6338,plain,(
% 99.18/12.93    $false|~sQ5_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1291,f1536])).
% 99.18/12.93  fof(f6346,plain,(
% 99.18/12.93    ~sQ5_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f6338])).
% 99.18/12.93  fof(f6996,plain,(
% 99.18/12.93    ![X0,X1,X2,X3]: (c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X3,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X2,tc_RealDef_Oreal))),
% 99.18/12.93    inference(resolution,[status(thm)],[f851,f1346])).
% 99.18/12.93  fof(f7573,plain,(
% 99.18/12.93    c_Transcendental_Oexp(c_Transcendental_Oln(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1),tc_RealDef_Oreal)=c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1),
% 99.18/12.93    inference(resolution,[status(thm)],[f880,f1227])).
% 99.18/12.93  fof(f7580,plain,(
% 99.18/12.93    c_Transcendental_Oexp(c_Transcendental_Oln(v_d2),tc_RealDef_Oreal)=v_d2),
% 99.18/12.93    inference(resolution,[status(thm)],[f880,f1319])).
% 99.18/12.93  fof(f7581,plain,(
% 99.18/12.93    c_Transcendental_Oexp(c_Transcendental_Oln(v_d1),tc_RealDef_Oreal)=v_d1),
% 99.18/12.93    inference(resolution,[status(thm)],[f880,f1318])).
% 99.18/12.93  fof(f7599,definition,(
% 99.18/12.93    sQ97_spl <=> (c_Transcendental_Oexp(c_Transcendental_Oln(v_d2),tc_RealDef_Oreal)=v_d2)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7601,plain,(
% 99.18/12.93    ~c_Transcendental_Oexp(c_Transcendental_Oln(v_d2),tc_RealDef_Oreal)=v_d2|sQ97_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7599])).
% 99.18/12.93  fof(f7610,definition,(
% 99.18/12.93    sQ100_spl <=> (class_Orderings_Olinorder(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7612,plain,(
% 99.18/12.93    ~class_Orderings_Olinorder(tc_RealDef_Oreal)|sQ100_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7610])).
% 99.18/12.93  fof(f7613,definition,(
% 99.18/12.93    sQ101_spl <=> (class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7615,plain,(
% 99.18/12.93    ~class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal)|sQ101_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7613])).
% 99.18/12.93  fof(f7620,definition,(
% 99.18/12.93    sQ103_spl <=> (class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7622,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal)|sQ103_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7620])).
% 99.18/12.93  fof(f7624,definition,(
% 99.18/12.93    sQ104_spl <=> (class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7626,plain,(
% 99.18/12.93    ~class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)|sQ104_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7624])).
% 99.18/12.93  fof(f7668,plain,(
% 99.18/12.93    $false|sQ104_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f7626,f1351])).
% 99.18/12.93  fof(f7669,plain,(
% 99.18/12.93    sQ104_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f7668])).
% 99.18/12.93  fof(f7670,plain,(
% 99.18/12.93    $false|sQ103_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f7622,f1390])).
% 99.18/12.93  fof(f7671,plain,(
% 99.18/12.93    sQ103_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f7670])).
% 99.18/12.93  fof(f7672,plain,(
% 99.18/12.93    $false|sQ101_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f7615,f1352])).
% 99.18/12.93  fof(f7673,plain,(
% 99.18/12.93    sQ101_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f7672])).
% 99.18/12.93  fof(f7674,plain,(
% 99.18/12.93    $false|sQ100_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f7612,f1396])).
% 99.18/12.93  fof(f7675,plain,(
% 99.18/12.93    sQ100_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f7674])).
% 99.18/12.93  fof(f7775,definition,(
% 99.18/12.93    sQ115_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_Transcendental_Opi)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7776,plain,(
% 99.18/12.93    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_Transcendental_Opi|~sQ115_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7775])).
% 99.18/12.93  fof(f7820,plain,(
% 99.18/12.93    ~v_d2=v_d2|sQ97_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f7580,f7601])).
% 99.18/12.93  fof(f7821,plain,(
% 99.18/12.93    $false|sQ97_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f7820])).
% 99.18/12.93  fof(f7822,plain,(
% 99.18/12.93    sQ97_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f7821])).
% 99.18/12.93  fof(f7889,definition,(
% 99.18/12.93    sQ125_spl <=> (v_d2=v_d2)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f7891,plain,(
% 99.18/12.93    ~v_d2=v_d2|sQ125_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f7889])).
% 99.18/12.93  fof(f7896,plain,(
% 99.18/12.93    $false|sQ125_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f7891])).
% 99.18/12.93  fof(f7897,plain,(
% 99.18/12.93    sQ125_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f7896])).
% 99.18/12.93  fof(f8004,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_NthRoot_Osqrt(v_d1),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f885,f1318])).
% 99.18/12.93  fof(f8013,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(v_d1),tc_RealDef_Oreal)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f8004])).
% 99.18/12.93  fof(f8108,definition,(
% 99.18/12.93    sQ130_spl <=> (c_Transcendental_Oexp(c_Transcendental_Oln(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1),tc_RealDef_Oreal)=c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f8110,plain,(
% 99.18/12.93    ~c_Transcendental_Oexp(c_Transcendental_Oln(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1),tc_RealDef_Oreal)=c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1|sQ130_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f8108])).
% 99.18/12.93  fof(f8112,plain,(
% 99.18/12.93    ~c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1=c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1|sQ130_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f7573,f8110])).
% 99.18/12.93  fof(f8113,plain,(
% 99.18/12.93    $false|sQ130_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f8112])).
% 99.18/12.93  fof(f8114,plain,(
% 99.18/12.93    sQ130_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f8113])).
% 99.18/12.93  fof(f8242,definition,(
% 99.18/12.93    sQ141_spl <=> (v_d1=v_d1)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f8244,plain,(
% 99.18/12.93    ~v_d1=v_d1|sQ141_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f8242])).
% 99.18/12.93  fof(f8263,plain,(
% 99.18/12.93    $false|sQ141_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f8244])).
% 99.18/12.93  fof(f8264,plain,(
% 99.18/12.93    sQ141_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f8263])).
% 99.18/12.93  fof(f8436,definition,(
% 99.18/12.93    ![X0]: (sQ147_spl <=> (~class_RealVector_Ometric__space(X0)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f8437,plain,(
% 99.18/12.93    ![X0]: (~class_RealVector_Ometric__space(X0)|~sQ147_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f8436])).
% 99.18/12.93  fof(f8442,plain,(
% 99.18/12.93    $false|~sQ147_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1385,f8437])).
% 99.18/12.93  fof(f8443,plain,(
% 99.18/12.93    ~sQ147_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f8442])).
% 99.18/12.93  fof(f8493,definition,(
% 99.18/12.93    sQ149_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f8495,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)|sQ149_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f8493])).
% 99.18/12.93  fof(f8498,plain,(
% 99.18/12.93    $false|sQ149_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f8495,f1222])).
% 99.18/12.93  fof(f8499,plain,(
% 99.18/12.93    sQ149_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f8498])).
% 99.18/12.93  fof(f9022,definition,(
% 99.18/12.93    sQ154_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f9023,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ154_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f9022])).
% 99.18/12.93  fof(f9043,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ154_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f9023])).
% 99.18/12.93  fof(f9044,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ154_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f9043])).
% 99.18/12.93  fof(f9045,plain,(
% 99.18/12.93    $false|~sQ154_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f9044,f1302])).
% 99.18/12.93  fof(f9046,plain,(
% 99.18/12.93    ~sQ154_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f9045])).
% 99.18/12.93  fof(f9065,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_NthRoot_Osqrt(v_d2),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1319,f885])).
% 99.18/12.93  fof(f9070,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(v_d2),tc_RealDef_Oreal)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f9065])).
% 99.18/12.93  fof(f9247,definition,(
% 99.18/12.93    sQ164_spl <=> (c_Transcendental_Opi=c_Transcendental_Opi)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f9249,plain,(
% 99.18/12.93    ~c_Transcendental_Opi=c_Transcendental_Opi|sQ164_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f9247])).
% 99.18/12.93  fof(f9254,plain,(
% 99.18/12.93    $false|sQ164_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f9249])).
% 99.18/12.93  fof(f9255,plain,(
% 99.18/12.93    sQ164_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f9254])).
% 99.18/12.93  fof(f9271,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_NthRoot_Osqrt(v_d1),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1318,f885])).
% 99.18/12.93  fof(f9275,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(v_d1),tc_RealDef_Oreal)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f9271])).
% 99.18/12.93  fof(f9304,definition,(
% 99.18/12.93    sQ166_spl <=> (class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f9306,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)|sQ166_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f9304])).
% 99.18/12.93  fof(f9307,definition,(
% 99.18/12.93    ![X0]: (sQ167_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f9308,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ167_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f9307])).
% 99.18/12.93  fof(f9311,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ167_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f3137,f9308])).
% 99.18/12.93  fof(f9312,plain,(
% 99.18/12.93    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ167_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f9311,f1302])).
% 99.18/12.93  fof(f9313,plain,(
% 99.18/12.93    $false|sQ166_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f9306,f1350])).
% 99.18/12.93  fof(f9314,plain,(
% 99.18/12.93    sQ166_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f9313])).
% 99.18/12.93  fof(f9316,definition,(
% 99.18/12.93    ![X0]: (sQ168_spl <=> (c_HOL_Oord__class_Oless(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),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f9317,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(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),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ168_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f9316])).
% 99.18/12.93  fof(f9320,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ168_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f9317])).
% 99.18/12.93  fof(f9321,plain,(
% 99.18/12.93    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ168_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f9320,f1302])).
% 99.18/12.93  fof(f9377,plain,(
% 99.18/12.93    $false|~sQ167_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1318,f9312])).
% 99.18/12.93  fof(f9384,plain,(
% 99.18/12.93    ~sQ167_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f9377])).
% 99.18/12.93  fof(f9403,plain,(
% 99.18/12.93    $false|~sQ168_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1319,f9321])).
% 99.18/12.93  fof(f9405,plain,(
% 99.18/12.93    ~sQ168_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f9403])).
% 99.18/12.93  fof(f9654,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d1)),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f8013,f885])).
% 99.18/12.93  fof(f9658,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d1)),tc_RealDef_Oreal)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f9654])).
% 99.18/12.93  fof(f9686,plain,(
% 99.18/12.93    $false|~sQ115_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f7776,f873])).
% 99.18/12.93  fof(f9687,plain,(
% 99.18/12.93    ~sQ115_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f9686])).
% 99.18/12.93  fof(f10381,definition,(
% 99.18/12.93    sQ198_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f10382,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ198_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f10381])).
% 99.18/12.93  fof(f10399,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ198_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f10382])).
% 99.18/12.93  fof(f10400,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ198_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f10399])).
% 99.18/12.93  fof(f10401,plain,(
% 99.18/12.93    $false|~sQ198_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f10400,f1302])).
% 99.18/12.93  fof(f10402,plain,(
% 99.18/12.93    ~sQ198_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f10401])).
% 99.18/12.93  fof(f11024,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_NthRoot_Osqrt(v_d2),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1319,f885])).
% 99.18/12.93  fof(f11034,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(v_d2),tc_RealDef_Oreal)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f11024])).
% 99.18/12.93  fof(f11184,definition,(
% 99.18/12.93    sQ206_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f11186,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal)|sQ206_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f11184])).
% 99.18/12.93  fof(f11188,plain,(
% 99.18/12.93    $false|sQ206_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f11186,f1227])).
% 99.18/12.93  fof(f11189,plain,(
% 99.18/12.93    sQ206_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f11188])).
% 99.18/12.93  fof(f11216,definition,(
% 99.18/12.93    sQ207_spl <=> (c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1=c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f11218,plain,(
% 99.18/12.93    ~c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1=c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1|sQ207_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f11216])).
% 99.18/12.93  fof(f11225,plain,(
% 99.18/12.93    $false|sQ207_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f11218])).
% 99.18/12.93  fof(f11226,plain,(
% 99.18/12.93    sQ207_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f11225])).
% 99.18/12.93  fof(f11448,definition,(
% 99.18/12.93    ![X0]: (sQ209_spl <=> (c_NthRoot_Osqrt(X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f11449,plain,(
% 99.18/12.93    ![X0]: (c_NthRoot_Osqrt(X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ209_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f11448])).
% 99.18/12.93  fof(f11580,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ209_spl),
% 99.18/12.93    inference(backward_demodulation,[status(thm)],[f11449,f9658])).
% 99.18/12.93  fof(f11588,plain,(
% 99.18/12.93    $false|~sQ209_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f11580,f1302])).
% 99.18/12.93  fof(f11589,plain,(
% 99.18/12.93    ~sQ209_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f11588])).
% 99.18/12.93  fof(f11820,definition,(
% 99.18/12.93    ![X0]: (sQ219_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f11821,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)|~sQ219_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f11820])).
% 99.18/12.93  fof(f11832,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)|~sQ219_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f2895,f11821])).
% 99.18/12.93  fof(f11833,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)|~sQ219_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f11832])).
% 99.18/12.93  fof(f11834,plain,(
% 99.18/12.93    ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)|~sQ219_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f11833,f1302])).
% 99.18/12.93  fof(f11874,plain,(
% 99.18/12.93    $false|~sQ219_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f11034,f11834])).
% 99.18/12.93  fof(f11875,plain,(
% 99.18/12.93    ~sQ219_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f11874])).
% 99.18/12.93  fof(f12102,definition,(
% 99.18/12.93    sQ223_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12103,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),tc_RealDef_Oreal)|~sQ223_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12102])).
% 99.18/12.93  fof(f12108,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ223_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f874,f12103])).
% 99.18/12.93  fof(f12109,plain,(
% 99.18/12.93    $false|~sQ223_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12108,f1302])).
% 99.18/12.93  fof(f12110,plain,(
% 99.18/12.93    ~sQ223_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12109])).
% 99.18/12.93  fof(f12475,definition,(
% 99.18/12.93    sQ252_spl <=> (class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12477,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal)|sQ252_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12475])).
% 99.18/12.93  fof(f12482,definition,(
% 99.18/12.93    ![X1,X2]: (sQ254_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X2,X1,tc_RealDef_Oreal)))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12483,plain,(
% 99.18/12.93    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ254_spl)),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12482])).
% 99.18/12.93  fof(f12490,definition,(
% 99.18/12.93    sQ256_spl <=> (class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12492,plain,(
% 99.18/12.93    ~class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal)|sQ256_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12490])).
% 99.18/12.93  fof(f12497,definition,(
% 99.18/12.93    sQ258_spl <=> (class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12499,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)|sQ258_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12497])).
% 99.18/12.93  fof(f12500,definition,(
% 99.18/12.93    sQ259_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12501,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ259_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12500])).
% 99.18/12.93  fof(f12504,definition,(
% 99.18/12.93    sQ260_spl <=> (class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12506,plain,(
% 99.18/12.93    ~class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)|sQ260_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12504])).
% 99.18/12.93  fof(f12537,plain,(
% 99.18/12.93    $false|sQ252_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12477,f1356])).
% 99.18/12.93  fof(f12538,plain,(
% 99.18/12.93    sQ252_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12537])).
% 99.18/12.93  fof(f12539,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ259_spl),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f3252,f12501])).
% 99.18/12.93  fof(f12540,plain,(
% 99.18/12.93    $false|~sQ259_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12539,f1302])).
% 99.18/12.93  fof(f12541,plain,(
% 99.18/12.93    ~sQ259_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12540])).
% 99.18/12.93  fof(f12545,plain,(
% 99.18/12.93    $false|sQ260_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12506,f1359])).
% 99.18/12.93  fof(f12546,plain,(
% 99.18/12.93    sQ260_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12545])).
% 99.18/12.93  fof(f12547,plain,(
% 99.18/12.93    $false|sQ258_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12499,f1378])).
% 99.18/12.93  fof(f12548,plain,(
% 99.18/12.93    sQ258_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12547])).
% 99.18/12.93  fof(f12549,plain,(
% 99.18/12.93    $false|sQ256_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12492,f1353])).
% 99.18/12.93  fof(f12550,plain,(
% 99.18/12.93    sQ256_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12549])).
% 99.18/12.93  fof(f12554,plain,(
% 99.18/12.93    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ254_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f3137,f12483])).
% 99.18/12.93  fof(f12555,plain,(
% 99.18/12.93    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ254_spl)),
% 99.18/12.93    inference(forward_demodulation,[status(thm)],[f3137,f12554])).
% 99.18/12.93  fof(f12556,plain,(
% 99.18/12.93    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ254_spl)),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12555,f1302])).
% 99.18/12.93  fof(f12589,plain,(
% 99.18/12.93    $false|~sQ254_spl),
% 99.18/12.93    inference(backward_subsumption_resolution,[status(thm)],[f1318,f12556])).
% 99.18/12.93  fof(f12591,plain,(
% 99.18/12.93    ~sQ254_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12589])).
% 99.18/12.93  fof(f12638,definition,(
% 99.18/12.93    sQ266_spl <=> (class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f12640,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal)|sQ266_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f12638])).
% 99.18/12.93  fof(f12714,plain,(
% 99.18/12.93    $false|sQ266_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f12640,f1365])).
% 99.18/12.93  fof(f12715,plain,(
% 99.18/12.93    sQ266_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f12714])).
% 99.18/12.93  fof(f12829,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f5752,f1222])).
% 99.18/12.93  fof(f12830,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f5752,f1227])).
% 99.18/12.93  fof(f12831,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(v_d2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f5752,f1319])).
% 99.18/12.93  fof(f12836,plain,(
% 99.18/12.93    ![X0,X1]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X1,X0),v_d2,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X1,X0),v_d1,tc_RealDef_Oreal))),
% 99.18/12.93    inference(resolution,[status(thm)],[f1239,f1320])).
% 99.18/12.93  fof(f12941,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1265,f5752])).
% 99.18/12.93  fof(f13004,definition,(
% 99.18/12.93    sQ292_spl <=> (c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f13005,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal)|~sQ292_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f13004])).
% 99.18/12.93  fof(f13008,plain,(
% 99.18/12.93    $false|~sQ292_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f13005,f1302])).
% 99.18/12.93  fof(f13009,plain,(
% 99.18/12.93    ~sQ292_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f13008])).
% 99.18/12.93  fof(f13025,definition,(
% 99.18/12.93    sQ293_spl <=> (c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f13026,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal)|~sQ293_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f13025])).
% 99.18/12.93  fof(f13029,plain,(
% 99.18/12.93    $false|~sQ293_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f13026,f1302])).
% 99.18/12.93  fof(f13030,plain,(
% 99.18/12.93    ~sQ293_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f13029])).
% 99.18/12.93  fof(f13212,definition,(
% 99.18/12.93    sQ303_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f13214,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal)|sQ303_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f13212])).
% 99.18/12.93  fof(f13228,plain,(
% 99.18/12.93    $false|sQ303_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f13214,f1265])).
% 99.18/12.93  fof(f13229,plain,(
% 99.18/12.93    sQ303_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f13228])).
% 99.18/12.93  fof(f13239,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1282,f5752])).
% 99.18/12.93  fof(f13266,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_Transcendental_Oln(v_d2),v_d2,tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1252,f1319])).
% 99.18/12.93  fof(f13267,plain,(
% 99.18/12.93    c_HOL_Oord__class_Oless(c_Transcendental_Oln(v_d1),v_d1,tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1252,f1318])).
% 99.18/12.93  fof(f13336,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(v_d2,c_Transcendental_Oln(v_d2),tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f13266,f5752])).
% 99.18/12.93  fof(f13405,definition,(
% 99.18/12.93    sQ314_spl <=> (class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f13407,plain,(
% 99.18/12.93    ~class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal)|sQ314_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f13405])).
% 99.18/12.93  fof(f13412,plain,(
% 99.18/12.93    $false|sQ314_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f13407,f1369])).
% 99.18/12.93  fof(f13413,plain,(
% 99.18/12.93    sQ314_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f13412])).
% 99.18/12.93  fof(f13445,definition,(
% 99.18/12.93    sQ317_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f13447,plain,(
% 99.18/12.93    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal)|sQ317_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f13445])).
% 99.18/12.93  fof(f13461,plain,(
% 99.18/12.93    $false|sQ317_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f13447,f1282])).
% 99.18/12.93  fof(f13462,plain,(
% 99.18/12.93    sQ317_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f13461])).
% 99.18/12.93  fof(f13475,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f1282])).
% 99.18/12.93  fof(f13476,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f1265])).
% 99.18/12.93  fof(f13483,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d2))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f9070])).
% 99.18/12.93  fof(f13484,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d1))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f9275])).
% 99.18/12.93  fof(f13487,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f1222])).
% 99.18/12.93  fof(f13488,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f1227])).
% 99.18/12.93  fof(f13490,plain,(
% 99.18/12.93    ~c_NthRoot_Osqrt(v_d1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 99.18/12.93    inference(resolution,[status(thm)],[f1266,f1318])).
% 99.18/12.93  fof(f13507,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X0,v_d1),v_d1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 99.18/12.93    inference(resolution,[status(thm)],[f1271,f1318])).
% 99.18/12.93  fof(f13569,plain,(
% 99.18/12.93    ![X0]: (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X0,v_d1),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 99.18/12.93    inference(resolution,[status(thm)],[f1273,f1318])).
% 99.18/12.93  fof(f14912,definition,(
% 99.18/12.93    sQ336_spl <=> (c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1=c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f14914,plain,(
% 99.18/12.93    ~c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1=c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1|sQ336_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f14912])).
% 99.18/12.93  fof(f14922,plain,(
% 99.18/12.93    $false|sQ336_spl),
% 99.18/12.93    inference(trivial_equality_resolution,[status(thm)],[f14914])).
% 99.18/12.93  fof(f14923,plain,(
% 99.18/12.93    sQ336_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f14922])).
% 99.18/12.93  fof(f15328,definition,(
% 99.18/12.93    sQ345_spl <=> (class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f15330,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal)|sQ345_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f15328])).
% 99.18/12.93  fof(f15331,definition,(
% 99.18/12.93    sQ346_spl <=> (class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f15333,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal)|sQ346_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f15331])).
% 99.18/12.93  fof(f15334,definition,(
% 99.18/12.93    sQ347_spl <=> (class_Power_Opower(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f15336,plain,(
% 99.18/12.93    ~class_Power_Opower(tc_RealDef_Oreal)|sQ347_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f15334])).
% 99.18/12.93  fof(f15341,definition,(
% 99.18/12.93    sQ349_spl <=> (class_Power_Opower(tc_nat))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f15343,plain,(
% 99.18/12.93    ~class_Power_Opower(tc_nat)|sQ349_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f15341])).
% 99.18/12.93  fof(f15345,definition,(
% 99.18/12.93    sQ350_spl <=> (class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal))),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f15347,plain,(
% 99.18/12.93    ~class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal)|sQ350_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f15345])).
% 99.18/12.93  fof(f15352,plain,(
% 99.18/12.93    $false|sQ345_spl),
% 99.18/12.93    inference(forward_subsumption_resolution,[status(thm)],[f15330,f1377])).
% 99.18/12.93  fof(f15353,plain,(
% 99.18/12.93    sQ345_spl),
% 99.18/12.93    inference(contradiction_clause,[status(thm)],[f15352])).
% 99.18/12.93  fof(f15409,definition,(
% 99.18/12.93    sQ351_spl <=> (c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1=c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1)),
% 99.18/12.93    introduced(definition,[new_symbols(definition,[sQ351_spl])],[split_symbol_definition])).
% 99.18/12.93  fof(f15411,plain,(
% 99.18/12.93    ~c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1=c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1|sQ351_spl),
% 99.18/12.93    inference(component_clause,[status(thm)],[f15409])).
% 99.18/12.93  fof(f15421,plain,(
% 99.18/12.95    $false|sQ351_spl),
% 99.18/12.95    inference(trivial_equality_resolution,[status(thm)],[f15411])).
% 99.18/12.95  fof(f15422,plain,(
% 99.18/12.95    sQ351_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f15421])).
% 99.18/12.95  fof(f15737,definition,(
% 99.18/12.95    ![X0]: (sQ359_spl <=> (~X0=X0))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f15738,plain,(
% 99.18/12.95    ![X0]: (~X0=X0|~sQ359_spl)),
% 99.18/12.95    inference(component_clause,[status(thm)],[f15737])).
% 99.18/12.95  fof(f15876,definition,(
% 99.18/12.95    sQ372_spl <=> (c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f15877,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ372_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f15876])).
% 99.18/12.95  fof(f16881,definition,(
% 99.18/12.95    ![X1,X2]: (sQ423_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f16882,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ423_spl)),
% 99.18/12.95    inference(component_clause,[status(thm)],[f16881])).
% 99.18/12.95  fof(f16896,definition,(
% 99.18/12.95    sQ426_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f16897,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ426_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f16896])).
% 99.18/12.95  fof(f16948,definition,(
% 99.18/12.95    ![X1,X2]: (sQ436_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f16949,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ436_spl)),
% 99.18/12.95    inference(component_clause,[status(thm)],[f16948])).
% 99.18/12.95  fof(f17130,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ372_spl),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f874,f15877])).
% 99.18/12.95  fof(f17131,plain,(
% 99.18/12.95    $false|~sQ372_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f17130,f1302])).
% 99.18/12.95  fof(f17132,plain,(
% 99.18/12.95    ~sQ372_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f17131])).
% 99.18/12.95  fof(f17601,definition,(
% 99.18/12.95    sQ468_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f17602,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal)|~sQ468_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f17601])).
% 99.18/12.95  fof(f17687,definition,(
% 99.18/12.95    sQ482_spl <=> (class_Ring__and__Field_Oordered__semiring__strict(tc_nat))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f17689,plain,(
% 99.18/12.95    ~class_Ring__and__Field_Oordered__semiring__strict(tc_nat)|sQ482_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f17687])).
% 99.18/12.95  fof(f19561,definition,(
% 99.18/12.95    sQ601_spl <=> (c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d2))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f19562,plain,(
% 99.18/12.95    c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d2))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ601_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f19561])).
% 99.18/12.95  fof(f19566,definition,(
% 99.18/12.95    sQ602_spl <=> (c_NthRoot_Osqrt(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f19567,plain,(
% 99.18/12.95    c_NthRoot_Osqrt(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ602_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f19566])).
% 99.18/12.95  fof(f19570,definition,(
% 99.18/12.95    sQ603_spl <=> (c_NthRoot_Osqrt(v_d1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ603_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f19571,plain,(
% 99.18/12.95    c_NthRoot_Osqrt(v_d1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ603_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f19570])).
% 99.18/12.95  fof(f19574,definition,(
% 99.18/12.95    sQ604_spl <=> (c_NthRoot_Osqrt(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f19575,plain,(
% 99.18/12.95    c_NthRoot_Osqrt(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ604_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f19574])).
% 99.18/12.95  fof(f19578,definition,(
% 99.18/12.95    sQ605_spl <=> (c_NthRoot_Osqrt(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f19579,plain,(
% 99.18/12.95    c_NthRoot_Osqrt(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ605_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f19578])).
% 99.18/12.95  fof(f19582,definition,(
% 99.18/12.95    sQ606_spl <=> (c_NthRoot_Osqrt(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ606_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f19583,plain,(
% 99.18/12.95    c_NthRoot_Osqrt(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ606_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f19582])).
% 99.18/12.95  fof(f20332,definition,(
% 99.18/12.95    ![X0]: (sQ644_spl <=> (c_HOL_Oord__class_Oless(c_RealDef_Oreal__of__preal(X0),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal)))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f20333,plain,(
% 99.18/12.95    ![X0]: (c_HOL_Oord__class_Oless(c_RealDef_Oreal__of__preal(X0),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal)|~sQ644_spl)),
% 99.18/12.95    inference(component_clause,[status(thm)],[f20332])).
% 99.18/12.95  fof(f21623,definition,(
% 99.18/12.95    sQ672_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d1)))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ672_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f21624,plain,(
% 99.18/12.95    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_NthRoot_Osqrt(c_NthRoot_Osqrt(v_d1))|~sQ672_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f21623])).
% 99.18/12.95  fof(f21820,definition,(
% 99.18/12.95    sQ725_spl <=> (c_Transcendental_Oln(v_d1)=v_d1)),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ725_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f21821,plain,(
% 99.18/12.95    c_Transcendental_Oln(v_d1)=v_d1|~sQ725_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f21820])).
% 99.18/12.95  fof(f21840,definition,(
% 99.18/12.95    sQ730_spl <=> (c_Transcendental_Oln(v_d2)=v_d2)),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f21841,plain,(
% 99.18/12.95    c_Transcendental_Oln(v_d2)=v_d2|~sQ730_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f21840])).
% 99.18/12.95  fof(f22068,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ436_spl)),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f3137,f16949])).
% 99.18/12.95  fof(f22069,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ436_spl)),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f3137,f22068])).
% 99.18/12.95  fof(f22070,plain,(
% 99.18/12.95    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ436_spl)),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f22069,f1302])).
% 99.18/12.95  fof(f22086,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ426_spl),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f3137,f16897])).
% 99.18/12.95  fof(f22087,plain,(
% 99.18/12.95    $false|~sQ426_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f22086,f1302])).
% 99.18/12.95  fof(f22088,plain,(
% 99.18/12.95    ~sQ426_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22087])).
% 99.18/12.95  fof(f22094,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ423_spl)),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f3137,f16882])).
% 99.18/12.95  fof(f22095,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ423_spl)),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f2895,f22094])).
% 99.18/12.95  fof(f22096,plain,(
% 99.18/12.95    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ423_spl)),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f22095,f1302])).
% 99.18/12.95  fof(f22099,plain,(
% 99.18/12.95    $false|sQ12_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f1900,f1336])).
% 99.18/12.95  fof(f22100,plain,(
% 99.18/12.95    sQ12_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22099])).
% 99.18/12.95  fof(f22101,plain,(
% 99.18/12.95    $false|~sQ359_spl),
% 99.18/12.95    inference(trivial_equality_resolution,[status(thm)],[f15738])).
% 99.18/12.95  fof(f22102,plain,(
% 99.18/12.95    ~sQ359_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22101])).
% 99.18/12.95  fof(f22103,plain,(
% 99.18/12.95    $false|~sQ644_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f20333,f1302])).
% 99.18/12.95  fof(f22104,plain,(
% 99.18/12.95    ~sQ644_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22103])).
% 99.18/12.95  fof(f22107,plain,(
% 99.18/12.95    $false|sQ482_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f17689,f1324])).
% 99.18/12.95  fof(f22108,plain,(
% 99.18/12.95    sQ482_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22107])).
% 99.18/12.95  fof(f22109,plain,(
% 99.18/12.95    $false|~sQ468_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f17602,f1302])).
% 99.18/12.95  fof(f22110,plain,(
% 99.18/12.95    ~sQ468_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22109])).
% 99.18/12.95  fof(f22111,plain,(
% 99.18/12.95    $false|sQ346_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f15333,f1381])).
% 99.18/12.95  fof(f22112,plain,(
% 99.18/12.95    sQ346_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22111])).
% 99.18/12.95  fof(f22113,plain,(
% 99.18/12.95    $false|sQ350_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f15347,f1363])).
% 99.18/12.95  fof(f22114,plain,(
% 99.18/12.95    sQ350_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22113])).
% 99.18/12.95  fof(f22115,plain,(
% 99.18/12.95    $false|sQ349_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f15343,f1345])).
% 99.18/12.95  fof(f22116,plain,(
% 99.18/12.95    sQ349_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22115])).
% 99.18/12.95  fof(f22117,plain,(
% 99.18/12.95    $false|sQ13_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f1903,f1328])).
% 99.18/12.95  fof(f22118,plain,(
% 99.18/12.95    sQ13_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22117])).
% 99.18/12.95  fof(f22119,plain,(
% 99.18/12.95    $false|sQ347_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f15336,f1399])).
% 99.18/12.95  fof(f22120,plain,(
% 99.18/12.95    sQ347_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22119])).
% 99.18/12.95  fof(f22121,plain,(
% 99.18/12.95    $false|sQ14_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f1906,f1337])).
% 99.18/12.95  fof(f22122,plain,(
% 99.18/12.95    sQ14_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22121])).
% 99.18/12.95  fof(f22126,plain,(
% 99.18/12.95    $false|~sQ603_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f19571,f13490])).
% 99.18/12.95  fof(f22127,plain,(
% 99.18/12.95    ~sQ603_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22126])).
% 99.18/12.95  fof(f22128,plain,(
% 99.18/12.95    $false|~sQ602_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f19567,f13488])).
% 99.18/12.95  fof(f22129,plain,(
% 99.18/12.95    ~sQ602_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22128])).
% 99.18/12.95  fof(f22130,plain,(
% 99.18/12.95    $false|~sQ604_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f19575,f13487])).
% 99.18/12.95  fof(f22131,plain,(
% 99.18/12.95    ~sQ604_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22130])).
% 99.18/12.95  fof(f22132,plain,(
% 99.18/12.95    $false|~sQ672_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f21624,f13484])).
% 99.18/12.95  fof(f22133,plain,(
% 99.18/12.95    ~sQ672_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22132])).
% 99.18/12.95  fof(f22134,plain,(
% 99.18/12.95    $false|~sQ601_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f19562,f13483])).
% 99.18/12.95  fof(f22135,plain,(
% 99.18/12.95    ~sQ601_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22134])).
% 99.18/12.95  fof(f22136,plain,(
% 99.18/12.95    $false|~sQ605_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f19579,f13476])).
% 99.18/12.95  fof(f22137,plain,(
% 99.18/12.95    ~sQ605_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22136])).
% 99.18/12.95  fof(f22138,plain,(
% 99.18/12.95    $false|~sQ606_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f19583,f13475])).
% 99.18/12.95  fof(f22139,plain,(
% 99.18/12.95    ~sQ606_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f22138])).
% 99.18/12.95  fof(f23042,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(v_d2,v_d2,tc_RealDef_Oreal)|~sQ730_spl),
% 99.18/12.95    inference(backward_demodulation,[status(thm)],[f21841,f13266])).
% 99.18/12.95  fof(f23048,plain,(
% 99.18/12.95    $false|~sQ730_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f23042,f1302])).
% 99.18/12.95  fof(f23049,plain,(
% 99.18/12.95    ~sQ730_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f23048])).
% 99.18/12.95  fof(f23541,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(v_d1,v_d1,tc_RealDef_Oreal)|~sQ725_spl),
% 99.18/12.95    inference(backward_demodulation,[status(thm)],[f21821,f13267])).
% 99.18/12.95  fof(f23546,plain,(
% 99.18/12.95    $false|~sQ725_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f23541,f1302])).
% 99.18/12.95  fof(f23547,plain,(
% 99.18/12.95    ~sQ725_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f23546])).
% 99.18/12.95  fof(f23822,definition,(
% 99.18/12.95    sQ774_spl <=> (c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ774_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f23823,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ774_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f23822])).
% 99.18/12.95  fof(f23825,definition,(
% 99.18/12.95    sQ775_spl <=> (c_HOL_Oord__class_Oless(v_d2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ775_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f23826,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(v_d2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ775_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f23825])).
% 99.18/12.95  fof(f23839,plain,(
% 99.18/12.95    $false|~sQ774_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f23823,f12830])).
% 99.18/12.95  fof(f23840,plain,(
% 99.18/12.95    ~sQ774_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f23839])).
% 99.18/12.95  fof(f23895,definition,(
% 99.18/12.95    sQ784_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ784_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f23896,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ784_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f23895])).
% 99.18/12.95  fof(f23909,plain,(
% 99.18/12.95    $false|~sQ784_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f23896,f12829])).
% 99.18/12.95  fof(f23910,plain,(
% 99.18/12.95    ~sQ784_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f23909])).
% 99.18/12.95  fof(f24155,definition,(
% 99.18/12.95    sQ793_spl <=> (c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ793_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f24156,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ793_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f24155])).
% 99.18/12.95  fof(f24169,plain,(
% 99.18/12.95    $false|~sQ793_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f24156,f12941])).
% 99.18/12.95  fof(f24170,plain,(
% 99.18/12.95    ~sQ793_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f24169])).
% 99.18/12.95  fof(f24224,definition,(
% 99.18/12.95    sQ802_spl <=> (c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ802_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f24225,plain,(
% 99.18/12.95    c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ802_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f24224])).
% 99.18/12.95  fof(f24238,plain,(
% 99.18/12.95    $false|~sQ802_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f24225,f13239])).
% 99.18/12.95  fof(f24239,plain,(
% 99.18/12.95    ~sQ802_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f24238])).
% 99.18/12.95  fof(f24316,plain,(
% 99.18/12.95    $false|~sQ436_spl),
% 99.18/12.95    inference(backward_subsumption_resolution,[status(thm)],[f1318,f22070])).
% 99.18/12.95  fof(f24323,plain,(
% 99.18/12.95    ~sQ436_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f24316])).
% 99.18/12.95  fof(f24382,plain,(
% 99.18/12.95    $false|~sQ423_spl),
% 99.18/12.95    inference(backward_subsumption_resolution,[status(thm)],[f1318,f22096])).
% 99.18/12.95  fof(f24390,plain,(
% 99.18/12.95    ~sQ423_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f24382])).
% 99.18/12.95  fof(f31741,plain,(
% 99.18/12.95    $false|~sQ775_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f23826,f12831])).
% 99.18/12.95  fof(f31742,plain,(
% 99.18/12.95    ~sQ775_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f31741])).
% 99.18/12.95  fof(f36600,plain,(
% 99.18/12.95    ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X1,tc_RealDef_Oreal))),
% 99.18/12.95    inference(resolution,[status(thm)],[f6996,f1302])).
% 99.18/12.95  fof(f36627,plain,(
% 99.18/12.95    sQ4_spl),
% 99.18/12.95    inference(split_clause,[status(thm)],[f36600,f1532])).
% 99.18/12.95  fof(f37051,definition,(
% 99.18/12.95    sQ1151_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(c_Transcendental_Oln(v_d1),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ1151_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f37053,plain,(
% 99.18/12.95    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(c_Transcendental_Oln(v_d1),tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ1151_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f37051])).
% 99.18/12.95  fof(f37057,plain,(
% 99.18/12.95    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)|sQ1151_spl),
% 99.18/12.95    inference(forward_demodulation,[status(thm)],[f7581,f37053])).
% 99.18/12.95  fof(f37058,plain,(
% 99.18/12.95    $false|sQ1151_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f37057,f1318])).
% 99.18/12.95  fof(f37059,plain,(
% 99.18/12.95    sQ1151_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f37058])).
% 99.18/12.95  fof(f39022,definition,(
% 99.18/12.95    ![X0,X1]: (sQ1232_spl <=> (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ1232_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f39023,plain,(
% 99.18/12.95    ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|~sQ1232_spl)),
% 99.18/12.95    inference(component_clause,[status(thm)],[f39022])).
% 99.18/12.95  fof(f39183,plain,(
% 99.18/12.95    ~c_HOL_Oord__class_Oless(c_Transcendental_Oln(v_d2),v_d2,tc_RealDef_Oreal)|~sQ1232_spl),
% 99.18/12.95    inference(resolution,[status(thm)],[f39023,f13336])).
% 99.18/12.95  fof(f39302,plain,(
% 99.18/12.95    $false|~sQ1232_spl),
% 99.18/12.95    inference(forward_subsumption_resolution,[status(thm)],[f39183,f13266])).
% 99.18/12.95  fof(f39303,plain,(
% 99.18/12.95    ~sQ1232_spl),
% 99.18/12.95    inference(contradiction_clause,[status(thm)],[f39302])).
% 99.18/12.95  fof(f40096,plain,(
% 99.18/12.95    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d2,v_d1),v_d1,tc_RealDef_Oreal)),
% 99.18/12.95    inference(resolution,[status(thm)],[f13569,f12836])).
% 99.18/12.95  fof(f40128,definition,(
% 99.18/12.95    sQ1267_spl <=> (c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d2,v_d1),v_d1,tc_RealDef_Oreal))),
% 99.18/12.95    introduced(definition,[new_symbols(definition,[sQ1267_spl])],[split_symbol_definition])).
% 99.18/12.95  fof(f40130,plain,(
% 99.18/12.95    ~c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d2,v_d1),v_d1,tc_RealDef_Oreal)|sQ1267_spl),
% 99.18/12.95    inference(component_clause,[status(thm)],[f40128])).
% 99.18/12.95  fof(f40131,plain,(
% 99.18/12.95    ~sQ19_spl|~sQ0_spl|~sQ1267_spl),
% 99.18/12.95    inference(split_clause,[status(thm)],[f40096,f2276,f1402,f40128])).
% 99.18/12.99  fof(f40206,plain,(
% 99.18/12.99    ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)|sQ1267_spl),
% 99.18/12.99    inference(resolution,[status(thm)],[f40130,f13507])).
% 99.18/12.99  fof(f40207,plain,(
% 99.18/12.99    ~sQ19_spl|sQ1267_spl),
% 99.18/12.99    inference(split_clause,[status(thm)],[f40206,f2276,f40128])).
% 99.18/12.99  fof(f40208,plain,(
% 99.18/12.99    $false),
% 99.18/12.99    inference(sat_refutation,[status(thm)],[f1410,f2281,f2554,f2920,f3111,f3503,f3548,f3568,f3571,f3602,f3620,f3846,f3848,f4275,f4791,f4794,f4820,f4823,f4830,f5256,f5611,f6123,f6215,f6275,f6346,f7669,f7671,f7673,f7675,f7822,f7897,f8114,f8264,f8443,f8499,f9046,f9255,f9314,f9384,f9405,f9687,f10402,f11189,f11226,f11589,f11875,f12110,f12538,f12541,f12546,f12548,f12550,f12591,f12715,f13009,f13030,f13229,f13413,f13462,f14923,f15353,f15422,f17132,f22088,f22100,f22102,f22104,f22108,f22110,f22112,f22114,f22116,f22118,f22120,f22122,f22127,f22129,f22131,f22133,f22135,f22137,f22139,f23049,f23547,f23840,f23910,f24170,f24239,f24323,f24390,f31742,f36627,f37059,f39303,f40131,f40207])).
% 99.18/12.99  % SZS output end CNFRefutation for theBenchmark.p
% 3.13/13.01  % Elapsed time: 12.634841 seconds
% 3.13/13.01  % CPU time: 99.743959 seconds
% 3.13/13.01  % Total memory used: 759.237 MB
% 3.13/13.01  % Net memory used: 730.883 MB
%------------------------------------------------------------------------------