%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG426-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:50:10 AM UTC 2026
% Result : Unsatisfiable 109.29s 14.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG426-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n018.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 13:22:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.41 % Drodi V4.1.1
% 109.29/14.30 % Refutation found
% 109.29/14.30 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 109.29/14.30 % SZS output start CNFRefutation for theBenchmark
% 109.29/14.30 fof(f7,axiom,(
% 109.29/14.30 (![T_a,V_a,V_b,V_c]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_a,c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a)| ~ c_Ring__and__Field_Odvd__class_Odvd(V_a,V_c,T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f10,axiom,(
% 109.29/14.30 (![T_a,V_b,V_c,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_b,V_c,T_a)| ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),V_c,T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f46,axiom,(
% 109.29/14.30 (![T_a,V_lx,V_ly,V_rx]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_rx,T_a),V_ly,T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f47,axiom,(
% 109.29/14.30 (![T_a,V_lx,V_ly,V_rx]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a) = c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_ly,V_rx,T_a),T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f88,axiom,(
% 109.29/14.30 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_a,V_a,T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f150,axiom,(
% 109.29/14.30 (![T_a,V_p,V_a,V_q]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))| ~ c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a)) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f254,axiom,(
% 109.29/14.30 (![T_a]: (( ~ class_SEQ_Obanach(T_a)| ~ class_RealVector_Oreal__normed__field(T_a)| c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Oone__class_Oone(T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f312,axiom,(
% 109.29/14.30 (![T_a,V_a,V_p,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f341,axiom,(
% 109.29/14.30 (![T_a,V_p,V_c]: (( ~ class_Ring__and__Field_Oidom(T_a)| c_Polynomial_Opoly(V_p,V_c,T_a) = c_HOL_Ozero__class_Ozero(T_a)| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(V_c,T_a),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),T_a),V_p,tc_Polynomial_Opoly(T_a)) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f357,axiom,(
% 109.29/14.30 (![T_a,V_a]: (( ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a)| c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f368,axiom,(
% 109.29/14.30 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f374,axiom,(
% 109.29/14.30 (![T_a,V_p,V_q,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(V_p,V_q,tc_Polynomial_Opoly(T_a)),V_x,T_a) = c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(V_p,V_x,T_a),c_Polynomial_Opoly(V_q,V_x,T_a),T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f446,axiom,(
% 109.29/14.30 (![T_a,V_p,V_c,V_q,V_r]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,V_q,T_a),tc_Polynomial_Opoly(T_a)) != c_Polynomial_OpCons(V_r,V_q,T_a)| V_q = c_Polynomial_Osynthetic__div(V_p,V_c,T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f453,axiom,(
% 109.29/14.30 (![T_a,V_a,V_p,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f473,axiom,(
% 109.29/14.30 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| V_a = c_HOL_Ozero__class_Ozero(T_a)| ~ c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f512,axiom,(
% 109.29/14.30 (![T_a,V_x]: (( ~ class_SEQ_Obanach(T_a)| ~ class_RealVector_Oreal__normed__field(T_a)| c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f513,axiom,(
% 109.29/14.30 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__add(T_a)| c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f558,axiom,(
% 109.29/14.30 (![V_p]: (( c_Polynomial_Opoly(V_p,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(V_p),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)| V_p = c_Polynomial_OpCons(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(V_p),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f560,axiom,(
% 109.29/14.30 v_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f561,axiom,(
% 109.29/14.30 (![T_a,V_p]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f570,axiom,(
% 109.29/14.30 (![T_a,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f572,negated_conjecture,(
% 109.29/14.30 (![V_x]: (c_Polynomial_Opoly(v_q,V_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f573,negated_conjecture,(
% 109.29/14.30 v_q != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f658,axiom,(
% 109.29/14.30 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f659,axiom,(
% 109.29/14.30 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f667,axiom,(
% 109.29/14.30 class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f668,axiom,(
% 109.29/14.30 class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f678,axiom,(
% 109.29/14.30 class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f685,axiom,(
% 109.29/14.30 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f689,axiom,(
% 109.29/14.30 class_SEQ_Obanach(tc_Complex_Ocomplex) ),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f694,axiom,(
% 109.29/14.30 (![T_1]: (( class_Ring__and__Field_Oring__no__zero__divisors(tc_Polynomial_Opoly(T_1))| ~ class_Ring__and__Field_Oidom(T_1) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f700,axiom,(
% 109.29/14.30 (![T_1]: (( class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(T_1))| ~ class_Ring__and__Field_Ocomm__semiring__1(T_1) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f716,axiom,(
% 109.29/14.30 (![T_1]: (( class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(T_1))| ~ class_OrderedGroup_Ocomm__monoid__add(T_1) ) ))),
% 109.29/14.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.29/14.30 fof(f741,plain,(
% 109.29/14.30 ![T_a,V_a,V_c]: ((~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_b]: c_Ring__and__Field_Odvd__class_Odvd(V_a,c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a)))|~c_Ring__and__Field_Odvd__class_Odvd(V_a,V_c,T_a))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f7])).
% 109.29/14.30 fof(f742,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0)|~c_Ring__and__Field_Odvd__class_Odvd(X1,X3,X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f741])).
% 109.29/14.30 fof(f747,plain,(
% 109.29/14.30 ![T_a,V_b,V_c]: ((~class_Ring__and__Field_Ocomm__semiring__1(T_a)|c_Ring__and__Field_Odvd__class_Odvd(V_b,V_c,T_a))|(![V_a]: ~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),V_c,T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f10])).
% 109.29/14.30 fof(f748,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,X2,X0)|~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(X3,X1,X0),X2,X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f747])).
% 109.29/14.30 fof(f816,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_lx,V_ly,V_rx]: c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a)=c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_rx,T_a),V_ly,T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f46])).
% 109.29/14.30 fof(f817,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0)=c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f816])).
% 109.29/14.30 fof(f818,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_lx,V_ly,V_rx]: c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a)=c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_ly,V_rx,T_a),T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f47])).
% 109.29/14.30 fof(f819,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0)=c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f818])).
% 109.29/14.30 fof(f897,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a]: c_Ring__and__Field_Odvd__class_Odvd(V_a,V_a,T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f88])).
% 109.29/14.30 fof(f898,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,X1,X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f897])).
% 109.29/14.30 fof(f1018,plain,(
% 109.29/14.30 ![T_a,V_p,V_q]: ((~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a]: c_Ring__and__Field_Odvd__class_Odvd(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))))|~c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f150])).
% 109.29/14.30 fof(f1019,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0))|~c_Ring__and__Field_Odvd__class_Odvd(X1,X3,tc_Polynomial_Opoly(X0)))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1018])).
% 109.29/14.30 fof(f1214,plain,(
% 109.29/14.30 ![X0]: (~class_SEQ_Obanach(X0)|~class_RealVector_Oreal__normed__field(X0)|c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Oone__class_Oone(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f254])).
% 109.29/14.30 fof(f1319,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_a,V_p,V_x]: c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a)=c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f312])).
% 109.29/14.30 fof(f1320,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,X0),X3,X0)=c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,X0),X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1319])).
% 109.29/14.30 fof(f1373,plain,(
% 109.29/14.30 ![X0,X1,X2]: (~class_Ring__and__Field_Oidom(X0)|c_Polynomial_Opoly(X1,X2,X0)=c_HOL_Ozero__class_Ozero(X0)|~c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(X2,X0),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X0),X1,tc_Polynomial_Opoly(X0)))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f341])).
% 109.29/14.30 fof(f1392,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Oring__no__zero__divisors(T_a)|(![V_a]: c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f357])).
% 109.29/14.30 fof(f1393,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Oring__no__zero__divisors(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1392])).
% 109.29/14.30 fof(f1414,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a]: c_Ring__and__Field_Odvd__class_Odvd(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f368])).
% 109.29/14.30 fof(f1415,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Ozero__class_Ozero(X0),X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1414])).
% 109.29/14.30 fof(f1425,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_p,V_q,V_x]: c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(V_p,V_q,tc_Polynomial_Opoly(T_a)),V_x,T_a)=c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(V_p,V_x,T_a),c_Polynomial_Opoly(V_q,V_x,T_a),T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f374])).
% 109.29/14.30 fof(f1426,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(X0)),X3,X0)=c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X1,X3,X0),c_Polynomial_Opoly(X2,X3,X0),X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1425])).
% 109.29/14.30 fof(f1552,plain,(
% 109.29/14.30 ![T_a,V_p,V_c,V_q]: ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_r]: ~c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,V_q,T_a),tc_Polynomial_Opoly(T_a))=c_Polynomial_OpCons(V_r,V_q,T_a)))|V_q=c_Polynomial_Osynthetic__div(V_p,V_c,T_a))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f446])).
% 109.29/14.30 fof(f1553,plain,(
% 109.29/14.30 ![X0,X1,X2,X3,X4]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|~c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0))=c_Polynomial_OpCons(X4,X3,X0)|X3=c_Polynomial_Osynthetic__div(X1,X2,X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1552])).
% 109.29/14.30 fof(f1565,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_a,V_p,V_x]: c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a)=c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f453])).
% 109.29/14.30 fof(f1566,plain,(
% 109.29/14.30 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0)=c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1565])).
% 109.29/14.30 fof(f1600,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|X1=c_HOL_Ozero__class_Ozero(X0)|~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(X0),X1,X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f473])).
% 109.29/14.30 fof(f1663,plain,(
% 109.29/14.30 ![T_a]: ((~class_SEQ_Obanach(T_a)|~class_RealVector_Oreal__normed__field(T_a))|(![V_x]: ~c_Transcendental_Oexp(V_x,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f512])).
% 109.29/14.30 fof(f1664,plain,(
% 109.29/14.30 ![X0,X1]: (~class_SEQ_Obanach(X0)|~class_RealVector_Oreal__normed__field(X0)|~c_Transcendental_Oexp(X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1663])).
% 109.29/14.30 fof(f1665,plain,(
% 109.29/14.30 ![T_a]: (~class_OrderedGroup_Omonoid__add(T_a)|(![V_a]: c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=V_a))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f513])).
% 109.29/14.30 fof(f1666,plain,(
% 109.29/14.30 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0)=X1)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1665])).
% 109.29/14.30 fof(f1743,plain,(
% 109.29/14.30 ![X0]: (c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(X0),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X0=c_Polynomial_OpCons(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f558])).
% 109.29/14.30 fof(f1745,plain,(
% 109.29/14.30 v_p=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f560])).
% 109.29/14.30 fof(f1746,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_p]: c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f561])).
% 109.29/14.30 fof(f1747,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(X0),X1,X0)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1746])).
% 109.29/14.30 fof(f1763,plain,(
% 109.29/14.30 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_x]: c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 109.29/14.30 inference(miniscoping,[status(thm)],[f570])).
% 109.29/14.30 fof(f1764,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f1763])).
% 109.29/14.30 fof(f1767,plain,(
% 109.29/14.30 ![X0]: (c_Polynomial_Opoly(v_q,X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f572])).
% 109.29/14.30 fof(f1768,plain,(
% 109.29/14.30 ~v_q=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f573])).
% 109.29/14.30 fof(f1853,plain,(
% 109.29/14.30 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f658])).
% 109.29/14.30 fof(f1854,plain,(
% 109.29/14.30 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f659])).
% 109.29/14.30 fof(f1862,plain,(
% 109.29/14.30 class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f667])).
% 109.29/14.30 fof(f1863,plain,(
% 109.29/14.30 class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f668])).
% 109.29/14.30 fof(f1873,plain,(
% 109.29/14.30 class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f678])).
% 109.29/14.30 fof(f1880,plain,(
% 109.29/14.30 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f685])).
% 109.29/14.30 fof(f1884,plain,(
% 109.29/14.30 class_SEQ_Obanach(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f689])).
% 109.29/14.30 fof(f1889,plain,(
% 109.29/14.30 ![X0]: (class_Ring__and__Field_Oring__no__zero__divisors(tc_Polynomial_Opoly(X0))|~class_Ring__and__Field_Oidom(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f694])).
% 109.29/14.30 fof(f1895,plain,(
% 109.29/14.30 ![X0]: (class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(X0))|~class_Ring__and__Field_Ocomm__semiring__1(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f700])).
% 109.29/14.30 fof(f1911,plain,(
% 109.29/14.30 ![X0]: (class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(X0))|~class_OrderedGroup_Ocomm__monoid__add(X0))),
% 109.29/14.30 inference(cnf_transformation,[status(thm)],[f716])).
% 109.29/14.30 fof(f3179,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X2,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex),c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1854,f1426])).
% 109.29/14.30 fof(f3180,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1854,f1566])).
% 109.29/14.30 fof(f3181,plain,(
% 109.29/14.30 ![X0]: (c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1854,f1764])).
% 109.29/14.30 fof(f3182,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1854,f1320])).
% 109.29/14.30 fof(f3196,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3181,f3182])).
% 109.29/14.30 fof(f3197,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_Osmult(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f1767,f3182])).
% 109.29/14.30 fof(f3220,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Opoly(c_Polynomial_Osmult(X2,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f3182,f3180])).
% 109.29/14.30 fof(f3221,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3197,f3220])).
% 109.29/14.30 fof(f3242,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(c_Polynomial_Osmult(c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f3182,f3179])).
% 109.29/14.30 fof(f3243,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_q,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X0,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3197,f3242])).
% 109.29/14.30 fof(f3247,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(c_Polynomial_Osmult(X0,v_q,tc_Complex_Ocomplex),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3197,f3242])).
% 109.29/14.30 fof(f3251,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_q,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f1767,f3242])).
% 109.29/14.30 fof(f3739,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(backward_demodulation,[status(thm)],[f1745,f3196])).
% 109.29/14.30 fof(f3741,plain,(
% 109.29/14.30 ~v_q=v_p),
% 109.29/14.30 inference(backward_demodulation,[status(thm)],[f1745,f1768])).
% 109.29/14.30 fof(f4035,plain,(
% 109.29/14.30 class_Ring__and__Field_Oring__no__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1889,f1880])).
% 109.29/14.30 fof(f4155,plain,(
% 109.29/14.30 class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1895,f1853])).
% 109.29/14.30 fof(f4258,plain,(
% 109.29/14.30 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(X0,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(resolution,[status(thm)],[f4155,f898])).
% 109.29/14.30 fof(f4262,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Otimes__class_Otimes(X1,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(resolution,[status(thm)],[f4258,f748])).
% 109.29/14.30 fof(f4272,plain,(
% 109.29/14.30 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Otimes__class_Otimes(X1,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(forward_subsumption_resolution,[status(thm)],[f4262,f4155])).
% 109.29/14.30 fof(f4873,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X2,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f817,f1853])).
% 109.29/14.30 fof(f4884,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f819,f1853])).
% 109.29/14.30 fof(f5076,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X2,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(backward_demodulation,[status(thm)],[f4884,f4873])).
% 109.29/14.30 fof(f5431,plain,(
% 109.29/14.30 class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1911,f1863])).
% 109.29/14.30 fof(f7086,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X0,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3242,f3739])).
% 109.29/14.30 fof(f7112,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_q,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f3243,f7086])).
% 109.29/14.30 fof(f8597,plain,(
% 109.29/14.30 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1415,f4155])).
% 109.29/14.30 fof(f8602,plain,(
% 109.29/14.30 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f1745,f8597])).
% 109.29/14.30 fof(f8735,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Otimes__class_Otimes(X1,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(resolution,[status(thm)],[f8602,f742])).
% 109.29/14.30 fof(f8741,plain,(
% 109.29/14.30 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Otimes__class_Otimes(X1,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(forward_subsumption_resolution,[status(thm)],[f8735,f4155])).
% 109.29/14.30 fof(f8844,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)|c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(resolution,[status(thm)],[f8741,f1373])).
% 109.29/14.30 fof(f8854,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)|c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_q,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f7112,f8844])).
% 109.29/14.30 fof(f8855,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_q,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_subsumption_resolution,[status(thm)],[f8854,f1880])).
% 109.29/14.30 fof(f9446,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(backward_demodulation,[status(thm)],[f8855,f7112])).
% 109.29/14.30 fof(f9456,plain,(
% 109.29/14.30 ![X0]: (c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_q,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3251,f8855])).
% 109.29/14.30 fof(f9485,plain,(
% 109.29/14.30 c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f3197,f9456])).
% 109.29/14.30 fof(f9556,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(paramodulation,[status(thm)],[f3247,f9446])).
% 109.29/14.30 fof(f9584,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f3739,f9556])).
% 109.29/14.30 fof(f9585,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f5076,f9584])).
% 109.29/14.30 fof(f9586,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f9485,f9585])).
% 109.29/14.30 fof(f9663,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.30 inference(backward_demodulation,[status(thm)],[f9586,f3221])).
% 109.29/14.30 fof(f13406,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=X0)),
% 109.29/14.30 inference(resolution,[status(thm)],[f1666,f5431])).
% 109.29/14.30 fof(f13407,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=X0)),
% 109.29/14.30 inference(resolution,[status(thm)],[f1666,f1873])).
% 109.29/14.30 fof(f13410,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Oplus__class_Oplus(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex))=X0)),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f1745,f13406])).
% 109.29/14.30 fof(f13436,plain,(
% 109.29/14.30 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=X0)),
% 109.29/14.30 inference(backward_demodulation,[status(thm)],[f13407,f9663])).
% 109.29/14.30 fof(f15976,plain,(
% 109.29/14.30 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)|c_Ring__and__Field_Odvd__class_Odvd(X0,c_Polynomial_Osmult(X1,c_HOL_Otimes__class_Otimes(X2,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1019,f4272])).
% 109.29/14.30 fof(f16004,plain,(
% 109.29/14.30 ![X0,X1,X2]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_Polynomial_Osmult(X1,c_HOL_Otimes__class_Otimes(X2,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(forward_subsumption_resolution,[status(thm)],[f15976,f1853])).
% 109.29/14.30 fof(f18740,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Otimes__class_Otimes(X0,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)))),
% 109.29/14.30 inference(resolution,[status(thm)],[f1393,f4035])).
% 109.29/14.30 fof(f18743,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Otimes__class_Otimes(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f1745,f18740])).
% 109.29/14.30 fof(f18744,plain,(
% 109.29/14.30 ![X0]: (c_HOL_Otimes__class_Otimes(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p)),
% 109.29/14.30 inference(forward_demodulation,[status(thm)],[f1745,f18743])).
% 109.29/14.30 fof(f23503,plain,(
% 109.29/14.30 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|c_Polynomial_Osmult(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.31 inference(resolution,[status(thm)],[f1600,f16004])).
% 109.29/14.31 fof(f23580,plain,(
% 109.29/14.31 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|c_Polynomial_Osmult(X0,c_HOL_Otimes__class_Otimes(X1,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f1745,f23503])).
% 109.29/14.31 fof(f23581,plain,(
% 109.29/14.31 ![X0]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f18744,f23580])).
% 109.29/14.31 fof(f23582,plain,(
% 109.29/14.31 ![X0]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex)=v_p)),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f1745,f23581])).
% 109.29/14.31 fof(f23583,plain,(
% 109.29/14.31 ![X0]: (c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex)=v_p)),
% 109.29/14.31 inference(forward_subsumption_resolution,[status(thm)],[f23582,f4155])).
% 109.29/14.31 fof(f36215,plain,(
% 109.29/14.31 ~class_SEQ_Obanach(tc_Complex_Ocomplex)|c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 109.29/14.31 inference(resolution,[status(thm)],[f1214,f1862])).
% 109.29/14.31 fof(f36217,plain,(
% 109.29/14.31 c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 109.29/14.31 inference(forward_subsumption_resolution,[status(thm)],[f36215,f1884])).
% 109.29/14.31 fof(f36533,plain,(
% 109.29/14.31 ~class_SEQ_Obanach(tc_Complex_Ocomplex)|~class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex)|~c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 109.29/14.31 inference(paramodulation,[status(thm)],[f36217,f1664])).
% 109.29/14.31 fof(f36534,plain,(
% 109.29/14.31 ~class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex)|~c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 109.29/14.31 inference(forward_subsumption_resolution,[status(thm)],[f36533,f1884])).
% 109.29/14.31 fof(f36537,plain,(
% 109.29/14.31 ~c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 109.29/14.31 inference(forward_subsumption_resolution,[status(thm)],[f36534,f1862])).
% 109.29/14.31 fof(f40273,plain,(
% 109.29/14.31 ![X0]: (c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 109.29/14.31 inference(resolution,[status(thm)],[f1747,f1854])).
% 109.29/14.31 fof(f40277,plain,(
% 109.29/14.31 ![X0]: (c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=v_p)),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f1745,f40273])).
% 109.29/14.31 fof(f74034,plain,(
% 109.29/14.31 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|~c_HOL_Oplus__class_Oplus(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_Polynomial_OpCons(X1,X2,tc_Complex_Ocomplex)|X2=c_Polynomial_Osynthetic__div(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.31 inference(paramodulation,[status(thm)],[f40277,f1553])).
% 109.29/14.31 fof(f74067,plain,(
% 109.29/14.31 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|~X0=c_Polynomial_OpCons(X1,X2,tc_Complex_Ocomplex)|X2=c_Polynomial_Osynthetic__div(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f13410,f74034])).
% 109.29/14.31 fof(f74068,plain,(
% 109.29/14.31 ![X2,X1]: (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|X2=c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X1,X2,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.31 inference(destructive_equality_resolution,[status(thm)],[f74067])).
% 109.29/14.31 fof(f74069,plain,(
% 109.29/14.31 ![X0,X1]: (X0=c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X1,X0,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 109.29/14.31 inference(forward_subsumption_resolution,[status(thm)],[f74068,f1854])).
% 109.29/14.31 fof(f89213,plain,(
% 109.29/14.31 ![X0]: (c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(X0),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X0=c_Polynomial_OpCons(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(X0),v_p,tc_Complex_Ocomplex))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f1745,f1743])).
% 109.29/14.31 fof(f89223,plain,(
% 109.29/14.31 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex))),
% 109.29/14.31 inference(resolution,[status(thm)],[f89213,f1553])).
% 109.29/14.31 fof(f89338,plain,(
% 109.29/14.31 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Oplus__class_Oplus(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f23583,f89223])).
% 109.29/14.31 fof(f89339,plain,(
% 109.29/14.31 ![X0,X1]: (c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f13410,f89338])).
% 109.29/14.31 fof(f89340,plain,(
% 109.29/14.31 ![X0,X1]: (c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(c_HOL_Oplus__class_Oplus(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex))),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex))),
% 109.29/14.31 inference(forward_demodulation,[status(thm)],[f23583,f89339])).
% 109.29/14.31 fof(f89341,plain,(
% 109.29/14.31 ![X0,X1]: (c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(X0),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex))),
% 17.56/14.44 inference(forward_demodulation,[status(thm)],[f13410,f89340])).
% 17.56/14.44 fof(f89342,plain,(
% 17.56/14.44 ![X0,X1]: (c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(X0),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex))),
% 17.56/14.44 inference(forward_subsumption_resolution,[status(thm)],[f89341,f1854])).
% 17.56/14.44 fof(f89890,plain,(
% 17.56/14.44 ![X0,X1]: (X0=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|v_p=c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex))),
% 17.56/14.44 inference(paramodulation,[status(thm)],[f13436,f89342])).
% 17.56/14.44 fof(f90394,plain,(
% 17.56/14.44 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|v_p=v_q)),
% 17.56/14.44 inference(paramodulation,[status(thm)],[f74069,f89890])).
% 17.56/14.44 fof(f90397,plain,(
% 17.56/14.44 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 17.56/14.44 inference(forward_subsumption_resolution,[status(thm)],[f90394,f3741])).
% 17.56/14.44 fof(f90590,plain,(
% 17.56/14.44 $false),
% 17.56/14.44 inference(backward_subsumption_resolution,[status(thm)],[f36537,f90397])).
% 17.56/14.44 % SZS output end CNFRefutation for theBenchmark.p
% 17.56/14.51 % Elapsed time: 14.134351 seconds
% 17.56/14.51 % CPU time: 111.111482 seconds
% 17.56/14.51 % Total memory used: 1.189 GB
% 17.56/14.51 % Net memory used: 1.160 GB
%------------------------------------------------------------------------------