%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV677-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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 : Wed Jul 20 21:44:47 EDT 2022
% Result : Unsatisfiable 133.26s 133.51s
% Output : Refutation 138.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 31
% Syntax : Number of clauses : 72 ( 29 unt; 9 nHn; 72 RR)
% Number of literals : 132 ( 0 equ; 57 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(426,axiom,
( ~ class_Ring__and__Field_Ofield(t_a)
| ~ equal(c_HOL_Ozero__class_Ozero(t_a),v_a) ),
file('SWV677-1.p',unknown),
[] ).
cnf(447,axiom,
( ~ class_Ring__and__Field_Odivision__ring(u)
| equal(v,c_HOL_Ozero__class_Ozero(u))
| equal(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v,u),w,u),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v,w,u),u)) ),
file('SWV677-1.p',unknown),
[] ).
cnf(556,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(u),v,u),c_HOL_Oinverse__class_Oinverse(v,u)) ),
file('SWV677-1.p',unknown),
[] ).
cnf(564,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| equal(v,c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(w,x,u),c_Power_Opower__class_Opower(v,x,u),u),c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(w,v,u),x,u)) ),
file('SWV677-1.p',unknown),
[] ).
cnf(568,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| ~ c_lessequals(v,w,tc_nat)
| equal(x,c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(x,v,u),c_Power_Opower__class_Opower(x,w,u),u),c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(x,u),c_HOL_Ominus__class_Ominus(w,v,tc_nat),u)) ),
file('SWV677-1.p',unknown),
[] ).
cnf(603,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| ~ c_lessequals(v,w,tc_nat)
| equal(x,c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(x,w,u),c_Power_Opower__class_Opower(x,v,u),u),c_Power_Opower__class_Opower(x,c_HOL_Ominus__class_Ominus(w,v,tc_nat),u)) ),
file('SWV677-1.p',unknown),
[] ).
cnf(604,axiom,
( c_lessequals(u,v,tc_nat)
| c_lessequals(v,u,tc_nat) ),
file('SWV677-1.p',unknown),
[] ).
cnf(614,axiom,
( ~ class_OrderedGroup_Omonoid__mult(u)
| equal(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(u),v,u),c_HOL_Oone__class_Oone(u)) ),
file('SWV677-1.p',unknown),
[] ).
cnf(638,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Oring__1__no__zero__divisors(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(639,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Ocancel__ab__semigroup__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(640,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Ocancel__semigroup__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(641,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Ono__zero__divisors(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(642,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Ocomm__semiring__1(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(643,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Oab__semigroup__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(644,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Odivision__ring(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(645,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Ocomm__monoid__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(646,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Ozero__neq__one(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(647,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Ocomm__ring__1(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(648,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Osemiring__1(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(649,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Osemiring__0(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(650,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Oab__group__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(651,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Omult__zero(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(652,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Omonoid__mult(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(653,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Omonoid__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(654,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_OrderedGroup_Ogroup__add(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(655,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Oring__1(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(656,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Ring__and__Field_Oidom(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(657,axiom,
( ~ class_Ring__and__Field_Ofield(u)
| class_Power_Opower(u) ),
file('SWV677-1.p',unknown),
[] ).
cnf(681,axiom,
class_Ring__and__Field_Ofield(t_a),
file('SWV677-1.p',unknown),
[] ).
cnf(682,axiom,
( ~ equal(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a))
| c_lessequals(v_n,v_m,tc_nat) ),
file('SWV677-1.p',unknown),
[] ).
cnf(683,axiom,
( ~ equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a),c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_m,v_n,tc_nat),t_a))
| ~ c_lessequals(v_n,v_m,tc_nat) ),
file('SWV677-1.p',unknown),
[] ).
cnf(685,plain,
~ equal(c_HOL_Ozero__class_Ozero(t_a),v_a),
inference(mrr,[status(thm)],[426,681]),
[iquote('0:MRR:426.0,681.0')] ).
cnf(721,plain,
equal(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),u,t_a),c_HOL_Oinverse__class_Oinverse(u,t_a)),
inference(res,[status(thm),theory(equality)],[681,556]),
[iquote('0:Res:681.0,556.0')] ).
cnf(724,plain,
class_Ring__and__Field_Oring__1__no__zero__divisors(t_a),
inference(res,[status(thm),theory(equality)],[681,638]),
[iquote('0:Res:681.0,638.0')] ).
cnf(725,plain,
class_OrderedGroup_Ocancel__ab__semigroup__add(t_a),
inference(res,[status(thm),theory(equality)],[681,639]),
[iquote('0:Res:681.0,639.0')] ).
cnf(726,plain,
class_OrderedGroup_Ocancel__semigroup__add(t_a),
inference(res,[status(thm),theory(equality)],[681,640]),
[iquote('0:Res:681.0,640.0')] ).
cnf(727,plain,
class_Ring__and__Field_Ono__zero__divisors(t_a),
inference(res,[status(thm),theory(equality)],[681,641]),
[iquote('0:Res:681.0,641.0')] ).
cnf(728,plain,
class_Ring__and__Field_Ocomm__semiring__1(t_a),
inference(res,[status(thm),theory(equality)],[681,642]),
[iquote('0:Res:681.0,642.0')] ).
cnf(729,plain,
class_OrderedGroup_Oab__semigroup__add(t_a),
inference(res,[status(thm),theory(equality)],[681,643]),
[iquote('0:Res:681.0,643.0')] ).
cnf(730,plain,
class_Ring__and__Field_Odivision__ring(t_a),
inference(res,[status(thm),theory(equality)],[681,644]),
[iquote('0:Res:681.0,644.0')] ).
cnf(731,plain,
class_OrderedGroup_Ocomm__monoid__add(t_a),
inference(res,[status(thm),theory(equality)],[681,645]),
[iquote('0:Res:681.0,645.0')] ).
cnf(732,plain,
class_Ring__and__Field_Ozero__neq__one(t_a),
inference(res,[status(thm),theory(equality)],[681,646]),
[iquote('0:Res:681.0,646.0')] ).
cnf(733,plain,
class_Ring__and__Field_Ocomm__ring__1(t_a),
inference(res,[status(thm),theory(equality)],[681,647]),
[iquote('0:Res:681.0,647.0')] ).
cnf(734,plain,
class_Ring__and__Field_Osemiring__1(t_a),
inference(res,[status(thm),theory(equality)],[681,648]),
[iquote('0:Res:681.0,648.0')] ).
cnf(735,plain,
class_Ring__and__Field_Osemiring__0(t_a),
inference(res,[status(thm),theory(equality)],[681,649]),
[iquote('0:Res:681.0,649.0')] ).
cnf(736,plain,
class_OrderedGroup_Oab__group__add(t_a),
inference(res,[status(thm),theory(equality)],[681,650]),
[iquote('0:Res:681.0,650.0')] ).
cnf(737,plain,
class_Ring__and__Field_Omult__zero(t_a),
inference(res,[status(thm),theory(equality)],[681,651]),
[iquote('0:Res:681.0,651.0')] ).
cnf(738,plain,
class_OrderedGroup_Omonoid__mult(t_a),
inference(res,[status(thm),theory(equality)],[681,652]),
[iquote('0:Res:681.0,652.0')] ).
cnf(739,plain,
class_OrderedGroup_Omonoid__add(t_a),
inference(res,[status(thm),theory(equality)],[681,653]),
[iquote('0:Res:681.0,653.0')] ).
cnf(740,plain,
class_OrderedGroup_Ogroup__add(t_a),
inference(res,[status(thm),theory(equality)],[681,654]),
[iquote('0:Res:681.0,654.0')] ).
cnf(741,plain,
class_Ring__and__Field_Oring__1(t_a),
inference(res,[status(thm),theory(equality)],[681,655]),
[iquote('0:Res:681.0,655.0')] ).
cnf(742,plain,
class_Ring__and__Field_Oidom(t_a),
inference(res,[status(thm),theory(equality)],[681,656]),
[iquote('0:Res:681.0,656.0')] ).
cnf(743,plain,
class_Power_Opower(t_a),
inference(res,[status(thm),theory(equality)],[681,657]),
[iquote('0:Res:681.0,657.0')] ).
cnf(782,plain,
( ~ class_Ring__and__Field_Odivision__ring(t_a)
| equal(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v_a,t_a),u,t_a),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v_a,u,t_a),t_a)) ),
inference(res,[status(thm),theory(equality)],[447,685]),
[iquote('0:Res:447.2,685.0')] ).
cnf(796,plain,
( ~ class_Ring__and__Field_Ofield(t_a)
| ~ c_lessequals(u,v,tc_nat)
| equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v,t_a),c_Power_Opower__class_Opower(v_a,u,t_a),t_a),c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v,u,tc_nat),t_a)) ),
inference(res,[status(thm),theory(equality)],[603,685]),
[iquote('0:Res:603.3,685.0')] ).
cnf(825,plain,
( ~ equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a),c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a))
| c_lessequals(v_n,v_m,tc_nat) ),
inference(rew,[status(thm),theory(equality)],[721,682]),
[iquote('0:Rew:721.0,682.0')] ).
cnf(833,plain,
equal(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v_a,t_a),u,t_a),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v_a,u,t_a),t_a)),
inference(mrr,[status(thm)],[782,730]),
[iquote('0:MRR:782.0,730.0')] ).
cnf(836,plain,
( ~ equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a),t_a))
| c_lessequals(v_n,v_m,tc_nat) ),
inference(rew,[status(thm),theory(equality)],[833,825]),
[iquote('0:Rew:833.0,825.0')] ).
cnf(837,plain,
( ~ c_lessequals(u,v,tc_nat)
| equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v,t_a),c_Power_Opower__class_Opower(v_a,u,t_a),t_a),c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v,u,tc_nat),t_a)) ),
inference(mrr,[status(thm)],[796,681]),
[iquote('0:MRR:796.0,681.0')] ).
cnf(838,plain,
( ~ equal(c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_m,v_n,tc_nat),t_a),c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_m,v_n,tc_nat),t_a))
| ~ c_lessequals(v_n,v_m,tc_nat) ),
inference(rew,[status(thm),theory(equality)],[837,683]),
[iquote('0:Rew:837.1,683.0')] ).
cnf(839,plain,
~ c_lessequals(v_n,v_m,tc_nat),
inference(obv,[status(thm),theory(equality)],[838]),
[iquote('0:Obv:838.0')] ).
cnf(840,plain,
~ equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a),t_a)),
inference(mrr,[status(thm)],[836,839]),
[iquote('0:MRR:836.1,839.0')] ).
cnf(891,plain,
c_lessequals(v_m,v_n,tc_nat),
inference(res,[status(thm),theory(equality)],[604,839]),
[iquote('0:Res:604.0,839.0')] ).
cnf(151661,plain,
( ~ class_OrderedGroup_Omonoid__mult(u)
| ~ class_Ring__and__Field_Ofield(u)
| equal(v,c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(u),c_Power_Opower__class_Opower(v,w,u),u),c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(u),v,u),w,u)) ),
inference(spr,[status(thm),theory(equality)],[614,564]),
[iquote('0:SpR:614.1,564.2')] ).
cnf(151693,plain,
( ~ class_OrderedGroup_Omonoid__mult(u)
| ~ class_Ring__and__Field_Ofield(u)
| equal(v,c_HOL_Ozero__class_Ozero(u))
| equal(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v,u),w,u),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v,w,u),u)) ),
inference(rew,[status(thm),theory(equality)],[556,151661]),
[iquote('0:Rew:556.1,151661.3,556.1,151661.3')] ).
cnf(151694,plain,
( ~ class_Ring__and__Field_Ofield(u)
| equal(v,c_HOL_Ozero__class_Ozero(u))
| equal(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v,u),w,u),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v,w,u),u)) ),
inference(ssi,[status(thm)],[151693,652]),
[iquote('0:SSi:151693.0,652.1')] ).
cnf(151695,plain,
( ~ class_Ring__and__Field_Ofield(u)
| ~ c_lessequals(v,w,tc_nat)
| equal(x,c_HOL_Ozero__class_Ozero(u))
| equal(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(x,v,u),c_Power_Opower__class_Opower(x,w,u),u),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(x,c_HOL_Ominus__class_Ominus(w,v,tc_nat),u),u)) ),
inference(rew,[status(thm),theory(equality)],[151694,568]),
[iquote('0:Rew:151694.2,568.3')] ).
cnf(159318,plain,
( ~ class_Ring__and__Field_Ofield(t_a)
| ~ c_lessequals(v_m,v_n,tc_nat)
| ~ equal(c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a),t_a),c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(v_a,c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a),t_a))
| equal(c_HOL_Ozero__class_Ozero(t_a),v_a) ),
inference(spl,[status(thm),theory(equality)],[151695,840]),
[iquote('0:SpL:151695.3,840.0')] ).
cnf(160345,plain,
( ~ class_Ring__and__Field_Ofield(t_a)
| ~ c_lessequals(v_m,v_n,tc_nat)
| equal(c_HOL_Ozero__class_Ozero(t_a),v_a) ),
inference(obv,[status(thm),theory(equality)],[159318]),
[iquote('0:Obv:159318.2')] ).
cnf(160346,plain,
( ~ c_lessequals(v_m,v_n,tc_nat)
| equal(c_HOL_Ozero__class_Ozero(t_a),v_a) ),
inference(ssi,[status(thm)],[160345,681,741,733,724,738,729,725,739,737,735,727,726,734,732,742,740,736,743,730,731,728]),
[iquote('0:SSi:160345.0,681.0,741.0,733.0,724.0,738.0,729.0,725.0,739.0,737.0,735.0,727.0,726.0,734.0,732.0,742.0,740.0,736.0,743.0,730.0,731.0,728.0')] ).
cnf(160347,plain,
equal(c_HOL_Ozero__class_Ozero(t_a),v_a),
inference(mrr,[status(thm)],[160346,891]),
[iquote('0:MRR:160346.0,891.0')] ).
cnf(160348,plain,
$false,
inference(mrr,[status(thm)],[160347,685]),
[iquote('0:MRR:160347.0,685.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SWV677-1 : TPTP v8.1.0. Released v4.1.0.
% 0.08/0.14 % Command : run_spass %d %s
% 0.15/0.36 % Computer : n025.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Tue Jun 14 14:26:55 EDT 2022
% 0.15/0.36 % CPUTime :
% 133.26/133.51
% 133.26/133.51 SPASS V 3.9
% 133.26/133.51 SPASS beiseite: Proof found.
% 133.26/133.51 % SZS status Theorem
% 133.26/133.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 133.26/133.51 SPASS derived 128530 clauses, backtracked 7620 clauses, performed 8 splits and kept 25891 clauses.
% 133.26/133.51 SPASS allocated 161681 KBytes.
% 133.26/133.51 SPASS spent 0:2:12.93 on the problem.
% 133.26/133.51 0:00:00.06 for the input.
% 133.26/133.51 0:00:00.00 for the FLOTTER CNF translation.
% 133.26/133.51 0:00:01.66 for inferences.
% 133.26/133.51 0:00:05.35 for the backtracking.
% 133.26/133.51 0:02:04.30 for the reduction.
% 133.26/133.51
% 133.26/133.51
% 133.26/133.51 Here is a proof with depth 1, length 72 :
% 133.26/133.51 % SZS output start Refutation
% See solution above
% 138.43/138.69 Formulae used in the proof : cls_nz_0 cls_nonzero__power__inverse_0 cls_inverse__eq__divide_0 cls_nonzero__power__divide_0 cls_power__diff__inverse_0 cls_power__diff_0 cls_nat__le__linear_0 cls_power__one_0 clsrel_Ring__and__Field_Ofield_Ring__and__Field_Oring__1__no__zero__divisors clsrel_Ring__and__Field_Ofield_OrderedGroup_Ocancel__ab__semigroup__add clsrel_Ring__and__Field_Ofield_OrderedGroup_Ocancel__semigroup__add clsrel_Ring__and__Field_Ofield_Ring__and__Field_Ono__zero__divisors clsrel_Ring__and__Field_Ofield_Ring__and__Field_Ocomm__semiring__1 clsrel_Ring__and__Field_Ofield_OrderedGroup_Oab__semigroup__add clsrel_Ring__and__Field_Ofield_Ring__and__Field_Odivision__ring clsrel_Ring__and__Field_Ofield_OrderedGroup_Ocomm__monoid__add clsrel_Ring__and__Field_Ofield_Ring__and__Field_Ozero__neq__one clsrel_Ring__and__Field_Ofield_Ring__and__Field_Ocomm__ring__1 clsrel_Ring__and__Field_Ofield_Ring__and__Field_Osemiring__1 clsrel_Ring__and__Field_Ofield_Ring__and__Field_Osemiring__0 clsrel_Ring__and__Field_Ofield_OrderedGroup_Oab__group__add clsrel_Ring__and__Field_Ofield_Ring__and__Field_Omult__zero clsrel_Ring__and__Field_Ofield_OrderedGroup_Omonoid__mult clsrel_Ring__and__Field_Ofield_OrderedGroup_Omonoid__add clsrel_Ring__and__Field_Ofield_OrderedGroup_Ogroup__add clsrel_Ring__and__Field_Ofield_Ring__and__Field_Oring__1 clsrel_Ring__and__Field_Ofield_Ring__and__Field_Oidom clsrel_Ring__and__Field_Ofield_Power_Opower tfree_tcs cls_conjecture_0 cls_conjecture_1
% 138.43/138.69
%------------------------------------------------------------------------------