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