%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWW185+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Mon Mar 7 00:44:53 EST 2011
% Result : Theorem 209.53s
% Output : Solution 209.85s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP15995/SWW185+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.97s, total lost is 0.97s
% not found
% Adding ~C to TBU ... ~conj_2:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...WARNING: TreeLimitedRun lost 0.11s, total lost is 1.08s
% not found
% Looking for CSA axiom ... fact_offset__poly__0:
% CSA axiom fact_offset__poly__0 found
% Looking for CSA axiom ... fact_offset__poly__single:
% CSA axiom fact_offset__poly__single found
% Looking for CSA axiom ... arity_Polynomial__Opoly__Rings_Ocomm__semiring__0:
% CSA axiom arity_Polynomial__Opoly__Rings_Ocomm__semiring__0 found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... conj_0:
% CSA axiom conj_0 found
% Looking for CSA axiom ... conj_1:
% CSA axiom conj_1 found
% Looking for CSA axiom ... tfree_0:
% CSA axiom tfree_0 found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... fact_synthetic__div__unique__lemma:
% CSA axiom fact_synthetic__div__unique__lemma found
% Looking for CSA axiom ... fact_pCons__0__0:
% CSA axiom fact_pCons__0__0 found
% Looking for CSA axiom ... fact_pCons__eq__0__iff:
% CSA axiom fact_pCons__eq__0__iff found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... fact_pcompose__0:
% CSA axiom fact_pcompose__0 found
% Looking for CSA axiom ... fact_synthetic__div__0:
% CSA axiom fact_synthetic__div__0 found
% Looking for CSA axiom ... fact_smult__0__left:
% CSA axiom fact_smult__0__left found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.14s, total lost is 1.22s
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... fact_smult__0__right:
% WARNING: TreeLimitedRun lost 0.12s, total lost is 1.34s
% CSA axiom fact_smult__0__right found
% Looking for CSA axiom ... fact_offset__poly__pCons:
% CSA axiom fact_offset__poly__pCons found
% Looking for CSA axiom ... fact_offset__poly__eq__0__lemma:
% WARNING: TreeLimitedRun lost 0.26s, total lost is 1.60s
% CSA axiom fact_offset__poly__eq__0__lemma found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.31s, total lost is 1.91s
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :fact_offset__poly__eq__0__lemma:fact_offset__poly__pCons:fact_smult__0__right:fact_smult__0__left:fact_synthetic__div__0:fact_pcompose__0:fact_pCons__eq__0__iff:fact_pCons__0__0:fact_synthetic__div__unique__lemma:tfree_0:conj_1:conj_0:arity_Polynomial__Opoly__Rings_Ocomm__semiring__0:fact_offset__poly__single:fact_offset__poly__0 (15)
% Unselected axioms are ... :fact_mult__poly__0__left:fact_mult__poly__0__right:fact_poly__0:arity_Polynomial__Opoly__Groups_Oab__semigroup__mult:arity_Polynomial__Opoly__Rings_Ocomm__semiring:arity_Polynomial__Opoly__Rings_Osemiring__0:arity_Polynomial__Opoly__Rings_Omult__zero:arity_Polynomial__Opoly__Rings_Osemiring:fact_one__poly__def:fact_pCons__eq__iff:arity_Nat__Onat__Rings_Ocomm__semiring__0:fact_add__pCons:fact_smult__add__left:fact_smult__add__right:fact_pcompose__pCons:fact_mult__pCons__left:fact_mult__pCons__right:fact_minus__pCons:fact_minus__poly__code_I2_J:fact_zero__reorient:fact_poly__rec__pCons:fact_monom__0:fact_add__poly__code_I2_J:fact_add__poly__code_I1_J:fact_degree__pCons__0:fact_synthetic__div__eq__0__iff:fact_pos__poly__pCons:arity_Int__Oint__Rings_Ocomm__semiring__0:fact_mult__poly__add__left:fact_degree__pCons__eq:fact_minus__poly__code_I1_J:fact_ext:fact_monom__eq__0:fact_monom__eq__0__iff:fact_smult__eq__0__iff:fact_poly__offset__poly:fact_smult__pCons:fact_poly__gcd_Oassoc:fact_poly__gcd_Oleft__commute:fact_poly__gcd_Ocommute:fact_poly__gcd__zero__iff:fact_poly__gcd__0__0:fact_linorder__neqE__linordered__idom:fact_pdivmod__rel__0__iff:fact_pdivmod__rel__by__0__iff:clrel_Rings_Ocomm__semiring__0__Groups_Ozero:arity_Polynomial__Opoly__Groups_Ozero:fact_poly__add:fact_poly__mult:fact_mult__smult__right:fact_mult__smult__left:clrel_Rings_Ocomm__semiring__0__Groups_Oab__semigroup__mult:clrel_Rings_Ocomm__semiring__0__Groups_Oab__semigroup__add:clrel_Rings_Ocomm__semiring__0__Groups_Ocomm__monoid__add:clrel_Rings_Ocomm__semiring__0__Rings_Ocomm__semiring:clrel_Rings_Ocomm__semiring__0__Groups_Omonoid__add:clrel_Rings_Ocomm__semiring__0__Rings_Osemiring__0:clrel_Rings_Ocomm__semiring__0__Rings_Omult__zero:clrel_Rings_Ocomm__semiring__0__Rings_Osemiring:fact_pCons__induct:fact_synthetic__div__pCons:arity_Polynomial__Opoly__Rings_Ocomm__semiring__1:arity_Polynomial__Opoly__Groups_Ocancel__comm__monoid__add:arity_Polynomial__Opoly__Groups_Ocomm__monoid__add:arity_Polynomial__Opoly__Rings_Olinordered__idom:arity_Polynomial__Opoly__Groups_Oab__group__add:arity_Polynomial__Opoly__Rings_Ocomm__ring__1:arity_Polynomial__Opoly__Rings_Ocomm__ring:arity_Polynomial__Opoly__Rings_Oidom:fact_degree__pCons__eq__if:fact_le__0__eq:fact_neq0__conv:fact_gr__implies__not0:fact_gr0I:fact_poly__rec__0:fact_coeff__0:fact_poly__pCons:fact_degree__0:fact_pdivmod__rel__0:fact_pdivmod__rel__by__0:fact_not__pos__poly__0:fact_monom__Suc:fact_Zero__not__Suc:fact_nat_Osimps_I2_J:fact_Suc__not__Zero:fact_nat_Osimps_I3_J:fact_Zero__neq__Suc:fact_Suc__neq__Zero:fact_dvd__smult__cancel:fact_smult__dvd:fact_dvd__smult__iff:fact_smult__dvd__iff:fact_mod__smult__right:fact_poly__gcd_Osimps_I2_J:fact_diffs0__imp__equal:fact_diff__self__eq__0:fact_minus__nat_Odiff__0:fact_nat_Osize_I3_J:fact_nat_Osize_I1_J:fact_pos__poly__total:fact_poly__rec_Osimps:fact_coeff__pCons__0:fact_mult__0:fact_mult__0__right:fact_mult__is__0:fact_mult__cancel1:fact_mult__cancel2:fact_nat__mult__eq__cancel__disj:fact_degree__minus:fact_pos__poly__add:fact_zminus__0:fact_zmod__zero:fact_zmod__self:fact_poly__pcompose:fact_add__monom:fact_degree__monom__eq:fact_minus__monom:fact_minus__add__distrib:fact_poly__gcd__dvd1:fact_poly__gcd__dvd2:fact_dvd__poly__gcd__iff:fact_poly__gcd__greatest:fact_even__less__0__iff:fact_zadd__zmult__distrib:fact_zadd__zmult__distrib2:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J:fact_crossproduct__eq:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J:fact_crossproduct__noteq:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J:fact_plus__nat_Oadd__0:fact_Nat_Oadd__0__right:fact_add__is__0:fact_add__eq__self__zero:fact_smult__smult:fact_mult__left_Oadd:fact_mult_Oadd__left:fact_mult__right_Oadd:fact_mult_Oadd__right:fact_nat__mult__commute:fact_nat__mult__assoc:fact_minus__zero:fact_neg__0__equal__iff__equal:fact_equal__neg__zero:fact_neg__equal__0__iff__equal:fact_neg__equal__zero:fact_inverse__zero:fact_inverse__nonzero__iff__nonzero:fact_nonzero__imp__inverse__nonzero:fact_nonzero__inverse__inverse__eq:fact_inverse__zero__imp__zero:fact_nonzero__inverse__eq__imp__eq:fact_mod__0:fact_mod__by__0:fact_mod__self:fact_right__minus__eq:fact_eq__iff__diff__eq__0:fact_diff__self:fact_diff__0__right:fact_leading__coeff__0__iff:fact_leading__coeff__neq__0:fact_combine__common__factor:fact_comm__semiring__class_Odistrib:fact_mult__zero__left:fact_mult_Ozero__left:fact_mult__left_Ozero:fact_mult__zero__right:fact_divisors__zero:fact_no__zero__divisors:fact_mult__eq__0__iff:fact_mult__right_Ozero:fact_mult_Ozero__right:fact_less__minus__self__iff:fact_field__inverse__zero:fact_n__not__Suc__n:fact_Suc__n__not__n:fact_nat_Oinject:fact_Suc__inject:fact_smult__1__left:fact_degree__1:fact_dvd__iff__poly__eq__0:fact_poly__eq__0__iff__dvd:fact_dvd__0__left:fact_int__0__neq__1:fact_expand__poly__eq:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J:fact_one__neq__zero:fact_zero__neq__one:fact_degree__pCons__le:fact_zmult__commute:fact_zmult__assoc:fact_zadd__0:fact_zadd__0__right:fact_Nat_Odiff__diff__eq:fact_eq__diff__iff:fact_diff__diff__cancel:fact_poly__eq__iff:fact_synthetic__div__correct:fact_synthetic__div__unique:fact_coeff__add:fact_add_Ocomm__neutral:fact_add__0__right:fact_double__zero__sym:fact_add__0:fact_add__0__left:fact_double__eq__0__iff:fact_add__0__iff:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J:fact_ab__semigroup__mult__class_Omult__ac_I1_J:fact_coeff__minus:fact_sum__squares__le__zero__iff:fact_times_Oidem:fact_mult__idem:fact_mult__left__idem:fact_one__dvd:fact_sum__squares__gt__zero__iff:fact_dvd_Oorder__refl:fact_dvd_Oorder__trans:fact_dvd_Ole__less__trans:fact_dvd_Oless__not__sym:fact_dvd_Oless__imp__le:fact_dvd_Oless__imp__not__less:fact_dvd_Oless__le__trans:fact_dvd_Oless__asym_H:fact_dvd_Oless__trans:fact_dvd_Oless__asym:fact_degree__linear__power:fact_pdivmod__rel__smult__left:fact_zadd__zless__mono:arity_Polynomial__Opoly__Rings_Olinordered__semidom:arity_Polynomial__Opoly__Groups_Ogroup__add:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J:fact_coeff__mult__degree__sum:fact_poly__smult:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J:fact_nat__add__commute:fact_nat__add__left__commute:fact_nat__add__assoc:fact_nat__add__left__cancel:fact_nat__add__right__cancel:fact_le0:fact_less__eq__nat_Osimps_I1_J:fact_ab__left__minus:fact_dvd__0__right:fact_less__zeroE:fact_not__less0:fact_less__nat__zero__code:fact_nat__mult__eq__cancel1:fact_division__ring__inverse__add:fact_inverse__add:fact_coeff__linear__power:arity_Polynomial__Opoly__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct:arity_Polynomial__Opoly__Groups_Oordered__cancel__ab__semigroup__add:arity_Polynomial__Opoly__Groups_Oordered__ab__semigroup__add__imp__le:arity_Polynomial__Opoly__Rings_Olinordered__comm__semiring__strict:arity_Polynomial__Opoly__Rings_Olinordered__semiring__1__strict:arity_Polynomial__Opoly__Rings_Olinordered__semiring__strict:arity_Polynomial__Opoly__Groups_Oordered__ab__semigroup__add:arity_Polynomial__Opoly__Groups_Oordered__comm__monoid__add:arity_Polynomial__Opoly__Groups_Olinordered__ab__group__add:arity_Polynomial__Opoly__Groups_Ocancel__ab__semigroup__add:arity_Polynomial__Opoly__Rings_Oring__1__no__zero__divisors:arity_Polynomial__Opoly__Rings_Oordered__cancel__semiring:arity_Polynomial__Opoly__Rings_Olinordered__ring__strict:arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors:arity_Polynomial__Opoly__Rings_Oordered__comm__semiring:arity_Polynomial__Opoly__Rings_Olinordered__semiring__1:arity_Polynomial__Opoly__Groups_Oordered__ab__group__add:arity_Polynomial__Opoly__Groups_Ocancel__semigroup__add:arity_Polynomial__Opoly__Rings_Olinordered__semiring:arity_Polynomial__Opoly__Groups_Ocomm__monoid__mult:arity_Polynomial__Opoly__Groups_Oab__semigroup__add:arity_Polynomial__Opoly__Rings_Oordered__semiring:arity_Polynomial__Opoly__Rings_Ono__zero__divisors:arity_Polynomial__Opoly__Rings_Olinordered__ring:arity_Polynomial__Opoly__Divides_Osemiring__div:arity_Polynomial__Opoly__Rings_Ozero__neq__one:arity_Polynomial__Opoly__Rings_Oordered__ring:arity_Polynomial__Opoly__Orderings_Opreorder:arity_Polynomial__Opoly__Orderings_Olinorder:arity_Polynomial__Opoly__Groups_Omonoid__mult:arity_Polynomial__Opoly__Groups_Omonoid__add:arity_Polynomial__Opoly__Divides_Oring__div:arity_Polynomial__Opoly__Orderings_Oorder:arity_Polynomial__Opoly__Int_Oring__char__0:arity_Polynomial__Opoly__Orderings_Oord:arity_Polynomial__Opoly__Groups_Ouminus:arity_Polynomial__Opoly__Rings_Oring__1:arity_Polynomial__Opoly__Power_Opower:arity_Polynomial__Opoly__Rings_Oring:arity_Polynomial__Opoly__Groups_Oone:arity_Polynomial__Opoly__Rings_Odvd:arity_Polynomial__Opoly__HOL_Oequal:fact_coeff__pCons__Suc:fact_degree__mult__eq:fact_mult__Suc__right:fact_mult__Suc:fact_mult__eq__1__iff:fact_degree__mult__le:fact_poly__1:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J:fact_coeff__1:fact_mult__eq__self__implies__10:fact_sum__squares__ge__zero:fact_nat__neq__iff:fact_linorder__neqE__nat:fact_less__not__refl2:fact_less__not__refl3:fact_not__sum__squares__lt__zero:fact_coeff__eq__0:fact_nat__mult__dvd__cancel__disj:fact_poly__power:fact_zdvd__antisym__nonneg:fact_pdivmod__rel__smult__right:fact_zminus__zminus:fact_less__degree__imp:fact_mod__eq__0__iff:fact_mod__mult__self3:fact_monom__eq__iff:fact_coeff__inject:fact_poly__zero:fact_mult__monom:fact_sum__squares__eq__zero__iff:fact_coeff__smult:fact_smult__monom:fact_poly__minus:fact_eq__imp__le:fact_le__antisym:fact_minus__minus:fact_equation__minus__iff:fact_minus__equation__iff:fact_neg__equal__iff__equal:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J:fact_degree__smult__le:fact_degree__monom__le:fact_le__degree:fact_eq__zero__or__degree__less:fact_gcd__lcm__complete__lattice__nat_Otop__greatest:fact_pdivmod__rel__unique:fact_pdivmod__rel__unique__mod:fact_pdivmod__rel__unique__div:fact_pdivmod__rel__mult:fact_zadd__commute:fact_zadd__left__commute:fact_zadd__assoc:fact_le__diff__iff:fact_diff__le__mono:fact_diff__le__mono2:fact_diff__le__self:arity_Nat__Onat__Groups_Ocancel__comm__monoid__add:arity_Nat__Onat__Groups_Oab__semigroup__mult:arity_Nat__Onat__Groups_Oab__semigroup__add:arity_Nat__Onat__Groups_Ocomm__monoid__add:arity_Nat__Onat__Rings_Ocomm__semiring:arity_Nat__Onat__Groups_Omonoid__add:arity_Nat__Onat__Rings_Osemiring__0:arity_Nat__Onat__Rings_Omult__zero:arity_Nat__Onat__Rings_Osemiring:fact_eq__poly__code_I2_J:fact_eq__poly__code_I3_J:fact_coeff__monom:fact_order__root:fact_add__scale__eq__noteq:fact_degree__smult__eq:fact_degree__pcompose__le:fact_one__reorient:fact_double__compl:fact_compl__eq__compl__iff:fact_dvd__mult__cancel__left:fact_dvd__mult__cancel__right:fact_less__iff__Suc__add:fact_le__less__Suc__eq:fact_nat__mult__less__cancel1:fact_mult__less__mono2:fact_mult__less__mono1:fact_mult__less__cancel2:fact_mult__less__cancel1:fact_nat__0__less__mult__iff:fact_dvd__imp__degree__le:fact_order__2:fact_order:fact_zdvd__mult__cancel:fact_zdvd__mono:fact_zless__linear:fact_zdiv__mono2__lemma:fact_zdiv__mono2__neg__lemma:fact_mod__mult__self2__is__0:fact_mod__mult__self1__is__0:fact_mod__mult__self1:fact_mod__mult__self2:fact_degree__mod__less:fact_zmod__eq__0__iff:fact_mult_Oprod__diff__prod:fact_eq__add__iff2:fact_eq__add__iff1:fact_mult__diff__mult:arity_Nat__Onat__Rings_Ocomm__semiring__1:arity_Nat__Onat__Groups_Ozero:fact_coeff__pCons:fact_add__right__imp__eq:fact_add__imp__eq:fact_add__left__imp__eq:fact_add__right__cancel:fact_add__left__cancel:fact_ab__semigroup__add__class_Oadd__ac_I1_J:fact_add__mult__distrib2:fact_add__mult__distrib:fact_left__add__mult__distrib:fact_order__degree:fact_convex__bound__le:fact_One__nat__def:fact_Suc__eq__plus1__left:fact_Suc__eq__plus1:fact_order__eq__iff:fact_order__eq__refl:fact_order__antisym__conv:fact_ord__eq__le__trans:fact_xt1_I3_J:fact_ord__le__eq__trans:fact_xt1_I4_J:fact_order__antisym:fact_xt1_I5_J:fact_linorder__neq__iff:fact_not__less__iff__gr__or__eq:fact_linorder__less__linear:fact_linorder__antisym__conv3:fact_linorder__neqE:fact_less__imp__neq:fact_order__less__imp__not__eq:fact_order__less__imp__not__eq2:fact_ord__eq__less__trans:fact_xt1_I1_J:fact_ord__less__eq__trans:fact_xt1_I2_J:fact_linorder__cases:fact_nonzero__inverse__mult__distrib:fact_degree__add__eq__right:fact_degree__add__eq__left:fact_dvd__1__iff__1:fact_dvd_Oeq__iff:fact_dvd_Ole__less:fact_dvd_Oless__le:fact_dvd_Oneq__le__trans:fact_dvd_Oeq__refl:fact_dvd_Oantisym__conv:fact_dvd_Ole__imp__less__or__eq:fact_dvd_Ole__neq__trans:fact_dvd_Oord__eq__le__trans:fact_dvd_Oord__le__eq__trans:fact_dvd__antisym:fact_dvd_Oantisym:fact_dvd_Oord__eq__less__trans:fact_dvd_Oless__imp__neq:fact_dvd_Oless__imp__not__eq:fact_dvd_Oless__imp__not__eq2:fact_dvd_Oord__less__eq__trans:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J:fact_pos__poly__def:fact_zdvd__reduce:fact_zdvd__period:fact_zmult__zless__mono2:fact_odd__nonzero:fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J:fact_mod__smult__left:fact_mod__1:fact_mod__Suc:fact_Suc__diff__le:fact_eq__poly__code_I4_J:fact_Suc__mult__cancel1:fact_one__is__add:fact_add__is__1:fact_nat__size:fact_smult__minus__left:fact_smult__minus__right:fact_nat__mult__eq__1__iff:fact_nat__mult__1__right:fact_nat__1__eq__mult__iff:fact_nat__mult__1:fact_minus__unique:fact_left__minus:fact_eq__neg__iff__add__eq__0:fact_right__minus:fact_split__mult__neg__le:fact_split__mult__pos__le:fact_mult__mono:fact_mult__mono_H:fact_mult__left__mono__neg:fact_mult__right__mono__neg:fact_comm__mult__left__mono:fact_mult__left__mono:fact_mult__right__mono:fact_mult__nonpos__nonpos:fact_mult__nonpos__nonneg:fact_mult__nonneg__nonpos2:fact_mult__nonneg__nonpos:fact_mult__nonneg__nonneg:fact_mult__le__0__iff:fact_zero__le__mult__iff:fact_zero__le__square:fact_Suc__mult__le__cancel1:fact_add__eq__0__iff:fact_poly__gcd__1__left:fact_poly__gcd__1__right:fact_poly__gcd__minus__right:fact_poly__gcd__minus__left:fact_mult__strict__left__mono__neg:fact_mult__strict__right__mono__neg:fact_comm__mult__strict__left__mono:fact_mult__strict__left__mono:fact_mult__strict__right__mono:fact_mult__neg__neg:fact_mult__neg__pos:fact_mult__less__cancel__left__neg:fact_zero__less__mult__pos2:fact_zero__less__mult__pos:fact_mult__pos__neg2:fact_mult__pos__neg:fact_mult__pos__pos:fact_mult__less__cancel__left__pos:fact_mult__less__cancel__left__disj:fact_mult__less__cancel__right__disj:fact_not__square__less__zero:fact_pos__poly__mult:fact_degree__le:fact_zle__trans:fact_zle__linear:fact_zle__refl:fact_q__pos__lemma:fact_q__neg__lemma:fact_unique__quotient__lemma:fact_unique__quotient__lemma__neg:fact_mod__poly__less:fact_poly__mod__minus__right:fact_poly__mod__minus__left:fact_mod__poly__eq:fact_mod__mult__distrib2:fact_mod__mult__distrib:fact_zmod__zminus1__not__zero:fact_zmod__zminus2__not__zero:fact_mod__lemma:fact_diff__add__0:arity_Int__Oint__Groups_Oab__semigroup__mult:arity_Int__Oint__Groups_Oab__semigroup__add:arity_Int__Oint__Groups_Ocomm__monoid__add:arity_Int__Oint__Rings_Ocomm__semiring:arity_Int__Oint__Groups_Oab__group__add:arity_Int__Oint__Groups_Omonoid__add:arity_Int__Oint__Rings_Osemiring__0:arity_Int__Oint__Rings_Omult__zero:arity_Int__Oint__Rings_Osemiring:fact_eq__poly__code_I1_J:fact_nat__case__0:fact_synthetic__div__correct_H:fact_add__nonneg__eq__0__iff:fact_degree__add__le:fact_poly__gcd__monic:fact_zero__less__Suc:fact_less__not__refl:fact_less__irrefl__nat:fact_nonzero__inverse__minus__eq:fact_gr0__conv__Suc:fact_less__Suc0:fact_less__Suc__eq__0__disj:fact_poly__dvd__antisym:fact_less__add__Suc1:fact_less__add__Suc2:fact_Suc__le__lessD:fact_Suc__leI:fact_le__imp__less__Suc:fact_Suc__le__eq:fact_less__Suc__eq__le:fact_less__eq__Suc__le:fact_degree__add__less:fact_n__less__m__mult__n:fact_n__less__n__mult__m:fact_one__less__mult:fact_nat__mult__dvd__cancel1:fact_dvd__mult__cancel:fact_nat__lt__two__imp__zero__or__one:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J:fact_pow__divides__pow__nat:fact_pow__divides__eq__nat:fact_nat__zero__less__power__iff:fact_zpower__zadd__distrib:fact_zero__less__power__nat__eq:fact_zmult__zminus:fact_zmult__1:fact_zmult__1__right:fact_power_Opower_Opower__0:fact_zadd__zminus__inverse2:fact_mod__by__1:fact_dvd__imp__mod__0:fact_dvd__eq__mod__eq__0:fact_zmod__zmult1__eq:fact_zmod__simps_I3_J:fact_mod__mult__self4:fact_le__mod__geq:fact_diff__is__0__eq_H:fact_diff__is__0__eq:fact_add__diff__inverse:fact_diff__add__assoc2:fact_add__diff__assoc2:fact_diff__add__assoc:fact_le__imp__diff__is__add:fact_le__add__diff__inverse2:fact_add__diff__assoc:fact_le__add__diff__inverse:fact_diff__diff__right:arity_Int__Oint__Rings_Olinordered__idom:arity_Int__Oint__Rings_Ocomm__semiring__1:arity_Int__Oint__Groups_Ozero:arity_Int__Oint__Rings_Oidom:help_c__fequal__1:help_c__fequal__2:fact_equal__poly__def:fact_square__eq__iff:fact_minus__mult__minus:fact_minus__mult__commute:fact_mult__left_Ominus:fact_mult_Ominus__left:fact_mult__right_Ominus:fact_mult_Ominus__right:fact_minus__mult__left:fact_minus__mult__right:fact_mult__1__left:fact_mult__1:fact_mult__1__right:fact_mult_Ocomm__neutral:fact_le__SucE:fact_le__Suc__eq:fact_double__add__le__zero__iff__single__add__le__zero:fact_zero__le__double__add__iff__zero__le__single__add:fact_dvdI:fact_dvd__refl:fact_dvd__trans:fact_dvd__smult:fact_smult__dvd__cancel:fact_less__SucE:fact_Suc__lessI:fact_less__antisym:fact_not__less__less__Suc__eq:fact_less__Suc__eq:fact_double__add__less__zero__iff__single__add__less__zero:fact_zero__less__double__add__iff__zero__less__single__add:fact_add__gr__0:fact_Suc__mult__less__cancel1:fact_convex__bound__lt:fact_dvd__1__left:fact_inverse__mult__distrib:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J:fact_poly__monom:fact_nat__power__less__imp__less:fact_power__commutes:fact_power__mult__distrib:fact_power__one:fact_dvd__power__same:fact_power__add:fact_pos__zmult__eq__1__iff:fact_zdvd__not__zless:fact_self__quotient__aux1:fact_self__quotient__aux2:fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J:fact_mod__mult__right__eq:fact_mod__mult__left__eq:fact_mod__mult__eq:fact_mod__mult__mult1:fact_mod__mult__mult2:fact_zmod__simps_I4_J:fact_mod__mult__cong:fact_mod__add__self2:fact_mod__add__self1:fact_mod__add__right__eq:fact_mod__add__left__eq:fact_mod__add__eq:fact_zmod__simps_I2_J:fact_zmod__simps_I1_J:fact_mod__add__cong:fact_zpower__zmod:fact_neg__mod__bound:fact_pos__mod__bound:fact_Divides_Otransfer__nat__int__function__closures_I2_J:fact_zmod__le__nonneg__dividend:fact_split__mod:fact_divmod__int__rel__mod__eq:fact_mod__geq:fact_mod__if:help_c__fFalse__1:help_c__fTrue__1:fact_coeff__inverse:fact_le__refl:fact_nat__le__linear:fact_le__trans:fact_le__minus__iff:fact_minus__le__iff:fact_neg__le__iff__le:fact_le__imp__neg__le:fact_le__iff__add:fact_mult__le__mono:fact_mult__le__mono2:fact_mult__le__mono1:fact_le__cube:fact_le__square:fact_le__Suc__ex__iff:fact_compl__mono:fact_compl__le__compl__iff:fact_bool_Osize_I2_J:fact_dvd__mult__right:fact_dvd__mult__left:fact_mult__dvd__mono:fact_dvd__mult:fact_dvd__mult2:fact_dvd__triv__right:fact_dvd__triv__left:fact_inverse__1:fact_nat__less__cases:fact_less__add__eq__less:fact_nat__less__le:fact_le__eq__less__or__eq:fact_le__neq__implies__less:fact_less__or__eq__imp__le:fact_not__one__less__zero:fact_zero__less__one:fact_neg__0__less__iff__less:fact_neg__less__0__iff__less:fact_neg__less__nonneg:fact_less__add__one:fact_left__inverse:fact_right__inverse:fact_bool_Osize_I1_J:fact_field__inverse:fact_inverse__positive__imp__positive:fact_inverse__negative__imp__negative:fact_power__Suc__0:fact_nat__power__eq__Suc__0__iff:fact_field__power__not__zero:fact_pdivmod__rel__def:fact_int__0__less__1:fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J:fact_mod__mod__cancel:fact_real__squared__diff__one__factored:fact_diff__less__Suc:arity_Int__Oint__Rings_Olinordered__semidom:arity_Int__Oint__Divides_Osemiring__div:arity_Int__Oint__Orderings_Oorder:fact_equal__refl:fact_nat__case__Suc:fact_add__Suc__shift:fact_add__Suc:fact_add__Suc__right:fact_not__one__le__zero:fact_zero__le__one:fact_neg__0__le__iff__le:fact_le__minus__self__iff:fact_neg__le__0__iff__le:fact_minus__le__self__iff:fact_Suc__leD:fact_le__SucI:fact_Suc__le__mono:fact_not__less__eq__eq:fact_Suc__n__not__le__n:fact_poly__gcd_Osimps_I1_J:fact_Suc__mono:fact_lessI:fact_minus__dvd__iff:fact_dvd__minus__iff:fact_Suc__less__SucD:fact_Suc__lessD:fact_less__trans__Suc:fact_less__SucI:fact_Suc__less__eq:fact_not__less__eq:fact_pos__add__strict:fact_add__less__le__mono:fact_add__le__less__mono:fact_nat__dvd__1__iff__1:fact_nat__dvd__not__less:fact_dvd__mult__cancel2:fact_dvd__mult__cancel1:fact_poly__gcd__unique:fact_dvd__pos__nat:fact_power__decreasing:fact_zadd__left__mono:fact_zminus__zadd__distrib:fact_zadd__strict__right__mono:fact_le__imp__0__less:fact_incr__mult__lemma:fact_dvd__mod__imp__dvd:fact_dvd__mod:fact_dvd__mod__iff:fact_field__le__mult__one__interval:fact_mod__Suc__eq__Suc__mod:fact_mod__less:fact_mod__less__divisor:fact_mod__less__eq__dividend:fact_zmult2__lemma__aux3:fact_zmult2__lemma__aux4:fact_zmult2__lemma__aux1:fact_zmult2__lemma__aux2:fact_less__add__iff1:fact_less__add__iff2:fact_division__ring__inverse__diff:fact_diff__less:fact_zero__less__diff:fact_less__diff__conv:fact_less__diff__iff:fact_diff__less__mono:fact_le__diff__conv2:fact_le__add__diff:fact_le__diff__conv:arity_Int__Oint__Groups_Ocancel__comm__monoid__add:arity_Int__Oint__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct:arity_Int__Oint__Groups_Oordered__cancel__ab__semigroup__add:arity_Int__Oint__Groups_Oordered__ab__semigroup__add__imp__le:arity_Int__Oint__Rings_Olinordered__comm__semiring__strict:arity_Int__Oint__Rings_Olinordered__semiring__1__strict:arity_Int__Oint__Rings_Olinordered__semiring__strict:arity_Int__Oint__Groups_Oordered__ab__semigroup__add:arity_Int__Oint__Groups_Oordered__comm__monoid__add:arity_Int__Oint__Groups_Olinordered__ab__group__add:arity_Int__Oint__Groups_Ocancel__ab__semigroup__add:arity_Int__Oint__Rings_Oring__1__no__zero__divisors:arity_Int__Oint__Rings_Oordered__cancel__semiring:arity_Int__Oint__Rings_Olinordered__ring__strict:arity_Int__Oint__Rings_Oring__no__zero__divisors:arity_Int__Oint__Rings_Oordered__comm__semiring:arity_Int__Oint__Rings_Olinordered__semiring__1:arity_Int__Oint__Groups_Oordered__ab__group__add:arity_Int__Oint__Groups_Ocancel__semigroup__add:arity_Int__Oint__Rings_Olinordered__semiring:arity_Int__Oint__Groups_Ocomm__monoid__mult:arity_Int__Oint__Rings_Oordered__semiring:arity_Int__Oint__Rings_Ono__zero__divisors:arity_Int__Oint__Rings_Olinordered__ring:arity_Int__Oint__Rings_Ozero__neq__one:arity_Int__Oint__Rings_Oordered__ring:arity_Int__Oint__Orderings_Opreorder:arity_Int__Oint__Orderings_Olinorder:arity_Int__Oint__Groups_Omonoid__mult:arity_Int__Oint__Rings_Ocomm__ring__1:arity_Int__Oint__Groups_Ogroup__add:arity_Int__Oint__Divides_Oring__div:arity_Int__Oint__Rings_Ocomm__ring:arity_Int__Oint__Int_Oring__char__0:arity_Int__Oint__Orderings_Oord:arity_Int__Oint__Groups_Ouminus:arity_Int__Oint__Rings_Oring__1:arity_Int__Oint__Power_Opower:arity_Int__Oint__Rings_Oring:arity_Int__Oint__Groups_Oone:arity_Int__Oint__Rings_Odvd:arity_Int__Oint__HOL_Oequal:fact_pCons__def:fact_minus__add:fact_add__minus__cancel:fact_minus__add__cancel:fact_add__leE:fact_add__leD1:fact_add__leD2:fact_add__le__mono:fact_add__le__mono1:fact_trans__le__add2:fact_trans__le__add1:fact_nat__add__left__cancel__le:fact_le__add1:fact_le__add2:fact_add__nonpos__nonpos:fact_add__increasing2:fact_add__increasing:fact_add__nonneg__nonneg:fact_order__refl:fact_termination__basic__simps_I3_J:fact_termination__basic__simps_I4_J:fact_linorder__linear:fact_order__trans:fact_xt1_I6_J:fact_linorder__le__cases:fact_order__less__irrefl:fact_order__less__not__sym:fact_order__less__imp__not__less:fact_order__less__asym_H:fact_xt1_I9_J:fact_order__less__trans:fact_xt1_I10_J:fact_order__less__asym:fact_dvd__add:fact_add__lessD1:fact_add__less__mono:fact_add__less__mono1:fact_trans__less__add2:fact_trans__less__add1:fact_nat__add__left__cancel__less:fact_not__add__less2:fact_not__add__less1:fact_termination__basic__simps_I1_J:fact_termination__basic__simps_I2_J:fact_less__imp__le__nat:fact_termination__basic__simps_I5_J:fact_add__neg__neg:fact_add__pos__pos:fact_realpow__two__disj:fact_degree__power__le:fact_dvd__power:fact_pow__divides__pow__int:fact_pow__divides__eq__int:fact_power__le__dvd:fact_dvd__power__le:fact_le__imp__power__dvd:fact_power__strict__increasing__iff:fact_power__less__imp__less__exp:fact_power__strict__increasing:fact_power__increasing:fact_power__eq__imp__eq__base:fact_uminus__dvd__conv_I1_J:fact_uminus__dvd__conv_I2_J:fact_power_Opower_Opower__Suc:fact_zless__le:fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J:fact_zdvd__zmod__imp__zdvd:fact_zdvd__zmod:fact_zminus__zmod:fact_zmod__zminus__zminus:fact_zmod__zminus2:fact_mod__neg__neg__trivial:fact_mod__pos__pos__trivial:fact_split__zmod:fact_le__add__iff2:fact_le__add__iff1:fact_dvd__diffD1:fact_dvd__diffD:fact_diff__add__inverse2:fact_diff__add__inverse:fact_diff__diff__left:fact_diff__cancel:fact_diff__cancel2:fact_mult__left__le__one__le:fact_mult__right__le__one__le:fact_one__le__mult__iff:fact_inverse__minus__eq:fact_order__less__le:fact_order__le__less:fact_linorder__antisym__conv1:fact_order__neq__le__trans:fact_xt1_I12_J:fact_linorder__antisym__conv2:fact_order__le__imp__less__or__eq:fact_order__le__neq__trans:fact_xt1_I11_J:fact_less__minus__iff:fact_minus__less__iff:fact_neg__less__iff__less:fact_nat__mult__le__cancel1:fact_mult__le__cancel2:fact_mult__le__cancel1:fact_dvd__reduce:fact_inverse__eq__1__iff:fact_inverse__nonnegative__iff__nonnegative:fact_inverse__nonpositive__iff__nonpositive:fact_inverse__positive__iff__positive:fact_inverse__negative__iff__negative:fact_positive__imp__inverse__positive:fact_negative__imp__inverse__negative:fact_less__imp__inverse__less:fact_less__imp__inverse__less__neg:fact_inverse__less__imp__less:fact_inverse__less__imp__less__neg:fact_unity__coeff__ex:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J:fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J:fact_gcd__lcm__complete__lattice__nat_Obot__least:fact_zpower__zpower:fact_nat__one__le__power:fact_power__one__right:fact_power__inject__exp:fact_power__0:fact_power__gt1__lemma:fact_power__less__power__Suc:fact_power__gt1:fact_zle__antisym:fact_zless__imp__add1__zle:fact_add1__zle__eq:fact_zle__add1__eq__le:fact_poly__gcd__code:fact_mod__minus__cong:fact_mod__minus__eq:fact_neg__mod__conj:fact_neg__mod__sign:fact_pos__mod__conj:fact_pos__mod__sign:fact_mod__diff__cong:fact_mod__diff__eq:fact_mod__diff__left__eq:fact_mod__diff__right__eq:arity_Nat__Onat__Rings_Olinordered__semiring__strict:arity_Nat__Onat__Rings_Olinordered__semidom:arity_Nat__Onat__Orderings_Opreorder:arity_Nat__Onat__Orderings_Olinorder:arity_Nat__Onat__Orderings_Oorder:fact_equal__eq:fact_nat_Osize_I2_J:fact_nat_Osize_I4_J:fact_square__eq__1__iff:fact_comm__ring__1__class_Onormalizing__ring__rules_I1_J:fact_add__le__cancel__right:fact_add__le__cancel__left:fact_add__right__mono:fact_add__left__mono:fact_add__mono:fact_add__le__imp__le__right:fact_add__le__imp__le__left:fact_inverse__inverse__eq:fact_inverse__eq__iff__eq:fact_inverse__eq__imp__eq:fact_linorder__not__less:fact_linorder__not__le:fact_linorder__le__less__linear:fact_less__le__not__le:fact_leI:fact_not__leE:fact_leD:fact_order__less__imp__le:fact_order__less__le__trans:fact_xt1_I7_J:fact_order__le__less__trans:fact_xt1_I8_J:fact_add__less__cancel__right:fact_add__less__cancel__left:fact_add__strict__right__mono:fact_add__strict__left__mono:fact_add__strict__mono:fact_add__less__imp__less__right:fact_add__less__imp__less__left:fact_inverse__unique:fact_mult__left__le__imp__le:fact_mult__right__le__imp__le:fact_mult__less__imp__less__left:fact_mult__left__less__imp__less:fact_mult__less__imp__less__right:fact_mult__right__less__imp__less:fact_mult__le__less__imp__less:fact_mult__less__le__imp__less:fact_mult__strict__mono_H:fact_mult__strict__mono:fact_mult__le__cancel__left__neg:fact_mult__le__cancel__left__pos:fact_one__le__inverse__iff:fact_inverse__less__1__iff:fact_one__le__inverse:fact_dvd__imp__le:fact_one__le__power:fact_power__Suc2:fact_power__Suc:fact_power__less__imp__less__base:fact_power__le__imp__le__base:fact_zdvd__imp__le:fact_ex__least__nat__less:fact_int__one__le__iff__zero__less:fact_zless__add1__eq:fact_odd__less__0:fact_mod__mod__trivial:fact_mod__le__divisor:arity_Nat__Onat__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct:arity_Nat__Onat__Groups_Oordered__cancel__ab__semigroup__add:arity_Nat__Onat__Groups_Oordered__ab__semigroup__add__imp__le:arity_Nat__Onat__Rings_Olinordered__comm__semiring__strict:arity_Nat__Onat__Groups_Oordered__ab__semigroup__add:arity_Nat__Onat__Groups_Oordered__comm__monoid__add:arity_Nat__Onat__Groups_Ocancel__ab__semigroup__add:arity_Nat__Onat__Rings_Oordered__cancel__semiring:arity_Nat__Onat__Rings_Oordered__comm__semiring:arity_Nat__Onat__Groups_Ocancel__semigroup__add:arity_Nat__Onat__Rings_Olinordered__semiring:arity_Nat__Onat__Groups_Ocomm__monoid__mult:arity_Nat__Onat__Rings_Oordered__semiring:arity_Nat__Onat__Rings_Ono__zero__divisors:arity_Nat__Onat__Divides_Osemiring__div:arity_Nat__Onat__Rings_Ozero__neq__one:arity_Nat__Onat__Groups_Omonoid__mult:arity_Nat__Onat__Orderings_Oord:arity_Nat__Onat__Power_Opower:arity_Nat__Onat__Groups_Oone:arity_Nat__Onat__Rings_Odvd:arity_Nat__Onat__HOL_Oequal:fact_equal:fact_eq__equal:fact_less__1__mult:fact_add__nonpos__neg:fact_add__neg__nonpos:fact_add__strict__increasing2:fact_add__strict__increasing:fact_add__nonneg__pos:fact_add__pos__nonneg:fact_zero__less__two:fact_order__1:fact_one__less__power:fact_power__dvd__imp__le:fact_power__mult:fact_zero__le__power:fact_power__mono:fact_zero__less__power:fact_nonzero__power__inverse:fact_power__inject__base:fact_power__0__left:fact_power__Suc__less:fact_power__strict__decreasing:fact_power__increasing__iff:fact_power__le__imp__le__exp:fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J:fact_Suc__times__mod__eq:fact_mod__pos__neg__trivial:fact_realpow__minus__mult:fact_one__less__inverse:fact_inverse__le__1__iff:fact_one__less__inverse__iff:fact_realpow__Suc__le__self:fact_power__strict__mono:fact_power__minus:fact_power__Suc__less__one:fact_le__fun__def:fact_le__funD:fact_le__funE:fact_uminus__apply:fact_less__fun__def:fact_le__imp__inverse__le:fact_le__imp__inverse__le__neg:fact_inverse__le__imp__le:fact_inverse__le__imp__le__neg:fact_power__inverse:fact_z3mod__def:fact_inf__period_I3_J:fact_inf__period_I4_J:arity_fun__Lattices_Oboolean__algebra:arity_fun__Orderings_Opreorder:arity_fun__Orderings_Oorder:arity_fun__Orderings_Oord:arity_fun__Groups_Ouminus:arity_HOL__Obool__Lattices_Oboolean__algebra:arity_HOL__Obool__Orderings_Opreorder:arity_HOL__Obool__Orderings_Oorder:arity_HOL__Obool__Orderings_Oord:arity_HOL__Obool__Groups_Ouminus:arity_HOL__Obool__HOL_Oequal:fact_power__0__Suc:fact_power__power__power:fact_power__eq__0__iff:arity_HOL__Obool__Enum_Oenum:arity_fun__Enum_Oenum:arity_fun__HOL_Oequal (1167)
% SZS status THM for /tmp/SystemOnTPTP15995/SWW185+1.tptp
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.28s, total lost is 2.19s
% found
% SZS output start Solution for /tmp/SystemOnTPTP15995/SWW185+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 19070
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.011 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:![X3]:![X4]:(class_Rings_Ocomm__semiring__0(X4)=>(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4),c_Polynomial_Osmult(X4,X3,X2),c_Polynomial_OpCons(X4,X1,X2))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4))=>X2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))),file('/tmp/SRASS.s.p', fact_offset__poly__eq__0__lemma)).
% fof(2, axiom,![X5]:![X2]:![X1]:![X4]:(class_Rings_Ocomm__semiring__0(X4)=>c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,c_Polynomial_OpCons(X4,X1,X2),X5)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4),c_Polynomial_Osmult(X4,X5,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,X2,X5)),c_Polynomial_OpCons(X4,X1,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,X2,X5)))),file('/tmp/SRASS.s.p', fact_offset__poly__pCons)).
% fof(10, axiom,class_Rings_Ocomm__semiring__0(t_a),file('/tmp/SRASS.s.p', tfree_0)).
% fof(11, axiom,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),file('/tmp/SRASS.s.p', conj_1)).
% fof(12, axiom,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=>v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),file('/tmp/SRASS.s.p', conj_0)).
% fof(14, axiom,![X5]:![X1]:![X4]:(class_Rings_Ocomm__semiring__0(X4)=>c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,c_Polynomial_OpCons(X4,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4))),X5)=c_Polynomial_OpCons(X4,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))),file('/tmp/SRASS.s.p', fact_offset__poly__single)).
% fof(16, conjecture,c_Polynomial_OpCons(t_a,v_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),file('/tmp/SRASS.s.p', conj_2)).
% fof(17, negated_conjecture,~(c_Polynomial_OpCons(t_a,v_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(assume_negation,[status(cth)],[16])).
% fof(18, negated_conjecture,~(c_Polynomial_OpCons(t_a,v_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(fof_simplification,[status(thm)],[17,theory(equality)])).
% fof(19, plain,![X1]:![X2]:![X3]:![X4]:(~(class_Rings_Ocomm__semiring__0(X4))|(~(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4),c_Polynomial_Osmult(X4,X3,X2),c_Polynomial_OpCons(X4,X1,X2))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))|X2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))),inference(fof_nnf,[status(thm)],[1])).
% fof(20, plain,![X5]:![X6]:![X7]:![X8]:(~(class_Rings_Ocomm__semiring__0(X8))|(~(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X8),c_Polynomial_Osmult(X8,X7,X6),c_Polynomial_OpCons(X8,X5,X6))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X8)))|X6=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X8)))),inference(variable_rename,[status(thm)],[19])).
% cnf(21,plain,(X1=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))|c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X2),c_Polynomial_Osmult(X2,X3,X1),c_Polynomial_OpCons(X2,X4,X1))!=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))|~class_Rings_Ocomm__semiring__0(X2)),inference(split_conjunct,[status(thm)],[20])).
% fof(22, plain,![X5]:![X2]:![X1]:![X4]:(~(class_Rings_Ocomm__semiring__0(X4))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,c_Polynomial_OpCons(X4,X1,X2),X5)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4),c_Polynomial_Osmult(X4,X5,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,X2,X5)),c_Polynomial_OpCons(X4,X1,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,X2,X5)))),inference(fof_nnf,[status(thm)],[2])).
% fof(23, plain,![X6]:![X7]:![X8]:![X9]:(~(class_Rings_Ocomm__semiring__0(X9))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X9,c_Polynomial_OpCons(X9,X8,X7),X6)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X9),c_Polynomial_Osmult(X9,X6,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X9,X7,X6)),c_Polynomial_OpCons(X9,X8,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X9,X7,X6)))),inference(variable_rename,[status(thm)],[22])).
% cnf(24,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,c_Polynomial_OpCons(X1,X2,X3),X4)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),c_Polynomial_Osmult(X1,X4,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,X3,X4)),c_Polynomial_OpCons(X1,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,X3,X4)))|~class_Rings_Ocomm__semiring__0(X1)),inference(split_conjunct,[status(thm)],[23])).
% cnf(49,plain,(class_Rings_Ocomm__semiring__0(t_a)),inference(split_conjunct,[status(thm)],[10])).
% cnf(50,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(split_conjunct,[status(thm)],[11])).
% fof(51, plain,(~(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(fof_nnf,[status(thm)],[12])).
% cnf(52,plain,(v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)!=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(split_conjunct,[status(thm)],[51])).
% fof(56, plain,![X5]:![X1]:![X4]:(~(class_Rings_Ocomm__semiring__0(X4))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X4,c_Polynomial_OpCons(X4,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4))),X5)=c_Polynomial_OpCons(X4,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))),inference(fof_nnf,[status(thm)],[14])).
% fof(57, plain,![X6]:![X7]:![X8]:(~(class_Rings_Ocomm__semiring__0(X8))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X8,c_Polynomial_OpCons(X8,X7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X8))),X6)=c_Polynomial_OpCons(X8,X7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X8)))),inference(variable_rename,[status(thm)],[56])).
% cnf(58,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,c_Polynomial_OpCons(X1,X2,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X3)=c_Polynomial_OpCons(X1,X2,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)))|~class_Rings_Ocomm__semiring__0(X1)),inference(split_conjunct,[status(thm)],[57])).
% cnf(62,negated_conjecture,(c_Polynomial_OpCons(t_a,v_a,v_p)!=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(split_conjunct,[status(thm)],[18])).
% cnf(66,plain,(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))=c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,X2,X3)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,c_Polynomial_OpCons(X1,X4,X2),X3)!=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))|~class_Rings_Ocomm__semiring__0(X1)),inference(spm,[status(thm)],[21,24,theory(equality)])).
% cnf(80,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|~class_Rings_Ocomm__semiring__0(t_a)),inference(spm,[status(thm)],[66,50,theory(equality)])).
% cnf(82,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|$false),inference(rw,[status(thm)],[80,49,theory(equality)])).
% cnf(83,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),inference(cn,[status(thm)],[82,theory(equality)])).
% cnf(85,plain,(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=v_p|$false),inference(rw,[status(thm)],[52,83,theory(equality)])).
% cnf(86,plain,(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=v_p),inference(cn,[status(thm)],[85,theory(equality)])).
% cnf(96,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X1,v_p),X2)=c_Polynomial_OpCons(t_a,X1,v_p)|~class_Rings_Ocomm__semiring__0(t_a)),inference(spm,[status(thm)],[58,86,theory(equality)])).
% cnf(98,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h)=v_p),inference(rw,[status(thm)],[50,86,theory(equality)])).
% cnf(99,negated_conjecture,(c_Polynomial_OpCons(t_a,v_a,v_p)!=v_p),inference(rw,[status(thm)],[62,86,theory(equality)])).
% cnf(108,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X1,v_p),X2)=c_Polynomial_OpCons(t_a,X1,v_p)|$false),inference(rw,[status(thm)],[96,49,theory(equality)])).
% cnf(109,plain,(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X1,v_p),X2)=c_Polynomial_OpCons(t_a,X1,v_p)),inference(cn,[status(thm)],[108,theory(equality)])).
% cnf(143,plain,(c_Polynomial_OpCons(t_a,v_a,v_p)=v_p),inference(rw,[status(thm)],[98,109,theory(equality)])).
% cnf(144,plain,($false),inference(sr,[status(thm)],[143,99,theory(equality)])).
% cnf(145,plain,($false),144,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 50
% # ...of these trivial : 0
% # ...subsumed : 1
% # ...remaining for further processing: 49
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 6
% # Generated clauses : 32
% # ...of the previous two non-trivial : 29
% # Contextual simplify-reflections : 1
% # Paramodulations : 32
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 25
% # Positive orientable unit clauses: 7
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 17
% # Current number of unprocessed clauses: 10
% # ...number of literals in the above : 21
% # Clause-clause subsumption calls (NU) : 17
% # Rec. Clause-clause subsumption calls : 17
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 4
% # Indexed BW rewrite successes : 4
% # Backwards rewriting index: 33 leaves, 1.36+/-1.039 terms/leaf
% # Paramod-from index: 16 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 29 leaves, 1.28+/-0.783 terms/leaf
% # -------------------------------------------------
% # User time : 0.012 s
% # System time : 0.003 s
% # Total time : 0.015 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.12 CPU 0.17 WC
% FINAL PrfWatch: 0.12 CPU 0.17 WC
% SZS output end Solution for /tmp/SystemOnTPTP15995/SWW185+1.tptp
%
%------------------------------------------------------------------------------