%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG426-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 : Tue Sep 29 09:30:31 AM UTC 2026
% Result : Unsatisfiable 3.04s 0.65s
% Output : Refutation 3.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 49
% Syntax : Number of formulae : 214 ( 70 unt; 7 def)
% Number of atoms : 425 ( 213 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 395 ( 184 ~; 204 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 8 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-3 aty)
% Number of variables : 247 ( 0 sgn 247 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,axiom,
! [X2,X3,X0,X1,X4] :
( c_Polynomial_OpCons(X1,X2,X0) != c_Polynomial_OpCons(X3,X4,X0)
| ~ class_HOL_Ozero(X0)
| X2 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pCons__eq__iff_1) ).
fof(f35,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_Polynomial_Odegree(c_Polynomial_Osmult(X1,X2,X0),X0) = c_Polynomial_Odegree(X2,X0)
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_degree__smult__eq_1) ).
fof(f36,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_Polynomial_Odegree(c_Polynomial_Osmult(X1,X2,X0),X0) = c_Polynomial_Odegree(X2,X0)
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f35]) ).
fof(f148,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_Polynomial_OpCons(c_Polynomial_Opoly(X2,X3,X0),c_Polynomial_Osynthetic__div(X2,X3,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_synthetic__div__pCons_0) ).
fof(f179,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(X0),X1,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Omul__1_0) ).
fof(f239,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X1,X0),X1,X0) = c_HOL_Oone__class_Oone(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_field__inverse_0) ).
fof(f240,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Oone__class_Oone(X0) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X1,X0),X1,X0)
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f239]) ).
fof(f294,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_Polynomial_Opoly__gcd(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(X1,c_Polynomial_Odegree(X1,X0),X0),X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_poly__gcd__code_0) ).
fof(f335,axiom,
! [X0] :
( ~ class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp__zero_0) ).
fof(f336,plain,
! [X0] :
( ~ class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_HOL_Oone__class_Oone(X0) = c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(reorient_equations,[],[f335]) ).
fof(f350,axiom,
! [X0,X1] :
( ~ class_HOL_Ozero(X0)
| 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_degree__pCons__0_0) ).
fof(f351,plain,
! [X0,X1] :
( ~ class_HOL_Ozero(X0)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X0) ),
inference(reorient_equations,[],[f350]) ).
fof(f429,axiom,
! [X2,X3,X0,X1] :
( ~ 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__smult__right_0) ).
fof(f430,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_HOL_Otimes__class_Otimes(c_Polynomial_Osmult(X1,X2,X0),X3,tc_Polynomial_Opoly(X0)) = c_Polynomial_Osmult(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_Polynomial_Opoly(X0)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__smult__left_0) ).
fof(f445,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| 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(c_Polynomial_Opoly(X1,X2,X0),c_Polynomial_Osynthetic__div(X1,X2,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_synthetic__div__correct_0) ).
fof(f488,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__eq__0__iff_2) ).
fof(f489,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(reorient_equations,[],[f488]) ).
fof(f490,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__eq__0__iff_1) ).
fof(f491,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
inference(reorient_equations,[],[f490]) ).
fof(f519,axiom,
! [X2,X3,X0,X1] :
( ~ 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_poly__mult_0) ).
fof(f585,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_synthetic__div__eq__0__iff_0) ).
fof(f586,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) != c_Polynomial_Osynthetic__div(X1,X2,X0)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(X1,X0) ),
inference(reorient_equations,[],[f585]) ).
fof(f587,axiom,
! [X2,X0,X1] :
( ~ 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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_synthetic__div__eq__0__iff_1) ).
fof(f588,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_HOL_Ozero__class_Ozero(tc_nat) != c_Polynomial_Odegree(X1,X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = c_Polynomial_Osynthetic__div(X1,X2,X0) ),
inference(reorient_equations,[],[f587]) ).
fof(f623,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_poly__pCons_0) ).
fof(f628,axiom,
! [X0,X1] :
( ~ class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_Transcendental_Oexp(c_HOL_Ouminus__class_Ouminus(X1,X0),X0) = c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X1,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp__minus_0) ).
fof(f730,axiom,
! [X0,X1] :
( ~ class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_Transcendental_Oexp(X1,X0) != c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp__not__eq__zero_0) ).
fof(f731,plain,
! [X0,X1] :
( ~ class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_HOL_Ozero__class_Ozero(X0) != c_Transcendental_Oexp(X1,X0) ),
inference(reorient_equations,[],[f730]) ).
fof(f732,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Omonoid__add(X0)
| c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_monoid__add__class_Oadd__0__right_0) ).
fof(f746,axiom,
! [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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_leading__coeff__0__iff_0) ).
fof(f747,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) != c_Polynomial_Ocoeff(X1,c_Polynomial_Odegree(X1,X0),X0)
| ~ class_HOL_Ozero(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = X1 ),
inference(reorient_equations,[],[f746]) ).
fof(f753,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_Polynomial_Osmult(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_smult__eq__0__iff_2) ).
fof(f754,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = c_Polynomial_Osmult(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) ),
inference(reorient_equations,[],[f753]) ).
fof(f794,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),tc_Polynomial_Opoly(X0)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__poly__code_I2_J_0) ).
fof(f803,axiom,
! [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_fundamental__theorem__of__algebra__alt_1) ).
fof(f804,plain,
! [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_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) = X0 ),
inference(reorient_equations,[],[f803]) ).
fof(f807,axiom,
v_p = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pe_0) ).
fof(f808,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_p,
inference(reorient_equations,[],[f807]) ).
fof(f815,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_Polynomial_Osmult(X1,X2,X0) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_smult__eq__0__iff_0) ).
fof(f816,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) != c_Polynomial_Osmult(X1,X2,X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = X2
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f815]) ).
fof(f817,axiom,
! [X0] :
( ~ class_HOL_Ozero(X0)
| c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pCons__0__0_0) ).
fof(f818,plain,
! [X0] :
( ~ class_HOL_Ozero(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) ),
inference(reorient_equations,[],[f817]) ).
fof(f831,negated_conjecture,
! [X0] : c_Polynomial_Opoly(v_q,X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f832,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_q,X0,tc_Complex_Ocomplex),
inference(reorient_equations,[],[f831]) ).
fof(f833,negated_conjecture,
v_q != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f834,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != v_q,
inference(reorient_equations,[],[f833]) ).
fof(f884,axiom,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__RealVector_Oreal__normed__field) ).
fof(f908,axiom,
class_SEQ_Obanach(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__SEQ_Obanach) ).
fof(f912,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Oring__no__zero__divisors) ).
fof(f919,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f920,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0) ).
fof(f928,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__field) ).
fof(f929,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__add) ).
fof(f939,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add) ).
fof(f944,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
fof(f946,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Oidom) ).
fof(f950,axiom,
class_SEQ_Obanach(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__SEQ_Obanach) ).
fof(f951,axiom,
class_HOL_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__HOL_Ozero) ).
fof(f961,axiom,
! [X0] :
( class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Polynomial__Opoly__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1035,plain,
! [X2,X3,X0,X1] :
( class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_Polynomial_OpCons(c_Polynomial_Opoly(X2,X3,X0),c_Polynomial_Osynthetic__div(X2,X3,X0),X0) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f1102,plain,
! [X0] :
( class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_HOL_Oone__class_Oone(X0) = c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f1128,plain,
! [X2,X3,X0,X1] :
( 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) ),
inference(consistent_polarity_flipping,[],[f429]) ).
fof(f1129,plain,
! [X2,X3,X0,X1] :
( class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_HOL_Otimes__class_Otimes(c_Polynomial_Osmult(X1,X2,X0),X3,tc_Polynomial_Opoly(X0)) = c_Polynomial_Osmult(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_Polynomial_Opoly(X0)),X0) ),
inference(consistent_polarity_flipping,[],[f430]) ).
fof(f1135,plain,
! [X2,X0,X1] :
( class_Ring__and__Field_Ocomm__semiring__0(X0)
| 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(c_Polynomial_Opoly(X1,X2,X0),c_Polynomial_Osynthetic__div(X1,X2,X0),X0) ),
inference(consistent_polarity_flipping,[],[f445]) ).
fof(f1150,plain,
! [X2,X3,X0,X1] :
( 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) ),
inference(consistent_polarity_flipping,[],[f519]) ).
fof(f1172,plain,
! [X2,X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) != c_Polynomial_Osynthetic__div(X1,X2,X0)
| class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(X1,X0) ),
inference(consistent_polarity_flipping,[],[f586]) ).
fof(f1173,plain,
! [X2,X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Polynomial_Odegree(X1,X0)
| class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = c_Polynomial_Osynthetic__div(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f588]) ).
fof(f1186,plain,
! [X2,X3,X0,X1] :
( class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0) ),
inference(consistent_polarity_flipping,[],[f623]) ).
fof(f1187,plain,
! [X0,X1] :
( class_SEQ_Obanach(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| c_Transcendental_Oexp(c_HOL_Ouminus__class_Ouminus(X1,X0),X0) = c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X1,X0),X0) ),
inference(consistent_polarity_flipping,[],[f628]) ).
fof(f1202,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) != c_Transcendental_Oexp(X1,X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| class_SEQ_Obanach(X0) ),
inference(consistent_polarity_flipping,[],[f731]) ).
fof(f1226,plain,
! [X0,X1] :
( class_OrderedGroup_Ocomm__monoid__add(X0)
| c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),tc_Polynomial_Opoly(X0)) = X1 ),
inference(consistent_polarity_flipping,[],[f794]) ).
fof(f1265,plain,
~ class_SEQ_Obanach(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f908]) ).
fof(f1271,plain,
~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(consistent_polarity_flipping,[],[f920]) ).
fof(f1276,plain,
~ class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(consistent_polarity_flipping,[],[f929]) ).
fof(f1286,plain,
~ class_SEQ_Obanach(tc_Complex_Ocomplex),
inference(consistent_polarity_flipping,[],[f950]) ).
fof(f1320,plain,
v_p != v_q,
inference(superposition,[],[f834,f808]) ).
fof(f1324,definition,
( spl0_3
<=> class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1325,plain,
( class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1326,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| spl0_3 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1331,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)
| spl0_3 ),
inference(resolution,[],[f1326,f961]) ).
fof(f1332,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f1331,f919]) ).
fof(f1333,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f1332]) ).
fof(f1355,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0
| ~ spl0_3 ),
inference(resolution,[],[f179,f1325]) ).
fof(f1405,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0,
inference(resolution,[],[f732,f939]) ).
fof(f1490,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(resolution,[],[f489,f912]) ).
fof(f1493,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(resolution,[],[f491,f912]) ).
fof(f1620,plain,
( ~ class_RealVector_Oreal__normed__field(tc_RealDef_Oreal)
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f1102,f1265]) ).
fof(f1621,plain,
( ~ class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(resolution,[],[f1102,f1286]) ).
fof(f1622,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f1621,f928]) ).
fof(f1623,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Oexp(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1620,f884]) ).
fof(f1644,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0,
inference(resolution,[],[f1226,f1276]) ).
fof(f1646,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0,
inference(forward_demodulation,[],[f1644,f808]) ).
fof(f1693,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(resolution,[],[f754,f946]) ).
fof(f1695,plain,
! [X0] : v_p = c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1693,f808]) ).
fof(f1780,plain,
! [X0] : 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),
inference(resolution,[],[f351,f951]) ).
fof(f1782,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1780,f808]) ).
fof(f1813,plain,
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),
inference(resolution,[],[f818,f951]) ).
fof(f1815,plain,
v_p = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1813,f808]) ).
fof(f1890,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex)
| class_SEQ_Obanach(tc_Complex_Ocomplex) ),
inference(superposition,[],[f1202,f1622]) ).
fof(f1891,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)
| class_SEQ_Obanach(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f1890,f928]) ).
fof(f1892,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f1891,f1286]) ).
fof(f1948,plain,
! [X0,X1] :
( v_p != c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex)
| ~ class_HOL_Ozero(tc_Complex_Ocomplex)
| v_p = X1 ),
inference(superposition,[],[f13,f1815]) ).
fof(f1950,plain,
! [X0,X1] :
( v_p != c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex)
| v_p = X1 ),
inference(forward_subsumption_resolution,[],[f1948,f951]) ).
fof(f2009,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(resolution,[],[f240,f944]) ).
fof(f2057,plain,
! [X0] :
( ~ class_RealVector_Oreal__normed__field(tc_RealDef_Oreal)
| c_Transcendental_Oexp(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f1187,f1265]) ).
fof(f2060,plain,
! [X0] : c_Transcendental_Oexp(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f2057,f884]) ).
fof(f2085,plain,
! [X0,X1] :
( c_Polynomial_Odegree(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Odegree(X1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(resolution,[],[f36,f946]) ).
fof(f2347,plain,
! [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_Polynomial_OpCons(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(X0),v_p,tc_Complex_Ocomplex) = X0 ),
inference(forward_demodulation,[],[f804,f808]) ).
fof(f2629,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(resolution,[],[f816,f946]) ).
fof(f2631,plain,
! [X0,X1] :
( v_p != c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_demodulation,[],[f2629,f808]) ).
fof(f2632,plain,
! [X0,X1] :
( v_p != c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex)
| v_p = X1
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_demodulation,[],[f2631,f808]) ).
fof(f2901,plain,
! [X2,X0,X1] : 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),
inference(resolution,[],[f1128,f1271]) ).
fof(f2905,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osmult(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),
inference(resolution,[],[f1129,f1271]) ).
fof(f3053,plain,
! [X0] : c_Polynomial_Opoly__gcd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(X0,c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),
inference(resolution,[],[f294,f944]) ).
fof(f3054,plain,
! [X0] : c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(X0,c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_Polynomial_Opoly__gcd(X0,v_p,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f3053,f808]) ).
fof(f3116,plain,
! [X2,X0,X1] : c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_Polynomial_OpCons(c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f1035,f1271]) ).
fof(f3305,plain,
! [X2,X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f1186,f1271]) ).
fof(f3344,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat)
| class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) ),
inference(superposition,[],[f1173,f1782]) ).
fof(f3346,plain,
! [X0,X1] :
( class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) ),
inference(trivial_inequality_removal,[],[f3344]) ).
fof(f3348,plain,
! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f3346,f1271]) ).
fof(f3350,plain,
! [X0,X1] : v_p = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_p,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f3348,f808]) ).
fof(f3375,plain,
! [X2,X0,X1] : 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),
inference(resolution,[],[f1150,f1271]) ).
fof(f3562,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Osmult(X1,c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_Polynomial_Opoly(X0,X1,tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f1135,f1271]) ).
fof(f4942,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__field(tc_RealDef_Oreal)
| class_SEQ_Obanach(tc_RealDef_Oreal) ),
inference(superposition,[],[f1202,f2060]) ).
fof(f4943,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| class_SEQ_Obanach(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f4942,f884]) ).
fof(f4946,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oinverse__class_Oinverse(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f4943,f1265]) ).
fof(f4956,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f4946,f1623]) ).
fof(f6409,definition,
( spl0_145
<=> ! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f6410,plain,
( ! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f6409]) ).
fof(f7088,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_RealDef_Oreal)
| ~ spl0_145 ),
inference(superposition,[],[f4956,f6410]) ).
fof(f7231,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ spl0_145 ),
inference(forward_demodulation,[],[f7088,f6410]) ).
fof(f7710,plain,
( $false
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f7231,f6410]) ).
fof(f7711,plain,
~ spl0_145,
inference(avatar_contradiction_clause,[],[f7710]) ).
fof(f19007,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Osmult(X0,X2,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(forward_demodulation,[],[f2905,f2901]) ).
fof(f21655,plain,
! [X0,X1] : c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3116,f832]) ).
fof(f21741,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X1,v_q,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(superposition,[],[f1172,f21655]) ).
fof(f21772,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X1,v_q,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f21741,f1271]) ).
fof(f21778,plain,
! [X0,X1] :
( v_p != c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X1,v_q,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(forward_demodulation,[],[f21772,f808]) ).
fof(f21783,definition,
( spl0_276
<=> ! [X1] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X1,v_q,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl0_276])],[avatar_definition]) ).
fof(f21784,plain,
( ! [X1] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_OpCons(X1,v_q,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(avatar_component_clause,[],[f21783]) ).
fof(f21786,definition,
( spl0_277
<=> ! [X0] : v_p != c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl0_277])],[avatar_definition]) ).
fof(f21787,plain,
( ! [X0] : v_p != c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_277 ),
inference(avatar_component_clause,[],[f21786]) ).
fof(f21788,plain,
( spl0_276
| spl0_277 ),
inference(avatar_split_clause,[],[f21778,f21786,f21783]) ).
fof(f21792,plain,
( ! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat)
| class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) )
| ~ spl0_276 ),
inference(superposition,[],[f1173,f21784]) ).
fof(f21794,plain,
( ! [X0,X1] :
( class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) )
| ~ spl0_276 ),
inference(trivial_inequality_removal,[],[f21792]) ).
fof(f21796,plain,
( ! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_subsumption_resolution,[],[f21794,f1271]) ).
fof(f21799,plain,
( ! [X0,X1] : v_p = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_demodulation,[],[f21796,f808]) ).
fof(f21860,plain,
( ! [X0] : v_p = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(superposition,[],[f21799,f21655]) ).
fof(f21871,plain,
( ! [X0] :
( v_p != v_p
| v_p = c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex) )
| ~ spl0_276 ),
inference(superposition,[],[f1950,f21860]) ).
fof(f21891,plain,
( ! [X0] : v_p = c_Polynomial_Osynthetic__div(v_q,X0,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(trivial_inequality_removal,[],[f21871]) ).
fof(f21923,plain,
( ! [X0,X1] : v_p != c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| ~ spl0_277 ),
inference(superposition,[],[f21787,f21655]) ).
fof(f22557,plain,
! [X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3305,f832]) ).
fof(f22657,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f22557,f1490]) ).
fof(f22669,plain,
! [X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = X0,
inference(forward_demodulation,[],[f22657,f1405]) ).
fof(f22672,plain,
! [X0] :
( c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex) = c_Polynomial_OpCons(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xfundamental__theorem__of__algebra__alt__1(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex)),v_p,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(superposition,[],[f22669,f2347]) ).
fof(f22678,plain,
! [X0,X1] :
( v_p = c_Polynomial_Osynthetic__div(c_Polynomial_OpCons(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(superposition,[],[f3350,f22672]) ).
fof(f22721,plain,
( ! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| ~ spl0_277 ),
inference(forward_subsumption_resolution,[],[f22678,f21923]) ).
fof(f22730,plain,
( spl0_145
| ~ spl0_277 ),
inference(avatar_split_clause,[],[f22721,f21786,f6409]) ).
fof(f23093,plain,
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != v_p
| class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(v_q,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(superposition,[],[f1172,f21891]) ).
fof(f23094,plain,
( class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(v_q,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_subsumption_resolution,[],[f23093,f808]) ).
fof(f23097,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(v_q,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_subsumption_resolution,[],[f23094,f1271]) ).
fof(f23099,plain,
( c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex) = c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q,tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(superposition,[],[f3054,f23097]) ).
fof(f23101,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex)
| ~ class_HOL_Ozero(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_q
| ~ spl0_276 ),
inference(superposition,[],[f747,f23097]) ).
fof(f23103,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_q
| ~ spl0_276 ),
inference(forward_subsumption_resolution,[],[f23101,f951]) ).
fof(f23105,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_subsumption_resolution,[],[f23103,f834]) ).
fof(f24334,plain,
! [X0,X1] : c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_q,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(X0,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3375,f832]) ).
fof(f24400,plain,
! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,v_q,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f24334,f1490]) ).
fof(f24598,plain,
! [X2,X0,X1] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Osmult(X1,v_q,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X2,tc_Complex_Ocomplex),
inference(superposition,[],[f24400,f19007]) ).
fof(f26040,plain,
( ! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_Osmult(X0,v_q,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| ~ spl0_3 ),
inference(superposition,[],[f24598,f1355]) ).
fof(f26168,plain,
( ! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ spl0_3 ),
inference(superposition,[],[f26040,f3054]) ).
fof(f29522,plain,
( c_Polynomial_Odegree(v_q,tc_Complex_Ocomplex) = c_Polynomial_Odegree(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(superposition,[],[f2085,f23099]) ).
fof(f29527,plain,
( v_p != c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex)
| v_p = v_q
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(superposition,[],[f2632,f23099]) ).
fof(f29547,definition,
( spl0_290
<=> c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl0_290])],[avatar_definition]) ).
fof(f29549,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_290 ),
inference(avatar_component_clause,[],[f29547]) ).
fof(f29554,plain,
( v_p != c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_subsumption_resolution,[],[f29527,f1320]) ).
fof(f29558,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276 ),
inference(forward_demodulation,[],[f29522,f23097]) ).
fof(f29562,definition,
( spl0_292
<=> v_p = c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl0_292])],[avatar_definition]) ).
fof(f29564,plain,
( v_p != c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex)
| spl0_292 ),
inference(avatar_component_clause,[],[f29562]) ).
fof(f29565,plain,
( spl0_290
| ~ spl0_292
| ~ spl0_276 ),
inference(avatar_split_clause,[],[f29554,f21783,f29562,f29547]) ).
fof(f29569,definition,
( spl0_293
<=> c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl0_293])],[avatar_definition]) ).
fof(f29571,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_293 ),
inference(avatar_component_clause,[],[f29569]) ).
fof(f29572,plain,
( spl0_290
| spl0_293
| ~ spl0_276 ),
inference(avatar_split_clause,[],[f29558,f21783,f29569,f29547]) ).
fof(f29582,plain,
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex)
| ~ spl0_290 ),
inference(superposition,[],[f2009,f29549]) ).
fof(f29590,plain,
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Ocoeff(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl0_276
| ~ spl0_290 ),
inference(forward_subsumption_resolution,[],[f29582,f23105]) ).
fof(f29597,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)
| ~ spl0_276
| ~ spl0_290 ),
inference(forward_demodulation,[],[f29590,f1493]) ).
fof(f29603,plain,
( $false
| ~ spl0_276
| ~ spl0_290 ),
inference(forward_subsumption_resolution,[],[f29597,f1892]) ).
fof(f29604,plain,
( ~ spl0_276
| ~ spl0_290 ),
inference(avatar_contradiction_clause,[],[f29603]) ).
fof(f29617,plain,
( ! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat)
| class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) )
| ~ spl0_293 ),
inference(superposition,[],[f1173,f29571]) ).
fof(f29619,plain,
( ! [X0] :
( class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) )
| ~ spl0_293 ),
inference(trivial_inequality_removal,[],[f29617]) ).
fof(f29621,plain,
( ! [X0] : c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ spl0_293 ),
inference(forward_subsumption_resolution,[],[f29619,f1271]) ).
fof(f29625,plain,
( ! [X0] : v_p = c_Polynomial_Osynthetic__div(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ spl0_293 ),
inference(forward_demodulation,[],[f29621,f808]) ).
fof(f29663,plain,
( ! [X0] : c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(c_Polynomial_Opoly(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex)
| ~ spl0_293 ),
inference(superposition,[],[f3562,f29625]) ).
fof(f29684,plain,
( ! [X0] : c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),c_Polynomial_Osmult(X0,v_p,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ spl0_3
| ~ spl0_293 ),
inference(forward_demodulation,[],[f29663,f26168]) ).
fof(f29695,plain,
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex),v_p,tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ spl0_3
| ~ spl0_293 ),
inference(forward_demodulation,[],[f29684,f1695]) ).
fof(f29706,plain,
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex) = c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex)
| ~ spl0_3
| ~ spl0_293 ),
inference(forward_demodulation,[],[f29695,f1646]) ).
fof(f29712,plain,
( v_p = c_Polynomial_Opoly__gcd(v_q,v_p,tc_Complex_Ocomplex)
| ~ spl0_3
| ~ spl0_293 ),
inference(forward_demodulation,[],[f29706,f1815]) ).
fof(f29716,plain,
( $false
| ~ spl0_3
| spl0_292
| ~ spl0_293 ),
inference(forward_subsumption_resolution,[],[f29712,f29564]) ).
fof(f29717,plain,
( ~ spl0_3
| spl0_292
| ~ spl0_293 ),
inference(avatar_contradiction_clause,[],[f29716]) ).
cnf(s3,plain,
spl0_3,
inference(sat_conversion,[],[f1333]) ).
cnf(s229,plain,
~ spl0_145,
inference(sat_conversion,[],[f7711]) ).
cnf(s411,plain,
( spl0_276
| spl0_277 ),
inference(sat_conversion,[],[f21788]) ).
cnf(s418,plain,
( spl0_145
| ~ spl0_277 ),
inference(sat_conversion,[],[f22730]) ).
cnf(s435,plain,
( ~ spl0_276
| spl0_290
| ~ spl0_292 ),
inference(sat_conversion,[],[f29565]) ).
cnf(s436,plain,
( ~ spl0_276
| spl0_290
| spl0_293 ),
inference(sat_conversion,[],[f29572]) ).
cnf(s441,plain,
( ~ spl0_276
| ~ spl0_290 ),
inference(sat_conversion,[],[f29604]) ).
cnf(s442,plain,
( ~ spl0_3
| spl0_292
| ~ spl0_293 ),
inference(sat_conversion,[],[f29717]) ).
cnf(s462,plain,
~ spl0_277,
inference(rat,[],[s418,s229]) ).
cnf(s463,plain,
spl0_276,
inference(rat,[],[s411,s462]) ).
cnf(s464,plain,
~ spl0_290,
inference(rat,[],[s441,s463]) ).
cnf(s465,plain,
spl0_293,
inference(rat,[],[s436,s463,s464]) ).
cnf(s466,plain,
~ spl0_292,
inference(rat,[],[s435,s463,s464]) ).
cnf(s468,plain,
~ spl0_3,
inference(rat,[],[s442,s465,s466]) ).
cnf(s484,plain,
$false,
inference(rat,[],[s3,s468]) ).
fof(f29719,plain,
$false,
inference(avatar_sat_refutation,[],[s484]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG426-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.12 % Computer : n012.cluster.edu
% 0.06/0.12 % Model : x86_64 x86_64
% 0.06/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.12 % Memory : 8046.5625MB
% 0.06/0.12 % OS : Linux 6.8.0-71-generic
% 0.06/0.12 % CPULimit : 300
% 0.06/0.12 % WCLimit : 300
% 0.06/0.12 % DateTime : Mon Sep 28 20:22:19 UTC 2026
% 0.06/0.12 % CPUTime :
% 0.06/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.13 Running first-order model finding
% 0.06/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.04/0.65 % (3701845)Will run a generic schedule for satisfiability detection.
% 3.04/0.65 % (3701851)% WARNING: option uhcvi not known.
% 3.04/0.65 % (3701853)dis+10_1_sil=32000:sp=arity:random_seed=206189978:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.04/0.65 % (3701854)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=992552523:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.04/0.65 % (3701850)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3579175189_2999 on theBenchmark for (2999ds/0Mi)
% 3.04/0.65 % (3701851)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1297997769:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.04/0.65 % (3701852)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1976454952:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.04/0.65 % (3701855)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3972389577:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.04/0.65 % (3701856)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3939650944:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.04/0.65 % (3701853)Instruction limit reached!
% 3.04/0.65 % (3701853)------------------------------
% 3.04/0.65 % (3701853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701853)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701853)Termination reason: Instruction limit
% 3.04/0.65 % (3701853)Termination phase: Saturation
% 3.04/0.65 % (3701853)Time elapsed: 0.036 s
% 3.04/0.65 % (3701853)Peak memory usage: 13 MB
% 3.04/0.65 % (3701853)Instructions burned: 103 (million)
% 3.04/0.65 % TRYING [1]
% 3.04/0.65 % TRYING [2]
% 3.04/0.65 % (3701854)Instruction limit reached!
% 3.04/0.65 % (3701854)------------------------------
% 3.04/0.65 % (3701854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701854)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701854)Termination reason: Instruction limit
% 3.04/0.65 % (3701854)Termination phase: Saturation
% 3.04/0.65 % (3701854)Time elapsed: 0.042 s
% 3.04/0.65 % (3701854)Peak memory usage: 13 MB
% 3.04/0.65 % (3701854)Instructions burned: 117 (million)
% 3.04/0.65 % (3701855)Instruction limit reached!
% 3.04/0.65 % (3701855)------------------------------
% 3.04/0.65 % (3701855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701855)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701855)Termination reason: Instruction limit
% 3.04/0.65 % (3701855)Termination phase: Saturation
% 3.04/0.65 % (3701855)Time elapsed: 0.042 s
% 3.04/0.65 % (3701855)Peak memory usage: 14 MB
% 3.04/0.65 % (3701855)Instructions burned: 132 (million)
% 3.04/0.65 % (3701864)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3551976894:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.04/0.65 % (3701866)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3717854849:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.04/0.65 % (3701865)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1825880020:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.04/0.65 % (3701856)Instruction limit reached!
% 3.04/0.65 % (3701856)------------------------------
% 3.04/0.65 % (3701856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701856)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701856)Termination reason: Instruction limit
% 3.04/0.65 % (3701856)Termination phase: Saturation
% 3.04/0.65 % (3701856)Time elapsed: 0.056 s
% 3.04/0.65 % (3701856)Peak memory usage: 15 MB
% 3.04/0.65 % (3701856)Instructions burned: 161 (million)
% 3.04/0.65 % (3701870)ott-21_1_sil=16000:fs=off:random_seed=954119213:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.04/0.65 % TRYING [1]
% 3.04/0.65 % TRYING [3]
% 3.04/0.65 % TRYING [2]
% 3.04/0.65 % (3701865)Instruction limit reached!
% 3.04/0.65 % (3701865)------------------------------
% 3.04/0.65 % (3701865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701865)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701865)Termination reason: Instruction limit
% 3.04/0.65 % (3701865)Termination phase: Saturation
% 3.04/0.65 % (3701865)Time elapsed: 0.041 s
% 3.04/0.65 % (3701865)Peak memory usage: 13 MB
% 3.04/0.65 % (3701865)Instructions burned: 131 (million)
% 3.04/0.65 % (3701872)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2163281994:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.04/0.65 % (3701870)Instruction limit reached!
% 3.04/0.65 % (3701870)------------------------------
% 3.04/0.65 % (3701870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701870)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701870)Termination reason: Instruction limit
% 3.04/0.65 % (3701870)Termination phase: Saturation
% 3.04/0.65 % (3701870)Time elapsed: 0.041 s
% 3.04/0.65 % (3701870)Peak memory usage: 12 MB
% 3.04/0.65 % (3701870)Instructions burned: 182 (million)
% 3.04/0.65 % (3701874)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1293280349:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.04/0.65 % TRYING [3]
% 3.04/0.65 % TRYING [1]
% 3.04/0.65 % TRYING [2]
% 3.04/0.65 % (3701864)Instruction limit reached!
% 3.04/0.65 % (3701864)------------------------------
% 3.04/0.65 % (3701864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701864)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701864)Termination reason: Instruction limit
% 3.04/0.65 % (3701864)Termination phase: Finite model building constraint generation
% 3.04/0.65 % (3701864)Time elapsed: 0.148 s
% 3.04/0.65 % (3701864)Peak memory usage: 31 MB
% 3.04/0.65 % (3701864)Instructions burned: 718 (million)
% 3.04/0.65 % (3701876)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=926772502:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 3.04/0.65 % (3701866)Instruction limit reached!
% 3.04/0.65 % (3701866)------------------------------
% 3.04/0.65 % (3701866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701866)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701866)Termination reason: Instruction limit
% 3.04/0.65 % (3701866)Termination phase: Saturation
% 3.04/0.65 % (3701866)Time elapsed: 0.183 s
% 3.04/0.65 % (3701866)Peak memory usage: 19 MB
% 3.04/0.65 % (3701866)Instructions burned: 686 (million)
% 3.04/0.65 % (3701878)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2720150675:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 3.04/0.65 % (3701872)Instruction limit reached!
% 3.04/0.65 % (3701872)------------------------------
% 3.04/0.65 % (3701872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701872)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701872)Termination reason: Instruction limit
% 3.04/0.65 % (3701872)Termination phase: Saturation
% 3.04/0.65 % (3701872)Time elapsed: 0.172 s
% 3.04/0.65 % (3701872)Peak memory usage: 15 MB
% 3.04/0.65 % (3701872)Instructions burned: 479 (million)
% 3.04/0.65 % (3701880)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1796814295:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 3.04/0.65 % (3701874)Instruction limit reached!
% 3.04/0.65 % (3701874)------------------------------
% 3.04/0.65 % (3701874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701874)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701874)Termination reason: Instruction limit
% 3.04/0.65 % (3701874)Termination phase: Finite model building SAT solving
% 3.04/0.65 % (3701874)Time elapsed: 0.221 s
% 3.04/0.65 % (3701874)Peak memory usage: 29 MB
% 3.04/0.65 % (3701874)Instructions burned: 867 (million)
% 3.04/0.65 % (3701882)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1446139433:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 3.04/0.65 % (3701851) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3701845-3701851"...
% 3.04/0.65 % (3701851)...printing done.
% 3.04/0.65 % (3701851)Refutation found. Thanks to Tanya!
% 3.04/0.65 % SZS status Unsatisfiable for theBenchmark
% 3.04/0.65 % SZS output start Proof for theBenchmark
% See solution above
% 3.04/0.65 % (3701851)------------------------------
% 3.04/0.65 % (3701851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.65 % (3701851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.65 % (3701851)CaDiCaL version: 2.1.3
% 3.04/0.65 % (3701851)Termination reason: Refutation
% 3.04/0.65 % (3701851)Time elapsed: 0.456 s
% 3.04/0.65 % (3701851)Peak memory usage: 25 MB
% 3.04/0.65 % (3701851)Instructions burned: 1386 (million)
% 3.04/0.65 % (3701845)Success in time 0.512 s
% 3.04/0.65 % Vampire exiting
%------------------------------------------------------------------------------