%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW233+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Sun Sep 27 09:13:58 AM UTC 2026
% Result : Theorem 74.87s 11.06s
% Output : CNFRefutation 74.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 57
% Syntax : Number of formulae : 280 ( 153 unt; 0 def)
% Number of atoms : 488 ( 130 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 369 ( 161 ~; 158 |; 5 &)
% ( 12 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-3 aty)
% Number of variables : 274 ( 19 sgn 82 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_real__le__refl,axiom,
! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w),
file('theBenchmark.p',fact_real__le__refl) ).
fof(fact_real__le__linear,axiom,
! [V_w,V_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w) ),
file('theBenchmark.p',fact_real__le__linear) ).
fof(fact_order__eq__iff,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Oorder(T_a)
=> ( V_x_2 = V_y_2
<=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) ) ),
file('theBenchmark.p',fact_order__eq__iff) ).
fof(fact_xt1_I4_J,axiom,
! [V_c,V_a,V_b,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_a)
=> ( V_b = V_c
=> c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_a) ) ) ),
file('theBenchmark.p',fact_xt1_I4_J) ).
fof(fact_norm__ge__zero,axiom,
! [V_x,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)) ),
file('theBenchmark.p',fact_norm__ge__zero) ).
fof(fact_ord__less__eq__trans,axiom,
! [V_c,V_b,V_a,T_a] :
( class_Orderings_Oord(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
=> ( V_b = V_c
=> c_Orderings_Oord__class_Oless(T_a,V_a,V_c) ) ) ),
file('theBenchmark.p',fact_ord__less__eq__trans) ).
fof(fact_less__eq__real__def,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> ( V_x_2 = V_y_2
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
file('theBenchmark.p',fact_less__eq__real__def) ).
fof(fact_real__less__def,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
file('theBenchmark.p',fact_real__less__def) ).
fof(fact_real__mult__1,axiom,
! [V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),V_z) = V_z,
file('theBenchmark.p',fact_real__mult__1) ).
fof(fact_real__add__mult__distrib,axiom,
! [V_w,V_z2,V_z1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z1,V_z2)),V_w) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z1),V_w),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z2),V_w)),
file('theBenchmark.p',fact_real__add__mult__distrib) ).
fof(fact_real__mult__commute,axiom,
! [V_w,V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_w) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_w),V_z),
file('theBenchmark.p',fact_real__mult__commute) ).
fof(fact_nat__le__linear,axiom,
! [V_n,V_m] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n,V_m)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m,V_n) ),
file('theBenchmark.p',fact_nat__le__linear) ).
fof(fact_plus__nat_Oadd__0,axiom,
! [V_n] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_n) = V_n,
file('theBenchmark.p',fact_plus__nat_Oadd__0) ).
fof(fact_real__of__nat__ge__zero,axiom,
! [V_n] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,V_n)),
file('theBenchmark.p',fact_real__of__nat__ge__zero) ).
fof(fact_order__trans,axiom,
! [V_z,V_y,V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)
=> c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_z) ) ) ),
file('theBenchmark.p',fact_order__trans) ).
fof(fact_abs__of__nonneg,axiom,
! [V_a,T_a] :
( class_Groups_Oordered__ab__group__add__abs(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
=> c_Groups_Oabs__class_Oabs(T_a,V_a) = V_a ) ),
file('theBenchmark.p',fact_abs__of__nonneg) ).
fof(fact_abs__le__D1,axiom,
! [V_b,V_a,T_a] :
( class_Groups_Oordered__ab__group__add__abs(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a),V_b)
=> c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b) ) ),
file('theBenchmark.p',fact_abs__le__D1) ).
fof(fact_linorder__neq__iff,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( V_x_2 != V_y_2
<=> ( c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) ) ),
file('theBenchmark.p',fact_linorder__neq__iff) ).
fof(fact_mult__less__cancel__right__disj,axiom,
! [V_b_2,V_ca_2,V_ab_2,T_a] :
( class_Rings_Olinordered__ring__strict(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_ab_2),V_ca_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_b_2),V_ca_2))
<=> ( ( c_Orderings_Oord__class_Oless(T_a,V_b_2,V_ab_2)
& c_Orderings_Oord__class_Oless(T_a,V_ca_2,c_Groups_Ozero__class_Ozero(T_a)) )
| ( c_Orderings_Oord__class_Oless(T_a,V_ab_2,V_b_2)
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_ca_2) ) ) ) ),
file('theBenchmark.p',fact_mult__less__cancel__right__disj) ).
fof(fact_linorder__antisym__conv1,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
<=> V_x_2 = V_y_2 ) ) ),
file('theBenchmark.p',fact_linorder__antisym__conv1) ).
fof(fact_less__le__not__le,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) ) ),
file('theBenchmark.p',fact_less__le__not__le) ).
fof(fact_linorder__not__less,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2) ) ),
file('theBenchmark.p',fact_linorder__not__less) ).
fof(fact_add__strict__right__mono,axiom,
! [V_c,V_b,V_a,T_a] :
( class_Groups_Oordered__cancel__ab__semigroup__add(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_c)) ) ),
file('theBenchmark.p',fact_add__strict__right__mono) ).
fof(fact_natceiling__mono,axiom,
! [V_y,V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)
=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(V_x),c_RComplete_Onatceiling(V_y)) ),
file('theBenchmark.p',fact_natceiling__mono) ).
fof(fact_natceiling__neg,axiom,
! [V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_RComplete_Onatceiling(V_x) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('theBenchmark.p',fact_natceiling__neg) ).
fof(fact_natceiling__le__eq__one,axiom,
! [V_x_2] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(V_x_2),c_Groups_Oone__class_Oone(tc_Nat_Onat))
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
file('theBenchmark.p',fact_natceiling__le__eq__one) ).
fof(fact_natfloor__mono,axiom,
! [V_y,V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)
=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatfloor(V_x),c_RComplete_Onatfloor(V_y)) ),
file('theBenchmark.p',fact_natfloor__mono) ).
fof(fact_natfloor__neg,axiom,
! [V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_RComplete_Onatfloor(V_x) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('theBenchmark.p',fact_natfloor__neg) ).
fof(fact_le__natfloor__eq__one,axiom,
! [V_x_2] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_RComplete_Onatfloor(V_x_2))
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),V_x_2) ),
file('theBenchmark.p',fact_le__natfloor__eq__one) ).
fof(fact_natfloor__real__of__nat,axiom,
! [V_n] : c_RComplete_Onatfloor(c_RealDef_Oreal(tc_Nat_Onat,V_n)) = V_n,
file('theBenchmark.p',fact_natfloor__real__of__nat) ).
fof(fact_natceiling__real__of__nat,axiom,
! [V_n] : c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,V_n)) = V_n,
file('theBenchmark.p',fact_natceiling__real__of__nat) ).
fof(fact_real__natceiling__ge,axiom,
! [V_x] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(V_x))),
file('theBenchmark.p',fact_real__natceiling__ge) ).
fof(fact_real__natfloor__le,axiom,
! [V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_x)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(V_x)),V_x) ),
file('theBenchmark.p',fact_real__natfloor__le) ).
fof(fact_le__natfloor__eq,axiom,
! [V_ab_2,V_x_2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_x_2)
=> ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_ab_2,c_RComplete_Onatfloor(V_x_2))
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,V_ab_2),V_x_2) ) ),
file('theBenchmark.p',fact_le__natfloor__eq) ).
fof(fact_natceiling__le__eq,axiom,
! [V_ab_2,V_x_2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_x_2)
=> ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(V_x_2),V_ab_2)
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,c_RealDef_Oreal(tc_Nat_Onat,V_ab_2)) ) ),
file('theBenchmark.p',fact_natceiling__le__eq) ).
fof(fact_natfloor__add,axiom,
! [V_a,V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_x)
=> c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,c_RealDef_Oreal(tc_Nat_Onat,V_a))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatfloor(V_x),V_a) ),
file('theBenchmark.p',fact_natfloor__add) ).
fof(fact_natceiling__add,axiom,
! [V_a,V_x] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_x)
=> c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,c_RealDef_Oreal(tc_Nat_Onat,V_a))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(V_x),V_a) ),
file('theBenchmark.p',fact_natceiling__add) ).
fof(fact_complex__mod__rcis,axiom,
! [V_a,V_r] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Orcis(V_r,V_a)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r),
file('theBenchmark.p',fact_complex__mod__rcis) ).
fof(fact_ln__less__self,axiom,
! [V_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_x)
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Oln(V_x),V_x) ),
file('theBenchmark.p',fact_ln__less__self) ).
fof(conj_0,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_1052,plain,
( c_Orderings_Oord__class_Oless__eq(A,B,D)
| ~ c_Orderings_Oord__class_Oless__eq(A,C,D)
| ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ class_Orderings_Opreorder(A) ),
inference(clausify,[status(thm)],[fact_order__trans]) ).
cnf(c_1058,plain,
( c_Groups_Oabs__class_Oabs(A,B) = B
| ~ c_Orderings_Oord__class_Oless__eq(A,c_Groups_Ozero__class_Ozero(A),B)
| ~ class_Groups_Oordered__ab__group__add__abs(A) ),
inference(clausify,[status(thm)],[fact_abs__of__nonneg]) ).
cnf(c_1091,plain,
( c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ c_Orderings_Oord__class_Oless__eq(A,c_Groups_Oabs__class_Oabs(A,B),C)
| ~ class_Groups_Oordered__ab__group__add__abs(A) ),
inference(clausify,[status(thm)],[fact_abs__le__D1]) ).
cnf(c_1136,plain,
( ~ c_Orderings_Oord__class_Oless(A,B,C)
| B != C
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[fact_linorder__neq__iff]) ).
cnf(c_1170,plain,
( c_Orderings_Oord__class_Oless(A,C,c_Groups_Ozero__class_Ozero(A))
| c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),C)
| ~ c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),C))
| ~ class_Rings_Olinordered__ring__strict(A) ),
inference(clausify,[status(thm)],[fact_mult__less__cancel__right__disj]) ).
cnf(c_1213,plain,
( C = B
| ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[fact_linorder__antisym__conv1]) ).
cnf(c_1217,plain,
( c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Opreorder(A) ),
inference(clausify,[status(thm)],[fact_less__le__not__le]) ).
cnf(c_1219,plain,
( c_Orderings_Oord__class_Oless__eq(A,C,B)
| ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Opreorder(A) ),
inference(clausify,[status(thm)],[fact_less__le__not__le]) ).
cnf(c_1224,plain,
( ~ c_Orderings_Oord__class_Oless__eq(A,C,B)
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[fact_linorder__not__less]) ).
cnf(c_1251,plain,
( c_Orderings_Oord__class_Oless(A,c_Groups_Oplus__class_Oplus(A,B,D),c_Groups_Oplus__class_Oplus(A,C,D))
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(A) ),
inference(clausify,[status(thm)],[fact_add__strict__right__mono]) ).
cnf(c_1382,plain,
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(A),c_RComplete_Onatceiling(B))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_natceiling__mono]) ).
fof(fact_natceiling__one,axiom,
c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
file('theBenchmark.p',fact_natceiling__one) ).
cnf(c_1383,plain,
c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
inference(clausify,[status(thm)],[fact_natceiling__one]) ).
cnf(c_1385,plain,
( c_RComplete_Onatceiling(A) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(clausify,[status(thm)],[fact_natceiling__neg]) ).
cnf(c_1386,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(A),c_Groups_Oone__class_Oone(tc_Nat_Onat)) ),
inference(clausify,[status(thm)],[fact_natceiling__le__eq__one]) ).
cnf(c_1391,plain,
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatfloor(A),c_RComplete_Onatfloor(B))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_natfloor__mono]) ).
fof(fact_natfloor__one,axiom,
c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
file('theBenchmark.p',fact_natfloor__one) ).
cnf(c_1392,plain,
c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
inference(clausify,[status(thm)],[fact_natfloor__one]) ).
cnf(c_1393,plain,
( c_RComplete_Onatfloor(A) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(clausify,[status(thm)],[fact_natfloor__neg]) ).
cnf(c_1394,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_RComplete_Onatfloor(A)) ),
inference(clausify,[status(thm)],[fact_le__natfloor__eq__one]) ).
cnf(c_1402,plain,
c_RComplete_Onatfloor(c_RealDef_Oreal(tc_Nat_Onat,A)) = A,
inference(clausify,[status(thm)],[fact_natfloor__real__of__nat]) ).
cnf(c_1403,plain,
c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)) = A,
inference(clausify,[status(thm)],[fact_natceiling__real__of__nat]) ).
cnf(c_1405,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(A))),
inference(clausify,[status(thm)],[fact_real__natceiling__ge]) ).
cnf(c_1413,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(A)),A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[fact_real__natfloor__le]) ).
cnf(c_1416,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,B),A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,c_RComplete_Onatfloor(A))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[fact_le__natfloor__eq]) ).
cnf(c_1419,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealDef_Oreal(tc_Nat_Onat,B))
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(A),B)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[fact_natceiling__le__eq]) ).
cnf(c_1425,plain,
( c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,A,c_RealDef_Oreal(tc_Nat_Onat,B))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatfloor(A),B)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[fact_natfloor__add]) ).
cnf(c_1428,plain,
( c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,A,c_RealDef_Oreal(tc_Nat_Onat,B))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(A),B)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[fact_natceiling__add]) ).
cnf(c_1491,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Orcis(A,B)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A),
inference(clausify,[status(thm)],[fact_complex__mod__rcis]) ).
cnf(c_1506,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Oln(A),A)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[fact_ln__less__self]) ).
fof(fact_ln__one,axiom,
c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('theBenchmark.p',fact_ln__one) ).
cnf(c_1511,plain,
c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[fact_ln__one]) ).
fof(arity_Nat__Onat__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_Nat_Onat),
file('theBenchmark.p',arity_Nat__Onat__Orderings_Opreorder) ).
cnf(c_1765,plain,
class_Orderings_Opreorder(tc_Nat_Onat),
inference(clausify,[status(thm)],[arity_Nat__Onat__Orderings_Opreorder]) ).
fof(arity_Nat__Onat__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_Nat_Onat),
file('theBenchmark.p',arity_Nat__Onat__Orderings_Olinorder) ).
cnf(c_1766,plain,
class_Orderings_Olinorder(tc_Nat_Onat),
inference(clausify,[status(thm)],[arity_Nat__Onat__Orderings_Olinorder]) ).
fof(arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add,axiom,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add) ).
cnf(c_1777,plain,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add]) ).
fof(arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs,axiom,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs) ).
cnf(c_1785,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs]) ).
fof(arity_RealDef__Oreal__Rings_Olinordered__ring__strict,axiom,
class_Rings_Olinordered__ring__strict(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Rings_Olinordered__ring__strict) ).
cnf(c_1792,plain,
class_Rings_Olinordered__ring__strict(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Rings_Olinordered__ring__strict]) ).
fof(arity_RealDef__Oreal__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Opreorder) ).
cnf(c_1809,plain,
class_Orderings_Opreorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Opreorder]) ).
fof(arity_RealDef__Oreal__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Olinorder) ).
cnf(c_1810,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Olinorder]) ).
fof(fact_h,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
file('theBenchmark.p',fact_h) ).
cnf(c_1902,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(clausify,[status(thm)],[fact_h]) ).
cnf(c_1903,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,A),
inference(clausify,[status(thm)],[fact_real__le__refl]) ).
cnf(c_1904,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__le__linear]) ).
cnf(c_1909,plain,
( ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ c_Orderings_Oord__class_Oless__eq(A,C,B)
| B = C
| ~ class_Orderings_Oorder(A) ),
inference(clausify,[status(thm)],[fact_order__eq__iff]) ).
cnf(c_1914,plain,
( c_Orderings_Oord__class_Oless__eq(A,D,C)
| D != B
| ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ class_Orderings_Oorder(A) ),
inference(clausify,[status(thm)],[fact_xt1_I4_J]) ).
fof(fact_real__zero__not__eq__one,axiom,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('theBenchmark.p',fact_real__zero__not__eq__one) ).
cnf(c_1924,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[fact_real__zero__not__eq__one]) ).
cnf(c_1925,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(A,B))
| ~ class_RealVector_Oreal__normed__vector(A) ),
inference(clausify,[status(thm)],[fact_norm__ge__zero]) ).
cnf(c_1959,plain,
( c_Orderings_Oord__class_Oless(A,B,D)
| D != C
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Oord(A) ),
inference(clausify,[status(thm)],[fact_ord__less__eq__trans]) ).
cnf(c_2013,plain,
( B != A
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_less__eq__real__def]) ).
cnf(c_2014,plain,
( B != A
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__less__def]) ).
cnf(c_2018,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A) = A,
inference(clausify,[status(thm)],[fact_real__mult__1]) ).
cnf(c_2019,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),C),B)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,A,C)),B),
inference(clausify,[status(thm)],[fact_real__add__mult__distrib]) ).
cnf(c_2067,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),B) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),B),A),
inference(clausify,[status(thm)],[fact_real__mult__commute]) ).
cnf(c_2183,plain,
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B) ),
inference(clausify,[status(thm)],[fact_nat__le__linear]) ).
cnf(c_2206,plain,
c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A) = A,
inference(clausify,[status(thm)],[fact_plus__nat_Oadd__0]) ).
cnf(c_2272,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A)),
inference(clausify,[status(thm)],[fact_real__of__nat__ge__zero]) ).
fof(fact_real__of__nat__1,axiom,
c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('theBenchmark.p',fact_real__of__nat__1) ).
cnf(c_2289,plain,
c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[fact_real__of__nat__1]) ).
fof(arity_Nat__Onat__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_Nat_Onat),
file('theBenchmark.p',arity_Nat__Onat__Orderings_Oorder) ).
cnf(c_2843,plain,
class_Orderings_Oorder(tc_Nat_Onat),
inference(clausify,[status(thm)],[arity_Nat__Onat__Orderings_Oorder]) ).
fof(arity_Nat__Onat__Orderings_Oord,axiom,
class_Orderings_Oord(tc_Nat_Onat),
file('theBenchmark.p',arity_Nat__Onat__Orderings_Oord) ).
cnf(c_2844,plain,
class_Orderings_Oord(tc_Nat_Onat),
inference(clausify,[status(thm)],[arity_Nat__Onat__Orderings_Oord]) ).
fof(arity_RealDef__Oreal__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Oorder) ).
cnf(c_2856,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Oorder]) ).
fof(arity_Complex__Ocomplex__RealVector_Oreal__normed__vector,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
cnf(c_2859,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[arity_Complex__Ocomplex__RealVector_Oreal__normed__vector]) ).
cnf(c_2880,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_3102,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),
inference(resolve,[status(thm)],[c_1903,c_1428]) ).
cnf(c_3103,plain,
c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),
inference(resolve,[status(thm)],[c_1903,c_1425]) ).
cnf(c_22739,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A) ),
inference(resolve,[status(thm)],[c_1903,c_1419]) ).
cnf(c_3108,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),
inference(resolve,[status(thm)],[c_2272,c_22739]) ).
cnf(c_3111,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_1903,c_1413]) ).
cnf(c_22740,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,A)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1903,c_1224]) ).
cnf(c_3144,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,A),
inference(resolve,[status(thm)],[c_1810,c_22740]) ).
cnf(c_22741,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1903,c_1091]) ).
cnf(c_3171,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)),
inference(resolve,[status(thm)],[c_1785,c_22741]) ).
cnf(c_22742,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1903,c_1058]) ).
cnf(c_3175,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_1785,c_22742]) ).
cnf(c_3256,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_3108,c_1386]) ).
cnf(c_3288,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),v_r____),
inference(resolve,[status(thm)],[c_1904,c_2880]) ).
cnf(c_3314,plain,
( c_RComplete_Onatfloor(A) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(resolve,[status(thm)],[c_1904,c_1393]) ).
cnf(c_22743,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_1904,c_1219]) ).
cnf(c_22744,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(copy,[status(thm)],[c_22743]) ).
cnf(c_3359,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_1809,c_22744]) ).
cnf(c_3454,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatfloor(A),c_RComplete_Onatfloor(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))),
inference(resolve,[status(thm)],[c_3171,c_1391]) ).
cnf(c_22745,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A),B)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3171,c_1052]) ).
cnf(c_3488,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A),B) ),
inference(resolve,[status(thm)],[c_1809,c_22745]) ).
cnf(c_3706,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_3256,c_1413]) ).
cnf(c_22746,plain,
( c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3256,c_1213]) ).
cnf(c_22747,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(copy,[status(thm)],[c_22746]) ).
cnf(c_22748,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(resolve,[status(thm)],[c_1810,c_22747]) ).
cnf(c_3732,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_1924,c_22748]) ).
cnf(c_22749,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3256,c_1058]) ).
cnf(c_3759,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_1785,c_22749]) ).
cnf(c_22750,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,v_r____)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3288,c_1052]) ).
cnf(c_3822,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,v_r____)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) ),
inference(resolve,[status(thm)],[c_1809,c_22750]) ).
cnf(c_3853,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_3732,c_1506]) ).
cnf(c_22751,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),A))
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3732,c_1251]) ).
cnf(c_3858,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),A)),
inference(resolve,[status(thm)],[c_1777,c_22751]) ).
cnf(c_3892,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))),
inference(resolve,[status(thm)],[c_2013,c_1403]) ).
cnf(c_3894,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_2013,c_1392]) ).
cnf(c_3896,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_2013,c_1383]) ).
cnf(c_22752,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(copy,[status(thm)],[c_1511]) ).
cnf(c_3900,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_2013,c_22752]) ).
cnf(c_22753,plain,
A = c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)),
inference(copy,[status(thm)],[c_1403]) ).
cnf(c_3906,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)),A),
inference(resolve,[status(thm)],[c_2013,c_22753]) ).
cnf(c_22754,plain,
c_Groups_Oone__class_Oone(tc_RealDef_Oreal) != c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_3853,c_2014]) ).
cnf(c_4234,plain,
c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(copy,[status(thm)],[c_22754]) ).
cnf(c_22755,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3853,c_1217]) ).
cnf(c_4239,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_1809,c_22755]) ).
cnf(c_4310,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),A),
inference(resolve,[status(thm)],[c_3892,c_1428]) ).
cnf(c_4324,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(A),c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)))),
inference(resolve,[status(thm)],[c_3892,c_1382]) ).
cnf(c_22756,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))))
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3892,c_1091]) ).
cnf(c_4379,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)))),
inference(resolve,[status(thm)],[c_1785,c_22756]) ).
cnf(c_4846,plain,
c_RComplete_Onatfloor(c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(resolve,[status(thm)],[c_3900,c_1393]) ).
cnf(c_4907,plain,
c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(resolve,[status(thm)],[c_3906,c_1385]) ).
cnf(c_4908,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))),c_RComplete_Onatceiling(A)),
inference(resolve,[status(thm)],[c_3906,c_1382]) ).
cnf(c_22757,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A),
inference(paramod,[status(thm)],[c_4907,c_4310]) ).
cnf(c_4952,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_RealDef_Oreal(tc_Nat_Onat,A))) = A,
inference(paramod,[status(thm)],[c_2206,c_22757]) ).
cnf(c_22758,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| A != c_Groups_Oone__class_Oone(tc_Nat_Onat)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1914,c_3896]) ).
cnf(c_22759,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Groups_Oone__class_Oone(tc_Nat_Onat) != A
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(copy,[status(thm)],[c_22758]) ).
cnf(c_5720,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Groups_Oone__class_Oone(tc_Nat_Onat) != A ),
inference(resolve,[status(thm)],[c_2856,c_22759]) ).
cnf(c_22760,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| A != c_Groups_Oone__class_Oone(tc_Nat_Onat)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1914,c_3894]) ).
cnf(c_22761,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Groups_Oone__class_Oone(tc_Nat_Onat) != A
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(copy,[status(thm)],[c_22760]) ).
cnf(c_5722,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Groups_Oone__class_Oone(tc_Nat_Onat) != A ),
inference(resolve,[status(thm)],[c_2856,c_22761]) ).
cnf(c_22762,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_4239,c_1909]) ).
cnf(c_22763,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2856,c_22762]) ).
cnf(c_5864,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_4234,c_22763]) ).
cnf(c_22764,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) ),
inference(paramod,[status(thm)],[c_4846,c_1394]) ).
cnf(c_5896,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_5864,c_22764]) ).
cnf(c_22765,plain,
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,A)
| ~ class_Orderings_Opreorder(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B) ),
inference(resolve,[status(thm)],[c_2183,c_1219]) ).
cnf(c_22766,plain,
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,A)
| ~ class_Orderings_Opreorder(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B) ),
inference(copy,[status(thm)],[c_22765]) ).
cnf(c_7054,plain,
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B) ),
inference(resolve,[status(thm)],[c_1765,c_22766]) ).
cnf(c_22767,plain,
( A = B
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_3359,c_1213]) ).
cnf(c_7240,plain,
( A = B
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_1810,c_22767]) ).
cnf(c_7344,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(A)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)) ),
inference(resolve,[status(thm)],[c_3454,c_1416]) ).
cnf(c_7870,plain,
c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_7054,c_5896]) ).
cnf(c_7940,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,A)),
inference(resolve,[status(thm)],[c_1925,c_2859]) ).
cnf(c_8035,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)),
inference(paramod,[status(thm)],[c_1491,c_7940]) ).
cnf(c_8068,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(A)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)),
inference(resolve,[status(thm)],[c_8035,c_7344]) ).
cnf(c_22768,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),B),A))
| ~ class_Rings_Olinordered__ring__strict(tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_2018,c_1170]) ).
cnf(c_8297,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),B),A)) ),
inference(resolve,[status(thm)],[c_1792,c_22768]) ).
cnf(c_22769,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),B),B)
| ~ class_Rings_Olinordered__ring__strict(tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_2018,c_1170]) ).
cnf(c_8298,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),B),B) ),
inference(resolve,[status(thm)],[c_1792,c_22769]) ).
cnf(c_22770,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) ),
inference(factor,[status(thm)],[c_8297]) ).
cnf(c_8415,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_3144,c_22770]) ).
cnf(c_22771,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(factor,[status(thm)],[c_8298]) ).
cnf(c_8416,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_3144,c_22771]) ).
cnf(c_22772,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))
| c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3111,c_1909]) ).
cnf(c_22773,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))
| c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2856,c_22772]) ).
cnf(c_8470,plain,
c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_2272,c_22773]) ).
cnf(c_22774,plain,
c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(paramod,[status(thm)],[c_8470,c_1403]) ).
cnf(c_8474,plain,
c_RComplete_Onatfloor(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(copy,[status(thm)],[c_22774]) ).
cnf(c_8494,plain,
c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),
inference(paramod,[status(thm)],[c_8474,c_3103]) ).
cnf(c_22775,plain,
( c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3706,c_1213]) ).
cnf(c_22776,plain,
( c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(copy,[status(thm)],[c_22775]) ).
cnf(c_8545,plain,
( c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(resolve,[status(thm)],[c_1810,c_22776]) ).
cnf(c_22777,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))),c_RComplete_Onatceiling(A))
| c_RComplete_Onatceiling(A) = c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)))
| ~ class_Orderings_Oorder(tc_Nat_Onat) ),
inference(resolve,[status(thm)],[c_4324,c_1909]) ).
cnf(c_22778,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))),c_RComplete_Onatceiling(A))
| c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))) = c_RComplete_Onatceiling(A)
| ~ class_Orderings_Oorder(tc_Nat_Onat) ),
inference(copy,[status(thm)],[c_22777]) ).
cnf(c_22779,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))),c_RComplete_Onatceiling(A))
| c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))) = c_RComplete_Onatceiling(A) ),
inference(resolve,[status(thm)],[c_2843,c_22778]) ).
cnf(c_8628,plain,
c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))) = c_RComplete_Onatceiling(A),
inference(resolve,[status(thm)],[c_4908,c_22779]) ).
cnf(c_8631,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(A))),
inference(paramod,[status(thm)],[c_8628,c_1405]) ).
cnf(c_22780,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),A),
inference(resolve,[status(thm)],[c_4379,c_1428]) ).
cnf(c_22781,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_RealDef_Oreal(tc_Nat_Onat,A))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),A),
inference(paramod,[status(thm)],[c_3175,c_22780]) ).
cnf(c_22782,plain,
A = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),A),
inference(paramod,[status(thm)],[c_4952,c_22781]) ).
cnf(c_22783,plain,
A = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),A),
inference(paramod,[status(thm)],[c_3175,c_22782]) ).
cnf(c_22784,plain,
A = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),
inference(paramod,[status(thm)],[c_8628,c_22783]) ).
cnf(c_8658,plain,
c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A) = A,
inference(copy,[status(thm)],[c_22784]) ).
cnf(c_8692,plain,
c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))) = A,
inference(paramod,[status(thm)],[c_8658,c_8494]) ).
cnf(c_8695,plain,
c_RComplete_Onatceiling(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))) = A,
inference(paramod,[status(thm)],[c_8658,c_3102]) ).
cnf(c_22785,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(A)))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_8068,c_1224]) ).
cnf(c_9101,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(A))),
inference(resolve,[status(thm)],[c_1810,c_22785]) ).
cnf(c_22786,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A) = A
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)
| c_RComplete_Onatfloor(A) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(resolve,[status(thm)],[c_3314,c_1058]) ).
cnf(c_10539,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A) = A
| c_RComplete_Onatfloor(A) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(resolve,[status(thm)],[c_1785,c_22786]) ).
cnf(c_11303,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)))),
inference(resolve,[status(thm)],[c_3488,c_1405]) ).
cnf(c_22787,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))),A)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_11303,c_1224]) ).
cnf(c_11330,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))),A),
inference(resolve,[status(thm)],[c_1810,c_22787]) ).
cnf(c_11363,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(paramod,[status(thm)],[c_3759,c_11330]) ).
cnf(c_11574,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r____),
inference(resolve,[status(thm)],[c_3822,c_7940]) ).
cnf(c_11580,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),v_r____),
inference(resolve,[status(thm)],[c_3822,c_1902]) ).
cnf(c_22788,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____) = v_r____
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_11574,c_1058]) ).
cnf(c_11682,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____) = v_r____,
inference(resolve,[status(thm)],[c_1785,c_22788]) ).
cnf(c_11706,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_r____),v_r____),
inference(paramod,[status(thm)],[c_11682,c_11580]) ).
cnf(c_22789,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r____,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_r____))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_11706,c_1224]) ).
cnf(c_12001,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r____,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_r____)),
inference(resolve,[status(thm)],[c_1810,c_22789]) ).
cnf(c_22790,plain,
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)
| A != c_Groups_Oone__class_Oone(tc_Nat_Onat)
| ~ class_Orderings_Oord(tc_Nat_Onat) ),
inference(resolve,[status(thm)],[c_1959,c_7870]) ).
cnf(c_22791,plain,
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)
| c_Groups_Oone__class_Oone(tc_Nat_Onat) != A
| ~ class_Orderings_Oord(tc_Nat_Onat) ),
inference(copy,[status(thm)],[c_22790]) ).
cnf(c_13262,plain,
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)
| c_Groups_Oone__class_Oone(tc_Nat_Onat) != A ),
inference(resolve,[status(thm)],[c_2844,c_22791]) ).
cnf(c_22792,plain,
A = c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)),
inference(copy,[status(thm)],[c_1403]) ).
cnf(c_22793,plain,
c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),
inference(resolve,[status(thm)],[c_13262,c_22792]) ).
cnf(c_13522,plain,
c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(paramod,[status(thm)],[c_2289,c_22793]) ).
cnf(c_22794,plain,
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Olinorder(tc_Nat_Onat) ),
inference(resolve,[status(thm)],[c_13522,c_1136]) ).
cnf(c_22795,plain,
( c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ class_Orderings_Olinorder(tc_Nat_Onat) ),
inference(copy,[status(thm)],[c_22794]) ).
cnf(c_13540,plain,
c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(resolve,[status(thm)],[c_1766,c_22795]) ).
cnf(c_22796,plain,
A = c_RComplete_Onatfloor(c_RealDef_Oreal(tc_Nat_Onat,A)),
inference(copy,[status(thm)],[c_1402]) ).
cnf(c_22797,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatfloor(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat))),c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_5720,c_22796]) ).
cnf(c_15057,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(paramod,[status(thm)],[c_2289,c_22797]) ).
cnf(c_22798,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_15057,c_1909]) ).
cnf(c_15064,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(resolve,[status(thm)],[c_2856,c_22798]) ).
cnf(c_22799,plain,
A = c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)),
inference(copy,[status(thm)],[c_1403]) ).
cnf(c_22800,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat))),c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_5722,c_22799]) ).
cnf(c_15088,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(paramod,[status(thm)],[c_2289,c_22800]) ).
cnf(c_15089,plain,
c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_15088,c_15064]) ).
cnf(c_22801,plain,
( c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatfloor(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(paramod,[status(thm)],[c_15089,c_8545]) ).
cnf(c_22802,plain,
( c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(paramod,[status(thm)],[c_15089,c_22801]) ).
cnf(c_15125,plain,
c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_11363,c_22802]) ).
cnf(c_22803,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(A)),c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A)))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_8631,c_1224]) ).
cnf(c_16166,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(A)),c_RComplete_Onatceiling(c_RealDef_Oreal(tc_Nat_Onat,A))),
inference(resolve,[status(thm)],[c_1810,c_22803]) ).
cnf(c_16184,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(A)),A),
inference(paramod,[status(thm)],[c_1403,c_16166]) ).
cnf(c_16408,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))),c_RealDef_Oreal(tc_Nat_Onat,A)),
inference(paramod,[status(thm)],[c_8692,c_9101]) ).
cnf(c_16414,plain,
c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(paramod,[status(thm)],[c_15125,c_8692]) ).
cnf(c_16454,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,A),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,A))),
inference(paramod,[status(thm)],[c_8695,c_16184]) ).
cnf(c_22804,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
inference(paramod,[status(thm)],[c_15125,c_16454]) ).
cnf(c_17030,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(paramod,[status(thm)],[c_15125,c_22804]) ).
cnf(c_22805,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_RealDef_Oreal(tc_Nat_Onat,c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(paramod,[status(thm)],[c_15125,c_16408]) ).
cnf(c_18894,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(paramod,[status(thm)],[c_15125,c_22805]) ).
cnf(c_22806,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| c_RComplete_Onatfloor(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(paramod,[status(thm)],[c_10539,c_18894]) ).
cnf(c_22807,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| c_RComplete_Onatceiling(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(paramod,[status(thm)],[c_16414,c_22806]) ).
cnf(c_19058,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_13540,c_22807]) ).
cnf(c_21554,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A)),
inference(paramod,[status(thm)],[c_2067,c_8415]) ).
cnf(c_21555,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(paramod,[status(thm)],[c_2067,c_8416]) ).
cnf(c_22808,plain,
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A)) ),
inference(resolve,[status(thm)],[c_7240,c_21555]) ).
cnf(c_22494,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_21554,c_22808]) ).
cnf(c_22809,plain,
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) ),
inference(resolve,[status(thm)],[c_7240,c_19058]) ).
cnf(c_22500,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_17030,c_22809]) ).
cnf(c_22810,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A),
inference(paramod,[status(thm)],[c_22500,c_2019]) ).
cnf(c_22811,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A),
inference(paramod,[status(thm)],[c_22494,c_22810]) ).
cnf(c_22812,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A),
inference(paramod,[status(thm)],[c_2018,c_22811]) ).
cnf(c_22661,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) = A,
inference(paramod,[status(thm)],[c_2018,c_22812]) ).
cnf(c_22737,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),A)),
inference(paramod,[status(thm)],[c_22661,c_3858]) ).
cnf(c_22738,plain,
$false,
inference(resolve,[status(thm)],[c_22737,c_12001]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW233+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n020.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 15:31:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 1900614 was started by sandbox on n020,
% 0.09/0.37 % Sat Sep 26 15:31:04 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.20/0.50
% 0.20/0.50 % From the command line: assign(max_seconds, 300).
% 0.20/0.50
% 0.20/0.50 % SInE: 716 to sos, 544 to usable, of 1260 axioms (tolerance 2.00, depth 0 fixpoint).
% 74.87/11.06
% 74.87/11.06 % given #500 (F,wt=10): 11567 -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),v_r____)). [back_unit_del(11523),unit_del(a,11546)].
% 74.87/11.06
% 74.87/11.06 % given #1000 (W,wt=10): 10758 c_RComplete_Onatceiling(A) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) | -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)). [resolve(3317,a,1224,c),unit_del(b,1810)].
% 74.87/11.06
% 74.87/11.06 % given #1500 (F,wt=14): 18888 -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Transcendental_Oln(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),v_r____),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))). [para(17515(a,1),13518(a,2,2)),rewrite([2279(5)])].
% 74.87/11.06
% 74.87/11.06 % SZS status Theorem for theBenchmark
% 74.87/11.06
% 74.87/11.06 % Proof 1 at 8.53 (+ 1.42) seconds.
% 74.87/11.06 % Length of proof is 188.
% 74.87/11.06 % Level of proof is 17.
% 74.87/11.06 % Maximum clause weight is 313.000.
% 74.87/11.06 % Given clauses 1823.
% 74.87/11.06
% 74.87/11.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------