%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWW287+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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 : 600s % DateTime : Thu Jul 21 02:21:28 EDT 2022 % Result : Theorem 8.32s 8.56s % Output : Proof 8.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SWW287+1 : TPTP v8.1.0. Released v5.2.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n018.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 : 600 % 0.12/0.33 % DateTime : Sun Jun 5 21:45:04 EDT 2022 % 0.12/0.33 % CPUTime : % 8.32/8.56 (* PROOF-FOUND *) % 8.32/8.56 % SZS status Theorem % 8.32/8.56 (* BEGIN-PROOF *) % 8.32/8.56 % SZS output start Proof % 8.32/8.56 Theorem conj_0 : ((forall B_x : zenon_U, (((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) B_x) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex)))->((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_q)) B_x) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex)))))<->((hBOOL (hAPP (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Polynomial_Odegree (tc_Complex_Ocomplex) (v_p)))))\/(((v_p) = (c_Groups_Ozero__class_Ozero (tc_Polynomial_Opoly (tc_Complex_Ocomplex))))/\((v_q) = (c_Groups_Ozero__class_Ozero (tc_Polynomial_Opoly (tc_Complex_Ocomplex))))))). % 8.32/8.56 Proof. % 8.32/8.56 assert (zenon_L1_ : forall (zenon_TB_x_btd : zenon_U), (~(((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) zenon_TB_x_btd) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex)))->((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_q)) zenon_TB_x_btd) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex))))) -> (hBOOL (hAPP (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Polynomial_Odegree (tc_Complex_Ocomplex) (v_p))))) -> False). % 8.32/8.56 do 1 intro. intros zenon_H493 zenon_H494. % 8.32/8.56 apply (zenon_notimply_s _ _ zenon_H493). zenon_intro zenon_H497. zenon_intro zenon_H496. % 8.32/8.56 generalize (fact__096_B_Bx_O_A_091_124_Ap_Advd_Aq_A_094_ASuc_An_059_Apoly_Ap_Ax_A_061_A0_059_Apoly_Aq_Ax_A_126_061_A0_A_124_093_A_061_061_062_AFalse_096 zenon_TB_x_btd). zenon_intro zenon_H498. % 8.32/8.56 apply (zenon_imply_s _ _ zenon_H498); [ zenon_intro zenon_H49a | zenon_intro zenon_H499 ]. % 8.32/8.56 cut ((hBOOL (hAPP (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Polynomial_Odegree (tc_Complex_Ocomplex) (v_p))))) = (hBOOL (hAPP (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Nat_OSuc (v_n____)))))). % 8.32/8.56 intro zenon_D_pnotp. % 8.32/8.56 apply zenon_H49a. % 8.32/8.56 rewrite <- zenon_D_pnotp. % 8.32/8.56 exact zenon_H494. % 8.32/8.56 cut (((hAPP (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Polynomial_Odegree (tc_Complex_Ocomplex) (v_p)))) = (hAPP (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Nat_OSuc (v_n____)))))); [idtac | apply NNPP; zenon_intro zenon_H49b]. % 8.32/8.56 congruence. % 8.32/8.56 cut (((hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Polynomial_Odegree (tc_Complex_Ocomplex) (v_p))) = (hAPP (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) (c_Nat_OSuc (v_n____))))); [idtac | apply NNPP; zenon_intro zenon_H49c]. % 8.32/8.56 cut (((hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)) = (hAPP (c_Rings_Odvd__class_Odvd (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_p)))); [idtac | apply NNPP; zenon_intro zenon_H49d]. % 8.32/8.56 congruence. % 8.32/8.56 apply zenon_H49d. apply refl_equal. % 8.32/8.56 cut (((c_Polynomial_Odegree (tc_Complex_Ocomplex) (v_p)) = (c_Nat_OSuc (v_n____)))); [idtac | apply NNPP; zenon_intro zenon_H49e]. % 8.32/8.56 cut (((hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)) = (hAPP (c_Power_Opower__class_Opower (tc_Polynomial_Opoly (tc_Complex_Ocomplex))) (v_q)))); [idtac | apply NNPP; zenon_intro zenon_H49f]. % 8.32/8.56 congruence. % 8.32/8.56 apply zenon_H49f. apply refl_equal. % 8.32/8.56 exact (zenon_H49e fact_n). % 8.32/8.56 apply (zenon_imply_s _ _ zenon_H499); [ zenon_intro zenon_H4a1 | zenon_intro zenon_H4a0 ]. % 8.32/8.56 exact (zenon_H4a1 zenon_H497). % 8.32/8.56 exact (zenon_H496 zenon_H4a0). % 8.32/8.56 (* end of lemma zenon_L1_ *) % 8.32/8.56 apply NNPP. intro zenon_G. % 8.32/8.56 apply (zenon_imply_s _ _ fact__096_091_124_AALL_Ax_O_Apoly_Ap_Ax_A_061_A0_A_N_N_062_Apoly_Aq_Ax_A_061_A0_059_Adegree_Ap_A_061_Adegree_Ap_059_Adegree_Ap_A_126_061_A0_A_124_093_061_061_062_Ap_Advd_Aq_A_094_Adegree_Ap_096); [ zenon_intro zenon_H4a3 | zenon_intro zenon_H4a2 ]. % 8.32/8.57 apply (zenon_notallex_s (fun B_x : zenon_U => (((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) B_x) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex)))->((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_q)) B_x) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex))))) zenon_H4a3); [ zenon_intro zenon_H4a4; idtac ]. % 8.32/8.57 elim zenon_H4a4. zenon_intro zenon_TB_x_btd. zenon_intro zenon_H493. % 8.32/8.57 apply (zenon_notequiv_s _ _ zenon_G); [ zenon_intro zenon_H4a3; zenon_intro zenon_H4a7 | zenon_intro zenon_H4a6; zenon_intro zenon_H4a5 ]. % 8.32/8.57 apply (zenon_or_s _ _ zenon_H4a7); [ zenon_intro zenon_H494 | zenon_intro zenon_H4a8 ]. % 8.32/8.57 apply (zenon_L1_ zenon_TB_x_btd); trivial. % 8.32/8.57 apply (zenon_and_s _ _ zenon_H4a8). zenon_intro zenon_H4aa. zenon_intro zenon_H4a9. % 8.32/8.57 exact (fact_pe zenon_H4aa). % 8.32/8.57 exact (zenon_H4a3 zenon_H4a6). % 8.32/8.57 apply (zenon_imply_s _ _ zenon_H4a2); [ zenon_intro zenon_H4ab | zenon_intro zenon_H494 ]. % 8.32/8.57 exact (zenon_H4ab fact_dp). % 8.32/8.57 apply (zenon_notequiv_s _ _ zenon_G); [ zenon_intro zenon_H4a3; zenon_intro zenon_H4a7 | zenon_intro zenon_H4a6; zenon_intro zenon_H4a5 ]. % 8.32/8.57 apply (zenon_notallex_s (fun B_x : zenon_U => (((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) B_x) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex)))->((hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_q)) B_x) = (c_Groups_Ozero__class_Ozero (tc_Complex_Ocomplex))))) zenon_H4a3); [ zenon_intro zenon_H4a4; idtac ]. % 8.32/8.57 elim zenon_H4a4. zenon_intro zenon_TB_x_btd. zenon_intro zenon_H493. % 8.32/8.57 apply (zenon_L1_ zenon_TB_x_btd); trivial. % 8.32/8.57 apply (zenon_notor_s _ _ zenon_H4a5). zenon_intro zenon_H4ad. zenon_intro zenon_H4ac. % 8.32/8.57 exact (zenon_H4ad zenon_H494). % 8.32/8.57 Qed. % 8.32/8.57 % SZS output end Proof % 8.32/8.57 (* END-PROOF *) % 8.32/8.57 nodes searched: 15748 % 8.32/8.57 max branch formulas: 16717 % 8.32/8.57 proof nodes created: 32 % 8.32/8.57 formulas created: 607598 % 8.32/8.57 %------------------------------------------------------------------------------