%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG437-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:49:25 AM UTC 2026
% Result : Unsatisfiable 38.31s 20.52s
% Output : CNFRefutation 17.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 45
% Syntax : Number of formulae : 214 ( 70 unt; 0 def)
% Number of atoms : 401 ( 240 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 370 ( 183 ~; 187 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 5 con; 0-3 aty)
% Number of variables : 399 ( 399 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f55,axiom,
! [T_a,V_a,V_p,V_c] :
( c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(V_a,V_p,T_a),V_c,T_a) = c_Polynomial_OpCons(hAPP(c_Polynomial_Opoly(V_p,T_a),V_c),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [T_a,V_p] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(V_p,T_a),T_a,T_a)
| c_Polynomial_Odegree(V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Int_Oring__char__0(T_a)
| ~ class_Ring__and__Field_Oidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [T_a,V_p] :
( ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(V_p,T_a),T_a,T_a)
| c_Polynomial_Odegree(V_p,T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Int_Oring__char__0(T_a)
| ~ class_Ring__and__Field_Oidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [T_a,V_a,V_e,V_b,V_d] :
( c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),V_e,T_a),V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a)
| ~ class_Ring__and__Field_Oring(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [T_a,V_p,V_h,V_x] :
( hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p,V_h,T_a),T_a),V_x) = hAPP(c_Polynomial_Opoly(V_p,T_a),c_HOL_Oplus__class_Oplus(V_h,V_x,T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [T_a,V_a,V_b] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [T_a,V_a,V_p,V_n] :
( hAPP(c_Polynomial_Ocoeff(c_Polynomial_Osmult(V_a,V_p,T_a),T_a),V_n) = c_HOL_Otimes__class_Otimes(V_a,hAPP(c_Polynomial_Ocoeff(V_p,T_a),V_n),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [T_a,V_x,V_x_H,V_y_H] :
( V_x_H = V_y_H
| c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,axiom,
! [T_a,V_x,V_y] :
( c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a)
| ~ class_Int_Onumber__ring(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,axiom,
! [T_a,V_a,V_b,V_c] :
( V_b = V_c
| c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Oplus__class_Oplus(V_a,V_c,T_a)
| ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f239,axiom,
! [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(hAPP(c_Polynomial_Opoly(V_p,T_a),V_c),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),tc_Polynomial_Opoly(T_a)) = V_p
| ~ class_Ring__and__Field_Ocomm__ring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,axiom,
! [T_a,V_a,V_p,V_x] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),T_a),V_x) = c_HOL_Otimes__class_Otimes(V_a,hAPP(c_Polynomial_Opoly(V_p,T_a),V_x),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f267,axiom,
! [T_a,V_p,V_c] :
( c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a),tc_Polynomial_Opoly(T_a)) = c_Polynomial_OpCons(hAPP(c_Polynomial_Opoly(V_p,T_a),V_c),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f298,axiom,
! [T_a,V_b] :
( c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__algebra(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f339,axiom,
! [T_a,V_a] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(V_a,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_HOL_Ozero(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f346,axiom,
! [T_a,V_p,V_q,V_x] :
( hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(V_p,V_q,tc_Polynomial_Opoly(T_a)),T_a),V_x) = c_HOL_Otimes__class_Otimes(hAPP(c_Polynomial_Opoly(V_p,T_a),V_x),hAPP(c_Polynomial_Opoly(V_q,T_a),V_x),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f366,axiom,
! [T_a,V_a,V_b] :
( c_HOL_Ouminus__class_Ouminus(V_a,T_a) = V_b
| c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f383,axiom,
! [T_a,V_p,V_c] :
( 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))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,axiom,
! [T_a,V_p,V_c] :
( c_Polynomial_Osynthetic__div(V_p,V_c,T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| c_Polynomial_Odegree(V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f386,axiom,
! [T_a,V_z,V_y] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_z,T_a),c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) = V_y
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f410,axiom,
! [T_a,V_a,V_p,V_x] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),T_a),V_x) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,hAPP(c_Polynomial_Opoly(V_p,T_a),V_x),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f425,axiom,
! [T_a,V_a,V_b] :
( V_a = V_b
| c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f450,axiom,
! [T_a,V_p] :
( V_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| hAPP(c_Polynomial_Ocoeff(V_p,T_a),c_Polynomial_Odegree(V_p,T_a)) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_HOL_Ozero(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f464,axiom,
! [T_a,V_a,V_p] :
( V_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| c_Polynomial_OpCons(V_a,V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_HOL_Ozero(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f482,axiom,
! [T_a,V_q] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_q,tc_Polynomial_Opoly(T_a)) = V_q
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f483,axiom,
! [T_a,V_p] :
( c_HOL_Oplus__class_Oplus(V_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a)) = V_p
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f485,axiom,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f495,axiom,
! [V_a,V_b,V_p] :
( V_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,c_Polynomial_OpCons(V_b,V_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xbasic__cqe__conv2__1(V_a,V_b,V_p)) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f508,axiom,
! [V_c,V_x] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(V_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_x) = V_c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f516,axiom,
! [V_x] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),V_x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f518,axiom,
( c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)
| v_p != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f523,negated_conjecture,
( c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) != c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)
| hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),v_x) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f524,negated_conjecture,
! [V_xa] :
( hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),V_xa) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f615,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f620,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f621,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f628,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f630,axiom,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f631,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f639,axiom,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f642,axiom,
class_Ring__and__Field_Oring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f643,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f645,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f646,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f648,axiom,
class_HOL_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f787,plain,
! [T_a] :
( ! [V_a,V_p,V_c] : c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(V_a,V_p,T_a),V_c,T_a) = c_Polynomial_OpCons(hAPP(c_Polynomial_Opoly(V_p,T_a),V_c),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f788,plain,
! [X0,X1,X2,X3] :
( c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_Polynomial_OpCons(hAPP(c_Polynomial_Opoly(X2,X0),X3),c_Polynomial_Osynthetic__div(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f787]) ).
fof(f801,plain,
! [X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(X1,X0),X0,X0)
| c_Polynomial_Odegree(X1,X0) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Int_Oring__char__0(X0)
| ~ class_Ring__and__Field_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f802,plain,
! [X0,X1] :
( ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(X1,X0),X0,X0)
| c_Polynomial_Odegree(X1,X0) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Int_Oring__char__0(X0)
| ~ class_Ring__and__Field_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f807,plain,
! [T_a] :
( ! [V_a,V_e,V_b,V_d] : c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),V_e,T_a),V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a)
| ~ class_Ring__and__Field_Oring(T_a) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f808,plain,
! [X0,X1,X2,X3,X4] :
( c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(X3,X1,X0),X2,X0),X4,X0),X0) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X3,X2,X0),X4,X0)
| ~ class_Ring__and__Field_Oring(X0) ),
inference(cnf_transformation,[status(thm)],[f807]) ).
fof(f809,plain,
! [T_a] :
( ! [V_p,V_h,V_x] : hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p,V_h,T_a),T_a),V_x) = hAPP(c_Polynomial_Opoly(V_p,T_a),c_HOL_Oplus__class_Oplus(V_h,V_x,T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f810,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,X2,X0),X0),X3) = hAPP(c_Polynomial_Opoly(X1,X0),c_HOL_Oplus__class_Oplus(X2,X3,X0))
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f809]) ).
fof(f847,plain,
! [T_a] :
( ! [V_a,V_b] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f87]) ).
fof(f848,plain,
! [X0,X1,X2] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X2,X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f847]) ).
fof(f873,plain,
! [T_a] :
( ! [V_a,V_p,V_n] : hAPP(c_Polynomial_Ocoeff(c_Polynomial_Osmult(V_a,V_p,T_a),T_a),V_n) = c_HOL_Otimes__class_Otimes(V_a,hAPP(c_Polynomial_Ocoeff(V_p,T_a),V_n),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f100]) ).
fof(f874,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Ocoeff(c_Polynomial_Osmult(X1,X2,X0),X0),X3) = c_HOL_Otimes__class_Otimes(X1,hAPP(c_Polynomial_Ocoeff(X2,X0),X3),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f873]) ).
fof(f899,plain,
! [V_x_H,V_y_H] :
( V_x_H = V_y_H
| ! [T_a] :
( ! [V_x] : c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f900,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| c_HOL_Ominus__class_Ominus(X1,X1,X0) != c_HOL_Ominus__class_Ominus(X2,X3,X0)
| ~ class_OrderedGroup_Oab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f899]) ).
fof(f1053,plain,
! [T_a] :
( ! [V_x,V_y] : c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a)
| ~ class_Int_Onumber__ring(T_a) ),
inference(miniscoping,[status(thm)],[f193]) ).
fof(f1054,plain,
! [X0,X1,X2] :
( c_HOL_Ominus__class_Ominus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X2,X0),X0)
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[status(thm)],[f1053]) ).
fof(f1074,plain,
! [V_b,V_c] :
( V_b = V_c
| ! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Oplus__class_Oplus(V_a,V_c,T_a)
| ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f1075,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| c_HOL_Oplus__class_Oplus(X1,X2,X0) != c_HOL_Oplus__class_Oplus(X1,X3,X0)
| ~ class_OrderedGroup_Ocancel__semigroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1074]) ).
fof(f1138,plain,
! [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(hAPP(c_Polynomial_Opoly(V_p,T_a),V_c),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),tc_Polynomial_Opoly(T_a)) = V_p
| ~ class_Ring__and__Field_Ocomm__ring__1(T_a) ),
inference(miniscoping,[status(thm)],[f239]) ).
fof(f1139,plain,
! [X0,X1,X2] :
( 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(hAPP(c_Polynomial_Opoly(X2,X0),X1),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),tc_Polynomial_Opoly(X0)) = X2
| ~ class_Ring__and__Field_Ocomm__ring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f1138]) ).
fof(f1161,plain,
! [T_a] :
( ! [V_a,V_p,V_x] : hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),T_a),V_x) = c_HOL_Otimes__class_Otimes(V_a,hAPP(c_Polynomial_Opoly(V_p,T_a),V_x),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f251]) ).
fof(f1162,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,X0),X0),X3) = c_HOL_Otimes__class_Otimes(X1,hAPP(c_Polynomial_Opoly(X2,X0),X3),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1161]) ).
fof(f1191,plain,
! [T_a] :
( ! [V_p,V_c] : c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a),tc_Polynomial_Opoly(T_a)) = c_Polynomial_OpCons(hAPP(c_Polynomial_Opoly(V_p,T_a),V_c),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f267]) ).
fof(f1192,plain,
! [X0,X1,X2] :
( c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Osmult(X2,c_Polynomial_Osynthetic__div(X1,X2,X0),X0),tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(hAPP(c_Polynomial_Opoly(X1,X0),X2),c_Polynomial_Osynthetic__div(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1191]) ).
fof(f1242,plain,
! [T_a] :
( ! [V_b] : c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__algebra(T_a) ),
inference(miniscoping,[status(thm)],[f298]) ).
fof(f1243,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_RealVector_Oreal__normed__algebra(X0) ),
inference(cnf_transformation,[status(thm)],[f1242]) ).
fof(f1309,plain,
! [T_a] :
( ! [V_a] : c_Polynomial_Odegree(c_Polynomial_OpCons(V_a,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_HOL_Ozero(T_a) ),
inference(miniscoping,[status(thm)],[f339]) ).
fof(f1310,plain,
! [X0,X1] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X0) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_HOL_Ozero(X0) ),
inference(cnf_transformation,[status(thm)],[f1309]) ).
fof(f1321,plain,
! [T_a] :
( ! [V_p,V_q,V_x] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(V_p,V_q,tc_Polynomial_Opoly(T_a)),T_a),V_x) = c_HOL_Otimes__class_Otimes(hAPP(c_Polynomial_Opoly(V_p,T_a),V_x),hAPP(c_Polynomial_Opoly(V_q,T_a),V_x),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f346]) ).
fof(f1322,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(X0)),X0),X3) = c_HOL_Otimes__class_Otimes(hAPP(c_Polynomial_Opoly(X1,X0),X3),hAPP(c_Polynomial_Opoly(X2,X0),X3),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1321]) ).
fof(f1356,plain,
! [X0,X1,X2] :
( c_HOL_Ouminus__class_Ouminus(X1,X0) = X2
| c_HOL_Oplus__class_Oplus(X1,X2,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f1387,plain,
! [T_a,V_p] :
( 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))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f383]) ).
fof(f1388,plain,
! [X0,X1,X2] :
( 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))
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1387]) ).
fof(f1389,plain,
! [T_a,V_p] :
( ! [V_c] : c_Polynomial_Osynthetic__div(V_p,V_c,T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| c_Polynomial_Odegree(V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f384]) ).
fof(f1390,plain,
! [X0,X1,X2] :
( c_Polynomial_Osynthetic__div(X1,X2,X0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| c_Polynomial_Odegree(X1,X0) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1389]) ).
fof(f1393,plain,
! [T_a] :
( ! [V_z,V_y] : c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_z,T_a),c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) = V_y
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
inference(miniscoping,[status(thm)],[f386]) ).
fof(f1394,plain,
! [X0,X1,X2] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Oplus__class_Oplus(X2,X1,X0),X0) = X2
| ~ class_OrderedGroup_Oab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1393]) ).
fof(f1434,plain,
! [T_a] :
( ! [V_a,V_p,V_x] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),T_a),V_x) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,hAPP(c_Polynomial_Opoly(V_p,T_a),V_x),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f410]) ).
fof(f1435,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X0),X3) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,hAPP(c_Polynomial_Opoly(X2,X0),X3),X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1434]) ).
fof(f1460,plain,
! [V_a,V_b] :
( V_a = V_b
| ! [T_a] :
( c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ) ),
inference(miniscoping,[status(thm)],[f425]) ).
fof(f1461,plain,
! [X0,X1,X2] :
( X1 = X2
| c_HOL_Ominus__class_Ominus(X1,X2,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_OrderedGroup_Oab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1460]) ).
fof(f1504,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| hAPP(c_Polynomial_Ocoeff(X1,X0),c_Polynomial_Odegree(X1,X0)) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_HOL_Ozero(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f1524,plain,
! [T_a,V_p] :
( V_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ! [V_a] : c_Polynomial_OpCons(V_a,V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_HOL_Ozero(T_a) ),
inference(miniscoping,[status(thm)],[f464]) ).
fof(f1525,plain,
! [X0,X1,X2] :
( X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| c_Polynomial_OpCons(X1,X2,X0) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_HOL_Ozero(X0) ),
inference(cnf_transformation,[status(thm)],[f1524]) ).
fof(f1557,plain,
! [T_a] :
( ! [V_q] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_q,tc_Polynomial_Opoly(T_a)) = V_q
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f482]) ).
fof(f1558,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,tc_Polynomial_Opoly(X0)) = X1
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1557]) ).
fof(f1559,plain,
! [T_a] :
( ! [V_p] : c_HOL_Oplus__class_Oplus(V_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a)) = V_p
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f483]) ).
fof(f1560,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),tc_Polynomial_Opoly(X0)) = X1
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1559]) ).
fof(f1563,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f485]) ).
fof(f1573,plain,
! [V_p] :
( V_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ! [V_a,V_b] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,c_Polynomial_OpCons(V_b,V_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xbasic__cqe__conv2__1(V_a,V_b,V_p)) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(miniscoping,[status(thm)],[f495]) ).
fof(f1574,plain,
! [X0,X1,X2] :
( X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,c_Polynomial_OpCons(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xbasic__cqe__conv2__1(X0,X1,X2)) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(cnf_transformation,[status(thm)],[f1573]) ).
fof(f1596,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = X0,
inference(cnf_transformation,[status(thm)],[f508]) ).
fof(f1607,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X0),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f1610,plain,
( c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)
| v_p != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f1617,plain,
( c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) != c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)
| hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),v_x) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(cnf_transformation,[status(thm)],[f523]) ).
fof(f1618,plain,
( ! [V_xa] : hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),V_xa) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) ),
inference(miniscoping,[status(thm)],[f524]) ).
fof(f1619,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),X0) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) ),
inference(cnf_transformation,[status(thm)],[f1618]) ).
fof(f1715,plain,
class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f1720,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f1721,plain,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f621]) ).
fof(f1728,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f628]) ).
fof(f1730,plain,
class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f630]) ).
fof(f1731,plain,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f631]) ).
fof(f1739,plain,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f639]) ).
fof(f1742,plain,
class_Ring__and__Field_Oring(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f642]) ).
fof(f1743,plain,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f643]) ).
fof(f1745,plain,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f645]) ).
fof(f1746,plain,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f646]) ).
fof(f1748,plain,
class_HOL_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f648]) ).
fof(f1784,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),X0) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),v_x) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1617,f1619]) ).
fof(f1787,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),X0) ),
inference(paramodulation,[status(thm)],[f1619,f1607]) ).
fof(f1788,plain,
( hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),v_x) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| v_p != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(resolution,[status(thm)],[f1610,f1617]) ).
fof(f1802,plain,
! [X0] : hAPP(c_Polynomial_Opoly(v_p,tc_Complex_Ocomplex),X0) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(backward_subsumption_resolution,[status(thm)],[f1784,f1787]) ).
fof(f1812,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| v_p != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(backward_demodulation,[status(thm)],[f1802,f1788]) ).
fof(f1817,plain,
v_p != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(trivial_equality_resolution,[status(thm)],[f1812]) ).
fof(f1929,plain,
! [X0,X1] :
( c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1607,f788]) ).
fof(f1932,plain,
! [X0,X1] : c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f1929,f1720]) ).
fof(f2034,plain,
! [X0,X1,X2] : c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X2,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f1932,f1932]) ).
fof(f2583,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1607,f810]) ).
fof(f2585,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f2583,f1720]) ).
fof(f2813,plain,
! [X0,X1,X2,X3] :
( ~ class_Ring__and__Field_Oring(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(X1,X1,X0),X2,X0),X3,X0) = X3
| ~ class_OrderedGroup_Ocancel__semigroup__add(X0) ),
inference(resolution,[status(thm)],[f1075,f808]) ).
fof(f3506,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(X0),X1,X0),X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(resolution,[status(thm)],[f1356,f848]) ).
fof(f3523,plain,
! [X0,X1] :
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(X0),X1,X0),X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3506]) ).
fof(f7513,plain,
! [X0,X1,X2] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X2,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f2034,f1388]) ).
fof(f7560,plain,
! [X0,X1,X2] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X2,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7513,f1720]) ).
fof(f7884,plain,
! [X0,X1] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1390,f7560]) ).
fof(f7917,plain,
! [X0,X1] :
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1932,f1390]) ).
fof(f7946,plain,
! [X0,X1] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f7884,f1720]) ).
fof(f7977,plain,
! [X0,X1] :
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f7917,f1720]) ).
fof(f8351,plain,
! [X0,X1] :
( c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_HOL_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f7977,f1525]) ).
fof(f8354,plain,
! [X0] :
( c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_HOL_Ozero(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[status(thm)],[f8351,f1310]) ).
fof(f8744,plain,
! [X0] :
( 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) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(backward_demodulation,[status(thm)],[f8792,f7977]) ).
fof(f8792,plain,
! [X0] : c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(forward_subsumption_resolution,[status(thm)],[f8354,f1748]) ).
fof(f9293,plain,
! [X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex,tc_Complex_Ocomplex)
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f7946,f801]) ).
fof(f9294,plain,
! [X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex,tc_Complex_Ocomplex)
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f9293,f1743]) ).
fof(f10329,plain,
! [X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex,tc_Complex_Ocomplex)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f9294,f1745]) ).
fof(f10331,plain,
! [X0] :
( ~ class_HOL_Ozero(tc_Complex_Ocomplex)
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex,tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f10329,f1310]) ).
fof(f10332,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f10331,f1748]) ).
fof(f10333,plain,
! [X0] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Oidom(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f10332,f802]) ).
fof(f10334,plain,
! [X0] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[status(thm)],[f10333,f1743]) ).
fof(f10337,plain,
( 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) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(backward_demodulation,[status(thm)],[f10338,f8744]) ).
fof(f10338,plain,
! [X0] : c_Polynomial_Odegree(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f10334,f1745]) ).
fof(f10343,plain,
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) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(trivial_equality_resolution,[status(thm)],[f10337]) ).
fof(f10924,plain,
! [X0] :
( 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(v_p,X0,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
| ~ class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1802,f1139]) ).
fof(f10986,plain,
! [X0] :
( 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(v_p,X0,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
| ~ class_Ring__and__Field_Ocomm__ring__1(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f10343,f10924]) ).
fof(f10987,plain,
! [X0] : 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(v_p,X0,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,
inference(forward_subsumption_resolution,[status(thm)],[f10986,f1730]) ).
fof(f11034,plain,
! [X0] :
( v_p = 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(v_p,X0,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f10987,f1560]) ).
fof(f11099,plain,
! [X0] : v_p = 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(v_p,X0,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(forward_subsumption_resolution,[status(thm)],[f11034,f1728]) ).
fof(f11111,plain,
c_HOL_Oplus__class_Oplus(v_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_p,
inference(backward_demodulation,[status(thm)],[f11099,f10987]) ).
fof(f12002,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1607,f1162]) ).
fof(f12017,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f12002,f1720]) ).
fof(f12064,plain,
! [X0,X1,X2] :
( hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X2) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f12017,f810]) ).
fof(f12079,plain,
! [X0,X1,X2] : hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X2) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f12064,f1720]) ).
fof(f13585,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(v_p,c_Polynomial_Osmult(X0,c_Polynomial_Osynthetic__div(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1802,f1192]) ).
fof(f13587,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_Osmult(X0,c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1607,f1192]) ).
fof(f13655,plain,
! [X0] : c_HOL_Oplus__class_Oplus(v_p,c_Polynomial_Osmult(X0,c_Polynomial_Osynthetic__div(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f13585,f1720]) ).
fof(f13659,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f8792,f13587]) ).
fof(f13660,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),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)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f8792,f13659]) ).
fof(f13661,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f10343,f13660]) ).
fof(f13662,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(forward_subsumption_resolution,[status(thm)],[f13661,f1720]) ).
fof(f13808,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)
| ~ class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f13662,f1558]) ).
fof(f13878,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f13808,f1728]) ).
fof(f13884,plain,
! [X0,X1,X2] : hAPP(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(X2,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f13878,f12079]) ).
fof(f13936,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f2585,f13884]) ).
fof(f13993,plain,
! [X0] :
( ~ class_Ring__and__Field_Oring(tc_Complex_Ocomplex)
| c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0
| ~ class_OrderedGroup_Ocancel__semigroup__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f13936,f2813]) ).
fof(f14252,plain,
! [X0] :
( ~ class_Ring__and__Field_Oring(tc_Complex_Ocomplex)
| c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13993,f1715]) ).
fof(f14779,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f14252,f1742]) ).
fof(f14812,plain,
! [X0] :
( c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex)
| ~ class_Int_Onumber__ring(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f14779,f1054]) ).
fof(f14905,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f14812,f1746]) ).
fof(f15433,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1
| c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex) != c_HOL_Ouminus__class_Ouminus(X1,tc_Complex_Ocomplex)
| ~ class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f14905,f900]) ).
fof(f15438,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f14905,f1461]) ).
fof(f15472,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1
| c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex) != c_HOL_Ouminus__class_Ouminus(X1,tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[status(thm)],[f15433,f1731]) ).
fof(f15475,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[status(thm)],[f15438,f1731]) ).
fof(f15988,plain,
! [X0] :
( ~ class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f15472,f3523]) ).
fof(f15997,plain,
! [X0] :
( ~ class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f14905,f15988]) ).
fof(f15998,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f15997,f1739]) ).
fof(f16001,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f15998,f15475]) ).
fof(f16103,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| ~ class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f15998,f1394]) ).
fof(f16231,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| ~ class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f14779,f16103]) ).
fof(f16232,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f16231,f1731]) ).
fof(f16456,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0,
inference(forward_demodulation,[status(thm)],[f16001,f16232]) ).
fof(f19084,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1802,f1322]) ).
fof(f19086,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1607,f1322]) ).
fof(f19114,plain,
! [X0,X1,X2] :
( hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X2) = c_HOL_Otimes__class_Otimes(hAPP(c_Polynomial_Opoly(X0,tc_Complex_Ocomplex),X2),X1,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1596,f1322]) ).
fof(f19142,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f19084,f1720]) ).
fof(f19144,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f19086,f1720]) ).
fof(f19186,plain,
! [X0,X1,X2] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X2) = c_HOL_Otimes__class_Otimes(hAPP(c_Polynomial_Opoly(X0,tc_Complex_Ocomplex),X2),X1,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f19114,f1720]) ).
fof(f21979,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f19142,f1243]) ).
fof(f22172,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f21979,f1721]) ).
fof(f22509,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(v_p,X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1),
inference(forward_demodulation,[status(thm)],[f19142,f19144]) ).
fof(f22637,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f22172,f22509]) ).
fof(f23139,plain,
! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X0),X1,tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f22637,f19186]) ).
fof(f23173,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f1607,f23139]) ).
fof(f23302,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Ocoeff(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f23173,f874]) ).
fof(f23559,plain,
! [X0,X1] : hAPP(c_Polynomial_Ocoeff(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f23302,f1720]) ).
fof(f24829,plain,
! [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))
| ~ class_HOL_Ozero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f23559,f1504]) ).
fof(f24857,plain,
! [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)),
inference(forward_subsumption_resolution,[status(thm)],[f24829,f1748]) ).
fof(f24935,plain,
c_HOL_Oplus__class_Oplus(v_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f24857,f13655]) ).
fof(f25001,plain,
v_p = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f11111,f24935]) ).
fof(f25310,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = 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)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1802,f1435]) ).
fof(f25422,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f13936,f25310]) ).
fof(f25423,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = X0
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f16456,f25422]) ).
fof(f25424,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f25423,f1720]) ).
fof(f30318,plain,
! [X0] :
( c_Polynomial_Osynthetic__div(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xbasic__cqe__conv2__1(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f25001,f1574]) ).
fof(f30349,plain,
! [X0] :
( c_Polynomial_Osynthetic__div(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f25424,f30318]) ).
fof(f34309,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| v_p = 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) ),
inference(paramodulation,[status(thm)],[f30349,f25001]) ).
fof(f34375,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| v_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(forward_demodulation,[status(thm)],[f10343,f34309]) ).
fof(f34376,plain,
! [X0] : X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f34375,f1817]) ).
fof(f34463,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f1563,f34376]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG437-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/15.41 % Computer : n010.cluster.edu
% 0.14/15.41 % Model : x86_64 x86_64
% 0.14/15.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/15.41 % Memory : 8046.5625MB
% 0.14/15.41 % OS : Linux 6.8.0-71-generic
% 0.14/15.41 % CPULimit : 300
% 0.14/15.41 % WCLimit : 300
% 0.14/15.41 % DateTime : Mon Sep 21 13:21:25 UTC 2026
% 0.14/15.42 % CPUTime :
% 0.14/15.46 % Drodi V4.1.1
% 38.31/20.52 % Refutation found
% 38.31/20.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 38.31/20.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.81/20.83 % Elapsed time: 5.401556 seconds
% 2.81/20.83 % CPU time: 40.972336 seconds
% 2.81/20.83 % Total memory used: 734.359 MB
% 2.81/20.83 % Net memory used: 714.412 MB
%------------------------------------------------------------------------------