%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWW290+1 : TPTP v9.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.m4mhcLThNR true
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 05:02:33 PM UTC 2025
% Result : Theorem 151.33s 22.31s
% Output : Refutation 151.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWW290+1 : TPTP v9.2.0. Released v5.2.0.
% 0.03/0.12 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.m4mhcLThNR true
% 0.11/0.33 % Computer : n005.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Wed Oct 1 12:09:53 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.11/0.33 % Running portfolio for 300 s
% 0.11/0.33 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.34 % Number of cores: 8
% 0.11/0.34 % Python version: Python 3.6.8
% 0.11/0.34 % Running in FO mode
% 0.47/0.60 % Total configuration time : 435
% 0.47/0.60 % Estimated wc time : 1092
% 0.47/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.66 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.49/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 151.33/22.31 % Solved by fo/fo3_bce.sh.
% 151.33/22.31 % BCE start: 853
% 151.33/22.31 % BCE eliminated: 51
% 151.33/22.31 % PE start: 802
% 151.33/22.31 logic: eq
% 151.33/22.31 % PE eliminated: 4
% 151.33/22.31 % done 7891 iterations in 21.563s
% 151.33/22.31 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 151.33/22.31 % SZS output start Refutation
% 151.33/22.31 thf(v_q_type, type, v_q: $i).
% 151.33/22.31 thf(c_Groups_Otimes__class_Otimes_type, type, c_Groups_Otimes__class_Otimes:
% 151.33/22.31 $i > $i).
% 151.33/22.31 thf(c_Groups_Oone__class_Oone_type, type, c_Groups_Oone__class_Oone: $i > $i).
% 151.33/22.31 thf(c_Orderings_Oord__class_Oless_type, type, c_Orderings_Oord__class_Oless:
% 151.33/22.31 $i > $i > $i > $o).
% 151.33/22.31 thf(class_Fields_Ofield_type, type, class_Fields_Ofield: $i > $o).
% 151.33/22.31 thf(c_Groups_Ozero__class_Ozero_type, type, c_Groups_Ozero__class_Ozero:
% 151.33/22.31 $i > $i).
% 151.33/22.31 thf(tc_Nat_Onat_type, type, tc_Nat_Onat: $i).
% 151.33/22.31 thf(hAPP_type, type, hAPP: $i > $i > $i).
% 151.33/22.31 thf(tc_Complex_Ocomplex_type, type, tc_Complex_Ocomplex: $i).
% 151.33/22.31 thf(c_Polynomial_Opdivmod__rel_type, type, c_Polynomial_Opdivmod__rel:
% 151.33/22.31 $i > $i > $i > $i > $i > $o).
% 151.33/22.31 thf(c_Polynomial_Odegree_type, type, c_Polynomial_Odegree: $i > $i > $i).
% 151.33/22.31 thf(c_Polynomial_Opoly_type, type, c_Polynomial_Opoly: $i > $i > $i).
% 151.33/22.31 thf(class_Rings_Ocomm__semiring__1_type, type, class_Rings_Ocomm__semiring__1:
% 151.33/22.31 $i > $o).
% 151.33/22.31 thf(c_Polynomial_OpCons_type, type, c_Polynomial_OpCons: $i > $i > $i > $i).
% 151.33/22.31 thf(class_Rings_Ocomm__semiring__0_type, type, class_Rings_Ocomm__semiring__0:
% 151.33/22.31 $i > $o).
% 151.33/22.31 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 151.33/22.31 thf(sk__type, type, sk_: $i > $i > $i).
% 151.33/22.31 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 151.33/22.31 thf(v_a_type, type, v_a: $i).
% 151.33/22.31 thf(class_Groups_Ocomm__monoid__add_type, type, class_Groups_Ocomm__monoid__add:
% 151.33/22.31 $i > $o).
% 151.33/22.31 thf(c_Groups_Oplus__class_Oplus_type, type, c_Groups_Oplus__class_Oplus:
% 151.33/22.31 $i > $i > $i > $i).
% 151.33/22.31 thf(tc_Polynomial_Opoly_type, type, tc_Polynomial_Opoly: $i > $i).
% 151.33/22.31 thf(c_Polynomial_Osmult_type, type, c_Polynomial_Osmult: $i > $i > $i > $i).
% 151.33/22.31 thf(arity_Polynomial__Opoly__Rings_Ocomm__semiring__1, axiom,
% 151.33/22.31 (![T_1:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_1 ) =>
% 151.33/22.31 ( class_Rings_Ocomm__semiring__1 @ ( tc_Polynomial_Opoly @ T_1 ) ) ))).
% 151.33/22.31 thf(zip_derived_cl843, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ (tc_Polynomial_Opoly @ X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Polynomial__Opoly__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J, axiom,
% 151.33/22.31 (![V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_a ) @
% 151.33/22.31 ( c_Groups_Oone__class_Oone @ T_a ) ) =
% 151.33/22.31 ( V_a ) ) ))).
% 151.33/22.31 thf(zip_derived_cl106, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X1) @ X0) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ X1)) = (X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X1))),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J])).
% 151.33/22.31 thf(fact_mult__smult__left, axiom,
% 151.33/22.31 (![V_q:$i,V_p:$i,V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__0 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 ( c_Polynomial_Osmult @ T_a @ V_a @ V_p ) ) @
% 151.33/22.31 V_q ) =
% 151.33/22.31 ( c_Polynomial_Osmult @
% 151.33/22.31 T_a @ V_a @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 V_p ) @
% 151.33/22.31 V_q ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl13, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @
% 151.33/22.31 (c_Polynomial_Osmult @ X0 @ X1 @ X2)) @
% 151.33/22.31 X3)
% 151.33/22.31 = (c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @
% 151.33/22.31 X2) @
% 151.33/22.31 X3)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mult__smult__left])).
% 151.33/22.31 thf(fact_mult__smult__right, axiom,
% 151.33/22.31 (![V_q:$i,V_a:$i,V_p:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__0 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 V_p ) @
% 151.33/22.31 ( c_Polynomial_Osmult @ T_a @ V_a @ V_q ) ) =
% 151.33/22.31 ( c_Polynomial_Osmult @
% 151.33/22.31 T_a @ V_a @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 V_p ) @
% 151.33/22.31 V_q ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl12, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @ X2) @
% 151.33/22.31 (c_Polynomial_Osmult @ X0 @ X1 @ X3))
% 151.33/22.31 = (c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @
% 151.33/22.31 X2) @
% 151.33/22.31 X3)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mult__smult__right])).
% 151.33/22.31 thf(zip_derived_cl4117, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X3)) @ X1) @
% 151.33/22.31 (c_Polynomial_Osmult @ X3 @ X2 @ X0))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X3)) @
% 151.33/22.31 (c_Polynomial_Osmult @ X3 @ X2 @ X1)) @
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X3)
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X3))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl13, zip_derived_cl12])).
% 151.33/22.31 thf(zip_derived_cl4121, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (~ (class_Rings_Ocomm__semiring__0 @ X3)
% 151.33/22.31 | ((hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X3)) @
% 151.33/22.31 X1) @
% 151.33/22.31 (c_Polynomial_Osmult @ X3 @ X2 @ X0))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X3)) @
% 151.33/22.31 (c_Polynomial_Osmult @ X3 @ X2 @ X1)) @
% 151.33/22.31 X0)))),
% 151.33/22.31 inference('simplify', [status(thm)], [zip_derived_cl4117])).
% 151.33/22.31 thf(conj_0, conjecture,
% 151.33/22.31 (( c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @
% 151.33/22.31 ( tc_Polynomial_Opoly @ tc_Complex_Ocomplex ) ) @
% 151.33/22.31 v_q ) @
% 151.33/22.31 ( c_Polynomial_OpCons @
% 151.33/22.31 tc_Complex_Ocomplex @ v_a @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @
% 151.33/22.31 ( tc_Polynomial_Opoly @ tc_Complex_Ocomplex ) ) ) ))).
% 151.33/22.31 thf(zf_stmt_0, negated_conjecture,
% 151.33/22.31 (( c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q ) !=
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @
% 151.33/22.31 ( tc_Polynomial_Opoly @ tc_Complex_Ocomplex ) ) @
% 151.33/22.31 v_q ) @
% 151.33/22.31 ( c_Polynomial_OpCons @
% 151.33/22.31 tc_Complex_Ocomplex @ v_a @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @
% 151.33/22.31 ( tc_Polynomial_Opoly @ tc_Complex_Ocomplex ) ) ) )),
% 151.33/22.31 inference('cnf.neg', [status(esa)], [conj_0])).
% 151.33/22.31 thf(zip_derived_cl852, plain,
% 151.33/22.31 (((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)
% 151.33/22.31 != (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 v_q) @
% 151.33/22.31 (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ v_a @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))))),
% 151.33/22.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 151.33/22.31 thf(fact_one__poly__def, axiom,
% 151.33/22.31 (![T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_a ) =>
% 151.33/22.31 ( ( c_Groups_Oone__class_Oone @ ( tc_Polynomial_Opoly @ T_a ) ) =
% 151.33/22.31 ( c_Polynomial_OpCons @
% 151.33/22.31 T_a @ ( c_Groups_Oone__class_Oone @ T_a ) @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl105, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((c_Groups_Oone__class_Oone @ (tc_Polynomial_Opoly @ X0))
% 151.33/22.31 = (c_Polynomial_OpCons @ X0 @ (c_Groups_Oone__class_Oone @ X0) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_one__poly__def])).
% 151.33/22.31 thf(arity_Complex__Ocomplex__Fields_Ofield, axiom,
% 151.33/22.31 (class_Fields_Ofield @ tc_Complex_Ocomplex)).
% 151.33/22.31 thf(zip_derived_cl839, plain, ( (class_Fields_Ofield @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)], [arity_Complex__Ocomplex__Fields_Ofield])).
% 151.33/22.31 thf(fact_pdivmod__rel__def, axiom,
% 151.33/22.31 (![V_r_2:$i,V_qa_2:$i,V_y_2:$i,V_x_2:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Fields_Ofield @ T_a ) =>
% 151.33/22.31 ( ( c_Polynomial_Opdivmod__rel @ T_a @ V_x_2 @ V_y_2 @ V_qa_2 @ V_r_2 ) <=>
% 151.33/22.31 ( ( ( ( V_y_2 ) !=
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) =>
% 151.33/22.31 ( ( c_Orderings_Oord__class_Oless @
% 151.33/22.31 tc_Nat_Onat @ ( c_Polynomial_Odegree @ T_a @ V_r_2 ) @
% 151.33/22.31 ( c_Polynomial_Odegree @ T_a @ V_y_2 ) ) |
% 151.33/22.31 ( ( V_r_2 ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) ) ) &
% 151.33/22.31 ( ( ( V_y_2 ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) =>
% 151.33/22.31 ( ( V_qa_2 ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) ) &
% 151.33/22.31 ( ( V_x_2 ) =
% 151.33/22.31 ( c_Groups_Oplus__class_Oplus @
% 151.33/22.31 ( tc_Polynomial_Opoly @ T_a ) @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @
% 151.33/22.31 ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 V_qa_2 ) @
% 151.33/22.31 V_y_2 ) @
% 151.33/22.31 V_r_2 ) ) ) ) ))).
% 151.33/22.31 thf(zf_stmt_1, type, zip_tseitin_1 : $i > $i > $i > $o).
% 151.33/22.31 thf(zf_stmt_2, axiom,
% 151.33/22.31 (![T_a:$i,V_y_2:$i,V_qa_2:$i]:
% 151.33/22.31 ( ( zip_tseitin_1 @ T_a @ V_y_2 @ V_qa_2 ) <=>
% 151.33/22.31 ( ( ( V_y_2 ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) =>
% 151.33/22.31 ( ( V_qa_2 ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) ) ))).
% 151.33/22.31 thf(zf_stmt_3, type, zip_tseitin_0 : $i > $i > $i > $o).
% 151.33/22.31 thf(zf_stmt_4, axiom,
% 151.33/22.31 (![T_a:$i,V_y_2:$i,V_r_2:$i]:
% 151.33/22.31 ( ( zip_tseitin_0 @ T_a @ V_y_2 @ V_r_2 ) <=>
% 151.33/22.31 ( ( ( V_y_2 ) !=
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) =>
% 151.33/22.31 ( ( ( V_r_2 ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) |
% 151.33/22.31 ( c_Orderings_Oord__class_Oless @
% 151.33/22.31 tc_Nat_Onat @ ( c_Polynomial_Odegree @ T_a @ V_r_2 ) @
% 151.33/22.31 ( c_Polynomial_Odegree @ T_a @ V_y_2 ) ) ) ) ))).
% 151.33/22.31 thf(zf_stmt_5, axiom,
% 151.33/22.31 (![V_r_2:$i,V_qa_2:$i,V_y_2:$i,V_x_2:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Fields_Ofield @ T_a ) =>
% 151.33/22.31 ( ( c_Polynomial_Opdivmod__rel @ T_a @ V_x_2 @ V_y_2 @ V_qa_2 @ V_r_2 ) <=>
% 151.33/22.31 ( ( ( V_x_2 ) =
% 151.33/22.31 ( c_Groups_Oplus__class_Oplus @
% 151.33/22.31 ( tc_Polynomial_Opoly @ T_a ) @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @
% 151.33/22.31 ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 V_qa_2 ) @
% 151.33/22.31 V_y_2 ) @
% 151.33/22.31 V_r_2 ) ) &
% 151.33/22.31 ( zip_tseitin_1 @ T_a @ V_y_2 @ V_qa_2 ) &
% 151.33/22.31 ( zip_tseitin_0 @ T_a @ V_y_2 @ V_r_2 ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl643, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 151.33/22.31 (~ (c_Polynomial_Opdivmod__rel @ X0 @ X1 @ X2 @ X3 @ X4)
% 151.33/22.31 | ((X1)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @ (tc_Polynomial_Opoly @ X0) @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @
% 151.33/22.31 X3) @
% 151.33/22.31 X2) @
% 151.33/22.31 X4))
% 151.33/22.31 | ~ (class_Fields_Ofield @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 151.33/22.31 thf(zip_derived_cl3973, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((X3)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex) @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X1) @
% 151.33/22.31 X2) @
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (c_Polynomial_Opdivmod__rel @ tc_Complex_Ocomplex @ X3 @ X2 @
% 151.33/22.31 X1 @ X0))),
% 151.33/22.31 inference('dp-resolution', [status(thm)],
% 151.33/22.31 [zip_derived_cl839, zip_derived_cl643])).
% 151.33/22.31 thf(zip_derived_cl839, plain, ( (class_Fields_Ofield @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)], [arity_Complex__Ocomplex__Fields_Ofield])).
% 151.33/22.31 thf(fact_pdivmod__rel__0, axiom,
% 151.33/22.31 (![V_y:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Fields_Ofield @ T_a ) =>
% 151.33/22.31 ( c_Polynomial_Opdivmod__rel @
% 151.33/22.31 T_a @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 V_y @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl111, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 ( (c_Polynomial_Opdivmod__rel @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0)) @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0)))
% 151.33/22.31 | ~ (class_Fields_Ofield @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_pdivmod__rel__0])).
% 151.33/22.31 thf(zip_derived_cl3965, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (c_Polynomial_Opdivmod__rel @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('dp-resolution', [status(thm)],
% 151.33/22.31 [zip_derived_cl839, zip_derived_cl111])).
% 151.33/22.31 thf(zip_derived_cl22541, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex) @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl3973, zip_derived_cl3965])).
% 151.33/22.31 thf(fact_add__poly__code_I2_J, axiom,
% 151.33/22.31 (![V_p:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Groups_Ocomm__monoid__add @ T_a ) =>
% 151.33/22.31 ( ( c_Groups_Oplus__class_Oplus @
% 151.33/22.31 ( tc_Polynomial_Opoly @ T_a ) @ V_p @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) =
% 151.33/22.31 ( V_p ) ) ))).
% 151.33/22.31 thf(zip_derived_cl69, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((c_Groups_Oplus__class_Oplus @ (tc_Polynomial_Opoly @ X1) @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X1))) = (
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (class_Groups_Ocomm__monoid__add @ X1))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_add__poly__code_I2_J])).
% 151.33/22.31 thf(zip_derived_cl23295, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (class_Groups_Ocomm__monoid__add @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl22541, zip_derived_cl69])).
% 151.33/22.31 thf(arity_Complex__Ocomplex__Groups_Ocomm__monoid__add, axiom,
% 151.33/22.31 (class_Groups_Ocomm__monoid__add @ tc_Complex_Ocomplex)).
% 151.33/22.31 thf(zip_derived_cl833, plain,
% 151.33/22.31 ( (class_Groups_Ocomm__monoid__add @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Groups_Ocomm__monoid__add])).
% 151.33/22.31 thf(zip_derived_cl23310, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl23295, zip_derived_cl833])).
% 151.33/22.31 thf(zip_derived_cl12, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @ X2) @
% 151.33/22.31 (c_Polynomial_Osmult @ X0 @ X1 @ X3))
% 151.33/22.31 = (c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ (tc_Polynomial_Opoly @ X0)) @
% 151.33/22.31 X2) @
% 151.33/22.31 X3)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mult__smult__right])).
% 151.33/22.31 thf(zip_derived_cl25960, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X1 @ X0))
% 151.33/22.31 = (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl23310, zip_derived_cl12])).
% 151.33/22.31 thf(zip_derived_cl23310, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl23295, zip_derived_cl833])).
% 151.33/22.31 thf(arity_Complex__Ocomplex__Rings_Ocomm__semiring__0, axiom,
% 151.33/22.31 (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex)).
% 151.33/22.31 thf(zip_derived_cl835, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__0])).
% 151.33/22.31 thf(zip_derived_cl26003, plain,
% 151.33/22.31 (![X1 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))
% 151.33/22.31 = (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl25960, zip_derived_cl23310, zip_derived_cl835])).
% 151.33/22.31 thf(fact_poly__smult, axiom,
% 151.33/22.31 (![V_x:$i,V_p:$i,V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__0 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( c_Polynomial_Opoly @
% 151.33/22.31 T_a @ ( c_Polynomial_Osmult @ T_a @ V_a @ V_p ) ) @
% 151.33/22.31 V_x ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_a ) @
% 151.33/22.31 ( hAPP @ ( c_Polynomial_Opoly @ T_a @ V_p ) @ V_x ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl87, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ X0 @ (c_Polynomial_Osmult @ X0 @ X1 @ X2)) @
% 151.33/22.31 X3)
% 151.33/22.31 = (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @
% 151.33/22.31 (hAPP @ (c_Polynomial_Opoly @ X0 @ X2) @ X3)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_poly__smult])).
% 151.33/22.31 thf(zip_derived_cl26034, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 X1) @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl26003, zip_derived_cl87])).
% 151.33/22.31 thf(fact_mpoly__base__conv_I1_J, axiom,
% 151.33/22.31 (![V_x:$i]:
% 151.33/22.31 ( ( c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Polynomial_Opoly @
% 151.33/22.31 tc_Complex_Ocomplex @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @
% 151.33/22.31 ( tc_Polynomial_Opoly @ tc_Complex_Ocomplex ) ) ) @
% 151.33/22.31 V_x ) ))).
% 151.33/22.31 thf(zip_derived_cl90, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mpoly__base__conv_I1_J])).
% 151.33/22.31 thf(zip_derived_cl90, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mpoly__base__conv_I1_J])).
% 151.33/22.31 thf(zip_derived_cl835, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__0])).
% 151.33/22.31 thf(zip_derived_cl26056, plain,
% 151.33/22.31 (![X1 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 X1) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl26034, zip_derived_cl90, zip_derived_cl90,
% 151.33/22.31 zip_derived_cl835])).
% 151.33/22.31 thf(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J, axiom,
% 151.33/22.31 (![V_rx:$i,V_ly:$i,V_lx:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ T_a ) @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_lx ) @ V_ly ) ) @
% 151.33/22.31 V_rx ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ T_a ) @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_lx ) @ V_rx ) ) @
% 151.33/22.31 V_ly ) ) ))).
% 151.33/22.31 thf(zip_derived_cl76, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @ X3)) @
% 151.33/22.31 X2)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @ X2)) @
% 151.33/22.31 X3))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J])).
% 151.33/22.31 thf(zip_derived_cl26501, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 X1) @
% 151.33/22.31 X0)) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl26056, zip_derived_cl76])).
% 151.33/22.31 thf(zip_derived_cl26056, plain,
% 151.33/22.31 (![X1 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 X1) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl26034, zip_derived_cl90, zip_derived_cl90,
% 151.33/22.31 zip_derived_cl835])).
% 151.33/22.31 thf(arity_Complex__Ocomplex__Rings_Ocomm__semiring__1, axiom,
% 151.33/22.31 (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)).
% 151.33/22.31 thf(zip_derived_cl834, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(zip_derived_cl26550, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl26501, zip_derived_cl26056, zip_derived_cl834])).
% 151.33/22.31 thf(zip_derived_cl90, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mpoly__base__conv_I1_J])).
% 151.33/22.31 thf(fact_ext, axiom,
% 151.33/22.31 (![V_g_2:$i,V_f_2:$i]:
% 151.33/22.31 ( ( ![B_x:$i]: ( ( hAPP @ V_f_2 @ B_x ) = ( hAPP @ V_g_2 @ B_x ) ) ) =>
% 151.33/22.31 ( ( V_f_2 ) = ( V_g_2 ) ) ))).
% 151.33/22.31 thf(zip_derived_cl0, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((X1) = (X0))
% 151.33/22.31 | ((hAPP @ X1 @ (sk_ @ X1 @ X0)) != (hAPP @ X0 @ (sk_ @ X1 @ X0))))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_ext])).
% 151.33/22.31 thf(zip_derived_cl3993, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((hAPP @ X0 @
% 151.33/22.31 (sk_ @ X0 @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))))
% 151.33/22.31 != (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex))
% 151.33/22.31 | ((X0)
% 151.33/22.31 = (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))))),
% 151.33/22.31 inference('sup-', [status(thm)], [zip_derived_cl90, zip_derived_cl0])).
% 151.33/22.31 thf(zip_derived_cl45436, plain,
% 151.33/22.31 ((((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 != (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex))
% 151.33/22.31 | ((hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex))
% 151.33/22.31 = (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))))),
% 151.33/22.31 inference('sup-', [status(thm)],
% 151.33/22.31 [zip_derived_cl26550, zip_derived_cl3993])).
% 151.33/22.31 thf(zip_derived_cl45466, plain,
% 151.33/22.31 (((hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex))
% 151.33/22.31 = (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))),
% 151.33/22.31 inference('simplify', [status(thm)], [zip_derived_cl45436])).
% 151.33/22.31 thf(fact_poly__pCons, axiom,
% 151.33/22.31 (![V_x:$i,V_p:$i,V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__0 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( c_Polynomial_Opoly @
% 151.33/22.31 T_a @ ( c_Polynomial_OpCons @ T_a @ V_a @ V_p ) ) @
% 151.33/22.31 V_x ) =
% 151.33/22.31 ( c_Groups_Oplus__class_Oplus @
% 151.33/22.31 T_a @ V_a @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_x ) @
% 151.33/22.31 ( hAPP @ ( c_Polynomial_Opoly @ T_a @ V_p ) @ V_x ) ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl85, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ X0 @ (c_Polynomial_OpCons @ X0 @ X1 @ X3)) @
% 151.33/22.31 X2)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @ X0 @ X1 @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X2) @
% 151.33/22.31 (hAPP @ (c_Polynomial_Opoly @ X0 @ X3) @ X2))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_poly__pCons])).
% 151.33/22.31 thf(zip_derived_cl45523, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))) @
% 151.33/22.31 X0)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @ tc_Complex_Ocomplex @ X1 @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @ X0) @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl45466, zip_derived_cl85])).
% 151.33/22.31 thf(fact_mpoly__base__conv_I2_J, axiom,
% 151.33/22.31 (![V_x:$i,V_c:$i]:
% 151.33/22.31 ( ( V_c ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Polynomial_Opoly @
% 151.33/22.31 tc_Complex_Ocomplex @
% 151.33/22.31 ( c_Polynomial_OpCons @
% 151.33/22.31 tc_Complex_Ocomplex @ V_c @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @
% 151.33/22.31 ( tc_Polynomial_Opoly @ tc_Complex_Ocomplex ) ) ) ) @
% 151.33/22.31 V_x ) ))).
% 151.33/22.31 thf(zip_derived_cl93, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 ((X0)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (c_Polynomial_Opoly @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))) @
% 151.33/22.31 X1))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_mpoly__base__conv_I2_J])).
% 151.33/22.31 thf(zip_derived_cl26550, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl26501, zip_derived_cl26056, zip_derived_cl834])).
% 151.33/22.31 thf(zip_derived_cl26056, plain,
% 151.33/22.31 (![X1 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 X1) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl26034, zip_derived_cl90, zip_derived_cl90,
% 151.33/22.31 zip_derived_cl835])).
% 151.33/22.31 thf(zip_derived_cl835, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__0])).
% 151.33/22.31 thf(zip_derived_cl45533, plain,
% 151.33/22.31 (![X1 : $i]:
% 151.33/22.31 ((X1)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @ tc_Complex_Ocomplex @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl45523, zip_derived_cl93, zip_derived_cl26550,
% 151.33/22.31 zip_derived_cl26056, zip_derived_cl835])).
% 151.33/22.31 thf(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J, axiom,
% 151.33/22.31 (![V_c:$i,V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_a ) =>
% 151.33/22.31 ( ( c_Groups_Oplus__class_Oplus @ T_a @ V_a @ V_c ) =
% 151.33/22.31 ( c_Groups_Oplus__class_Oplus @ T_a @ V_c @ V_a ) ) ))).
% 151.33/22.31 thf(zip_derived_cl55, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 151.33/22.31 (((c_Groups_Oplus__class_Oplus @ X0 @ X2 @ X1)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @ X0 @ X1 @ X2))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J])).
% 151.33/22.31 thf(zip_derived_cl45782, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((c_Groups_Oplus__class_Oplus @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex) @ X0) = (
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl45533, zip_derived_cl55])).
% 151.33/22.31 thf(zip_derived_cl834, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(zip_derived_cl45814, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Oplus__class_Oplus @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex) @ X0) = (
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl45782, zip_derived_cl834])).
% 151.33/22.31 thf(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J, axiom,
% 151.33/22.31 (![V_a:$i,V_m:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_a ) =>
% 151.33/22.31 ( ( c_Groups_Oplus__class_Oplus @
% 151.33/22.31 T_a @ V_m @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_a ) @ V_m ) ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( c_Groups_Otimes__class_Otimes @ T_a ) @
% 151.33/22.31 ( c_Groups_Oplus__class_Oplus @
% 151.33/22.31 T_a @ V_a @ ( c_Groups_Oone__class_Oone @ T_a ) ) ) @
% 151.33/22.31 V_m ) ) ))).
% 151.33/22.31 thf(zip_derived_cl120, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 151.33/22.31 (((c_Groups_Oplus__class_Oplus @ X0 @ X2 @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @ X2))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @
% 151.33/22.31 (c_Groups_Oplus__class_Oplus @ X0 @ X1 @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ X0))) @
% 151.33/22.31 X2))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J])).
% 151.33/22.31 thf(zip_derived_cl46398, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((c_Groups_Oplus__class_Oplus @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl45814, zip_derived_cl120])).
% 151.33/22.31 thf(zip_derived_cl26550, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl26501, zip_derived_cl26056, zip_derived_cl834])).
% 151.33/22.31 thf(zip_derived_cl45533, plain,
% 151.33/22.31 (![X1 : $i]:
% 151.33/22.31 ((X1)
% 151.33/22.31 = (c_Groups_Oplus__class_Oplus @ tc_Complex_Ocomplex @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl45523, zip_derived_cl93, zip_derived_cl26550,
% 151.33/22.31 zip_derived_cl26056, zip_derived_cl835])).
% 151.33/22.31 thf(zip_derived_cl834, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(zip_derived_cl46426, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((X0)
% 151.33/22.31 = (hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ tc_Complex_Ocomplex)) @
% 151.33/22.31 X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl46398, zip_derived_cl26550,
% 151.33/22.31 zip_derived_cl45533, zip_derived_cl834])).
% 151.33/22.31 thf(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J, axiom,
% 151.33/22.31 (![V_b:$i,V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__1 @ T_a ) =>
% 151.33/22.31 ( ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_a ) @ V_b ) =
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_b ) @ V_a ) ) ))).
% 151.33/22.31 thf(zip_derived_cl80, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 151.33/22.31 (((hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X2) @ X1)
% 151.33/22.31 = (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @ X2))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J])).
% 151.33/22.31 thf(zip_derived_cl71802, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @ X0) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ tc_Complex_Ocomplex)) = (X0))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl46426, zip_derived_cl80])).
% 151.33/22.31 thf(zip_derived_cl834, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(zip_derived_cl71874, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((hAPP @
% 151.33/22.31 (hAPP @ (c_Groups_Otimes__class_Otimes @ tc_Complex_Ocomplex) @ X0) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ tc_Complex_Ocomplex)) = (X0))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl71802, zip_derived_cl834])).
% 151.33/22.31 thf(fact_smult__0__right, axiom,
% 151.33/22.31 (![V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__0 @ T_a ) =>
% 151.33/22.31 ( ( c_Polynomial_Osmult @
% 151.33/22.31 T_a @ V_a @
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) =
% 151.33/22.31 ( c_Groups_Ozero__class_Ozero @ ( tc_Polynomial_Opoly @ T_a ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl16, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i]:
% 151.33/22.31 (((c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0)))
% 151.33/22.31 = (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_smult__0__right])).
% 151.33/22.31 thf(fact_smult__pCons, axiom,
% 151.33/22.31 (![V_p:$i,V_b:$i,V_a:$i,T_a:$i]:
% 151.33/22.31 ( ( class_Rings_Ocomm__semiring__0 @ T_a ) =>
% 151.33/22.31 ( ( c_Polynomial_Osmult @
% 151.33/22.31 T_a @ V_a @ ( c_Polynomial_OpCons @ T_a @ V_b @ V_p ) ) =
% 151.33/22.31 ( c_Polynomial_OpCons @
% 151.33/22.31 T_a @
% 151.33/22.31 ( hAPP @
% 151.33/22.31 ( hAPP @ ( c_Groups_Otimes__class_Otimes @ T_a ) @ V_a ) @ V_b ) @
% 151.33/22.31 ( c_Polynomial_Osmult @ T_a @ V_a @ V_p ) ) ) ))).
% 151.33/22.31 thf(zip_derived_cl3, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 151.33/22.31 (((c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (c_Polynomial_OpCons @ X0 @ X2 @ X3))
% 151.33/22.31 = (c_Polynomial_OpCons @ X0 @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @ X2) @
% 151.33/22.31 (c_Polynomial_Osmult @ X0 @ X1 @ X3)))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('cnf', [status(esa)], [fact_smult__pCons])).
% 151.33/22.31 thf(zip_derived_cl4173, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 151.33/22.31 (((c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (c_Polynomial_OpCons @ X0 @ X2 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0))))
% 151.33/22.31 = (c_Polynomial_OpCons @ X0 @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @ X2) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0)
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ X0))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl16, zip_derived_cl3])).
% 151.33/22.31 thf(zip_derived_cl4176, plain,
% 151.33/22.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 151.33/22.31 (~ (class_Rings_Ocomm__semiring__0 @ X0)
% 151.33/22.31 | ((c_Polynomial_Osmult @ X0 @ X1 @
% 151.33/22.31 (c_Polynomial_OpCons @ X0 @ X2 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0))))
% 151.33/22.31 = (c_Polynomial_OpCons @ X0 @
% 151.33/22.31 (hAPP @ (hAPP @ (c_Groups_Otimes__class_Otimes @ X0) @ X1) @
% 151.33/22.31 X2) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @ (tc_Polynomial_Opoly @ X0)))))),
% 151.33/22.31 inference('simplify', [status(thm)], [zip_derived_cl4173])).
% 151.33/22.31 thf(zip_derived_cl74337, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Polynomial_OpCons @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))
% 151.33/22.31 = (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)],
% 151.33/22.31 [zip_derived_cl71874, zip_derived_cl4176])).
% 151.33/22.31 thf(zip_derived_cl835, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__0])).
% 151.33/22.31 thf(zip_derived_cl74411, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Polynomial_OpCons @ tc_Complex_Ocomplex @
% 151.33/22.31 (c_Groups_Oone__class_Oone @ tc_Complex_Ocomplex) @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))
% 151.33/22.31 = (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl74337, zip_derived_cl835])).
% 151.33/22.31 thf(zip_derived_cl74575, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 (((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Oone__class_Oone @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))
% 151.33/22.31 = (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup+', [status(thm)], [zip_derived_cl105, zip_derived_cl74411])).
% 151.33/22.31 thf(zip_derived_cl834, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(zip_derived_cl74578, plain,
% 151.33/22.31 (![X0 : $i]:
% 151.33/22.31 ((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Oone__class_Oone @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))
% 151.33/22.31 = (c_Polynomial_OpCons @ tc_Complex_Ocomplex @ X0 @
% 151.33/22.31 (c_Groups_Ozero__class_Ozero @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl74575, zip_derived_cl834])).
% 151.33/22.31 thf(zip_derived_cl120964, plain,
% 151.33/22.31 (((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)
% 151.33/22.31 != (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 v_q) @
% 151.33/22.31 (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @
% 151.33/22.31 (c_Groups_Oone__class_Oone @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl852, zip_derived_cl74578])).
% 151.33/22.31 thf(zip_derived_cl121084, plain,
% 151.33/22.31 ((((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)
% 151.33/22.31 != (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('sup-', [status(thm)],
% 151.33/22.31 [zip_derived_cl4121, zip_derived_cl120964])).
% 151.33/22.31 thf(zip_derived_cl835, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__0 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__0])).
% 151.33/22.31 thf(zip_derived_cl121091, plain,
% 151.33/22.31 (((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)
% 151.33/22.31 != (hAPP @
% 151.33/22.31 (hAPP @
% 151.33/22.31 (c_Groups_Otimes__class_Otimes @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)) @
% 151.33/22.31 (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)) @
% 151.33/22.31 (c_Groups_Oone__class_Oone @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))))),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl121084, zip_derived_cl835])).
% 151.33/22.31 thf(zip_derived_cl121606, plain,
% 151.33/22.31 ((((c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q)
% 151.33/22.31 != (c_Polynomial_Osmult @ tc_Complex_Ocomplex @ v_a @ v_q))
% 151.33/22.31 | ~ (class_Rings_Ocomm__semiring__1 @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex)))),
% 151.33/22.31 inference('sup-', [status(thm)],
% 151.33/22.31 [zip_derived_cl106, zip_derived_cl121091])).
% 151.33/22.31 thf(zip_derived_cl121613, plain,
% 151.33/22.31 (~ (class_Rings_Ocomm__semiring__1 @
% 151.33/22.31 (tc_Polynomial_Opoly @ tc_Complex_Ocomplex))),
% 151.33/22.31 inference('simplify', [status(thm)], [zip_derived_cl121606])).
% 151.33/22.31 thf(zip_derived_cl121623, plain,
% 151.33/22.31 (~ (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('sup-', [status(thm)],
% 151.33/22.31 [zip_derived_cl843, zip_derived_cl121613])).
% 151.33/22.31 thf(zip_derived_cl834, plain,
% 151.33/22.31 ( (class_Rings_Ocomm__semiring__1 @ tc_Complex_Ocomplex)),
% 151.33/22.31 inference('cnf', [status(esa)],
% 151.33/22.31 [arity_Complex__Ocomplex__Rings_Ocomm__semiring__1])).
% 151.33/22.31 thf(zip_derived_cl121624, plain, ($false),
% 151.33/22.31 inference('demod', [status(thm)],
% 151.33/22.31 [zip_derived_cl121623, zip_derived_cl834])).
% 151.33/22.31
% 151.33/22.31 % SZS output end Refutation
% 151.33/22.31
% 151.33/22.31
% 151.33/22.31 % Terminating...
% 151.89/22.39 % Runner terminated.
% 151.92/22.41 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------