%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWW257+1 : TPTP v9.0.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.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:42 AM UTC 2025
% Result : Theorem 6.97s 7.17s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWW257+1 : TPTP v9.0.0. Released v5.2.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n014.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % 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:20:54 EDT 2025
% 0.12/0.33 % CPUTime :
% 6.97/7.17 % SZS status Theorem
% 6.97/7.17 % SZS output start Proof
% 6.97/7.17 tff(c_Groups_Ouminus__class_Ouminus_type, type, (
% 6.97/7.17 c_Groups_Ouminus__class_Ouminus: ( $i * $i ) > $i)).
% 6.97/7.17 tff(c_Groups_Oone__class_Oone_type, type, (
% 6.97/7.17 c_Groups_Oone__class_Oone: $i > $i)).
% 6.97/7.17 tff(tc_Complex_Ocomplex_type, type, (
% 6.97/7.17 tc_Complex_Ocomplex: $i)).
% 6.97/7.17 tff(hAPP_type, type, (
% 6.97/7.17 hAPP: ( $i * $i ) > $i)).
% 6.97/7.17 tff(v_a_____type, type, (
% 6.97/7.17 v_a____: $i)).
% 6.97/7.17 tff(v_k_____type, type, (
% 6.97/7.17 v_k____: $i)).
% 6.97/7.17 tff(tptp_fun_B_z_1_type, type, (
% 6.97/7.17 tptp_fun_B_z_1: $i)).
% 6.97/7.17 tff(c_Power_Opower__class_Opower_type, type, (
% 6.97/7.17 c_Power_Opower__class_Opower: $i > $i)).
% 6.97/7.17 tff(c_Groups_Otimes__class_Otimes_type, type, (
% 6.97/7.17 c_Groups_Otimes__class_Otimes: $i > $i)).
% 6.97/7.17 tff(c_Groups_Ominus__class_Ominus_type, type, (
% 6.97/7.17 c_Groups_Ominus__class_Ominus: ( $i * $i * $i ) > $i)).
% 6.97/7.17 tff(tc_Nat_Onat_type, type, (
% 6.97/7.17 tc_Nat_Onat: $i)).
% 6.97/7.17 tff(class_Groups_Ogroup__add_type, type, (
% 6.97/7.17 class_Groups_Ogroup__add: $i > $o)).
% 6.97/7.17 tff(c_Groups_Ozero__class_Ozero_type, type, (
% 6.97/7.17 c_Groups_Ozero__class_Ozero: $i > $i)).
% 6.97/7.17 tff(c_Groups_Oplus__class_Oplus_type, type, (
% 6.97/7.17 c_Groups_Oplus__class_Oplus: ( $i * $i * $i ) > $i)).
% 6.97/7.17 tff(class_Rings_Ocomm__semiring__1_type, type, (
% 6.97/7.17 class_Rings_Ocomm__semiring__1: $i > $o)).
% 6.97/7.17 tff(c_Nat_OSuc_type, type, (
% 6.97/7.17 c_Nat_OSuc: $i > $i)).
% 6.97/7.17 tff(class_Power_Opower_type, type, (
% 6.97/7.17 class_Power_Opower: $i > $o)).
% 6.97/7.17 tff(v_thesis_____type, type, (
% 6.97/7.17 v_thesis____: $o)).
% 6.97/7.17 tff(1,plain,
% 6.97/7.17 (class_Groups_Ogroup__add(tc_Complex_Ocomplex) <=> class_Groups_Ogroup__add(tc_Complex_Ocomplex)),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(2,axiom,(class_Groups_Ogroup__add(tc_Complex_Ocomplex)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','arity_Complex__Ocomplex__Groups_Ogroup__add')).
% 6.97/7.17 tff(3,plain,
% 6.97/7.17 (class_Groups_Ogroup__add(tc_Complex_Ocomplex)),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[2, 1])).
% 6.97/7.17 tff(4,plain,
% 6.97/7.17 (^[V_b: $i, V_a: $i, T_a: $i] : refl(((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)))) <=> ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)))))),
% 6.97/7.17 inference(bind,[status(th)],[])).
% 6.97/7.17 tff(5,plain,
% 6.97/7.17 (![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(quant_intro,[status(thm)],[4])).
% 6.97/7.17 tff(6,plain,
% 6.97/7.17 (![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(7,plain,
% 6.97/7.17 (^[V_b: $i, V_a: $i, T_a: $i] : trans(monotonicity(rewrite(((c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)) => (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b)) <=> ((~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))) | (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b))), ((class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)) => (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b))) <=> (class_Groups_Ogroup__add(T_a) => ((~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))) | (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b))))), rewrite((class_Groups_Ogroup__add(T_a) => ((~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))) | (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b))) <=> ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))), ((class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)) => (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b))) <=> ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))))),
% 6.97/7.17 inference(bind,[status(th)],[])).
% 6.97/7.17 tff(8,plain,
% 6.97/7.17 (![V_b: $i, V_a: $i, T_a: $i] : (class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)) => (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(quant_intro,[status(thm)],[7])).
% 6.97/7.17 tff(9,axiom,(![V_b: $i, V_a: $i, T_a: $i] : (class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a)) => (c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_minus__unique')).
% 6.97/7.17 tff(10,plain,
% 6.97/7.17 (![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[9, 8])).
% 6.97/7.17 tff(11,plain,
% 6.97/7.17 (![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[10, 6])).
% 6.97/7.17 tff(12,plain,(
% 6.97/7.17 ![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(skolemize,[status(sab)],[11])).
% 6.97/7.17 tff(13,plain,
% 6.97/7.17 (![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[12, 5])).
% 6.97/7.17 tff(14,plain,
% 6.97/7.17 (?[B_z: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) <=> ?[B_z: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(15,axiom,(?[B_z: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact__096EX_Az_O_A1_A_L_Az_A_K_A_Ia_A_K_Az_A_094_A_Ik_A_N_A1_J_J_A_061_A0_096')).
% 6.97/7.17 tff(16,plain,
% 6.97/7.17 (?[B_z: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[15, 14])).
% 6.97/7.17 tff(17,plain,(
% 6.97/7.17 c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 6.97/7.17 inference(skolemize,[status(sab)],[16])).
% 6.97/7.17 tff(18,plain,
% 6.97/7.17 (((~![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))) | ((c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) | (~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))) <=> ((~![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))) | (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) | (~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(19,plain,
% 6.97/7.17 ((~![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))) | ((c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) | (~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.17 inference(quant_inst,[status(thm)],[])).
% 6.97/7.17 tff(20,plain,
% 6.97/7.17 ((~![V_b: $i, V_a: $i, T_a: $i] : ((c_Groups_Ouminus__class_Ouminus(T_a, V_a) = V_b) | (~class_Groups_Ogroup__add(T_a)) | (~(c_Groups_Oplus__class_Oplus(T_a, V_a, V_b) = c_Groups_Ozero__class_Ozero(T_a))))) | (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) | (~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[19, 18])).
% 6.97/7.17 tff(21,plain,
% 6.97/7.17 (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.17 inference(unit_resolution,[status(thm)],[20, 17, 13, 3])).
% 6.97/7.17 tff(22,plain,
% 6.97/7.17 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex))),
% 6.97/7.17 inference(symmetry,[status(thm)],[21])).
% 6.97/7.17 tff(23,plain,
% 6.97/7.17 (class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) <=> class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(24,axiom,(class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','arity_Complex__Ocomplex__Rings_Ocomm__semiring__1')).
% 6.97/7.17 tff(25,plain,
% 6.97/7.17 (class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[24, 23])).
% 6.97/7.17 tff(26,plain,
% 6.97/7.17 (^[V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : refl(((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))) <=> ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))))),
% 6.97/7.17 inference(bind,[status(th)],[])).
% 6.97/7.17 tff(27,plain,
% 6.97/7.17 (![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))) <=> ![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(quant_intro,[status(thm)],[26])).
% 6.97/7.17 tff(28,plain,
% 6.97/7.17 (![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))) <=> ![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(29,plain,
% 6.97/7.17 (^[V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : rewrite((class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))) <=> ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))))),
% 6.97/7.17 inference(bind,[status(th)],[])).
% 6.97/7.17 tff(30,plain,
% 6.97/7.17 (![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : (class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry)))) <=> ![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(quant_intro,[status(thm)],[29])).
% 6.97/7.17 tff(31,axiom,(![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : (class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J')).
% 6.97/7.17 tff(32,plain,
% 6.97/7.17 (![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[31, 30])).
% 6.97/7.17 tff(33,plain,
% 6.97/7.17 (![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[32, 28])).
% 6.97/7.17 tff(34,plain,(
% 6.97/7.17 ![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(skolemize,[status(sab)],[33])).
% 6.97/7.17 tff(35,plain,
% 6.97/7.17 (![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))),
% 6.97/7.17 inference(modus_ponens,[status(thm)],[34, 27])).
% 6.97/7.17 tff(36,plain,
% 6.97/7.17 (((~![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))) | ((~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ((~![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))) | (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))),
% 6.97/7.17 inference(rewrite,[status(thm)],[])).
% 6.97/7.17 tff(37,plain,
% 6.97/7.17 ((~![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))) | ((~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))),
% 6.97/7.17 inference(quant_inst,[status(thm)],[])).
% 6.97/7.17 tff(38,plain,
% 6.97/7.17 ((~![V_ry: $i, V_rx: $i, V_lx: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), V_ry)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_rx), hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_lx), V_ry))))) | (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[37, 36])).
% 6.97/7.18 tff(39,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[38, 35, 25])).
% 6.97/7.18 tff(40,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(symmetry,[status(thm)],[39])).
% 6.97/7.18 tff(41,plain,
% 6.97/7.18 (^[V_q: $i, V_x: $i, T_a: $i] : refl(((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))) <=> ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(42,plain,
% 6.97/7.18 (![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))) <=> ![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[41])).
% 6.97/7.18 tff(43,plain,
% 6.97/7.18 (![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))) <=> ![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(44,plain,
% 6.97/7.18 (^[V_q: $i, V_x: $i, T_a: $i] : rewrite((class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))) <=> ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(45,plain,
% 6.97/7.18 (![V_q: $i, V_x: $i, T_a: $i] : (class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q)))) <=> ![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[44])).
% 6.97/7.18 tff(46,axiom,(![V_q: $i, V_x: $i, T_a: $i] : (class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J')).
% 6.97/7.18 tff(47,plain,
% 6.97/7.18 (![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[46, 45])).
% 6.97/7.18 tff(48,plain,
% 6.97/7.18 (![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[47, 43])).
% 6.97/7.18 tff(49,plain,(
% 6.97/7.18 ![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(skolemize,[status(sab)],[48])).
% 6.97/7.18 tff(50,plain,
% 6.97/7.18 (![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[49, 42])).
% 6.97/7.18 tff(51,plain,
% 6.97/7.18 (((~![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))) | ((~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))) <=> ((~![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))) | (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(52,plain,
% 6.97/7.18 ((~![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))) | ((~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))),
% 6.97/7.18 inference(quant_inst,[status(thm)],[])).
% 6.97/7.18 tff(53,plain,
% 6.97/7.18 ((~![V_q: $i, V_x: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_x), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), V_q)) = hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_x), c_Nat_OSuc(V_q))))) | (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[52, 51])).
% 6.97/7.18 tff(54,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[53, 50, 25])).
% 6.97/7.18 tff(55,plain,
% 6.97/7.18 (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
% 6.97/7.18 inference(symmetry,[status(thm)],[54])).
% 6.97/7.18 tff(56,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(monotonicity,[status(thm)],[55])).
% 6.97/7.18 tff(57,plain,
% 6.97/7.18 (^[V_b: $i, V_a: $i, T_a: $i] : refl(((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))) <=> ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(58,plain,
% 6.97/7.18 (![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[57])).
% 6.97/7.18 tff(59,plain,
% 6.97/7.18 (![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(60,plain,
% 6.97/7.18 (^[V_b: $i, V_a: $i, T_a: $i] : rewrite((class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))) <=> ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(61,plain,
% 6.97/7.18 (![V_b: $i, V_a: $i, T_a: $i] : (class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[60])).
% 6.97/7.18 tff(62,axiom,(![V_b: $i, V_a: $i, T_a: $i] : (class_Rings_Ocomm__semiring__1(T_a) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J')).
% 6.97/7.18 tff(63,plain,
% 6.97/7.18 (![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[62, 61])).
% 6.97/7.18 tff(64,plain,
% 6.97/7.18 (![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[63, 59])).
% 6.97/7.18 tff(65,plain,(
% 6.97/7.18 ![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(skolemize,[status(sab)],[64])).
% 6.97/7.18 tff(66,plain,
% 6.97/7.18 (![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[65, 58])).
% 6.97/7.18 tff(67,plain,
% 6.97/7.18 (((~![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))) | ((~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))), v_a____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ((~![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))) | (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))), v_a____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(68,plain,
% 6.97/7.18 ((~![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))) | ((~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))), v_a____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))),
% 6.97/7.18 inference(quant_inst,[status(thm)],[])).
% 6.97/7.18 tff(69,plain,
% 6.97/7.18 ((~![V_b: $i, V_a: $i, T_a: $i] : ((~class_Rings_Ocomm__semiring__1(T_a)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_a), V_b) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_b), V_a)))) | (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)) | (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))), v_a____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[68, 67])).
% 6.97/7.18 tff(70,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))), v_a____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), v_a____), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[69, 66, 25])).
% 6.97/7.18 tff(71,plain,
% 6.97/7.18 (class_Power_Opower(tc_Complex_Ocomplex) <=> class_Power_Opower(tc_Complex_Ocomplex)),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(72,axiom,(class_Power_Opower(tc_Complex_Ocomplex)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','arity_Complex__Ocomplex__Power_Opower')).
% 6.97/7.18 tff(73,plain,
% 6.97/7.18 (class_Power_Opower(tc_Complex_Ocomplex)),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[72, 71])).
% 6.97/7.18 tff(74,plain,
% 6.97/7.18 (^[V_m: $i, V_n: $i, T_a: $i] : refl(((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))))) <=> ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(75,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))))) <=> ![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[74])).
% 6.97/7.18 tff(76,plain,
% 6.97/7.18 (^[V_m: $i, V_n: $i, T_a: $i] : rewrite(((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(77,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[76])).
% 6.97/7.18 tff(78,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(79,plain,
% 6.97/7.18 (^[V_m: $i, V_n: $i, T_a: $i] : trans(monotonicity(rewrite((((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))) <=> (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))), ((class_Power_Opower(T_a) => (((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> (class_Power_Opower(T_a) => (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))))), rewrite((class_Power_Opower(T_a) => (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))), ((class_Power_Opower(T_a) => (((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(80,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : (class_Power_Opower(T_a) => (((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) <=> ![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[79])).
% 6.97/7.18 tff(81,axiom,(![V_m: $i, V_n: $i, T_a: $i] : (class_Power_Opower(T_a) => (((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) => (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_realpow__num__eq__if')).
% 6.97/7.18 tff(82,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[81, 80])).
% 6.97/7.18 tff(83,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[82, 78])).
% 6.97/7.18 tff(84,plain,(
% 6.97/7.18 ![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a))) & ((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))),
% 6.97/7.18 inference(skolemize,[status(sab)],[83])).
% 6.97/7.18 tff(85,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[84, 77])).
% 6.97/7.18 tff(86,plain,
% 6.97/7.18 (![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[85, 75])).
% 6.97/7.18 tff(87,plain,
% 6.97/7.18 (((~![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))) | ((~class_Power_Opower(tc_Complex_Ocomplex)) | (~((~((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))) | (~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))) <=> ((~![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))) | (~class_Power_Opower(tc_Complex_Ocomplex)) | (~((~((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))) | (~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(88,plain,
% 6.97/7.18 ((~![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))) | ((~class_Power_Opower(tc_Complex_Ocomplex)) | (~((~((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))) | (~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))),
% 6.97/7.18 inference(quant_inst,[status(thm)],[])).
% 6.97/7.18 tff(89,plain,
% 6.97/7.18 ((~![V_m: $i, V_n: $i, T_a: $i] : ((~class_Power_Opower(T_a)) | (~((~((~(V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = c_Groups_Oone__class_Oone(T_a)))) | (~((V_n = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), V_n) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a), V_m), hAPP(hAPP(c_Power_Opower__class_Opower(T_a), V_m), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, V_n, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))))) | (~class_Power_Opower(tc_Complex_Ocomplex)) | (~((~((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))) | (~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[88, 87])).
% 6.97/7.18 tff(90,plain,
% 6.97/7.18 (~((~((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))) | (~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[89, 86, 73])).
% 6.97/7.18 tff(91,plain,
% 6.97/7.18 (((~((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))) | (~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))))) | ((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))),
% 6.97/7.18 inference(tautology,[status(thm)],[])).
% 6.97/7.18 tff(92,plain,
% 6.97/7.18 ((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[91, 90])).
% 6.97/7.18 tff(93,plain,
% 6.97/7.18 ((~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) <=> (~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(94,axiom,(~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_kas_I2_J')).
% 6.97/7.18 tff(95,plain,
% 6.97/7.18 (~(v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[94, 93])).
% 6.97/7.18 tff(96,plain,
% 6.97/7.18 ((~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))) | (v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(tautology,[status(thm)],[])).
% 6.97/7.18 tff(97,plain,
% 6.97/7.18 ((~((v_k____ = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))))) | (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[96, 95])).
% 6.97/7.18 tff(98,plain,
% 6.97/7.18 (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[97, 92])).
% 6.97/7.18 tff(99,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), B_z!1), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)),
% 6.97/7.18 inference(symmetry,[status(thm)],[98])).
% 6.97/7.18 tff(100,plain,
% 6.97/7.18 (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)),
% 6.97/7.18 inference(transitivity,[status(thm)],[55, 99])).
% 6.97/7.18 tff(101,plain,
% 6.97/7.18 (hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))) = hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____))),
% 6.97/7.18 inference(monotonicity,[status(thm)],[100])).
% 6.97/7.18 tff(102,plain,
% 6.97/7.18 (hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)) = hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 6.97/7.18 inference(symmetry,[status(thm)],[101])).
% 6.97/7.18 tff(103,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat, v_k____, c_Groups_Oone__class_Oone(tc_Nat_Onat))))), v_a____)),
% 6.97/7.18 inference(monotonicity,[status(thm)],[102])).
% 6.97/7.18 tff(104,plain,
% 6.97/7.18 (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex))),
% 6.97/7.18 inference(transitivity,[status(thm)],[103, 70, 56, 40, 22])).
% 6.97/7.18 tff(105,plain,
% 6.97/7.18 (^[V_y_2: $i, V_x_2: $i, T_a: $i] : refl(((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))) <=> ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(106,plain,
% 6.97/7.18 (![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))) <=> ![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[105])).
% 6.97/7.18 tff(107,plain,
% 6.97/7.18 (![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))) <=> ![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(108,plain,
% 6.97/7.18 (^[V_y_2: $i, V_x_2: $i, T_a: $i] : rewrite((class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))) <=> ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))))),
% 6.97/7.18 inference(bind,[status(th)],[])).
% 6.97/7.18 tff(109,plain,
% 6.97/7.18 (![V_y_2: $i, V_x_2: $i, T_a: $i] : (class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2)))) <=> ![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(quant_intro,[status(thm)],[108])).
% 6.97/7.18 tff(110,axiom,(![V_y_2: $i, V_x_2: $i, T_a: $i] : (class_Groups_Ogroup__add(T_a) => ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_add__eq__0__iff')).
% 6.97/7.18 tff(111,plain,
% 6.97/7.18 (![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[110, 109])).
% 6.97/7.18 tff(112,plain,
% 6.97/7.18 (![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[111, 107])).
% 6.97/7.18 tff(113,plain,(
% 6.97/7.18 ![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(skolemize,[status(sab)],[112])).
% 6.97/7.18 tff(114,plain,
% 6.97/7.18 (![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[113, 106])).
% 6.97/7.18 tff(115,plain,
% 6.97/7.18 (((~![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))) | ((~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | ((c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) <=> (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))))) <=> ((~![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))) | (~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | ((c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) <=> (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(116,plain,
% 6.97/7.18 ((~![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))) | ((~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | ((c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) <=> (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))))),
% 6.97/7.18 inference(quant_inst,[status(thm)],[])).
% 6.97/7.18 tff(117,plain,
% 6.97/7.18 ((~![V_y_2: $i, V_x_2: $i, T_a: $i] : ((~class_Groups_Ogroup__add(T_a)) | ((c_Groups_Oplus__class_Oplus(T_a, V_x_2, V_y_2) = c_Groups_Ozero__class_Ozero(T_a)) <=> (V_y_2 = c_Groups_Ouminus__class_Ouminus(T_a, V_x_2))))) | (~class_Groups_Ogroup__add(tc_Complex_Ocomplex)) | ((c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) <=> (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex))))),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[116, 115])).
% 6.97/7.18 tff(118,plain,
% 6.97/7.18 ((c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) <=> (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_z!1), v_k____)), v_a____) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)))),
% 6.97/7.18 inference(unit_resolution,[status(thm)],[117, 114, 3])).
% 6.97/7.18 tff(119,plain,
% 6.97/7.18 ((~v_thesis____) <=> (~v_thesis____)),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(120,axiom,(~v_thesis____), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conj_1')).
% 6.97/7.18 tff(121,plain,
% 6.97/7.18 (~v_thesis____),
% 6.97/7.18 inference(modus_ponens,[status(thm)],[120, 119])).
% 6.97/7.18 tff(122,plain,
% 6.97/7.18 ((v_thesis____ | ![B_w: $i] : (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) <=> (v_thesis____ | ![B_w: $i] : (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(123,plain,
% 6.97/7.18 ((v_thesis____ | ![B_w: $i] : (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) <=> (v_thesis____ | ![B_w: $i] : (~(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(124,plain,
% 6.97/7.18 ((~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))) <=> (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(125,plain,
% 6.97/7.18 ((v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) <=> (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.18 inference(monotonicity,[status(thm)],[124])).
% 6.97/7.18 tff(126,plain,
% 6.97/7.18 ((v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) <=> (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.18 inference(rewrite,[status(thm)],[])).
% 6.97/7.18 tff(127,plain,
% 6.97/7.18 ((?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) => v_thesis____) <=> (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))),
% 6.97/7.19 inference(rewrite,[status(thm)],[])).
% 6.97/7.19 tff(128,axiom,(?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) => v_thesis____), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conj_0')).
% 6.97/7.19 tff(129,plain,
% 6.97/7.19 (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 6.97/7.19 inference(modus_ponens,[status(thm)],[128, 127])).
% 6.97/7.19 tff(130,plain,
% 6.97/7.19 (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 6.97/7.19 inference(modus_ponens,[status(thm)],[129, 125])).
% 6.97/7.19 tff(131,plain,
% 6.97/7.19 (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 6.97/7.19 inference(modus_ponens,[status(thm)],[130, 126])).
% 6.97/7.19 tff(132,plain,
% 6.97/7.19 (v_thesis____ | (~?[B_w: $i] : (c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex), B_w), v_k____)), v_a____)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 6.97/7.19 inference(modus_ponens,[status(thm)],[131, 125])).
% 6.97/7.19 Proof display could not be completed: monotonicity rule is not handled
% 7.05/7.26 % E exiting
%------------------------------------------------------------------------------