%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG372-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 18:03:30 EDT 2022
% Result : Unsatisfiable 2.84s 3.06s
% Output : Refutation 2.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 126
% Syntax : Number of clauses : 159 ( 129 unt; 3 nHn; 159 RR)
% Number of literals : 194 ( 0 equ; 46 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 76 ( 75 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(116,axiom,
( ~ class_OrderedGroup_Opordered__ab__group__add__abs(u)
| equal(c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(u),u),c_HOL_Ozero__class_Ozero(u)) ),
file('ALG372-1.p',unknown),
[] ).
cnf(132,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| equal(c_HOL_Oplus__class_Oplus(v,c_HOL_Ozero__class_Ozero(u),u),v) ),
file('ALG372-1.p',unknown),
[] ).
cnf(155,axiom,
( ~ class_Lattices_Oupper__semilattice(u)
| equal(c_Lattices_Oupper__semilattice__class_Osup(v,v,u),v) ),
file('ALG372-1.p',unknown),
[] ).
cnf(298,axiom,
( ~ class_Lattices_Oupper__semilattice(u)
| c_lessequals(v,c_Lattices_Oupper__semilattice__class_Osup(v,w,u),u) ),
file('ALG372-1.p',unknown),
[] ).
cnf(315,axiom,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(v,w,u)
| equal(v,w)
| c_HOL_Oord__class_Oless(v,w,u) ),
file('ALG372-1.p',unknown),
[] ).
cnf(338,axiom,
( ~ class_Orderings_Opreorder(u)
| ~ c_HOL_Oord__class_Oless(v,w,u)
| ~ c_lessequals(w,v,u) ),
file('ALG372-1.p',unknown),
[] ).
cnf(415,axiom,
( ~ class_Int_Onumber__ring(u)
| equal(c_HOL_Oplus__class_Oplus(v,c_HOL_Ouminus__class_Ouminus(w,u),u),c_HOL_Ominus__class_Ominus(v,w,u)) ),
file('ALG372-1.p',unknown),
[] ).
cnf(460,axiom,
( ~ class_OrderedGroup_Opordered__ab__group__add__abs(u)
| equal(c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(v,u),u),c_HOL_Oabs__class_Oabs(v,u)) ),
file('ALG372-1.p',unknown),
[] ).
cnf(481,axiom,
( ~ class_OrderedGroup_Oab__group__add(u)
| equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(v,w,u),u),c_HOL_Ominus__class_Ominus(w,v,u)) ),
file('ALG372-1.p',unknown),
[] ).
cnf(486,axiom,
( ~ c_lessequals(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal)
| c_lessequals(u,v,tc_RealDef_Oreal) ),
file('ALG372-1.p',unknown),
[] ).
cnf(664,axiom,
( ~ class_OrderedGroup_Opordered__ab__group__add(u)
| ~ c_HOL_Oord__class_Oless(v,c_HOL_Ozero__class_Ozero(u),u)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(u),c_HOL_Ouminus__class_Ouminus(v,u),u) ),
file('ALG372-1.p',unknown),
[] ).
cnf(684,axiom,
( ~ class_RealVector_Oreal__normed__vector(u)
| equal(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(u),u),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
file('ALG372-1.p',unknown),
[] ).
cnf(728,axiom,
c_lessequals(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(u,tc_Complex_Ocomplex),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(u,tc_Complex_Ocomplex),tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(753,axiom,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(756,axiom,
class_OrderedGroup_Ocancel__comm__monoid__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(757,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(758,axiom,
class_OrderedGroup_Ocancel__comm__monoid__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(759,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(797,axiom,
class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(798,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(799,axiom,
class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(800,axiom,
class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(801,axiom,
class_OrderedGroup_Olordered__ab__group__add__meet(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(802,axiom,
class_OrderedGroup_Olordered__ab__group__add__join(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(803,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(804,axiom,
class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(805,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(806,axiom,
class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(807,axiom,
class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(808,axiom,
class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(809,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(810,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(811,axiom,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(812,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(813,axiom,
class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(814,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(815,axiom,
class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(816,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(817,axiom,
class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(818,axiom,
class_Ring__and__Field_Opordered__ring__abs(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(819,axiom,
class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(820,axiom,
class_Ring__and__Field_Oordered__semiring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(821,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(822,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(823,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(824,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(825,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(826,axiom,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(827,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(828,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(829,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(830,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(831,axiom,
class_Ring__and__Field_Opordered__ring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(832,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(833,axiom,
class_Ring__and__Field_Olordered__ring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(834,axiom,
class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(835,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(836,axiom,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(837,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(838,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(839,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(840,axiom,
class_Lattices_Oupper__semilattice(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(841,axiom,
class_Lattices_Olower__semilattice(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(842,axiom,
class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(843,axiom,
class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(844,axiom,
class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(845,axiom,
class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(846,axiom,
class_Ring__and__Field_Omult__mono(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(847,axiom,
class_Ring__and__Field_Ocomm__ring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(848,axiom,
class_OrderedGroup_Omonoid__mult(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(849,axiom,
class_Lattices_Odistrib__lattice(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(850,axiom,
class_Ring__and__Field_Osemiring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(851,axiom,
class_RealVector_Oreal__algebra(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(852,axiom,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(853,axiom,
class_RealVector_Oreal__vector(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(854,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(855,axiom,
class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(856,axiom,
class_RealVector_Oreal__field(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(857,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(858,axiom,
class_Ring__and__Field_Oring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(859,axiom,
class_Ring__and__Field_Oidom(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(860,axiom,
class_Nat_Osemiring__char__0(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(861,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(862,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(863,axiom,
class_Lattices_Olattice(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(864,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(865,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(866,axiom,
class_Power_Opower(tc_RealDef_Oreal),
file('ALG372-1.p',unknown),
[] ).
cnf(867,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(868,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(869,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(870,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(871,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(872,axiom,
class_RealVector_Oreal__normed__algebra__1(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(873,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(874,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(875,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(876,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(877,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(878,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(879,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(880,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(881,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(882,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(883,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(884,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(885,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(886,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(887,axiom,
class_RealVector_Oreal__algebra__1(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(888,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(889,axiom,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(890,axiom,
class_Ring__and__Field_Ocomm__ring(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(891,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(892,axiom,
class_Ring__and__Field_Osemiring(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(893,axiom,
class_RealVector_Oreal__algebra(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(894,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(895,axiom,
class_RealVector_Oreal__vector(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(896,axiom,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(897,axiom,
class_RealVector_Oreal__field(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(898,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(899,axiom,
class_Ring__and__Field_Oring(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(900,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(901,axiom,
class_Nat_Osemiring__char__0(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(902,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(903,axiom,
class_Power_Opower(tc_Complex_Ocomplex),
file('ALG372-1.p',unknown),
[] ).
cnf(952,axiom,
( ~ equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
file('ALG372-1.p',unknown),
[] ).
cnf(1007,plain,
( ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(spr,[status(thm),theory(equality)],[684,728]),
[iquote('0:SpR:684.1,728.0')] ).
cnf(1012,plain,
c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[1007,897,872,870,893,867,903,901,892,891,886,883,881,880,878,869,757,894,890,873,871,868,889,756,899,887,884,876,902,895,877,882,885,900,888,879,896,875,898,874]),
[iquote('0:SSi:1007.0,897.0,872.0,870.0,893.0,867.0,903.0,901.0,892.0,891.0,886.0,883.0,881.0,880.0,878.0,869.0,757.0,894.0,890.0,873.0,871.0,868.0,889.0,756.0,899.0,887.0,884.0,876.0,902.0,895.0,877.0,882.0,885.0,900.0,888.0,879.0,896.0,875.0,898.0,874.0')] ).
cnf(1096,plain,
( ~ class_Lattices_Oupper__semilattice(tc_RealDef_Oreal)
| c_lessequals(u,c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[298,486]),
[iquote('0:Res:298.1,486.0')] ).
cnf(1101,plain,
c_lessequals(u,c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[1096,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:1096.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(1482,plain,
( ~ class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)
| c_lessequals(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(spr,[status(thm),theory(equality)],[460,1101]),
[iquote('0:SpR:460.1,1101.0')] ).
cnf(1504,plain,
c_lessequals(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[1482,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:1482.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(1710,plain,
( ~ class_Lattices_Oupper__semilattice(tc_RealDef_Oreal)
| c_lessequals(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(spr,[status(thm),theory(equality)],[155,1504]),
[iquote('0:SpR:155.1,1504.0')] ).
cnf(1715,plain,
c_lessequals(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[1710,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:1710.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(3892,plain,
( ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[1715,338]),
[iquote('0:Res:1715.0,338.2')] ).
cnf(3983,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[3892,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:3892.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(4255,plain,
( ~ class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(spl,[status(thm),theory(equality)],[460,3983]),
[iquote('0:SpL:460.1,3983.0')] ).
cnf(4260,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[4255,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:4255.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(5992,plain,
( ~ class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(spl,[status(thm),theory(equality)],[116,4260]),
[iquote('0:SpL:116.1,4260.0')] ).
cnf(7724,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[5992,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:5992.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(11030,plain,
( ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[1012,315]),
[iquote('0:Res:1012.0,315.1')] ).
cnf(11128,plain,
( equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(ssi,[status(thm)],[11030,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:11030.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(14180,plain,
( ~ class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[664,7724]),
[iquote('0:Res:664.2,7724.0')] ).
cnf(14188,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[14180,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:14180.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(14189,plain,
equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(mrr,[status(thm)],[11128,14188]),
[iquote('0:MRR:11128.1,14188.0')] ).
cnf(14320,plain,
( ~ class_Int_Onumber__ring(tc_RealDef_Oreal)
| equal(c_HOL_Oplus__class_Oplus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[14189,415]),
[iquote('0:SpR:14189.0,415.1')] ).
cnf(14350,plain,
equal(c_HOL_Oplus__class_Oplus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[14320,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:14320.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(14544,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal)
| equal(c_HOL_Ominus__class_Ominus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),u) ),
inference(spr,[status(thm),theory(equality)],[14350,132]),
[iquote('0:SpR:14350.0,132.1')] ).
cnf(14556,plain,
equal(c_HOL_Ominus__class_Ominus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(ssi,[status(thm)],[14544,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:14544.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(14576,plain,
( ~ class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)
| equal(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[14556,481]),
[iquote('0:SpR:14556.0,481.1')] ).
cnf(14582,plain,
equal(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[14576,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:14576.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(14662,plain,
( ~ class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)
| equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[14582,481]),
[iquote('0:SpR:14582.0,481.1')] ).
cnf(14669,plain,
( ~ class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)
| equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal),u) ),
inference(rew,[status(thm),theory(equality)],[14556,14662]),
[iquote('0:Rew:14556.0,14662.1')] ).
cnf(14670,plain,
equal(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(u,tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(ssi,[status(thm)],[14669,833,856,819,812,802,801,855,851,842,803,799,866,860,850,848,846,838,835,830,829,827,820,817,810,807,759,852,849,847,821,818,816,809,805,800,845,758,858,843,836,815,797,825,823,865,864,861,853,862,831,826,808,834,798,837,863,859,844,828,804,841,840,854,813,824,857,806,814,811,839,822,832]),
[iquote('0:SSi:14669.0,833.0,856.0,819.0,812.0,802.0,801.0,855.0,851.0,842.0,803.0,799.0,866.0,860.0,850.0,848.0,846.0,838.0,835.0,830.0,829.0,827.0,820.0,817.0,810.0,807.0,759.0,852.0,849.0,847.0,821.0,818.0,816.0,809.0,805.0,800.0,845.0,758.0,858.0,843.0,836.0,815.0,797.0,825.0,823.0,865.0,864.0,861.0,853.0,862.0,831.0,826.0,808.0,834.0,798.0,837.0,863.0,859.0,844.0,828.0,804.0,841.0,840.0,854.0,813.0,824.0,857.0,806.0,814.0,811.0,839.0,822.0,832.0')] ).
cnf(14679,plain,
( ~ equal(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
inference(rew,[status(thm),theory(equality)],[14670,952]),
[iquote('0:Rew:14670.0,952.0')] ).
cnf(14701,plain,
~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal),
inference(obv,[status(thm),theory(equality)],[14679]),
[iquote('0:Obv:14679.0')] ).
cnf(14796,plain,
( ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(spl,[status(thm),theory(equality)],[684,14701]),
[iquote('0:SpL:684.1,14701.0')] ).
cnf(14806,plain,
~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal),
inference(ssi,[status(thm)],[14796,897,872,870,893,867,903,901,892,891,886,883,881,880,878,869,757,894,890,873,871,868,889,756,899,887,884,876,902,895,877,882,885,900,888,879,896,875,898,874]),
[iquote('0:SSi:14796.0,897.0,872.0,870.0,893.0,867.0,903.0,901.0,892.0,891.0,886.0,883.0,881.0,880.0,878.0,869.0,757.0,894.0,890.0,873.0,871.0,868.0,889.0,756.0,899.0,887.0,884.0,876.0,902.0,895.0,877.0,882.0,885.0,900.0,888.0,879.0,896.0,875.0,898.0,874.0')] ).
cnf(14807,plain,
$false,
inference(mrr,[status(thm)],[14806,753]),
[iquote('0:MRR:14806.0,753.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG372-1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Thu Jun 9 06:01:19 EDT 2022
% 0.13/0.35 % CPUTime :
% 2.84/3.06
% 2.84/3.06 SPASS V 3.9
% 2.84/3.06 SPASS beiseite: Proof found.
% 2.84/3.06 % SZS status Theorem
% 2.84/3.06 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.84/3.06 SPASS derived 11237 clauses, backtracked 185 clauses, performed 2 splits and kept 3775 clauses.
% 2.84/3.06 SPASS allocated 87418 KBytes.
% 2.84/3.06 SPASS spent 0:00:02.68 on the problem.
% 2.84/3.06 0:00:00.07 for the input.
% 2.84/3.06 0:00:00.00 for the FLOTTER CNF translation.
% 2.84/3.06 0:00:00.13 for inferences.
% 2.84/3.06 0:00:00.05 for the backtracking.
% 2.84/3.06 0:00:02.30 for the reduction.
% 2.84/3.06
% 2.84/3.06
% 2.84/3.06 Here is a proof with depth 7, length 159 :
% 2.84/3.06 % SZS output start Refutation
% See solution above
% 2.93/3.13 Formulae used in the proof : cls_abs__eq__0_1 cls_class__semiring_Osemiring__rules_I6_J_0 cls_sup__idem_0 cls_sup__ge1_0 cls_order__less__le_2 cls_less__le__not__le_1 cls_class__ring_Osub__add_0 cls_abs__minus__cancel_0 cls_minus__diff__eq_0 cls_abs__le__interval__iff_1 cls_neg__0__less__iff__less_1 cls_norm__zero_0 cls_complex__mod__minus__le__complex__mod_0 cls_CHAINED_0 clsarity_Complex__Ocomplex__OrderedGroup_Ocancel__comm__monoid__add clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__ring__1 clsarity_RealDef__Oreal__OrderedGroup_Ocancel__comm__monoid__add clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__ring__1 clsarity_RealDef__Oreal__OrderedGroup_Opordered__cancel__ab__semigroup__add clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__semigroup__add__imp__le clsarity_RealDef__Oreal__Ring__and__Field_Oordered__comm__semiring__strict clsarity_RealDef__Oreal__Ring__and__Field_Opordered__cancel__semiring clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add__meet clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add__join clsarity_RealDef__Oreal__Ring__and__Field_Oring__1__no__zero__divisors clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semiring__strict clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__semigroup__add clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add__abs clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add__abs clsarity_RealDef__Oreal__OrderedGroup_Opordered__comm__monoid__add clsarity_RealDef__Oreal__Ring__and__Field_Oring__no__zero__divisors clsarity_RealDef__Oreal__OrderedGroup_Ocancel__ab__semigroup__add clsarity_RealDef__Oreal__Ring__and__Field_Oordered__ring__strict clsarity_RealDef__Oreal__RealVector_Oreal__normed__div__algebra clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add clsarity_RealDef__Oreal__OrderedGroup_Oordered__ab__group__add clsarity_RealDef__Oreal__OrderedGroup_Ocancel__semigroup__add clsarity_RealDef__Oreal__Ring__and__Field_Opordered__semiring clsarity_RealDef__Oreal__Ring__and__Field_Opordered__ring__abs clsarity_RealDef__Oreal__RealVector_Oreal__normed__algebra__1 clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semiring clsarity_RealDef__Oreal__Ring__and__Field_Ono__zero__divisors clsarity_RealDef__Oreal__Ring__and__Field_Odivision__by__zero clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semidom clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1 clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__0 clsarity_RealDef__Oreal__RealVector_Oreal__normed__algebra clsarity_RealDef__Oreal__OrderedGroup_Oab__semigroup__mult clsarity_RealDef__Oreal__RealVector_Oreal__normed__vector clsarity_RealDef__Oreal__OrderedGroup_Ocomm__monoid__mult clsarity_RealDef__Oreal__OrderedGroup_Oab__semigroup__add clsarity_RealDef__Oreal__Ring__and__Field_Opordered__ring clsarity_RealDef__Oreal__Ring__and__Field_Oordered__field clsarity_RealDef__Oreal__Ring__and__Field_Olordered__ring clsarity_RealDef__Oreal__Ring__and__Field_Odivision__ring clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring clsarity_RealDef__Oreal__RealVector_Oreal__normed__field clsarity_RealDef__Oreal__OrderedGroup_Ocomm__monoid__add clsarity_RealDef__Oreal__Ring__and__Field_Ozero__neq__one clsarity_RealDef__Oreal__Ring__and__Field_Oordered__idom clsarity_RealDef__Oreal__Lattices_Oupper__semilattice clsarity_RealDef__Oreal__Lattices_Olower__semilattice clsarity_RealDef__Oreal__Ring__and__Field_Omult__mono1 clsarity_RealDef__Oreal__RealVector_Oreal__algebra__1 clsarity_RealDef__Oreal__OrderedGroup_Oab__group__add clsarity_RealDef__Oreal__Ring__and__Field_Omult__zero clsarity_RealDef__Oreal__Ring__and__Field_Omult__mono clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__ring clsarity_RealDef__Oreal__OrderedGroup_Omonoid__mult clsarity_RealDef__Oreal__Lattices_Odistrib__lattice clsarity_RealDef__Oreal__Ring__and__Field_Osemiring clsarity_RealDef__Oreal__RealVector_Oreal__algebra clsarity_RealDef__Oreal__OrderedGroup_Omonoid__add clsarity_RealDef__Oreal__RealVector_Oreal__vector clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add clsarity_RealDef__Oreal__Ring__and__Field_Oabs__if clsarity_RealDef__Oreal__RealVector_Oreal__field clsarity_RealDef__Oreal__Ring__and__Field_Ofield clsarity_RealDef__Oreal__Ring__and__Field_Oring clsarity_RealDef__Oreal__Ring__and__Field_Oidom clsarity_RealDef__Oreal__Nat_Osemiring__char__0 clsarity_RealDef__Oreal__Orderings_Opreorder clsarity_RealDef__Oreal__Orderings_Olinorder clsarity_RealDef__Oreal__Lattices_Olattice clsarity_RealDef__Oreal__Orderings_Oorder clsarity_RealDef__Oreal__Int_Onumber__ring clsarity_RealDef__Oreal__Power_Opower clsarity_Complex__Ocomplex__Ring__and__Field_Oring__1__no__zero__divisors clsarity_Complex__Ocomplex__Ring__and__Field_Oring__no__zero__divisors clsarity_Complex__Ocomplex__OrderedGroup_Ocancel__ab__semigroup__add clsarity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra clsarity_Complex__Ocomplex__OrderedGroup_Ocancel__semigroup__add clsarity_Complex__Ocomplex__RealVector_Oreal__normed__algebra__1 clsarity_Complex__Ocomplex__Ring__and__Field_Ono__zero__divisors clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1 clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0 clsarity_Complex__Ocomplex__RealVector_Oreal__normed__algebra clsarity_Complex__Ocomplex__OrderedGroup_Oab__semigroup__mult clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__mult clsarity_Complex__Ocomplex__OrderedGroup_Oab__semigroup__add clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__ring clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring clsarity_Complex__Ocomplex__RealVector_Oreal__normed__field clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__add clsarity_Complex__Ocomplex__Ring__and__Field_Ozero__neq__one clsarity_Complex__Ocomplex__RealVector_Oreal__algebra__1 clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add clsarity_Complex__Ocomplex__Ring__and__Field_Omult__zero clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__ring clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult clsarity_Complex__Ocomplex__Ring__and__Field_Osemiring clsarity_Complex__Ocomplex__RealVector_Oreal__algebra clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add clsarity_Complex__Ocomplex__RealVector_Oreal__vector clsarity_Complex__Ocomplex__OrderedGroup_Ogroup__add clsarity_Complex__Ocomplex__RealVector_Oreal__field clsarity_Complex__Ocomplex__Ring__and__Field_Ofield clsarity_Complex__Ocomplex__Ring__and__Field_Oring clsarity_Complex__Ocomplex__Ring__and__Field_Oidom clsarity_Complex__Ocomplex__Nat_Osemiring__char__0 clsarity_Complex__Ocomplex__Int_Onumber__ring clsarity_Complex__Ocomplex__Power_Opower cls_conjecture_0
% 2.93/3.13
%------------------------------------------------------------------------------