%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG427-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 : n019.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 83.67s 11.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG427-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.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 13:20:49 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.41 % Drodi V4.1.1
% 83.67/11.09 % Refutation found
% 83.67/11.09 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 83.67/11.09 % SZS output start CNFRefutation for theBenchmark
% 83.67/11.09 fof(f14,axiom,(
% 83.67/11.09 (![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) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f61,axiom,(
% 83.67/11.09 (![T_a,V_p]: (( ~ class_Ring__and__Field_Oidom(T_a)| c_Polynomial_Odegree(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f67,axiom,(
% 83.67/11.09 (![T_a,V_a,V_b,V_p]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Osmult(V_a,c_Polynomial_OpCons(V_b,V_p,T_a),T_a) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_Polynomial_Osmult(V_a,V_p,T_a),T_a) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f72,axiom,(
% 83.67/11.09 (![V_p]: (( v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(V_p) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)| 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) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f88,axiom,(
% 83.67/11.09 (![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) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f90,axiom,(
% 83.67/11.09 (![T_a,V_lx,V_rx,V_ry]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a) = c_HOL_Otimes__class_Otimes(V_rx,c_HOL_Otimes__class_Otimes(V_lx,V_ry,T_a),T_a) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f145,axiom,(
% 83.67/11.09 (![T_a,V_p]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Polynomial_Osmult(c_HOL_Oone__class_Oone(T_a),V_p,T_a) = V_p ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f185,axiom,(
% 83.67/11.09 (![T_a,V_a,V_b,V_p]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Osmult(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_p,T_a) = c_HOL_Oplus__class_Oplus(c_Polynomial_Osmult(V_a,V_p,T_a),c_Polynomial_Osmult(V_b,V_p,T_a),tc_Polynomial_Opoly(T_a)) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f209,axiom,(
% 83.67/11.09 (![T_a,V_a,V_b]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_a,c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),T_a) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f225,axiom,(
% 83.67/11.09 (![T_a,V_x,V_y]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f230,axiom,(
% 83.67/11.09 (![T_a,V_a,V_p,V_n]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Ocoeff(c_Polynomial_Osmult(V_a,V_p,T_a),V_n,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Ocoeff(V_p,V_n,T_a),T_a) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f321,axiom,(
% 83.67/11.09 (![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) ) ))),
% 83.67/11.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.09 fof(f364,axiom,(
% 83.67/11.09 (![T_a,V_c,V_p]: (( ~ class_Ring__and__Field_Ocomm__ring__1(T_a)| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(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),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),tc_Polynomial_Opoly(T_a)),c_Polynomial_OpCons(c_Polynomial_Opoly(V_p,V_c,T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),tc_Polynomial_Opoly(T_a)) = V_p ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f387,axiom,(
% 83.67/11.10 (![T_a,V_p,V_a,V_q]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_HOL_Otimes__class_Otimes(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a)) = c_Polynomial_Osmult(V_a,c_HOL_Otimes__class_Otimes(V_p,V_q,tc_Polynomial_Opoly(T_a)),T_a) ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f454,axiom,(
% 83.67/11.10 (![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) ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f483,axiom,(
% 83.67/11.10 (![T_a,V_p,V_c]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Odegree(V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_nat)| c_Polynomial_Osynthetic__div(V_p,V_c,T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f586,axiom,(
% 83.67/11.10 (![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 ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f597,axiom,(
% 83.67/11.10 (![T_a,V_p]: (( ~ class_HOL_Ozero(T_a)| c_Polynomial_Ocoeff(V_p,c_Polynomial_Odegree(V_p,T_a),T_a) != c_HOL_Ozero__class_Ozero(T_a)| V_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f637,axiom,(
% 83.67/11.10 (![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) ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f662,axiom,(
% 83.67/11.10 (![V_k]: (( v_p != c_Polynomial_OpCons(V_k,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)| v_thesis____| V_k = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ))),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f663,axiom,(
% 83.67/11.10 v_p != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f665,axiom,(
% 83.67/11.10 c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f666,negated_conjecture,(
% 83.67/11.10 ~ v_thesis____ ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f764,axiom,(
% 83.67/11.10 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f765,axiom,(
% 83.67/11.10 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f775,axiom,(
% 83.67/11.10 class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f782,axiom,(
% 83.67/11.10 class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f788,axiom,(
% 83.67/11.10 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f792,axiom,(
% 83.67/11.10 class_HOL_Ozero(tc_Complex_Ocomplex) ),
% 83.67/11.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 83.67/11.10 fof(f859,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f14])).
% 83.67/11.10 fof(f860,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f859])).
% 83.67/11.10 fof(f945,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Oidom(T_a)|(![V_p]: c_Polynomial_Odegree(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),T_a)=c_HOL_Ozero__class_Ozero(tc_nat)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f61])).
% 83.67/11.10 fof(f946,plain,(
% 83.67/11.10 ![X0,X1]: (~class_Ring__and__Field_Oidom(X0)|c_Polynomial_Odegree(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(X0),X1,X0),X0)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f945])).
% 83.67/11.10 fof(f955,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_a,V_b,V_p]: c_Polynomial_Osmult(V_a,c_Polynomial_OpCons(V_b,V_p,T_a),T_a)=c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_Polynomial_Osmult(V_a,V_p,T_a),T_a)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f67])).
% 83.67/11.10 fof(f956,plain,(
% 83.67/11.10 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,X3,X0),X0)=c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,X0),c_Polynomial_Osmult(X1,X3,X0),X0))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f955])).
% 83.67/11.10 fof(f963,plain,(
% 83.67/11.10 ![X0]: (~v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(X0)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|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))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f72])).
% 83.67/11.10 fof(f994,plain,(
% 83.67/11.10 ![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)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f88])).
% 83.67/11.10 fof(f995,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f994])).
% 83.67/11.10 fof(f998,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_lx,V_rx,V_ry]: c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a)=c_HOL_Otimes__class_Otimes(V_rx,c_HOL_Otimes__class_Otimes(V_lx,V_ry,T_a),T_a)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f90])).
% 83.67/11.10 fof(f999,plain,(
% 83.67/11.10 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0)=c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X1,X3,X0),X0))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f998])).
% 83.67/11.10 fof(f1097,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_p]: c_Polynomial_Osmult(c_HOL_Oone__class_Oone(T_a),V_p,T_a)=V_p))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f145])).
% 83.67/11.10 fof(f1098,plain,(
% 83.67/11.10 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Polynomial_Osmult(c_HOL_Oone__class_Oone(X0),X1,X0)=X1)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1097])).
% 83.67/11.10 fof(f1162,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_a,V_b,V_p]: c_Polynomial_Osmult(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_p,T_a)=c_HOL_Oplus__class_Oplus(c_Polynomial_Osmult(V_a,V_p,T_a),c_Polynomial_Osmult(V_b,V_p,T_a),tc_Polynomial_Opoly(T_a))))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f185])).
% 83.67/11.10 fof(f1163,plain,(
% 83.67/11.10 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(c_HOL_Oplus__class_Oplus(X1,X2,X0),X3,X0)=c_HOL_Oplus__class_Oplus(c_Polynomial_Osmult(X1,X3,X0),c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0)))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1162])).
% 83.67/11.10 fof(f1206,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a,V_b]: c_Ring__and__Field_Odvd__class_Odvd(V_a,c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),T_a)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f209])).
% 83.67/11.10 fof(f1207,plain,(
% 83.67/11.10 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,c_HOL_Otimes__class_Otimes(X1,X2,X0),X0))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1206])).
% 83.67/11.10 fof(f1236,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_x,V_y]: c_HOL_Otimes__class_Otimes(V_x,V_y,T_a)=c_HOL_Otimes__class_Otimes(V_y,V_x,T_a)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f225])).
% 83.67/11.10 fof(f1237,plain,(
% 83.67/11.10 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(X1,X2,X0)=c_HOL_Otimes__class_Otimes(X2,X1,X0))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1236])).
% 83.67/11.10 fof(f1246,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_a,V_p,V_n]: c_Polynomial_Ocoeff(c_Polynomial_Osmult(V_a,V_p,T_a),V_n,T_a)=c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Ocoeff(V_p,V_n,T_a),T_a)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f230])).
% 83.67/11.10 fof(f1247,plain,(
% 83.67/11.10 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Ocoeff(c_Polynomial_Osmult(X1,X2,X0),X3,X0)=c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Ocoeff(X2,X3,X0),X0))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1246])).
% 83.67/11.10 fof(f1410,plain,(
% 83.67/11.10 ![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)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f321])).
% 83.67/11.10 fof(f1411,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1410])).
% 83.67/11.10 fof(f1477,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__ring__1(T_a)|(![V_c,V_p]: c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(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),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),tc_Polynomial_Opoly(T_a)),c_Polynomial_OpCons(c_Polynomial_Opoly(V_p,V_c,T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),tc_Polynomial_Opoly(T_a))=V_p))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f364])).
% 83.67/11.10 fof(f1478,plain,(
% 83.67/11.10 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__ring__1(X0)|c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(X1,X0),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X0),c_Polynomial_Osynthetic__div(X2,X1,X0),tc_Polynomial_Opoly(X0)),c_Polynomial_OpCons(c_Polynomial_Opoly(X2,X1,X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),tc_Polynomial_Opoly(X0))=X2)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1477])).
% 83.67/11.10 fof(f1518,plain,(
% 83.67/11.10 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_p,V_a,V_q]: c_HOL_Otimes__class_Otimes(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))=c_Polynomial_Osmult(V_a,c_HOL_Otimes__class_Otimes(V_p,V_q,tc_Polynomial_Opoly(T_a)),T_a)))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f387])).
% 83.67/11.10 fof(f1519,plain,(
% 83.67/11.10 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0))=c_Polynomial_Osmult(X2,c_HOL_Otimes__class_Otimes(X1,X3,tc_Polynomial_Opoly(X0)),X0))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1518])).
% 83.67/11.10 fof(f1633,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f454])).
% 83.67/11.10 fof(f1680,plain,(
% 83.67/11.10 ![T_a,V_p]: ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)|~c_Polynomial_Odegree(V_p,T_a)=c_HOL_Ozero__class_Ozero(tc_nat))|(![V_c]: c_Polynomial_Osynthetic__div(V_p,V_c,T_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f483])).
% 83.67/11.10 fof(f1681,plain,(
% 83.67/11.10 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|~c_Polynomial_Odegree(X1,X0)=c_HOL_Ozero__class_Ozero(tc_nat)|c_Polynomial_Osynthetic__div(X1,X2,X0)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1680])).
% 83.67/11.10 fof(f1843,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(miniscoping,[status(thm)],[f586])).
% 83.67/11.10 fof(f1844,plain,(
% 83.67/11.10 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0)=X1)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f1843])).
% 83.67/11.10 fof(f1864,plain,(
% 83.67/11.10 ![X0,X1]: (~class_HOL_Ozero(X0)|~c_Polynomial_Ocoeff(X1,c_Polynomial_Odegree(X1,X0),X0)=c_HOL_Ozero__class_Ozero(X0)|X1=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f597])).
% 83.67/11.10 fof(f1933,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f637])).
% 83.67/11.10 fof(f1979,plain,(
% 83.67/11.10 ![X0]: (~v_p=c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)|v_thesis____|X0=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f662])).
% 83.67/11.10 fof(f1980,plain,(
% 83.67/11.10 ~v_p=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f663])).
% 83.67/11.10 fof(f1982,plain,(
% 83.67/11.10 c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_nat)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f665])).
% 83.67/11.10 fof(f1983,plain,(
% 83.67/11.10 ~v_thesis____),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f666])).
% 83.67/11.10 fof(f2081,plain,(
% 83.67/11.10 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f764])).
% 83.67/11.10 fof(f2082,plain,(
% 83.67/11.10 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f765])).
% 83.67/11.10 fof(f2092,plain,(
% 83.67/11.10 class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f775])).
% 83.67/11.10 fof(f2099,plain,(
% 83.67/11.10 class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f782])).
% 83.67/11.10 fof(f2105,plain,(
% 83.67/11.10 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f788])).
% 83.67/11.10 fof(f2109,plain,(
% 83.67/11.10 class_HOL_Ozero(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(cnf_transformation,[status(thm)],[f792])).
% 83.67/11.10 fof(f2157,plain,(
% 83.67/11.10 ![X0]: (~v_p=c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)|X0=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(forward_subsumption_resolution,[status(thm)],[f1979,f1983])).
% 83.67/11.10 fof(f2318,plain,(
% 83.67/11.10 ![X0]: (c_Polynomial_Osmult(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=X0)),
% 83.67/11.10 inference(resolution,[status(thm)],[f2081,f1098])).
% 83.67/11.10 fof(f2321,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f2081,f999])).
% 83.67/11.10 fof(f2322,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(resolution,[status(thm)],[f2081,f995])).
% 83.67/11.10 fof(f2327,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~c_Ring__and__Field_Odvd__class_Odvd(X0,X2,tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f2081,f860])).
% 83.67/11.10 fof(f2339,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_Polynomial_Osmult(c_HOL_Oplus__class_Oplus(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(c_Polynomial_Osmult(X0,X2,tc_Complex_Ocomplex),c_Polynomial_Osmult(X1,X2,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(resolution,[status(thm)],[f2082,f1163])).
% 83.67/11.10 fof(f2343,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_Polynomial_Osmult(X0,c_Polynomial_OpCons(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),c_Polynomial_Osmult(X0,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f2082,f956])).
% 83.67/11.10 fof(f2373,plain,(
% 83.67/11.10 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1207,f2081])).
% 83.67/11.10 fof(f2402,plain,(
% 83.67/11.10 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1237,f2081])).
% 83.67/11.10 fof(f2406,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_Polynomial_Ocoeff(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Ocoeff(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1247,f2082])).
% 83.67/11.10 fof(f2477,plain,(
% 83.67/11.10 ![X0]: (c_Polynomial_Odegree(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 83.67/11.10 inference(resolution,[status(thm)],[f2105,f946])).
% 83.67/11.10 fof(f2678,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1411,f2082])).
% 83.67/11.10 fof(f2880,plain,(
% 83.67/11.10 ![X0,X1]: (c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(X1,X0,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(c_Polynomial_Opoly(X1,X0,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=X1)),
% 83.67/11.10 inference(resolution,[status(thm)],[f1478,f2092])).
% 83.67/11.10 fof(f2995,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Osmult(X1,X2,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_Polynomial_Osmult(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1519,f2082])).
% 83.67/11.10 fof(f3658,plain,(
% 83.67/11.10 ![X0,X1]: (~c_Polynomial_Odegree(X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_nat)|c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1681,f2082])).
% 83.67/11.10 fof(f4567,plain,(
% 83.67/11.10 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=X0)),
% 83.67/11.10 inference(resolution,[status(thm)],[f1844,f2099])).
% 83.67/11.10 fof(f4676,plain,(
% 83.67/11.10 ![X0]: (~c_Polynomial_Ocoeff(X0,c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X0=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(resolution,[status(thm)],[f1864,f2109])).
% 83.67/11.10 fof(f5297,plain,(
% 83.67/11.10 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_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(v_p)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 83.67/11.10 inference(resolution,[status(thm)],[f1933,f2157])).
% 83.67/11.10 fof(f5298,plain,(
% 83.67/11.10 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)),
% 83.67/11.10 inference(forward_subsumption_resolution,[status(thm)],[f5297,f963])).
% 83.67/11.10 fof(f26086,plain,(
% 83.67/11.10 ![X0]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f5298,f2678])).
% 83.67/11.10 fof(f26165,plain,(
% 83.67/11.10 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(v_p,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(X1,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f26086,f2678])).
% 83.67/11.10 fof(f26178,plain,(
% 83.67/11.10 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(v_p,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_Polynomial_Opoly(X1,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f2321,f26165])).
% 83.67/11.10 fof(f26234,plain,(
% 83.67/11.10 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(v_p,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f26165,f2373])).
% 83.67/11.10 fof(f26266,plain,(
% 83.67/11.10 ![X0,X1]: (c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(v_p,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f2678,f26178])).
% 83.67/11.10 fof(f26301,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(v_p,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f26234,f2327])).
% 83.67/11.10 fof(f33297,plain,(
% 83.67/11.10 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f5298,f2880])).
% 83.67/11.10 fof(f33485,plain,(
% 83.67/11.10 ![X0,X1,X2]: (c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f26266,f26301])).
% 83.67/11.10 fof(f33518,plain,(
% 83.67/11.10 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f5298,f33485])).
% 83.67/11.10 fof(f33556,plain,(
% 83.67/11.10 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(X1,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f26086,f33518])).
% 83.67/11.10 fof(f34156,plain,(
% 83.67/11.10 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),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),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f5298,f33556])).
% 83.67/11.10 fof(f34179,plain,(
% 83.67/11.10 ![X0]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)|c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),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),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(resolution,[status(thm)],[f34156,f1633])).
% 83.67/11.10 fof(f34203,plain,(
% 83.67/11.10 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),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),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(forward_subsumption_resolution,[status(thm)],[f34179,f2081])).
% 83.67/11.10 fof(f34228,plain,(
% 83.67/11.10 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),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),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f2322,f34203])).
% 83.67/11.10 fof(f34328,plain,(
% 83.67/11.10 ![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))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f34203,f34228])).
% 83.67/11.10 fof(f34665,plain,(
% 83.67/11.10 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f2402,f34328])).
% 83.67/11.10 fof(f45168,plain,(
% 83.67/11.10 ![X0]: (c_Polynomial_Osynthetic__div(v_p,X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(resolution,[status(thm)],[f3658,f1982])).
% 83.67/11.10 fof(f53183,plain,(
% 83.67/11.10 ![X0]: (~c_Polynomial_Ocoeff(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|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)))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f2477,f4676])).
% 83.67/11.10 fof(f53192,plain,(
% 83.67/11.10 ![X0]: (~c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Ocoeff(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|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)))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f2406,f53183])).
% 83.67/11.10 fof(f53193,plain,(
% 83.67/11.10 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|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)))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f34665,f53192])).
% 83.67/11.10 fof(f53194,plain,(
% 83.67/11.10 ![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)))),
% 83.67/11.10 inference(trivial_equality_resolution,[status(thm)],[f53193])).
% 83.67/11.10 fof(f53246,plain,(
% 83.67/11.10 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f2995,f53194])).
% 83.67/11.10 fof(f53282,plain,(
% 83.67/11.10 ![X0,X1]: (c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f53194,f2343])).
% 83.67/11.10 fof(f53283,plain,(
% 83.67/11.10 ![X0,X1]: (c_Polynomial_Osmult(c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f53194,f2339])).
% 83.67/11.10 fof(f53291,plain,(
% 83.67/11.10 ![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)))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f53194,f53246])).
% 83.67/11.10 fof(f53325,plain,(
% 83.67/11.10 ![X0]: (c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f53194,f53282])).
% 83.67/11.10 fof(f53326,plain,(
% 83.67/11.10 c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f34665,f53325])).
% 83.67/11.10 fof(f53327,plain,(
% 83.67/11.10 ![X0,X1]: (c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f4567,f53283])).
% 83.67/11.10 fof(f56016,plain,(
% 83.67/11.10 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p),
% 83.67/11.10 inference(backward_demodulation,[status(thm)],[f53326,f33297])).
% 83.67/11.10 fof(f56438,plain,(
% 83.67/11.10 ![X0]: (c_Polynomial_Osmult(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(paramodulation,[status(thm)],[f2318,f53327])).
% 83.67/11.10 fof(f56452,plain,(
% 83.67/11.10 ![X0]: (X0=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f2318,f56438])).
% 83.67/11.10 fof(f56643,plain,(
% 83.67/11.10 c_HOL_Otimes__class_Otimes(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p),
% 83.67/11.10 inference(backward_demodulation,[status(thm)],[f56452,f56016])).
% 83.67/11.10 fof(f56904,plain,(
% 83.67/11.10 c_HOL_Otimes__class_Otimes(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__2(v_p),tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p),
% 83.67/11.10 inference(backward_demodulation,[status(thm)],[f45168,f56643])).
% 83.67/11.10 fof(f57000,plain,(
% 83.67/11.10 c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p),
% 83.67/11.10 inference(forward_demodulation,[status(thm)],[f53291,f56904])).
% 84.54/11.23 fof(f57001,plain,(
% 84.54/11.23 $false),
% 84.54/11.23 inference(forward_subsumption_resolution,[status(thm)],[f57000,f1980])).
% 84.54/11.23 % SZS output end CNFRefutation for theBenchmark.p
% 84.54/11.23 % Elapsed time: 10.863907 seconds
% 84.54/11.23 % CPU time: 85.163451 seconds
% 84.54/11.23 % Total memory used: 673.091 MB
% 84.54/11.23 % Net memory used: 658.880 MB
%------------------------------------------------------------------------------