%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWW277+1 : TPTP v9.0.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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 05:36:45 AM UTC 2025
% Result : Theorem 1.21s 1.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SWW277+1 : TPTP v9.0.0. Released v5.2.0.
% 0.06/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n007.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 11:24:05 EDT 2025
% 0.11/0.32 % CPUTime :
% 1.21/1.39 % SZS status Theorem
% 1.21/1.39 % SZS output start Proof
% 1.21/1.39 tff(hAPP_type, type, (
% 1.21/1.39 hAPP: ( $i * $i ) > $i)).
% 1.21/1.39 tff(c_Divides_Odiv__class_Odiv_type, type, (
% 1.21/1.39 c_Divides_Odiv__class_Odiv: ( $i * $i * $i ) > $i)).
% 1.21/1.39 tff(c_Polynomial_OpCons_type, type, (
% 1.21/1.39 c_Polynomial_OpCons: ( $i * $i * $i ) > $i)).
% 1.21/1.39 tff(c_Groups_Ozero__class_Ozero_type, type, (
% 1.21/1.39 c_Groups_Ozero__class_Ozero: $i > $i)).
% 1.21/1.39 tff(tc_Polynomial_Opoly_type, type, (
% 1.21/1.39 tc_Polynomial_Opoly: $i > $i)).
% 1.21/1.39 tff(tc_Complex_Ocomplex_type, type, (
% 1.21/1.39 tc_Complex_Ocomplex: $i)).
% 1.21/1.39 tff(c_Groups_Oone__class_Oone_type, type, (
% 1.21/1.39 c_Groups_Oone__class_Oone: $i > $i)).
% 1.21/1.39 tff(c_Groups_Ouminus__class_Ouminus_type, type, (
% 1.21/1.39 c_Groups_Ouminus__class_Ouminus: ( $i * $i ) > $i)).
% 1.21/1.39 tff(v_a_____type, type, (
% 1.21/1.39 v_a____: $i)).
% 1.21/1.39 tff(v_s_____type, type, (
% 1.21/1.39 v_s____: $i)).
% 1.21/1.39 tff(c_Groups_Otimes__class_Otimes_type, type, (
% 1.21/1.39 c_Groups_Otimes__class_Otimes: $i > $i)).
% 1.21/1.39 tff(class_Divides_Osemiring__div_type, type, (
% 1.21/1.39 class_Divides_Osemiring__div: $i > $o)).
% 1.21/1.39 tff(class_Fields_Ofield_type, type, (
% 1.21/1.39 class_Fields_Ofield: $i > $o)).
% 1.21/1.39 tff(hBOOL_type, type, (
% 1.21/1.39 hBOOL: $i > $o)).
% 1.21/1.39 tff(c_Rings_Odvd__class_Odvd_type, type, (
% 1.21/1.39 c_Rings_Odvd__class_Odvd: $i > $i)).
% 1.21/1.39 tff(v_thesis_____type, type, (
% 1.21/1.39 v_thesis____: $o)).
% 1.21/1.39 tff(1,plain,
% 1.21/1.39 (^[T_1: $i] : refl((class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1))) <=> (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1))))),
% 1.21/1.39 inference(bind,[status(th)],[])).
% 1.21/1.39 tff(2,plain,
% 1.21/1.39 (![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1))) <=> ![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(quant_intro,[status(thm)],[1])).
% 1.21/1.39 tff(3,plain,
% 1.21/1.39 (![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1))) <=> ![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(4,plain,
% 1.21/1.39 (^[T_1: $i] : rewrite((class_Fields_Ofield(T_1) => class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1))) <=> (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1))))),
% 1.21/1.39 inference(bind,[status(th)],[])).
% 1.21/1.39 tff(5,plain,
% 1.21/1.39 (![T_1: $i] : (class_Fields_Ofield(T_1) => class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1))) <=> ![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(quant_intro,[status(thm)],[4])).
% 1.21/1.39 tff(6,axiom,(![T_1: $i] : (class_Fields_Ofield(T_1) => class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','arity_Polynomial__Opoly__Divides_Osemiring__div')).
% 1.21/1.39 tff(7,plain,
% 1.21/1.39 (![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[6, 5])).
% 1.21/1.39 tff(8,plain,
% 1.21/1.39 (![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[7, 3])).
% 1.21/1.39 tff(9,plain,(
% 1.21/1.39 ![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(skolemize,[status(sab)],[8])).
% 1.21/1.39 tff(10,plain,
% 1.21/1.39 (![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[9, 2])).
% 1.21/1.39 tff(11,plain,
% 1.21/1.39 (class_Fields_Ofield(tc_Complex_Ocomplex) <=> class_Fields_Ofield(tc_Complex_Ocomplex)),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(12,axiom,(class_Fields_Ofield(tc_Complex_Ocomplex)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','arity_Complex__Ocomplex__Fields_Ofield')).
% 1.21/1.39 tff(13,plain,
% 1.21/1.39 (class_Fields_Ofield(tc_Complex_Ocomplex)),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[12, 11])).
% 1.21/1.39 tff(14,plain,
% 1.21/1.39 (((~![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))) | (class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) | (~class_Fields_Ofield(tc_Complex_Ocomplex)))) <=> ((~![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))) | class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) | (~class_Fields_Ofield(tc_Complex_Ocomplex)))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(15,plain,
% 1.21/1.39 ((~![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))) | (class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) | (~class_Fields_Ofield(tc_Complex_Ocomplex)))),
% 1.21/1.39 inference(quant_inst,[status(thm)],[])).
% 1.21/1.39 tff(16,plain,
% 1.21/1.39 ((~![T_1: $i] : (class_Divides_Osemiring__div(tc_Polynomial_Opoly(T_1)) | (~class_Fields_Ofield(T_1)))) | class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) | (~class_Fields_Ofield(tc_Complex_Ocomplex))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[15, 14])).
% 1.21/1.39 tff(17,plain,
% 1.21/1.39 (class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 1.21/1.39 inference(unit_resolution,[status(thm)],[16, 13, 10])).
% 1.21/1.39 tff(18,plain,
% 1.21/1.39 (^[V_b: $i, V_a: $i, T_a: $i] : refl(((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a))) <=> ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a))))),
% 1.21/1.39 inference(bind,[status(th)],[])).
% 1.21/1.39 tff(19,plain,
% 1.21/1.39 (![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(quant_intro,[status(thm)],[18])).
% 1.21/1.39 tff(20,plain,
% 1.21/1.39 (![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(21,plain,
% 1.21/1.39 (^[V_b: $i, V_a: $i, T_a: $i] : trans(monotonicity(rewrite((hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b)) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b)) <=> ((~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b))), ((class_Divides_Osemiring__div(T_a) => (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b)) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b))) <=> (class_Divides_Osemiring__div(T_a) => ((~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b))))), rewrite((class_Divides_Osemiring__div(T_a) => ((~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b))) <=> ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))), ((class_Divides_Osemiring__div(T_a) => (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b)) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b))) <=> ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))))),
% 1.21/1.39 inference(bind,[status(th)],[])).
% 1.21/1.39 tff(22,plain,
% 1.21/1.39 (![V_b: $i, V_a: $i, T_a: $i] : (class_Divides_Osemiring__div(T_a) => (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b)) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(quant_intro,[status(thm)],[21])).
% 1.21/1.39 tff(23,axiom,(![V_b: $i, V_a: $i, T_a: $i] : (class_Divides_Osemiring__div(T_a) => (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b)) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','fact_dvd__mult__div__cancel')).
% 1.21/1.39 tff(24,plain,
% 1.21/1.39 (![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[23, 22])).
% 1.21/1.39 tff(25,plain,
% 1.21/1.39 (![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[24, 20])).
% 1.21/1.39 tff(26,plain,(
% 1.21/1.39 ![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(skolemize,[status(sab)],[25])).
% 1.21/1.39 tff(27,plain,
% 1.21/1.39 (![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[26, 19])).
% 1.21/1.39 tff(28,plain,
% 1.21/1.39 (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____)) <=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(29,axiom,(hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','fact__096_091_058_N_Aa_M_A1_058_093_Advd_As_096')).
% 1.21/1.39 tff(30,plain,
% 1.21/1.39 (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[29, 28])).
% 1.21/1.39 tff(31,plain,
% 1.21/1.39 (((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | ((~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____))) <=> ((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(32,plain,
% 1.21/1.39 (((hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))) <=> ((~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(33,plain,
% 1.21/1.39 (((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))) <=> ((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | ((~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____)))),
% 1.21/1.39 inference(monotonicity,[status(thm)],[32])).
% 1.21/1.39 tff(34,plain,
% 1.21/1.39 (((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))) <=> ((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____))),
% 1.21/1.39 inference(transitivity,[status(thm)],[33, 31])).
% 1.21/1.39 tff(35,plain,
% 1.21/1.39 ((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),
% 1.21/1.39 inference(quant_inst,[status(thm)],[])).
% 1.21/1.39 tff(36,plain,
% 1.21/1.39 ((~![V_b: $i, V_a: $i, T_a: $i] : ((hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), c_Divides_Odiv__class_Odiv(T_a, V_b, V_a)) = V_b) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a), V_a), V_b))) | (~class_Divides_Osemiring__div(T_a)))) | (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), v_s____))) | (~class_Divides_Osemiring__div(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____)),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[35, 34])).
% 1.21/1.39 tff(37,plain,
% 1.21/1.39 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))) = v_s____),
% 1.21/1.39 inference(unit_resolution,[status(thm)],[36, 30, 27, 17])).
% 1.21/1.39 tff(38,plain,
% 1.21/1.39 (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Divides_Odiv__class_Odiv(tc_Polynomial_Opoly(tc_Complex_Ocomplex), v_s____, c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))))),
% 1.21/1.39 inference(symmetry,[status(thm)],[37])).
% 1.21/1.39 tff(39,plain,
% 1.21/1.39 ((~v_thesis____) <=> (~v_thesis____)),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(40,axiom,(~v_thesis____), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conj_1')).
% 1.21/1.39 tff(41,plain,
% 1.21/1.39 (~v_thesis____),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[40, 39])).
% 1.21/1.39 tff(42,plain,
% 1.21/1.39 ((v_thesis____ | ![B_u: $i] : (~(v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))) <=> (v_thesis____ | ![B_u: $i] : (~(v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u))))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(43,plain,
% 1.21/1.39 ((v_thesis____ | ![B_u: $i] : (~(v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))) <=> (v_thesis____ | ![B_u: $i] : (~(v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u))))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(44,plain,
% 1.21/1.39 ((~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u))) <=> (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(45,plain,
% 1.21/1.39 ((v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))) <=> (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u))))),
% 1.21/1.39 inference(monotonicity,[status(thm)],[44])).
% 1.21/1.39 tff(46,plain,
% 1.21/1.39 ((v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))) <=> (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u))))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(47,plain,
% 1.21/1.39 ((?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)) => v_thesis____) <=> (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u))))),
% 1.21/1.39 inference(rewrite,[status(thm)],[])).
% 1.21/1.39 tff(48,axiom,(?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)) => v_thesis____), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conj_0')).
% 1.21/1.39 tff(49,plain,
% 1.21/1.39 (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[48, 47])).
% 1.21/1.39 tff(50,plain,
% 1.21/1.39 (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[49, 45])).
% 1.21/1.39 tff(51,plain,
% 1.21/1.39 (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[50, 46])).
% 1.21/1.39 tff(52,plain,
% 1.21/1.39 (v_thesis____ | (~?[B_u: $i] : (v_s____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), B_u)))),
% 1.21/1.39 inference(modus_ponens,[status(thm)],[51, 45])).
% 1.21/1.39 Proof display could not be completed: monotonicity rule is not handled
% 1.21/1.46 % E exiting
%------------------------------------------------------------------------------