%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ALG367-1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 04:58:59 AM UTC 2025
% Result : Unsatisfiable 2.95s 3.10s
% Output : Proof 2.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG367-1 : TPTP v9.0.0. Released v4.1.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu Jun 19 11:09:33 EDT 2025
% 0.13/0.33 % CPUTime :
% 2.95/3.10 % SZS status Unsatisfiable
% 2.95/3.10 % SZS output start Proof
% 2.95/3.10 tff(c_Polynomial_Odegree_type, type, (
% 2.95/3.10 c_Polynomial_Odegree: ( $i * $i ) > $i)).
% 2.95/3.10 tff(tc_Complex_Ocomplex_type, type, (
% 2.95/3.10 tc_Complex_Ocomplex: $i)).
% 2.95/3.10 tff(v_p_type, type, (
% 2.95/3.10 v_p: $i)).
% 2.95/3.10 tff(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly_type, type, (
% 2.95/3.10 c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly: ( $i * $i * $i ) > $i)).
% 2.95/3.10 tff(v_z_type, type, (
% 2.95/3.10 v_z: $i)).
% 2.95/3.10 tff(c_Polynomial_Opoly_type, type, (
% 2.95/3.10 c_Polynomial_Opoly: ( $i * $i * $i ) > $i)).
% 2.95/3.10 tff(c_HOL_Oplus__class_Oplus_type, type, (
% 2.95/3.10 c_HOL_Oplus__class_Oplus: ( $i * $i * $i ) > $i)).
% 2.95/3.10 tff(v_sko__local__Xthat__1_type, type, (
% 2.95/3.10 v_sko__local__Xthat__1: ( $i * $i * $i ) > $i)).
% 2.95/3.10 tff(class_Ring__and__Field_Ocomm__semiring__0_type, type, (
% 2.95/3.10 class_Ring__and__Field_Ocomm__semiring__0: $i > $o)).
% 2.95/3.10 tff(v_thesis_____type, type, (
% 2.95/3.10 v_thesis____: $o)).
% 2.95/3.10 tff(1,assumption,(~(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))), introduced(assumption)).
% 2.95/3.10 tff(2,plain,
% 2.95/3.10 (class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) <=> class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(3,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')).
% 2.95/3.10 tff(4,plain,
% 2.95/3.10 (class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[3, 2])).
% 2.95/3.10 tff(5,plain,
% 2.95/3.10 (^[V_x: $i, T_a: $i, V_p: $i, V_h: $i] : refl(((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a))) <=> ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a))))),
% 2.95/3.10 inference(bind,[status(th)],[])).
% 2.95/3.10 tff(6,plain,
% 2.95/3.10 (![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a))) <=> ![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))),
% 2.95/3.10 inference(quant_intro,[status(thm)],[5])).
% 2.95/3.10 tff(7,plain,
% 2.95/3.10 (![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a))) <=> ![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(8,axiom,(![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_poly__offset__poly_0')).
% 2.95/3.10 tff(9,plain,
% 2.95/3.10 (![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[8, 7])).
% 2.95/3.10 tff(10,plain,(
% 2.95/3.10 ![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))),
% 2.95/3.10 inference(skolemize,[status(sab)],[9])).
% 2.95/3.10 tff(11,plain,
% 2.95/3.10 (![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[10, 6])).
% 2.95/3.10 tff(12,plain,
% 2.95/3.10 (((~![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))) | ((~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))) <=> ((~![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))) | (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(13,plain,
% 2.95/3.10 ((~![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))) | ((~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))),
% 2.95/3.10 inference(quant_inst,[status(thm)],[])).
% 2.95/3.10 tff(14,plain,
% 2.95/3.10 ((~![V_x: $i, T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), V_x, T_a) = c_Polynomial_Opoly(V_p, c_HOL_Oplus__class_Oplus(V_h, V_x, T_a), T_a)))) | (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[13, 12])).
% 2.95/3.10 tff(15,plain,
% 2.95/3.10 ($false),
% 2.95/3.10 inference(unit_resolution,[status(thm)],[14, 11, 4, 1])).
% 2.95/3.10 tff(16,plain,(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)), inference(lemma,lemma(discharge,[]))).
% 2.95/3.10 tff(17,plain,
% 2.95/3.10 ((~v_thesis____) <=> (~v_thesis____)),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(18,axiom,(~v_thesis____), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_conjecture_0')).
% 2.95/3.10 tff(19,plain,
% 2.95/3.10 (~v_thesis____),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[18, 17])).
% 2.95/3.10 tff(20,plain,
% 2.95/3.10 (^[V_q: $i] : refl((v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))) <=> (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))))),
% 2.95/3.10 inference(bind,[status(th)],[])).
% 2.95/3.10 tff(21,plain,
% 2.95/3.10 (![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))) <=> ![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(quant_intro,[status(thm)],[20])).
% 2.95/3.10 tff(22,plain,
% 2.95/3.10 (![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))) <=> ![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(23,plain,
% 2.95/3.10 (^[V_q: $i] : trans(monotonicity(rewrite(((~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))) | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))) <=> ((~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))), ((((~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))) | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))) | v_thesis____) <=> (((~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))) | v_thesis____))), rewrite((((~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))) | v_thesis____) <=> (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))), ((((~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))) | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))) | v_thesis____) <=> (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))))),
% 2.95/3.10 inference(bind,[status(th)],[])).
% 2.95/3.10 tff(24,plain,
% 2.95/3.10 (![V_q: $i] : (((~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))) | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))) | v_thesis____) <=> ![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(quant_intro,[status(thm)],[23])).
% 2.95/3.10 tff(25,axiom,(![V_q: $i] : (((~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))) | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))) | v_thesis____)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_that_0')).
% 2.95/3.10 tff(26,plain,
% 2.95/3.10 (![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[25, 24])).
% 2.95/3.10 tff(27,plain,
% 2.95/3.10 (![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[26, 22])).
% 2.95/3.10 tff(28,plain,(
% 2.95/3.10 ![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(skolemize,[status(sab)],[27])).
% 2.95/3.10 tff(29,plain,
% 2.95/3.10 (![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[28, 21])).
% 2.95/3.10 tff(30,plain,
% 2.95/3.10 (((~![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))) | (v_thesis____ | (~(c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))) <=> ((~![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))) | v_thesis____ | (~(c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(31,plain,
% 2.95/3.10 ((~![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))) | (v_thesis____ | (~(c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))),
% 2.95/3.10 inference(quant_inst,[status(thm)],[])).
% 2.95/3.10 tff(32,plain,
% 2.95/3.10 ((~![V_q: $i] : (v_thesis____ | (~(c_Polynomial_Odegree(V_q, tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(V_q, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, V_q, v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex))))) | v_thesis____ | (~(c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))) | (~(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_p, c_HOL_Oplus__class_Oplus(v_z, v_sko__local__Xthat__1(v_p, c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), v_z), tc_Complex_Ocomplex), tc_Complex_Ocomplex)))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[31, 30])).
% 2.95/3.10 tff(33,plain,
% 2.95/3.10 (~(c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))),
% 2.95/3.10 inference(unit_resolution,[status(thm)],[32, 29, 19, 16])).
% 2.95/3.10 tff(34,plain,
% 2.95/3.10 (^[T_a: $i, V_p: $i, V_h: $i] : refl(((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a))) <=> ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a))))),
% 2.95/3.10 inference(bind,[status(th)],[])).
% 2.95/3.10 tff(35,plain,
% 2.95/3.10 (![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a))) <=> ![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))),
% 2.95/3.10 inference(quant_intro,[status(thm)],[34])).
% 2.95/3.10 tff(36,plain,
% 2.95/3.10 (![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a))) <=> ![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))),
% 2.95/3.10 inference(rewrite,[status(thm)],[])).
% 2.95/3.10 tff(37,axiom,(![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_degree__offset__poly_0')).
% 2.95/3.10 tff(38,plain,
% 2.95/3.10 (![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))),
% 2.95/3.10 inference(modus_ponens,[status(thm)],[37, 36])).
% 2.95/3.10 tff(39,plain,(
% 2.95/3.10 ![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))),
% 2.95/3.14 inference(skolemize,[status(sab)],[38])).
% 2.95/3.14 tff(40,plain,
% 2.95/3.14 (![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))),
% 2.95/3.14 inference(modus_ponens,[status(thm)],[39, 35])).
% 2.95/3.14 tff(41,plain,
% 2.95/3.14 (((~![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))) | ((~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))) <=> ((~![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))) | (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))),
% 2.95/3.14 inference(rewrite,[status(thm)],[])).
% 2.95/3.14 tff(42,plain,
% 2.95/3.14 ((~![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))) | ((~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex)))),
% 2.95/3.14 inference(quant_inst,[status(thm)],[])).
% 2.95/3.14 tff(43,plain,
% 2.95/3.14 ((~![T_a: $i, V_p: $i, V_h: $i] : ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p, V_h, T_a), T_a) = c_Polynomial_Odegree(V_p, T_a)))) | (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)) | (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p, v_z, tc_Complex_Ocomplex), tc_Complex_Ocomplex) = c_Polynomial_Odegree(v_p, tc_Complex_Ocomplex))),
% 2.95/3.14 inference(modus_ponens,[status(thm)],[42, 41])).
% 2.95/3.14 tff(44,plain,
% 2.95/3.14 ($false),
% 2.95/3.14 inference(unit_resolution,[status(thm)],[43, 40, 4, 33])).
% 2.95/3.14 % SZS output end Proof
% 2.99/3.15 % E exiting
%------------------------------------------------------------------------------