%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG340-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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:24 EDT 2022
% Result : Unsatisfiable 15.07s 15.29s
% Output : Refutation 15.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 90
% Syntax : Number of clauses : 105 ( 88 unt; 6 nHn; 105 RR)
% Number of literals : 131 ( 0 equ; 25 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 55 ( 54 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(214,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(u),tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(360,axiom,
( ~ c_lessequals(u,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(u,c_RealDef_Oreal__of__preal(v),tc_RealDef_Oreal) ),
file('ALG340-1.p',unknown),
[] ).
cnf(368,axiom,
( c_lessequals(u,v,tc_RealDef_Oreal)
| c_lessequals(v,u,tc_RealDef_Oreal) ),
file('ALG340-1.p',unknown),
[] ).
cnf(376,axiom,
( ~ class_Orderings_Opreorder(u)
| ~ c_HOL_Oord__class_Oless(v,w,u)
| ~ c_lessequals(w,x,u)
| c_HOL_Oord__class_Oless(v,x,u) ),
file('ALG340-1.p',unknown),
[] ).
cnf(378,axiom,
c_lessequals(u,u,tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(379,axiom,
( ~ c_lessequals(u,v,tc_RealDef_Oreal)
| ~ c_lessequals(v,w,tc_RealDef_Oreal)
| c_lessequals(u,w,tc_RealDef_Oreal) ),
file('ALG340-1.p',unknown),
[] ).
cnf(387,axiom,
~ c_HOL_Oord__class_Oless(u,u,tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(392,axiom,
( ~ class_Ring__and__Field_Oidom(u)
| equal(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(u)),v,u),c_HOL_Ozero__class_Ozero(u)) ),
file('ALG340-1.p',unknown),
[] ).
cnf(426,axiom,
( ~ class_Orderings_Olinorder(u)
| c_lessequals(v,w,u)
| c_HOL_Oord__class_Oless(w,v,u) ),
file('ALG340-1.p',unknown),
[] ).
cnf(430,axiom,
class_OrderedGroup_Ocancel__comm__monoid__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(431,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(432,axiom,
class_OrderedGroup_Ocancel__comm__monoid__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(433,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(434,axiom,
class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(435,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(436,axiom,
class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(437,axiom,
class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(438,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(439,axiom,
class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(440,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(441,axiom,
class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(442,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(443,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(444,axiom,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(445,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(446,axiom,
class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(447,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(448,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(449,axiom,
class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(450,axiom,
class_Ring__and__Field_Oordered__semiring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(451,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(452,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(453,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(454,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(455,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(456,axiom,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(457,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(458,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(459,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(460,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(461,axiom,
class_Ring__and__Field_Opordered__ring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(462,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(463,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(464,axiom,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(465,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(466,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(467,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(468,axiom,
class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(469,axiom,
class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(470,axiom,
class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(471,axiom,
class_Ring__and__Field_Omult__mono(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(472,axiom,
class_OrderedGroup_Omonoid__mult(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(473,axiom,
class_Ring__and__Field_Osemiring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(474,axiom,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(475,axiom,
class_Ring__and__Field_Osgn__if(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(476,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(477,axiom,
class_Ring__and__Field_Oidom(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(478,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(479,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(480,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(481,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(482,axiom,
class_Power_Opower(tc_RealDef_Oreal),
file('ALG340-1.p',unknown),
[] ).
cnf(483,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(484,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(485,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(486,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(487,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(488,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(489,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(490,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(491,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(492,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(493,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(494,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(495,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(496,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(497,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(498,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(499,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(500,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(501,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(502,axiom,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(503,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(504,axiom,
class_Ring__and__Field_Osemiring(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(505,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(506,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(507,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(508,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(509,axiom,
class_Power_Opower(tc_Complex_Ocomplex),
file('ALG340-1.p',unknown),
[] ).
cnf(552,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(u),tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_RealDef_Oreal) ),
file('ALG340-1.p',unknown),
[] ).
cnf(625,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(u,c_RealDef_Oreal__of__preal(v),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[368,360]),
[iquote('0:Res:368.1,360.0')] ).
cnf(632,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(u),tc_RealDef_Oreal),
inference(res,[status(thm),theory(equality)],[625,387]),
[iquote('0:Res:625.1,387.0')] ).
cnf(1143,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| ~ c_lessequals(u,v,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(u,w,tc_RealDef_Oreal)
| c_lessequals(w,v,tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[426,379]),
[iquote('0:Res:426.1,379.0')] ).
cnf(1146,plain,
( ~ c_lessequals(u,v,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(u,w,tc_RealDef_Oreal)
| c_lessequals(w,v,tc_RealDef_Oreal) ),
inference(ssi,[status(thm)],[1143,475,468,446,436,482,473,472,471,466,464,463,460,459,457,450,449,445,443,438,474,451,448,440,437,433,470,469,461,442,432,453,434,456,481,479,455,458,447,480,478,441,477,435,465,439,476,454,467,444,452,462]),
[iquote('0:SSi:1143.0,475.0,468.0,446.0,436.0,482.0,473.0,472.0,471.0,466.0,464.0,463.0,460.0,459.0,457.0,450.0,449.0,445.0,443.0,438.0,474.0,451.0,448.0,440.0,437.0,433.0,470.0,469.0,461.0,442.0,432.0,453.0,434.0,456.0,481.0,479.0,455.0,458.0,447.0,480.0,478.0,441.0,477.0,435.0,465.0,439.0,476.0,454.0,467.0,444.0,452.0,462.0')] ).
cnf(1640,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal)
| c_lessequals(u,c_RealDef_Oreal__of__preal(v),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[632,1146]),
[iquote('0:Res:632.0,1146.0')] ).
cnf(27309,plain,
( ~ class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_RealDef_Oreal) ),
inference(spl,[status(thm),theory(equality)],[392,552]),
[iquote('0:SpL:392.1,552.1')] ).
cnf(27323,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(u),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(c_RealDef_Oreal__of__preal(u)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[1640,552]),
[iquote('0:Res:1640.1,552.1')] ).
cnf(27345,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_RealDef_Oreal) ),
inference(ssi,[status(thm)],[27309,509,504,503,500,498,497,496,495,493,486,485,483,505,488,487,431,502,501,484,430,492,508,491,494,507,499,506,490,489]),
[iquote('0:SSi:27309.0,509.0,504.0,503.0,500.0,498.0,497.0,496.0,495.0,493.0,486.0,485.0,483.0,505.0,488.0,487.0,431.0,502.0,501.0,484.0,430.0,492.0,508.0,491.0,494.0,507.0,499.0,506.0,490.0,489.0')] ).
cnf(27349,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(c_RealDef_Oreal__of__preal(u)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(mrr,[status(thm)],[27323,214]),
[iquote('0:MRR:27323.0,214.0')] ).
cnf(43675,plain,
( ~ class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(spr,[status(thm),theory(equality)],[392,27349]),
[iquote('0:SpR:392.1,27349.0')] ).
cnf(43693,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[43675,509,504,503,500,498,497,496,495,493,486,485,483,505,488,487,431,502,501,484,430,492,508,491,494,507,499,506,490,489]),
[iquote('0:SSi:43675.0,509.0,504.0,503.0,500.0,498.0,497.0,496.0,495.0,493.0,486.0,485.0,483.0,505.0,488.0,487.0,431.0,502.0,501.0,484.0,430.0,492.0,508.0,491.0,494.0,507.0,499.0,506.0,490.0,489.0')] ).
cnf(43715,plain,
( ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[43693,376]),
[iquote('0:Res:43693.0,376.1')] ).
cnf(43722,plain,
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal) ),
inference(ssi,[status(thm)],[43715,475,468,446,436,482,473,472,471,466,464,463,460,459,457,450,449,445,443,438,474,451,448,440,437,433,470,469,461,442,432,453,434,456,481,479,455,458,447,480,478,441,477,435,465,439,476,454,467,444,452,462]),
[iquote('0:SSi:43715.0,475.0,468.0,446.0,436.0,482.0,473.0,472.0,471.0,466.0,464.0,463.0,460.0,459.0,457.0,450.0,449.0,445.0,443.0,438.0,474.0,451.0,448.0,440.0,437.0,433.0,470.0,469.0,461.0,442.0,432.0,453.0,434.0,456.0,481.0,479.0,455.0,458.0,447.0,480.0,478.0,441.0,477.0,435.0,465.0,439.0,476.0,454.0,467.0,444.0,452.0,462.0')] ).
cnf(43723,plain,
~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),u,tc_RealDef_Oreal),
inference(mrr,[status(thm)],[43722,27345]),
[iquote('0:MRR:43722.1,27345.0')] ).
cnf(43724,plain,
$false,
inference(unc,[status(thm)],[43723,378]),
[iquote('0:UnC:43723.0,378.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.08 % Problem : ALG340-1 : TPTP v8.1.0. Released v4.1.0.
% 0.04/0.09 % Command : run_spass %d %s
% 0.09/0.28 % Computer : n024.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 600
% 0.09/0.28 % DateTime : Wed Jun 8 19:17:49 EDT 2022
% 0.09/0.29 % CPUTime :
% 15.07/15.29
% 15.07/15.29 SPASS V 3.9
% 15.07/15.29 SPASS beiseite: Proof found.
% 15.07/15.29 % SZS status Theorem
% 15.07/15.29 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.07/15.29 SPASS derived 36219 clauses, backtracked 1194 clauses, performed 4 splits and kept 9492 clauses.
% 15.07/15.29 SPASS allocated 105110 KBytes.
% 15.07/15.29 SPASS spent 0:0:14.95 on the problem.
% 15.07/15.29 0:00:00.04 for the input.
% 15.07/15.29 0:00:00.00 for the FLOTTER CNF translation.
% 15.07/15.29 0:00:00.49 for inferences.
% 15.07/15.29 0:00:00.69 for the backtracking.
% 15.07/15.29 0:0:13.56 for the reduction.
% 15.07/15.29
% 15.07/15.29
% 15.07/15.29 Here is a proof with depth 6, length 105 :
% 15.07/15.29 % SZS output start Refutation
% See solution above
% 15.07/15.29 Formulae used in the proof : cls_real__gt__zero__preal__Ex_1 cls_real__less__all__preal_0 cls_real__le__linear_0 cls_order__less__le__trans_0 cls_real__le__refl_0 cls_real__le__trans_0 cls_real__less__def_1 cls_order__root_1 cls_linorder__not__le_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__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__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_Ocancel__semigroup__add clsarity_RealDef__Oreal__Ring__and__Field_Opordered__semiring 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_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__Ring__and__Field_Omult__mono1 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__OrderedGroup_Omonoid__mult clsarity_RealDef__Oreal__Ring__and__Field_Osemiring clsarity_RealDef__Oreal__OrderedGroup_Omonoid__add clsarity_RealDef__Oreal__Ring__and__Field_Osgn__if clsarity_RealDef__Oreal__Ring__and__Field_Ofield clsarity_RealDef__Oreal__Ring__and__Field_Oidom clsarity_RealDef__Oreal__Orderings_Opreorder clsarity_RealDef__Oreal__Orderings_Olinorder 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__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_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__OrderedGroup_Oab__group__add clsarity_Complex__Ocomplex__Ring__and__Field_Omult__zero clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult clsarity_Complex__Ocomplex__Ring__and__Field_Osemiring clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add clsarity_Complex__Ocomplex__Ring__and__Field_Ofield clsarity_Complex__Ocomplex__Ring__and__Field_Oidom clsarity_Complex__Ocomplex__Int_Onumber__ring clsarity_Complex__Ocomplex__Power_Opower cls_conjecture_1
% 15.80/16.01
%------------------------------------------------------------------------------