%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG380-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n028.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:32 EDT 2022
% Result : Unsatisfiable 30.82s 31.00s
% Output : Refutation 31.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 124
% Syntax : Number of clauses : 169 ( 137 unt; 0 nHn; 169 RR)
% Number of literals : 214 ( 0 equ; 54 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 66 ( 65 usr; 1 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 11 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
( ~ class_OrderedGroup_Oab__group__add(u)
| equal(c_HOL_Oplus__class_Oplus(v,c_HOL_Oplus__class_Oplus(w,x,u),u),c_HOL_Oplus__class_Oplus(w,c_HOL_Oplus__class_Oplus(v,x,u),u)) ),
file('ALG380-1.p',unknown),
[] ).
cnf(36,axiom,
equal(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v,u,tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(41,axiom,
( ~ class_Ring__and__Field_Odivision__by__zero(u)
| ~ class_Ring__and__Field_Odivision__ring(u)
| equal(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Oinverse(v,u),u),v) ),
file('ALG380-1.p',unknown),
[] ).
cnf(42,axiom,
( ~ class_OrderedGroup_Ogroup__add(u)
| equal(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(v,w,u),w,u),v) ),
file('ALG380-1.p',unknown),
[] ).
cnf(133,axiom,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi)),
file('ALG380-1.p',unknown),
[] ).
cnf(215,axiom,
( ~ class_OrderedGroup_Omonoid__add(u)
| equal(c_HOL_Oplus__class_Oplus(v,c_HOL_Ozero__class_Ozero(u),u),v) ),
file('ALG380-1.p',unknown),
[] ).
cnf(236,axiom,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(v,w,u)
| ~ c_lessequals(w,v,u)
| equal(w,v) ),
file('ALG380-1.p',unknown),
[] ).
cnf(432,axiom,
equal(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),w,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(u,c_HOL_Otimes__class_Otimes(v,w,tc_RealDef_Oreal),tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(433,axiom,
equal(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(w,v,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(u,w,tc_RealDef_Oreal),v,tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(455,axiom,
( ~ class_RealVector_Oreal__normed__vector(u)
| c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v,u),tc_RealDef_Oreal) ),
file('ALG380-1.p',unknown),
[] ).
cnf(565,axiom,
( ~ class_Ring__and__Field_Odivision__by__zero(u)
| ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(v,w,u),u),c_HOL_Oinverse__class_Odivide(w,v,u)) ),
file('ALG380-1.p',unknown),
[] ).
cnf(590,axiom,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),u,tc_RealDef_Oreal)
| equal(c_NthRoot_Osqrt(c_Power_Opower__class_Opower(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)),u) ),
file('ALG380-1.p',unknown),
[] ).
cnf(615,axiom,
equal(c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(u),c_NthRoot_Osqrt(v),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal))),
file('ALG380-1.p',unknown),
[] ).
cnf(620,axiom,
equal(c_Complex_Orcis(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(w,x,tc_RealDef_Oreal)),c_HOL_Otimes__class_Otimes(c_Complex_Orcis(u,w),c_Complex_Orcis(v,x),tc_Complex_Ocomplex)),
file('ALG380-1.p',unknown),
[] ).
cnf(687,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(u)
| equal(c_HOL_Oplus__class_Oplus(v,v,u),c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(u),c_HOL_Oone__class_Oone(u),u),v,u)) ),
file('ALG380-1.p',unknown),
[] ).
cnf(803,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Otimes__class_Otimes(v,c_HOL_Oinverse__class_Oinverse(w,u),u),c_HOL_Oinverse__class_Odivide(v,w,u)) ),
file('ALG380-1.p',unknown),
[] ).
cnf(893,axiom,
( ~ class_Orderings_Oorder(u)
| c_lessequals(v,v,u) ),
file('ALG380-1.p',unknown),
[] ).
cnf(946,axiom,
equal(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(u,u,tc_RealDef_Oreal)),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(947,axiom,
equal(c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(u,v),tc_Complex_Ocomplex),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(965,axiom,
equal(c_NthRoot_Osqrt(c_Power_Opower__class_Opower(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(992,axiom,
equal(c_HOL_Ominus__class_Ominus(u,c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
file('ALG380-1.p',unknown),
[] ).
cnf(995,axiom,
equal(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
file('ALG380-1.p',unknown),
[] ).
cnf(1031,axiom,
( ~ class_Ring__and__Field_Odivision__by__zero(u)
| ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(v,w,u),x,u),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(v,x,u),w,u)) ),
file('ALG380-1.p',unknown),
[] ).
cnf(1061,axiom,
class_Orderings_Oorder(tc_nat),
file('ALG380-1.p',unknown),
[] ).
cnf(1117,axiom,
class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1118,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1119,axiom,
class_Ring__and__Field_Oordered__comm__semiring__strict(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1120,axiom,
class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1121,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1122,axiom,
class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1123,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1124,axiom,
class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1125,axiom,
class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1126,axiom,
class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1127,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1128,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1129,axiom,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1130,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1131,axiom,
class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1132,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1133,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1134,axiom,
class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1135,axiom,
class_Ring__and__Field_Opordered__ring__abs(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1136,axiom,
class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1137,axiom,
class_Ring__and__Field_Oordered__semiring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1138,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1139,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1140,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1141,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1142,axiom,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1143,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1144,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1145,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1146,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1147,axiom,
class_Ring__and__Field_Opordered__ring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1148,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1149,axiom,
class_Ring__and__Field_Olordered__ring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1150,axiom,
class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1151,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1152,axiom,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1153,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1154,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1155,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1156,axiom,
class_Ring__and__Field_Osemiring__1(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1157,axiom,
class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1158,axiom,
class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1159,axiom,
class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1160,axiom,
class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1161,axiom,
class_Ring__and__Field_Omult__mono(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1162,axiom,
class_OrderedGroup_Omonoid__mult(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1163,axiom,
class_Ring__and__Field_Osemiring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1164,axiom,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1165,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1166,axiom,
class_Ring__and__Field_Osgn__if(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1167,axiom,
class_Ring__and__Field_Oabs__if(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1168,axiom,
class_RealVector_Oreal__field(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1169,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1170,axiom,
class_Ring__and__Field_Oring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1171,axiom,
class_Ring__and__Field_Oidom(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1172,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1173,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1174,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1175,axiom,
class_Int_Oring__char__0(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1176,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1177,axiom,
class_Power_Opower(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1178,axiom,
class_Int_Onumber(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1179,axiom,
class_HOL_Oeq(tc_RealDef_Oreal),
file('ALG380-1.p',unknown),
[] ).
cnf(1180,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1181,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1182,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1183,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1184,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1185,axiom,
class_RealVector_Oreal__normed__algebra__1(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1186,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1187,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1188,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1189,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1190,axiom,
class_OrderedGroup_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1191,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1192,axiom,
class_OrderedGroup_Ocomm__monoid__mult(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1193,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1194,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1195,axiom,
class_Ring__and__Field_Ocomm__semiring(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1196,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1197,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1198,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1199,axiom,
class_Ring__and__Field_Osemiring__1(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1200,axiom,
class_RealVector_Oreal__algebra__1(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1201,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1202,axiom,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1203,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1204,axiom,
class_Ring__and__Field_Osemiring(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1205,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1206,axiom,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1207,axiom,
class_RealVector_Oreal__field(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1208,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1209,axiom,
class_Ring__and__Field_Oring(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1210,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1211,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1212,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1213,axiom,
class_Power_Opower(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1214,axiom,
class_Int_Onumber(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1215,axiom,
class_HOL_Oeq(tc_Complex_Ocomplex),
file('ALG380-1.p',unknown),
[] ).
cnf(1216,axiom,
~ equal(c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)),
file('ALG380-1.p',unknown),
[] ).
cnf(1251,plain,
( ~ class_RealVector_Oreal__normed__vector(u)
| c_lessequals(c_Transcendental_Osin(c_Transcendental_Opi),c_RealVector_Onorm__class_Onorm(v,u),tc_RealDef_Oreal) ),
inference(rew,[status(thm),theory(equality)],[133,455]),
[iquote('0:Rew:133.0,455.1')] ).
cnf(1312,plain,
( ~ c_lessequals(c_Transcendental_Osin(c_Transcendental_Opi),u,tc_RealDef_Oreal)
| equal(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),u) ),
inference(rew,[status(thm),theory(equality)],[965,590,133]),
[iquote('0:Rew:965.0,590.1,133.0,590.0')] ).
cnf(1453,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),u)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),u) ),
inference(res,[status(thm),theory(equality)],[236,1216]),
[iquote('0:Res:236.3,1216.0')] ).
cnf(1631,plain,
( ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| c_lessequals(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(spr,[status(thm),theory(equality)],[947,1251]),
[iquote('0:SpR:947.0,1251.1')] ).
cnf(1638,plain,
c_lessequals(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(ssi,[status(thm)],[1631,1180,1213,1207,1195,1193,1190,1183,1182,1205,1198,1192,1186,1184,1181,1211,1209,1204,1202,1196,1215,1206,1201,1185,1199,1210,1203,1214,1200,1189,1197,1194,1191,1188,1208,1212,1187]),
[iquote('0:SSi:1631.0,1180.0,1213.0,1207.0,1195.0,1193.0,1190.0,1183.0,1182.0,1205.0,1198.0,1192.0,1186.0,1184.0,1181.0,1211.0,1209.0,1204.0,1202.0,1196.0,1215.0,1206.0,1201.0,1185.0,1199.0,1210.0,1203.0,1214.0,1200.0,1189.0,1197.0,1194.0,1191.0,1188.0,1208.0,1212.0,1187.0')] ).
cnf(1786,plain,
( ~ class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal)
| equal(c_HOL_Oplus__class_Oplus(u,c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),u) ),
inference(spr,[status(thm),theory(equality)],[133,215]),
[iquote('0:SpR:133.0,215.1')] ).
cnf(1787,plain,
equal(c_HOL_Oplus__class_Oplus(u,c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),u),
inference(ssi,[status(thm)],[1786,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:1786.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(1947,plain,
equal(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(u,tc_RealDef_Oreal)),
inference(res,[status(thm),theory(equality)],[1638,1312]),
[iquote('0:Res:1638.0,1312.0')] ).
cnf(10463,plain,
( ~ class_Ring__and__Field_Ofield(tc_RealDef_Oreal)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v,u,tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[803,36]),
[iquote('0:SpR:803.1,36.0')] ).
cnf(10495,plain,
equal(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(u,tc_RealDef_Oreal),v,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v,u,tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[10463,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:10463.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(12332,plain,
equal(c_HOL_Otimes__class_Otimes(u,c_HOL_Oinverse__class_Oinverse(v,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(u,v,tc_RealDef_Oreal)),
inference(spr,[status(thm),theory(equality)],[10495,36]),
[iquote('0:SpR:10495.0,36.0')] ).
cnf(12361,plain,
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal)
| equal(c_HOL_Oinverse__class_Odivide(u,c_HOL_Oinverse__class_Oinverse(v,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v,u,tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[41,10495]),
[iquote('0:SpR:41.2,10495.0')] ).
cnf(12390,plain,
equal(c_HOL_Oinverse__class_Odivide(u,c_HOL_Oinverse__class_Oinverse(v,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v,u,tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[12361,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:12361.1,12361.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(13195,plain,
equal(c_HOL_Otimes__class_Otimes(u,c_HOL_Otimes__class_Otimes(v,c_HOL_Oinverse__class_Oinverse(w,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),w,tc_RealDef_Oreal)),
inference(spr,[status(thm),theory(equality)],[432,12332]),
[iquote('0:SpR:432.0,12332.0')] ).
cnf(13270,plain,
equal(c_HOL_Otimes__class_Otimes(u,c_HOL_Oinverse__class_Odivide(v,w,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),w,tc_RealDef_Oreal)),
inference(rew,[status(thm),theory(equality)],[12332,13195]),
[iquote('0:Rew:12332.0,13195.0')] ).
cnf(23305,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal)
| equal(c_HOL_Otimes__class_Otimes(u,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(u,u,tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[687,36]),
[iquote('0:SpR:687.1,36.0')] ).
cnf(23361,plain,
equal(c_HOL_Otimes__class_Otimes(u,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(u,u,tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[23305,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:23305.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(23362,plain,
equal(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(rew,[status(thm),theory(equality)],[23361,995]),
[iquote('0:Rew:23361.0,995.0')] ).
cnf(23363,plain,
equal(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(rew,[status(thm),theory(equality)],[36,23362]),
[iquote('0:Rew:36.0,23362.0')] ).
cnf(23364,plain,
equal(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),u,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(rew,[status(thm),theory(equality)],[13270,23363]),
[iquote('0:Rew:13270.0,23363.0')] ).
cnf(26170,plain,
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ofield(tc_RealDef_Oreal)
| equal(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(u,v,tc_RealDef_Oreal),w,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(w,c_HOL_Oinverse__class_Odivide(v,u,tc_RealDef_Oreal),tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[565,12390]),
[iquote('0:SpR:565.2,12390.0')] ).
cnf(26240,plain,
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ofield(tc_RealDef_Oreal)
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),w,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v,c_HOL_Oinverse__class_Odivide(w,u,tc_RealDef_Oreal),tc_RealDef_Oreal)) ),
inference(rew,[status(thm),theory(equality)],[1031,26170]),
[iquote('0:Rew:1031.2,26170.2')] ).
cnf(26241,plain,
equal(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),w,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v,c_HOL_Oinverse__class_Odivide(w,u,tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[26240,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:26240.1,26240.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(26256,plain,
equal(c_HOL_Oinverse__class_Odivide(u,c_HOL_Oinverse__class_Odivide(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(rew,[status(thm),theory(equality)],[26241,23364]),
[iquote('0:Rew:26241.0,23364.0')] ).
cnf(26265,plain,
equal(c_HOL_Otimes__class_Otimes(u,c_HOL_Oinverse__class_Odivide(v,w,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v,c_HOL_Oinverse__class_Odivide(w,u,tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(rew,[status(thm),theory(equality)],[26241,13270]),
[iquote('0:Rew:26241.0,13270.0')] ).
cnf(33675,plain,
equal(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(u,v,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(w,c_HOL_Oinverse__class_Oinverse(v,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(u,w,tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(v,tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(spr,[status(thm),theory(equality)],[12332,433]),
[iquote('0:SpR:12332.0,433.0')] ).
cnf(33782,plain,
equal(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(u,v,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(w,v,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(u,w,tc_RealDef_Oreal),v,tc_RealDef_Oreal)),
inference(rew,[status(thm),theory(equality)],[12332,33675]),
[iquote('0:Rew:12332.0,33675.0,12332.0,33675.0')] ).
cnf(34061,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal)
| equal(c_Complex_Orcis(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),w,tc_RealDef_Oreal)),c_HOL_Otimes__class_Otimes(c_Complex_Orcis(u,w),c_Complex_Orcis(v,w),tc_Complex_Ocomplex)) ),
inference(spr,[status(thm),theory(equality)],[687,620]),
[iquote('0:SpR:687.1,620.0')] ).
cnf(34078,plain,
equal(c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(u),v),c_Complex_Orcis(c_NthRoot_Osqrt(w),x),tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(u,w,tc_RealDef_Oreal)),c_HOL_Oplus__class_Oplus(v,x,tc_RealDef_Oreal))),
inference(spr,[status(thm),theory(equality)],[615,620]),
[iquote('0:SpR:615.0,620.0')] ).
cnf(34161,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),u)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),u) ),
inference(rew,[status(thm),theory(equality)],[34078,1453]),
[iquote('0:Rew:34078.0,1453.1')] ).
cnf(34195,plain,
equal(c_Complex_Orcis(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),w,tc_RealDef_Oreal)),c_HOL_Otimes__class_Otimes(c_Complex_Orcis(u,w),c_Complex_Orcis(v,w),tc_Complex_Ocomplex)),
inference(ssi,[status(thm)],[34061,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:34061.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(34234,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),u)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),u) ),
inference(rew,[status(thm),theory(equality)],[1947,34161,946]),
[iquote('0:Rew:1947.0,34161.1,946.0,34161.1')] ).
cnf(34235,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_a,v_a,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_HOL_Oinverse__class_Odivide(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),u) ),
inference(rew,[status(thm),theory(equality)],[26265,34234,34195,33782]),
[iquote('0:Rew:26265.0,34234.2,34195.0,34234.2,33782.0,34234.1')] ).
cnf(34236,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_a,v_a,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),u) ),
inference(rew,[status(thm),theory(equality)],[1947,34235,946,615,26256]),
[iquote('0:Rew:1947.0,34235.2,946.0,34235.2,615.0,34235.2,26256.0,34235.2')] ).
cnf(34237,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_a,v_a,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),u) ),
inference(mrr,[status(thm)],[34236,893]),
[iquote('0:MRR:34236.2,893.1')] ).
cnf(39251,plain,
( ~ class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)
| equal(c_HOL_Oplus__class_Oplus(u,c_HOL_Oplus__class_Oplus(v,c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v,u,tc_RealDef_Oreal)) ),
inference(spr,[status(thm),theory(equality)],[1787,3]),
[iquote('0:SpR:1787.0,3.1')] ).
cnf(39345,plain,
( ~ class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal)
| equal(c_HOL_Oplus__class_Oplus(u,v,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v,u,tc_RealDef_Oreal)) ),
inference(rew,[status(thm),theory(equality)],[1787,39251]),
[iquote('0:Rew:1787.0,39251.1')] ).
cnf(39346,plain,
equal(c_HOL_Oplus__class_Oplus(u,v,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v,u,tc_RealDef_Oreal)),
inference(ssi,[status(thm)],[39345,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:39345.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(40352,plain,
( ~ class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal)
| equal(c_HOL_Oplus__class_Oplus(u,c_HOL_Ominus__class_Ominus(v,u,tc_RealDef_Oreal),tc_RealDef_Oreal),v) ),
inference(spr,[status(thm),theory(equality)],[39346,42]),
[iquote('0:SpR:39346.0,42.1')] ).
cnf(40554,plain,
equal(c_HOL_Oplus__class_Oplus(u,c_HOL_Ominus__class_Ominus(v,u,tc_RealDef_Oreal),tc_RealDef_Oreal),v),
inference(ssi,[status(thm)],[40352,1167,1149,1166,1157,1125,1121,1119,1177,1168,1161,1151,1146,1143,1137,1134,1130,1128,1164,1154,1145,1138,1135,1133,1127,1123,1120,1175,1170,1163,1160,1152,1179,1165,1159,1136,1117,1156,1131,1171,1162,1178,1158,1142,1132,1172,1153,1173,1147,1126,1118,1174,1150,1122,1144,1140,1124,1141,1169,1176,1129,1155,1139,1148]),
[iquote('0:SSi:40352.0,1167.0,1149.0,1166.0,1157.0,1125.0,1121.0,1119.0,1177.0,1168.0,1161.0,1151.0,1146.0,1143.0,1137.0,1134.0,1130.0,1128.0,1164.0,1154.0,1145.0,1138.0,1135.0,1133.0,1127.0,1123.0,1120.0,1175.0,1170.0,1163.0,1160.0,1152.0,1179.0,1165.0,1159.0,1136.0,1117.0,1156.0,1131.0,1171.0,1162.0,1178.0,1158.0,1142.0,1132.0,1172.0,1153.0,1173.0,1147.0,1126.0,1118.0,1174.0,1150.0,1122.0,1144.0,1140.0,1124.0,1141.0,1169.0,1176.0,1129.0,1155.0,1139.0,1148.0')] ).
cnf(57402,plain,
equal(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(u,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(spr,[status(thm),theory(equality)],[992,40554]),
[iquote('0:SpR:992.0,40554.0')] ).
cnf(57425,plain,
equal(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(u,u,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),u),
inference(rew,[status(thm),theory(equality)],[33782,57402]),
[iquote('0:Rew:33782.0,57402.0')] ).
cnf(57436,plain,
( ~ class_Orderings_Oorder(u)
| ~ c_lessequals(c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),u) ),
inference(rew,[status(thm),theory(equality)],[57425,34237]),
[iquote('0:Rew:57425.0,34237.1')] ).
cnf(57452,plain,
~ class_Orderings_Oorder(u),
inference(mrr,[status(thm)],[57436,893]),
[iquote('0:MRR:57436.1,893.1')] ).
cnf(57453,plain,
$false,
inference(unc,[status(thm)],[57452,1061]),
[iquote('0:UnC:57452.0,1061.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG380-1 : TPTP v8.1.0. Released v4.1.0.
% 0.06/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n028.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 8 00:20:15 EDT 2022
% 0.12/0.34 % CPUTime :
% 30.82/31.00
% 30.82/31.00 SPASS V 3.9
% 30.82/31.00 SPASS beiseite: Proof found.
% 30.82/31.00 % SZS status Theorem
% 30.82/31.00 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.82/31.00 SPASS derived 41545 clauses, backtracked 351 clauses, performed 2 splits and kept 13855 clauses.
% 30.82/31.00 SPASS allocated 121336 KBytes.
% 30.82/31.00 SPASS spent 0:0:30.57 on the problem.
% 30.82/31.00 0:00:00.09 for the input.
% 30.82/31.00 0:00:00.00 for the FLOTTER CNF translation.
% 30.82/31.00 0:00:00.59 for inferences.
% 30.82/31.00 0:00:00.25 for the backtracking.
% 30.82/31.00 0:0:29.15 for the reduction.
% 30.82/31.00
% 30.82/31.00
% 30.82/31.00 Here is a proof with depth 4, length 169 :
% 30.82/31.00 % SZS output start Refutation
% See solution above
% 31.57/31.77 Formulae used in the proof : cls_add__cancel__21_1 cls_real__mult__commute_0 cls_inverse__inverse__eq_0 cls_diff__add__cancel_0 cls_sin__pi_0 cls_monoid__add__class_Oadd__0__right_0 cls_order__antisym__conv_0 cls_real__mult__assoc_0 cls_real__add__mult__distrib_0 cls_norm__ge__zero_0 cls_inverse__divide_0 cls_real__sqrt__unique_0 cls_real__sqrt__mult_0 cls_rcis__mult_0 cls_class__semiring_Osemiring__rules_I4_J_0 cls_divide__inverse_0 cls_order__eq__iff_0 cls_real__sqrt__abs2_0 cls_complex__mod__rcis_0 cls_real__sqrt__abs_0 cls_real__minus__half__eq_0 cls_real__sum__of__halves_0 cls_mult__frac__num_0 clsarity_nat__Orderings_Oorder 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__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_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__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__Ring__and__Field_Osemiring__1 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__OrderedGroup_Omonoid__mult clsarity_RealDef__Oreal__Ring__and__Field_Osemiring clsarity_RealDef__Oreal__OrderedGroup_Omonoid__add clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add clsarity_RealDef__Oreal__Ring__and__Field_Osgn__if 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__Orderings_Opreorder clsarity_RealDef__Oreal__Orderings_Olinorder clsarity_RealDef__Oreal__Orderings_Oorder clsarity_RealDef__Oreal__Int_Oring__char__0 clsarity_RealDef__Oreal__Int_Onumber__ring clsarity_RealDef__Oreal__Power_Opower clsarity_RealDef__Oreal__Int_Onumber clsarity_RealDef__Oreal__HOL_Oeq 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__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__Ring__and__Field_Osemiring__1 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__OrderedGroup_Omonoid__mult clsarity_Complex__Ocomplex__Ring__and__Field_Osemiring clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add 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__Int_Oring__char__0 clsarity_Complex__Ocomplex__Int_Onumber__ring clsarity_Complex__Ocomplex__Power_Opower clsarity_Complex__Ocomplex__Int_Onumber clsarity_Complex__Ocomplex__HOL_Oeq cls_conjecture_0
% 31.57/31.77
%------------------------------------------------------------------------------