%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ALG419-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:56:04 AM UTC 2026
% Result : Unsatisfiable 81.86s 12.54s
% Output : CNFRefutation 81.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 57
% Syntax : Number of clauses : 252 ( 89 unt; 30 nHn; 128 RR)
% Number of literals : 477 ( 203 equ; 213 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-3 aty)
% Number of variables : 424 ( 41 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_dvd__mult__right_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X4,X2,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__mult__right_0) ).
cnf(cls_s_0,axiom,
v_pa____ = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_s_0) ).
cnf(clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__semiring__1,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__semiring__1) ).
cnf(clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
cnf(cls_dvd__triv__left_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,c_HOL_Otimes__class_Otimes(X2,X3,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__triv__left_0) ).
cnf(clsarity_Polynomial__Opoly__Divides_Osemiring__div,axiom,
( ~ class_Ring__and__Field_Ofield(X1)
| class_Divides_Osemiring__div(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Polynomial__Opoly__Divides_Osemiring__div) ).
cnf(cls_dvd__mult__div__cancel_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_HOL_Otimes__class_Otimes(X2,c_Divides_Odiv__class_Odiv(X3,X2,X1),X1) = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__mult__div__cancel_0) ).
cnf(clsarity_Complex__Ocomplex__Ring__and__Field_Ofield,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
cnf(cls_Suc__leI_0,axiom,
( ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_lessequals(c_Suc(X1),X2,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__leI_0) ).
cnf(cls_mod__self_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(X2,X2,X1) = c_HOL_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__self_0) ).
cnf(cls_div__mult__self2__is__id_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| X3 = c_HOL_Ozero__class_Ozero(X1)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X3,X1),X3,X1) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_div__mult__self2__is__id_0) ).
cnf(cls_sne_0,axiom,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sne_0) ).
cnf(cls_le__SucE_0,axiom,
( ~ c_lessequals(X1,c_Suc(X2),tc_nat)
| c_lessequals(X1,X2,tc_nat)
| X1 = c_Suc(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__SucE_0) ).
cnf(cls_gr0I_0,axiom,
( X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr0I_0) ).
cnf(cls_nat_Osimps_I3_J_0,axiom,
c_Suc(X1) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
cnf(cls_dvd__eq__mod__eq__0_1,axiom,
( c_Divides_Odiv__class_Omod(X2,X3,X1) != c_HOL_Ozero__class_Ozero(X1)
| ~ class_Divides_Osemiring__div(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__eq__mod__eq__0_1) ).
cnf(cls_class__semiring_Osemiring__rules_I16_J_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X3,X1),X4,X1) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I16_J_0) ).
cnf(cls_class__semiring_Omul__a_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X3,X1),X4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Omul__a_0) ).
cnf(cls_not__less__eq_1,axiom,
( ~ c_HOL_Oord__class_Oless(X2,c_Suc(X1),tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
cnf(cls_Suc__le__eq_0,axiom,
( ~ c_lessequals(c_Suc(X1),X2,tc_nat)
| c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__le__eq_0) ).
cnf(cls_conjecture_2,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(cls_conjecture_0,negated_conjecture,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_dvd__imp__mod__0_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(X2,X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__imp__mod__0_0) ).
cnf(cls_class__semiring_Omul__c_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,X3,X1) = c_HOL_Otimes__class_Otimes(X3,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Omul__c_0) ).
cnf(cls_mod__poly__less_0,axiom,
( ~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X3,X1),tc_nat)
| ~ class_Ring__and__Field_Ofield(X1)
| c_Divides_Odiv__class_Omod(X2,X3,tc_Polynomial_Opoly(X1)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__poly__less_0) ).
cnf(cls_nat__neq__iff_0,axiom,
( X2 = X1
| c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__neq__iff_0) ).
cnf(cls_pne_0,axiom,
v_pa____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pne_0) ).
cnf(cls_minus__dvd__iff_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(X2,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_minus__dvd__iff_0) ).
cnf(cls_not__less__eq_0,axiom,
( c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,c_Suc(X2),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_0) ).
cnf(clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__ring__1,axiom,
( ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| class_Ring__and__Field_Ocomm__ring__1(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__ring__1) ).
cnf(clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__ring__1,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__ring__1) ).
cnf(cls_degree__1_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Polynomial_Odegree(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(X1)),X1) = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_degree__1_0) ).
cnf(cls_less__not__refl_0,axiom,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
cnf(cls_mod__div__trivial_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Odiv(c_Divides_Odiv__class_Omod(X2,X3,X1),X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__div__trivial_0) ).
cnf(cls_mult__poly__0__left_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__0(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X2,tc_Polynomial_Opoly(X1)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__poly__0__left_0) ).
cnf(cls_square__eq__iff_1,axiom,
( ~ class_Ring__and__Field_Oidom(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(X2,X1),c_HOL_Ouminus__class_Ouminus(X2,X1),X1) = c_HOL_Otimes__class_Otimes(X2,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_square__eq__iff_1) ).
cnf(cls_mod__div__decomp_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| X2 = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X3,X1),c_Divides_Odiv__class_Omod(X2,X3,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__div__decomp_0) ).
cnf(clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0) ).
cnf(cls_dvd__mult__left_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__mult__left_0) ).
cnf(cls_class__semiring_Osemiring__rules_I3_J_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X3,X2,X1),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X3,c_HOL_Oone__class_Oone(X1),X1),X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I3_J_0) ).
cnf(clsarity_Polynomial__Opoly__Ring__and__Field_Oidom,axiom,
( ~ class_Ring__and__Field_Oidom(X1)
| class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Polynomial__Opoly__Ring__and__Field_Oidom) ).
cnf(cls_dvd__minus__iff_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X2,c_HOL_Ouminus__class_Ouminus(X3,X1),X1)
| ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__minus__iff_0) ).
cnf(cls_mod__div__equality2_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X2,c_Divides_Odiv__class_Odiv(X3,X2,X1),X1),c_Divides_Odiv__class_Omod(X3,X2,X1),X1) = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__div__equality2_0) ).
cnf(clsarity_Complex__Ocomplex__Ring__and__Field_Oidom,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Oidom) ).
cnf(cls_class__semiring_Osemiring__rules_I19_J_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1) = c_HOL_Otimes__class_Otimes(X3,c_HOL_Otimes__class_Otimes(X2,X4,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I19_J_0) ).
cnf(cls_dvd__div__mult_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X4,X1) = c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__div__mult_0) ).
cnf(cls_dvd__0__left_0,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(X1),X2,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| X2 = c_HOL_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dvd__0__left_0) ).
cnf(cls_div__mult__self1__is__id_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| X2 = c_HOL_Ozero__class_Ozero(X1)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X3,X1),X2,X1) = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_div__mult__self1__is__id_0) ).
cnf(cls_mod__mult__self1__is__0_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X2,X3,X1),X2,X1) = c_HOL_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__mult__self1__is__0_0) ).
cnf(cls_semiring__div__class_Omod__div__equality_H_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_HOL_Oplus__class_Oplus(c_Divides_Odiv__class_Omod(X2,X3,X1),c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X3,X1),X1) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_semiring__div__class_Omod__div__equality_H_0) ).
cnf(cls_mod__mult__self2__is__0_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X2,X3,X1),X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__mult__self2__is__0_0) ).
cnf(cls_square__eq__iff_0,axiom,
( c_HOL_Otimes__class_Otimes(X2,X2,X1) != c_HOL_Otimes__class_Otimes(X3,X3,X1)
| ~ class_Ring__and__Field_Oidom(X1)
| X2 = X3
| X2 = c_HOL_Ouminus__class_Ouminus(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_square__eq__iff_0) ).
cnf(cls_mod__mult__self2_0,axiom,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1),X3,X1) = c_Divides_Odiv__class_Omod(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__mult__self2_0) ).
cnf(cls_natgb_Oadd__r0__iff_0,axiom,
( X1 != c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)
| X2 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_natgb_Oadd__r0__iff_0) ).
cnf(cls_degree__mult__eq_0,axiom,
( ~ class_Ring__and__Field_Oidom(X1)
| X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| X3 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X2,X3,tc_Polynomial_Opoly(X1)),X1) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X3,X1),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_degree__mult__eq_0) ).
cnf(cls_degree__linear__power_0,axiom,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X2,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(X1),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X1),X1),X3,tc_Polynomial_Opoly(X1)),X1) = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_degree__linear__power_0) ).
cnf(cls_oa_0,axiom,
c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_oa_0) ).
cnf(c_0_57,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X4,X2,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__mult__right_0]) ).
cnf(c_0_58,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X4,X2,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
c_0_57 ).
cnf(c_0_59,axiom,
v_pa____ = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
cls_s_0 ).
cnf(c_0_60,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(X1)) ),
inference(fof_simplification,[status(thm)],[clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__semiring__1]) ).
cnf(c_0_61,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_62,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(X1)) ),
c_0_60 ).
cnf(c_0_63,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1 ).
cnf(c_0_64,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,c_HOL_Otimes__class_Otimes(X2,X3,X1),X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__triv__left_0]) ).
cnf(c_0_65,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_62]),c_0_63])]) ).
cnf(c_0_66,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,c_HOL_Otimes__class_Otimes(X2,X3,X1),X1) ),
c_0_64 ).
cnf(c_0_67,plain,
( ~ class_Ring__and__Field_Ofield(X1)
| class_Divides_Osemiring__div(tc_Polynomial_Opoly(X1)) ),
inference(fof_simplification,[status(thm)],[clsarity_Polynomial__Opoly__Divides_Osemiring__div]) ).
cnf(c_0_68,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_HOL_Otimes__class_Otimes(X2,c_Divides_Odiv__class_Odiv(X3,X2,X1),X1) = X3 ),
inference(fof_simplification,[status(thm)],[cls_dvd__mult__div__cancel_0]) ).
cnf(c_0_69,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_65,c_0_66]) ).
cnf(c_0_70,plain,
( ~ class_Ring__and__Field_Ofield(X1)
| class_Divides_Osemiring__div(tc_Polynomial_Opoly(X1)) ),
c_0_67 ).
cnf(c_0_71,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
clsarity_Complex__Ocomplex__Ring__and__Field_Ofield ).
cnf(c_0_72,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_lessequals(c_Suc(X1),X2,tc_nat) ),
inference(fof_simplification,[status(thm)],[cls_Suc__leI_0]) ).
cnf(c_0_73,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(X2,X2,X1) = c_HOL_Ozero__class_Ozero(X1) ),
inference(fof_simplification,[status(thm)],[cls_mod__self_0]) ).
cnf(c_0_74,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_HOL_Otimes__class_Otimes(X2,c_Divides_Odiv__class_Odiv(X3,X2,X1),X1) = X3 ),
c_0_68 ).
cnf(c_0_75,plain,
c_Ring__and__Field_Odvd__class_Odvd(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_62]),c_0_63])]) ).
cnf(c_0_76,plain,
class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_77,plain,
( ~ class_Divides_Osemiring__div(X1)
| X3 = c_HOL_Ozero__class_Ozero(X1)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X3,X1),X3,X1) = X2 ),
inference(fof_simplification,[status(thm)],[cls_div__mult__self2__is__id_0]) ).
cnf(c_0_78,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(fof_simplification,[status(thm)],[cls_sne_0]) ).
cnf(c_0_79,plain,
( ~ c_lessequals(X1,c_Suc(X2),tc_nat)
| c_lessequals(X1,X2,tc_nat)
| X1 = c_Suc(X2) ),
inference(fof_simplification,[status(thm)],[cls_le__SucE_0]) ).
cnf(c_0_80,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_lessequals(c_Suc(X1),X2,tc_nat) ),
c_0_72 ).
cnf(c_0_81,axiom,
( X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
cls_gr0I_0 ).
cnf(c_0_82,plain,
c_Suc(X1) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(fof_simplification,[status(thm)],[cls_nat_Osimps_I3_J_0]) ).
cnf(c_0_83,plain,
( c_Divides_Odiv__class_Omod(X2,X3,X1) != c_HOL_Ozero__class_Ozero(X1)
| ~ class_Divides_Osemiring__div(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__eq__mod__eq__0_1]) ).
cnf(c_0_84,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(X2,X2,X1) = c_HOL_Ozero__class_Ozero(X1) ),
c_0_73 ).
cnf(c_0_85,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X3,X1),X4,X1) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_class__semiring_Osemiring__rules_I16_J_0]) ).
cnf(c_0_86,plain,
c_HOL_Otimes__class_Otimes(v_s____,c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_75]),c_0_76])]) ).
cnf(c_0_87,plain,
( ~ class_Divides_Osemiring__div(X1)
| X3 = c_HOL_Ozero__class_Ozero(X1)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X3,X1),X3,X1) = X2 ),
c_0_77 ).
cnf(c_0_88,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
c_0_78 ).
cnf(c_0_89,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X3,X1),X4,X1) ),
inference(fof_simplification,[status(thm)],[cls_class__semiring_Omul__a_0]) ).
cnf(c_0_90,plain,
( ~ c_HOL_Oord__class_Oless(X2,c_Suc(X1),tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
inference(fof_simplification,[status(thm)],[cls_not__less__eq_1]) ).
cnf(c_0_91,plain,
( ~ c_lessequals(c_Suc(X1),X2,tc_nat)
| c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
inference(fof_simplification,[status(thm)],[cls_Suc__le__eq_0]) ).
cnf(c_0_92,plain,
( ~ c_lessequals(X1,c_Suc(X2),tc_nat)
| c_lessequals(X1,X2,tc_nat)
| X1 = c_Suc(X2) ),
c_0_79 ).
cnf(c_0_93,plain,
( c_lessequals(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat)
| X1 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(spm,[status(thm)],[c_0_80,c_0_81]) ).
cnf(c_0_94,plain,
c_Suc(X1) != c_HOL_Ozero__class_Ozero(tc_nat),
c_0_82 ).
cnf(c_0_95,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_nat),
inference(fof_simplification,[status(thm)],[cls_conjecture_2]) ).
cnf(c_0_96,plain,
( c_Divides_Odiv__class_Omod(X2,X3,X1) != c_HOL_Ozero__class_Ozero(X1)
| ~ class_Divides_Osemiring__div(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1) ),
c_0_83 ).
cnf(c_0_97,plain,
c_Divides_Odiv__class_Omod(X1,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_84,c_0_76]) ).
cnf(c_0_98,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X3,X1),X4,X1) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1) ),
c_0_85 ).
cnf(c_0_99,plain,
c_HOL_Otimes__class_Otimes(v_s____,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_87]),c_0_76])]),c_0_88]) ).
cnf(c_0_100,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X2,X3,X1),X4,X1) ),
c_0_89 ).
cnf(c_0_101,plain,
( ~ c_HOL_Oord__class_Oless(X2,c_Suc(X1),tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
c_0_90 ).
cnf(c_0_102,negated_conjecture,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),tc_nat),
cls_conjecture_0 ).
cnf(c_0_103,plain,
( ~ c_lessequals(c_Suc(X1),X2,tc_nat)
| c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
c_0_91 ).
cnf(c_0_104,plain,
( c_lessequals(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_93]),c_0_94]) ).
cnf(c_0_105,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_nat),
c_0_95 ).
cnf(c_0_106,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(X2,X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__imp__mod__0_0]) ).
cnf(c_0_107,plain,
c_Ring__and__Field_Odvd__class_Odvd(X1,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_97]),c_0_76])]) ).
cnf(c_0_108,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,X3,X1) = c_HOL_Otimes__class_Otimes(X3,X2,X1) ),
inference(fof_simplification,[status(thm)],[cls_class__semiring_Omul__c_0]) ).
cnf(c_0_109,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_98,c_0_99]) ).
cnf(c_0_110,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_100,c_0_99]) ).
cnf(c_0_111,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
inference(spm,[status(thm)],[c_0_101,c_0_102]) ).
cnf(c_0_112,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(X1) ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
cnf(c_0_113,plain,
( ~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X3,X1),tc_nat)
| ~ class_Ring__and__Field_Ofield(X1)
| c_Divides_Odiv__class_Omod(X2,X3,tc_Polynomial_Opoly(X1)) = X2 ),
inference(fof_simplification,[status(thm)],[cls_mod__poly__less_0]) ).
cnf(c_0_114,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Polynomial_Odegree(v_pa____,tc_Complex_Ocomplex),tc_nat),
inference(spm,[status(thm)],[c_0_105,c_0_59]) ).
cnf(c_0_115,axiom,
( X2 = X1
| c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
cls_nat__neq__iff_0 ).
cnf(c_0_116,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(X2,X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
c_0_106 ).
cnf(c_0_117,plain,
c_Ring__and__Field_Odvd__class_Odvd(v_s____,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_65,c_0_107]) ).
cnf(c_0_118,plain,
v_pa____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(fof_simplification,[status(thm)],[cls_pne_0]) ).
cnf(c_0_119,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,X3,X1) = c_HOL_Otimes__class_Otimes(X3,X2,X1) ),
c_0_108 ).
cnf(c_0_120,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109,c_0_62]),c_0_63])]) ).
cnf(c_0_121,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_62]),c_0_63])]) ).
cnf(c_0_122,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(X2,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_minus__dvd__iff_0]) ).
cnf(c_0_123,negated_conjecture,
( ~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Suc(X1),tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
inference(spm,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_124,axiom,
( c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,c_Suc(X2),tc_nat) ),
cls_not__less__eq_0 ).
cnf(c_0_125,plain,
( ~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X3,X1),tc_nat)
| ~ class_Ring__and__Field_Ofield(X1)
| c_Divides_Odiv__class_Omod(X2,X3,tc_Polynomial_Opoly(X1)) = X2 ),
c_0_113 ).
cnf(c_0_126,negated_conjecture,
( c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_pa____,tc_Complex_Ocomplex),c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),tc_nat)
| c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_pa____,tc_Complex_Ocomplex) ),
inference(spm,[status(thm)],[c_0_114,c_0_115]) ).
cnf(c_0_127,plain,
c_Divides_Odiv__class_Omod(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_117]),c_0_76])]) ).
cnf(c_0_128,plain,
v_pa____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
c_0_118 ).
cnf(c_0_129,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X3)
| c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(X3)) = c_HOL_Otimes__class_Otimes(X2,X1,tc_Polynomial_Opoly(X3)) ),
inference(spm,[status(thm)],[c_0_119,c_0_62]) ).
cnf(c_0_130,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(rw,[status(thm)],[c_0_120,c_0_121]) ).
cnf(c_0_131,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(X2,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
c_0_122 ).
cnf(c_0_132,plain,
( ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| class_Ring__and__Field_Ocomm__ring__1(tc_Polynomial_Opoly(X1)) ),
inference(fof_simplification,[status(thm)],[clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__ring__1]) ).
cnf(c_0_133,negated_conjecture,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),tc_nat) ),
inference(spm,[status(thm)],[c_0_123,c_0_124]) ).
cnf(c_0_134,negated_conjecture,
c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_pa____,tc_Complex_Ocomplex),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125,c_0_126]),c_0_127]),c_0_71])]),c_0_128]) ).
cnf(c_0_135,plain,
c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_130]),c_0_63])]) ).
cnf(c_0_136,plain,
( ~ class_Ring__and__Field_Ocomm__ring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Ouminus__class_Ouminus(X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_131,c_0_107]) ).
cnf(c_0_137,plain,
( ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| class_Ring__and__Field_Ocomm__ring__1(tc_Polynomial_Opoly(X1)) ),
c_0_132 ).
cnf(c_0_138,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__ring__1 ).
cnf(c_0_139,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_130,c_0_119]) ).
cnf(c_0_140,negated_conjecture,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,c_Polynomial_Odegree(v_pa____,tc_Complex_Ocomplex),tc_nat) ),
inference(rw,[status(thm)],[c_0_133,c_0_134]) ).
cnf(c_0_141,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Polynomial_Odegree(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(X1)),X1) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(fof_simplification,[status(thm)],[cls_degree__1_0]) ).
cnf(c_0_142,plain,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
inference(fof_simplification,[status(thm)],[cls_less__not__refl_0]) ).
cnf(c_0_143,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(rw,[status(thm)],[c_0_121,c_0_135]) ).
cnf(c_0_144,plain,
c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Ouminus__class_Ouminus(X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_136,c_0_137]),c_0_138])]) ).
cnf(c_0_145,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rw,[status(thm)],[c_0_139,c_0_135]) ).
cnf(c_0_146,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Odiv(c_Divides_Odiv__class_Omod(X2,X3,X1),X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
inference(fof_simplification,[status(thm)],[cls_mod__div__trivial_0]) ).
cnf(c_0_147,negated_conjecture,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat)
| c_Divides_Odiv__class_Omod(X1,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125,c_0_140]),c_0_71])]) ).
cnf(c_0_148,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Polynomial_Odegree(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(X1)),X1) = c_HOL_Ozero__class_Ozero(tc_nat) ),
c_0_141 ).
cnf(c_0_149,plain,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
c_0_142 ).
cnf(c_0_150,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__0(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X2,tc_Polynomial_Opoly(X1)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
inference(fof_simplification,[status(thm)],[cls_mult__poly__0__left_0]) ).
cnf(c_0_151,plain,
( ~ class_Ring__and__Field_Oidom(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(X2,X1),c_HOL_Ouminus__class_Ouminus(X2,X1),X1) = c_HOL_Otimes__class_Otimes(X2,X2,X1) ),
inference(fof_simplification,[status(thm)],[cls_square__eq__iff_1]) ).
cnf(c_0_152,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_98,c_0_143]) ).
cnf(c_0_153,plain,
c_HOL_Otimes__class_Otimes(X1,c_Divides_Odiv__class_Odiv(c_HOL_Ouminus__class_Ouminus(X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ouminus__class_Ouminus(X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_144]),c_0_76])]) ).
cnf(c_0_154,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_145,c_0_62]),c_0_63])]) ).
cnf(c_0_155,plain,
( ~ class_Divides_Osemiring__div(X1)
| X2 = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X3,X1),c_Divides_Odiv__class_Omod(X2,X3,X1),X1) ),
inference(fof_simplification,[status(thm)],[cls_mod__div__decomp_0]) ).
cnf(c_0_156,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Odiv(c_Divides_Odiv__class_Omod(X2,X3,X1),X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
c_0_146 ).
cnf(c_0_157,negated_conjecture,
c_Divides_Odiv__class_Omod(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_147,c_0_148]),c_0_63])]),c_0_149]) ).
cnf(c_0_158,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__0(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X2,tc_Polynomial_Opoly(X1)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
c_0_150 ).
cnf(c_0_159,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0 ).
cnf(c_0_160,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__mult__left_0]) ).
cnf(c_0_161,plain,
( ~ class_Ring__and__Field_Oidom(X1)
| c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(X2,X1),c_HOL_Ouminus__class_Ouminus(X2,X1),X1) = c_HOL_Otimes__class_Otimes(X2,X2,X1) ),
c_0_151 ).
cnf(c_0_162,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_152,c_0_62]),c_0_63])]) ).
cnf(c_0_163,plain,
c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,c_Divides_Odiv__class_Odiv(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_135,c_0_153]) ).
cnf(c_0_164,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_98,c_0_154]) ).
cnf(c_0_165,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X3,X2,X1),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X3,c_HOL_Oone__class_Oone(X1),X1),X2,X1) ),
inference(fof_simplification,[status(thm)],[cls_class__semiring_Osemiring__rules_I3_J_0]) ).
cnf(c_0_166,plain,
( ~ class_Divides_Osemiring__div(X1)
| X2 = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X3,X1),c_Divides_Odiv__class_Omod(X2,X3,X1),X1) ),
c_0_155 ).
cnf(c_0_167,negated_conjecture,
c_Divides_Odiv__class_Odiv(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_156,c_0_157]),c_0_76])]) ).
cnf(c_0_168,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_158,c_0_159]) ).
cnf(c_0_169,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
c_0_160 ).
cnf(c_0_170,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X2)
| ~ class_Ring__and__Field_Oidom(X2)
| c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(X1,X2),c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(X1,X2),X3,X2),X2) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X1,X2),X3,X2) ),
inference(spm,[status(thm)],[c_0_100,c_0_161]) ).
cnf(c_0_171,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_162,c_0_153]),c_0_163]) ).
cnf(c_0_172,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_s____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164,c_0_62]),c_0_63])]) ).
cnf(c_0_173,plain,
( ~ class_Ring__and__Field_Oidom(X1)
| class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(X1)) ),
inference(fof_simplification,[status(thm)],[clsarity_Polynomial__Opoly__Ring__and__Field_Oidom]) ).
cnf(c_0_174,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X3,X2,X1),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X3,c_HOL_Oone__class_Oone(X1),X1),X2,X1) ),
c_0_165 ).
cnf(c_0_175,negated_conjecture,
c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_166,c_0_157]),c_0_167]),c_0_168]),c_0_76])]) ).
cnf(c_0_176,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X2,c_HOL_Ouminus__class_Ouminus(X3,X1),X1)
| ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__minus__iff_0]) ).
cnf(c_0_177,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_169,c_0_144]) ).
cnf(c_0_178,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X2,c_Divides_Odiv__class_Odiv(X3,X2,X1),X1),c_Divides_Odiv__class_Omod(X3,X2,X1),X1) = X3 ),
inference(fof_simplification,[status(thm)],[cls_mod__div__equality2_0]) ).
cnf(c_0_179,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_171]),c_0_172]),c_0_99]) ).
cnf(c_0_180,plain,
( ~ class_Ring__and__Field_Oidom(X1)
| class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(X1)) ),
c_0_173 ).
cnf(c_0_181,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
clsarity_Complex__Ocomplex__Ring__and__Field_Oidom ).
cnf(c_0_182,negated_conjecture,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_174,c_0_175]),c_0_168]) ).
cnf(c_0_183,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X2,c_HOL_Ouminus__class_Ouminus(X3,X1),X1)
| ~ class_Ring__and__Field_Ocomm__ring__1(X1)
| c_Ring__and__Field_Odvd__class_Odvd(X2,X3,X1) ),
c_0_176 ).
cnf(c_0_184,plain,
c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_62]),c_0_63])]) ).
cnf(c_0_185,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X2,c_Divides_Odiv__class_Odiv(X3,X2,X1),X1),c_Divides_Odiv__class_Omod(X3,X2,X1),X1) = X3 ),
c_0_178 ).
cnf(c_0_186,plain,
c_HOL_Otimes__class_Otimes(X1,c_Divides_Odiv__class_Odiv(X1,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_107]),c_0_76])]) ).
cnf(c_0_187,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1) = c_HOL_Otimes__class_Otimes(X3,c_HOL_Otimes__class_Otimes(X2,X4,X1),X1) ),
inference(fof_simplification,[status(thm)],[cls_class__semiring_Osemiring__rules_I19_J_0]) ).
cnf(c_0_188,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_179,c_0_180]),c_0_181])]) ).
cnf(c_0_189,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X4,X1) = c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__div__mult_0]) ).
cnf(c_0_190,negated_conjecture,
c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_182,c_0_62]),c_0_63])]) ).
cnf(c_0_191,plain,
( ~ class_Ring__and__Field_Ocomm__ring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_183,c_0_184]) ).
cnf(c_0_192,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_185,c_0_186]),c_0_97]),c_0_76])]) ).
cnf(c_0_193,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1) = c_HOL_Otimes__class_Otimes(X3,c_HOL_Otimes__class_Otimes(X2,X4,X1),X1) ),
c_0_187 ).
cnf(c_0_194,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_62]),c_0_63])]) ).
cnf(c_0_195,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(X1),X2,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| X2 = c_HOL_Ozero__class_Ozero(X1) ),
inference(fof_simplification,[status(thm)],[cls_dvd__0__left_0]) ).
cnf(c_0_196,plain,
( ~ class_Divides_Osemiring__div(X1)
| X2 = c_HOL_Ozero__class_Ozero(X1)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X3,X1),X2,X1) = X3 ),
inference(fof_simplification,[status(thm)],[cls_div__mult__self1__is__id_0]) ).
cnf(c_0_197,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(X3,X2,X1)
| ~ class_Divides_Osemiring__div(X1)
| c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X4,X1) = c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X4,X1),X3,X1) ),
c_0_189 ).
cnf(c_0_198,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X2,X3,X1),X2,X1) = c_HOL_Ozero__class_Ozero(X1) ),
inference(fof_simplification,[status(thm)],[cls_mod__mult__self1__is__0_0]) ).
cnf(c_0_199,negated_conjecture,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_119,c_0_190]) ).
cnf(c_0_200,plain,
c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_137]),c_0_138])]) ).
cnf(c_0_201,negated_conjecture,
c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(rw,[status(thm)],[c_0_190,c_0_192]) ).
cnf(c_0_202,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_193,c_0_194]) ).
cnf(c_0_203,plain,
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(X1),X2,X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| X2 = c_HOL_Ozero__class_Ozero(X1) ),
c_0_195 ).
cnf(c_0_204,plain,
( ~ class_Divides_Osemiring__div(X1)
| X2 = c_HOL_Ozero__class_Ozero(X1)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X2,X3,X1),X2,X1) = X3 ),
c_0_196 ).
cnf(c_0_205,plain,
c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_197,c_0_117]),c_0_76])]) ).
cnf(c_0_206,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_HOL_Oplus__class_Oplus(c_Divides_Odiv__class_Omod(X2,X3,X1),c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X3,X1),X1) = X2 ),
inference(fof_simplification,[status(thm)],[cls_semiring__div__class_Omod__div__equality_H_0]) ).
cnf(c_0_207,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X2,X3,X1),X2,X1) = c_HOL_Ozero__class_Ozero(X1) ),
c_0_198 ).
cnf(c_0_208,negated_conjecture,
c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_199,c_0_62]),c_0_63])]) ).
cnf(c_0_209,negated_conjecture,
c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_200,c_0_201]) ).
cnf(c_0_210,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X2,X3,X1),X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
inference(fof_simplification,[status(thm)],[cls_mod__mult__self2__is__0_0]) ).
cnf(c_0_211,plain,
c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_202,c_0_62]),c_0_63])]) ).
cnf(c_0_212,plain,
( c_HOL_Otimes__class_Otimes(X2,X2,X1) != c_HOL_Otimes__class_Otimes(X3,X3,X1)
| ~ class_Ring__and__Field_Oidom(X1)
| X2 = X3
| X2 = c_HOL_Ouminus__class_Ouminus(X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_square__eq__iff_0]) ).
cnf(c_0_213,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_203,c_0_144]) ).
cnf(c_0_214,plain,
( ~ class_Divides_Osemiring__div(X4)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X4)
| c_HOL_Otimes__class_Otimes(X1,X2,X4) = c_HOL_Ozero__class_Ozero(X4)
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X4),X4),c_HOL_Otimes__class_Otimes(X1,X2,X4),X4) = X3 ),
inference(spm,[status(thm)],[c_0_204,c_0_100]) ).
cnf(c_0_215,plain,
c_HOL_Otimes__class_Otimes(v_s____,c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(rw,[status(thm)],[c_0_86,c_0_205]) ).
cnf(c_0_216,plain,
c_HOL_Otimes__class_Otimes(v_s____,c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_pa____,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_117]),c_0_76])]) ).
cnf(c_0_217,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1),X3,X1) = c_Divides_Odiv__class_Omod(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_mod__mult__self2_0]) ).
cnf(c_0_218,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_HOL_Oplus__class_Oplus(c_Divides_Odiv__class_Omod(X2,X3,X1),c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(X2,X3,X1),X3,X1),X1) = X2 ),
c_0_206 ).
cnf(c_0_219,negated_conjecture,
c_Divides_Odiv__class_Omod(X1,c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_207,c_0_201]),c_0_76])]) ).
cnf(c_0_220,negated_conjecture,
c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(rw,[status(thm)],[c_0_208,c_0_192]) ).
cnf(c_0_221,negated_conjecture,
c_Divides_Odiv__class_Odiv(X1,c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_209]),c_0_201]),c_0_76])]) ).
cnf(c_0_222,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X2,X3,X1),X3,X1) = c_HOL_Ozero__class_Ozero(X1) ),
c_0_210 ).
cnf(c_0_223,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ouminus__class_Ouminus(v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_204,c_0_211]),c_0_76])]),c_0_88]) ).
cnf(c_0_224,plain,
( X1 != c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)
| X2 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(fof_simplification,[status(thm)],[cls_natgb_Oadd__r0__iff_0]) ).
cnf(c_0_225,plain,
( ~ class_Ring__and__Field_Oidom(X1)
| X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| X3 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X2,X3,tc_Polynomial_Opoly(X1)),X1) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X3,X1),tc_nat) ),
inference(fof_simplification,[status(thm)],[cls_degree__mult__eq_0]) ).
cnf(c_0_226,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X2,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(X1),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X1),X1),X3,tc_Polynomial_Opoly(X1)),X1) = X3 ),
inference(fof_simplification,[status(thm)],[cls_degree__linear__power_0]) ).
cnf(c_0_227,plain,
( c_HOL_Otimes__class_Otimes(X2,X2,X1) != c_HOL_Otimes__class_Otimes(X3,X3,X1)
| ~ class_Ring__and__Field_Oidom(X1)
| X2 = X3
| X2 = c_HOL_Ouminus__class_Ouminus(X3,X1) ),
c_0_212 ).
cnf(c_0_228,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_213,c_0_62]),c_0_63])]) ).
cnf(c_0_229,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_214,c_0_215]),c_0_216]),c_0_216]),c_0_76])]),c_0_128]) ).
cnf(c_0_230,plain,
( ~ class_Divides_Osemiring__div(X1)
| c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X3,X4,X1),X1),X3,X1) = c_Divides_Odiv__class_Omod(X2,X3,X1) ),
c_0_217 ).
cnf(c_0_231,negated_conjecture,
c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_218,c_0_219]),c_0_220]),c_0_221]),c_0_76])]) ).
cnf(c_0_232,plain,
c_Divides_Odiv__class_Omod(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_222,c_0_168]),c_0_76])]) ).
cnf(c_0_233,plain,
( ~ class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_161,c_0_223]) ).
cnf(c_0_234,plain,
( X1 != c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)
| X2 = c_HOL_Ozero__class_Ozero(tc_nat) ),
c_0_224 ).
cnf(c_0_235,plain,
( ~ class_Ring__and__Field_Oidom(X1)
| X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| X3 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X2,X3,tc_Polynomial_Opoly(X1)),X1) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X3,X1),tc_nat) ),
c_0_225 ).
cnf(c_0_236,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X2,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(X1),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X1),X1),X3,tc_Polynomial_Opoly(X1)),X1) = X3 ),
c_0_226 ).
cnf(c_0_237,plain,
c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_59]),c_0_76])]),c_0_88]) ).
cnf(c_0_238,plain,
c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(fof_simplification,[status(thm)],[cls_oa_0]) ).
cnf(c_0_239,plain,
( ~ class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Otimes__class_Otimes(X1,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| X1 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_227,c_0_168]),c_0_228])]) ).
cnf(c_0_240,plain,
c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_229,c_0_62]),c_0_63])]) ).
cnf(c_0_241,negated_conjecture,
c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_230,c_0_231]),c_0_232]),c_0_76])]) ).
cnf(c_0_242,plain,
c_Divides_Odiv__class_Odiv(c_HOL_Otimes__class_Otimes(v_pa____,c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_233,c_0_180]),c_0_181])]) ).
cnf(c_0_243,plain,
( ~ class_Ring__and__Field_Oidom(X2)
| c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X3,X1,tc_Polynomial_Opoly(X2)),X2) != c_Polynomial_Odegree(X3,X2)
| X1 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| X3 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| c_Polynomial_Odegree(X1,X2) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(spm,[status(thm)],[c_0_234,c_0_235]) ).
cnf(c_0_244,plain,
c_Polynomial_Odegree(c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_236,c_0_237]),c_0_63])]) ).
cnf(c_0_245,plain,
c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat),
c_0_238 ).
cnf(c_0_246,plain,
( c_HOL_Otimes__class_Otimes(X1,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| X1 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_239,c_0_180]),c_0_181])]) ).
cnf(c_0_247,plain,
c_HOL_Otimes__class_Otimes(X1,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_166,c_0_240]),c_0_241]),c_0_192]),c_0_76])]) ).
cnf(c_0_248,plain,
c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Otimes__class_Otimes(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(v_pa____,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(rw,[status(thm)],[c_0_242,c_0_205]) ).
cnf(c_0_249,plain,
c_Divides_Odiv__class_Odiv(v_pa____,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_243,c_0_216]),c_0_244]),c_0_134]),c_0_181])]),c_0_245]),c_0_88]) ).
cnf(c_0_250,plain,
c_HOL_Otimes__class_Otimes(v_pa____,v_pa____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_246,c_0_247]),c_0_128]) ).
cnf(c_0_251,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_248,c_0_249]),c_0_168]),c_0_250]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG419-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 13:15:12 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 81.86/12.54 % Version: 3.5.1
% 81.86/12.54 % Preprocessing class: FSLMSMSMSSSNFFN.
% 81.86/12.54 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 81.86/12.54 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 81.86/12.54 % Starting new_bool_3 with 600s (2) cores
% 81.86/12.54 % Starting new_bool_1 with 300s (1) cores
% 81.86/12.54 % Starting sh5l with 300s (1) cores
% 81.86/12.54 % new_bool_3 with pid 2395632 completed with status 0
% 81.86/12.54 % Result found by new_bool_3
% 81.86/12.54 % Preprocessing class: FSLMSMSMSSSNFFN.
% 81.86/12.54 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 81.86/12.54 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 81.86/12.54 % Starting new_bool_3 with 600s (2) cores
% 81.86/12.54 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 81.86/12.54 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 81.86/12.54 % Search class: FGHSM-FSLM32-DFFFFFNN
% 81.86/12.54 % Scheduled 13 strats onto 2 cores with 600 seconds (600 total)
% 81.86/12.54 % Starting SubtermCWHack with 55s (1) cores
% 81.86/12.54 % Starting new_bool_3 with 61s (1) cores
% 81.86/12.54 % new_bool_3 with pid 2395636 completed with status 0
% 81.86/12.54 % Result found by new_bool_3
% 81.86/12.54 % Preprocessing class: FSLMSMSMSSSNFFN.
% 81.86/12.54 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 81.86/12.54 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 81.86/12.54 % Starting new_bool_3 with 600s (2) cores
% 81.86/12.54 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 81.86/12.54 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 81.86/12.54 % Search class: FGHSM-FSLM32-DFFFFFNN
% 81.86/12.54 % Scheduled 13 strats onto 2 cores with 600 seconds (600 total)
% 81.86/12.54 % Starting SubtermCWHack with 55s (1) cores
% 81.86/12.54 % Starting new_bool_3 with 61s (1) cores
% 81.86/12.54 % Preprocessing time : 0.006 s
% 81.86/12.54 % Presaturation interreduction done
% 81.86/12.54
% 81.86/12.54 % Proof found!
% 81.86/12.54 % SZS status Unsatisfiable
% 81.86/12.54 % SZS output start CNFRefutation
% See solution above
% 81.86/12.54 % Parsed axioms : 998
% 81.86/12.54 % Removed by relevancy pruning/SinE : 624
% 81.86/12.54 % Initial clauses : 374
% 81.86/12.54 % Removed in clause preprocessing : 0
% 81.86/12.54 % Initial clauses in saturation : 374
% 81.86/12.54 % Processed clauses : 47307
% 81.86/12.54 % ...of these trivial : 1737
% 81.86/12.54 % ...subsumed : 37395
% 81.86/12.54 % ...remaining for further processing : 8175
% 81.86/12.54 % Other redundant clauses eliminated : 2744
% 81.86/12.54 % Clauses deleted for lack of memory : 0
% 81.86/12.54 % Backward-subsumed : 507
% 81.86/12.54 % Backward-rewritten : 1280
% 81.86/12.54 % Generated clauses : 548502
% 81.86/12.54 % ...of the previous two non-redundant : 446011
% 81.86/12.54 % ...aggressively subsumed : 0
% 81.86/12.54 % Contextual simplify-reflections : 32
% 81.86/12.54 % Paramodulations : 545660
% 81.86/12.54 % Factorizations : 30
% 81.86/12.54 % NegExts : 0
% 81.86/12.54 % Equation resolutions : 2798
% 81.86/12.54 % Disequality decompositions : 0
% 81.86/12.54 % Total rewrite steps : 579449
% 81.86/12.54 % ...of those cached : 551612
% 81.86/12.54 % Propositional unsat checks : 1
% 81.86/12.54 % Propositional check models : 0
% 81.86/12.54 % Propositional check unsatisfiable : 0
% 81.86/12.54 % Propositional clauses : 0
% 81.86/12.54 % Propositional clauses after purity: 0
% 81.86/12.54 % Propositional unsat core size : 0
% 81.86/12.54 % Propositional preprocessing time : 0.000
% 81.86/12.54 % Propositional encoding time : 0.193
% 81.86/12.54 % Propositional solver time : 0.150
% 81.86/12.54 % Success case prop preproc time : 0.000
% 81.86/12.54 % Success case prop encoding time : 0.000
% 81.86/12.54 % Success case prop solver time : 0.000
% 81.86/12.54 % Current number of processed clauses : 6070
% 81.86/12.54 % Positive orientable unit clauses : 1561
% 81.86/12.54 % Positive unorientable unit clauses: 26
% 81.86/12.54 % Negative unit clauses : 995
% 81.86/12.54 % Non-unit-clauses : 3488
% 81.86/12.54 % Current number of unprocessed clauses: 385722
% 81.86/12.54 % ...number of literals in the above : 959286
% 81.86/12.54 % Current number of archived formulas : 0
% 81.86/12.54 % Current number of archived clauses : 2105
% 81.86/12.54 % Clause-clause subsumption calls (NU) : 1476420
% 81.86/12.54 % Rec. Clause-clause subsumption calls : 1105859
% 81.86/12.54 % Non-unit clause-clause subsumptions : 15200
% 81.86/12.54 % Unit Clause-clause subsumption calls : 330462
% 81.86/12.54 % Rewrite failures with RHS unbound : 0
% 81.86/12.54 % BW rewrite match attempts : 11005
% 81.86/12.54 % BW rewrite match successes : 985
% 81.86/12.54 % Condensation attempts : 0
% 81.86/12.54 % Condensation successes : 0
% 81.86/12.54 % Termbank termtop insertions : 11826027
% 81.86/12.54 % Search garbage collected termcells : 2518
% 81.86/12.54
% 81.86/12.54 % -------------------------------------------------
% 81.86/12.54 % User time : 11.185 s
% 81.86/12.54 % System time : 0.368 s
% 81.86/12.54 % Total time : 11.553 s
% 81.86/12.54 % Maximum resident set size: 4760 pages
% 81.86/12.54
% 81.86/12.54 % -------------------------------------------------
% 81.86/12.54 % User time : 21.968 s
% 81.86/12.54 % System time : 0.829 s
% 81.86/12.54 % Total time : 22.797 s
% 81.86/12.54 % Maximum resident set size: 5120 pages
% 81.86/12.54 % E exiting
%------------------------------------------------------------------------------