%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV204+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n011.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 : Wed Jul 20 23:03:18 EDT 2022 % Result : Theorem 9.84s 10.07s % Output : Proof 9.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWV204+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.08/0.14 % Command : run_zenon %s %d % 0.14/0.36 % Computer : n011.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Thu Jun 16 04:31:36 EDT 2022 % 0.14/0.36 % CPUTime : % 9.84/10.07 (* PROOF-FOUND *) % 9.84/10.07 % SZS status Theorem % 9.84/10.07 (* BEGIN-PROOF *) % 9.84/10.07 % SZS output start Proof % 9.84/10.07 Theorem quaternion_ds1_inuse_0015 : ((((a_select2 (rho_defuse) (n0)) = (use))/\(((a_select2 (rho_defuse) (n1)) = (use))/\(((a_select2 (rho_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n0)) = (use))/\(((a_select2 (sigma_defuse) (n1)) = (use))/\(((a_select2 (sigma_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n3)) = (use))/\(((a_select2 (sigma_defuse) (n4)) = (use))/\(((a_select2 (sigma_defuse) (n5)) = (use))/\(((a_select3 (u_defuse) (n0) (n0)) = (use))/\(((a_select3 (u_defuse) (n1) (n0)) = (use))/\(((a_select3 (u_defuse) (n2) (n0)) = (use))/\(((a_select2 (xinit_defuse) (n3)) = (use))/\(((a_select2 (xinit_defuse) (n4)) = (use))/\(((a_select2 (xinit_defuse) (n5)) = (use))/\(((a_select2 (xinit_mean_defuse) (n0)) = (use))/\(((a_select2 (xinit_mean_defuse) (n1)) = (use))/\(((a_select2 (xinit_mean_defuse) (n2)) = (use))/\(((a_select2 (xinit_mean_defuse) (n3)) = (use))/\(((a_select2 (xinit_mean_defuse) (n4)) = (use))/\(((a_select2 (xinit_mean_defuse) (n5)) = (use))/\(((a_select2 (xinit_noise_defuse) (n0)) = (use))/\(((a_select2 (xinit_noise_defuse) (n1)) = (use))/\(((a_select2 (xinit_noise_defuse) (n2)) = (use))/\(((a_select2 (xinit_noise_defuse) (n3)) = (use))/\(((a_select2 (xinit_noise_defuse) (n4)) = (use))/\(((a_select2 (xinit_noise_defuse) (n5)) = (use))/\((forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (n998)))))->((a_select3 (u_defuse) A B) = (use)))))/\(forall C : zenon_U, (forall D : zenon_U, (((leq (n0) C)/\((leq (n0) D)/\((leq C (n2))/\(leq D (n998)))))->((a_select3 (z_defuse) C D) = (use)))))))))))))))))))))))))))))))))->(forall E : zenon_U, (((leq (n0) E)/\(leq E (n2)))->((a_select2 (rho_defuse) E) = (use))))). % 9.84/10.07 Proof. % 9.84/10.07 assert (zenon_L1_ : (~((rho_defuse) = (rho_defuse))) -> False). % 9.84/10.07 do 0 intro. intros zenon_H5c. % 9.84/10.07 apply zenon_H5c. apply refl_equal. % 9.84/10.07 (* end of lemma zenon_L1_ *) % 9.84/10.07 assert (zenon_L2_ : forall (zenon_TE_dr : zenon_U), (gt (succ zenon_TE_dr) (n0)) -> (~(leq (n0) zenon_TE_dr)) -> False). % 9.84/10.07 do 1 intro. intros zenon_H5d zenon_H5e. % 9.84/10.07 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H60. % 9.84/10.07 generalize (zenon_H60 zenon_TE_dr). zenon_intro zenon_H61. % 9.84/10.07 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H5e; zenon_intro zenon_H63 | zenon_intro zenon_H62; zenon_intro zenon_H5d ]. % 9.84/10.07 exact (zenon_H63 zenon_H5d). % 9.84/10.07 exact (zenon_H5e zenon_H62). % 9.84/10.07 (* end of lemma zenon_L2_ *) % 9.84/10.07 assert (zenon_L3_ : forall (zenon_TE_dr : zenon_U), (gt (succ (n2)) zenon_TE_dr) -> (~(leq zenon_TE_dr (n2))) -> False). % 9.84/10.07 do 1 intro. intros zenon_H64 zenon_H65. % 9.84/10.07 generalize (leq_succ_gt_equiv zenon_TE_dr). zenon_intro zenon_H66. % 9.84/10.07 generalize (zenon_H66 (n2)). zenon_intro zenon_H67. % 9.84/10.07 apply (zenon_equiv_s _ _ zenon_H67); [ zenon_intro zenon_H65; zenon_intro zenon_H69 | zenon_intro zenon_H68; zenon_intro zenon_H64 ]. % 9.84/10.07 exact (zenon_H69 zenon_H64). % 9.84/10.07 exact (zenon_H65 zenon_H68). % 9.84/10.07 (* end of lemma zenon_L3_ *) % 9.84/10.07 assert (zenon_L4_ : (~((use) = (use))) -> False). % 9.84/10.07 do 0 intro. intros zenon_H6a. % 9.84/10.07 apply zenon_H6a. apply refl_equal. % 9.84/10.07 (* end of lemma zenon_L4_ *) % 9.84/10.07 apply NNPP. intro zenon_G. % 9.84/10.07 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 9.84/10.07 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 9.84/10.07 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 9.84/10.07 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 9.84/10.07 apply (zenon_notallex_s (fun E : zenon_U => (((leq (n0) E)/\(leq E (n2)))->((a_select2 (rho_defuse) E) = (use)))) zenon_H6b); [ zenon_intro zenon_H73; idtac ]. % 9.84/10.07 elim zenon_H73. zenon_intro zenon_TE_dr. zenon_intro zenon_H74. % 9.84/10.07 apply (zenon_notimply_s _ _ zenon_H74). zenon_intro zenon_H76. zenon_intro zenon_H75. % 9.84/10.07 apply (zenon_and_s _ _ zenon_H76). zenon_intro zenon_H62. zenon_intro zenon_H68. % 9.84/10.07 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H60. % 9.84/10.07 generalize (zenon_H60 zenon_TE_dr). zenon_intro zenon_H61. % 9.84/10.07 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H5e; zenon_intro zenon_H63 | zenon_intro zenon_H62; zenon_intro zenon_H5d ]. % 9.84/10.07 exact (zenon_H5e zenon_H62). % 9.84/10.07 generalize (leq_succ_gt_equiv zenon_TE_dr). zenon_intro zenon_H66. % 9.84/10.07 generalize (zenon_H66 (n2)). zenon_intro zenon_H67. % 9.84/10.07 apply (zenon_equiv_s _ _ zenon_H67); [ zenon_intro zenon_H65; zenon_intro zenon_H69 | zenon_intro zenon_H68; zenon_intro zenon_H64 ]. % 9.84/10.07 exact (zenon_H65 zenon_H68). % 9.84/10.07 cut (((a_select2 (rho_defuse) (n0)) = (use)) = ((a_select2 (rho_defuse) zenon_TE_dr) = (use))). % 9.84/10.07 intro zenon_D_pnotp. % 9.84/10.07 apply zenon_H75. % 9.84/10.07 rewrite <- zenon_D_pnotp. % 9.84/10.07 exact zenon_H6e. % 9.84/10.07 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 9.84/10.07 cut (((a_select2 (rho_defuse) (n0)) = (a_select2 (rho_defuse) zenon_TE_dr))); [idtac | apply NNPP; zenon_intro zenon_H77]. % 9.84/10.07 congruence. % 9.84/10.07 elim (classic ((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr))); [ zenon_intro zenon_H78 | zenon_intro zenon_H79 ]. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr)) = ((a_select2 (rho_defuse) (n0)) = (a_select2 (rho_defuse) zenon_TE_dr))). % 9.84/10.07 intro zenon_D_pnotp. % 9.84/10.07 apply zenon_H77. % 9.84/10.07 rewrite <- zenon_D_pnotp. % 9.84/10.07 exact zenon_H78. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) (n0)))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 9.84/10.07 congruence. % 9.84/10.07 cut ((zenon_TE_dr = (n0))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 9.84/10.07 cut (((rho_defuse) = (rho_defuse))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 9.84/10.07 congruence. % 9.84/10.07 apply zenon_H5c. apply refl_equal. % 9.84/10.07 cut (((a_select2 (rho_defuse) (n1)) = (use)) = ((a_select2 (rho_defuse) zenon_TE_dr) = (use))). % 9.84/10.07 intro zenon_D_pnotp. % 9.84/10.07 apply zenon_H75. % 9.84/10.07 rewrite <- zenon_D_pnotp. % 9.84/10.07 exact zenon_H70. % 9.84/10.07 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 9.84/10.07 cut (((a_select2 (rho_defuse) (n1)) = (a_select2 (rho_defuse) zenon_TE_dr))); [idtac | apply NNPP; zenon_intro zenon_H7c]. % 9.84/10.07 congruence. % 9.84/10.07 elim (classic ((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr))); [ zenon_intro zenon_H78 | zenon_intro zenon_H79 ]. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr)) = ((a_select2 (rho_defuse) (n1)) = (a_select2 (rho_defuse) zenon_TE_dr))). % 9.84/10.07 intro zenon_D_pnotp. % 9.84/10.07 apply zenon_H7c. % 9.84/10.07 rewrite <- zenon_D_pnotp. % 9.84/10.07 exact zenon_H78. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) (n1)))); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 9.84/10.07 congruence. % 9.84/10.07 cut ((zenon_TE_dr = (n1))); [idtac | apply NNPP; zenon_intro zenon_H7e]. % 9.84/10.07 cut (((rho_defuse) = (rho_defuse))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 9.84/10.07 congruence. % 9.84/10.07 apply zenon_H5c. apply refl_equal. % 9.84/10.07 cut (((a_select2 (rho_defuse) (n2)) = (use)) = ((a_select2 (rho_defuse) zenon_TE_dr) = (use))). % 9.84/10.07 intro zenon_D_pnotp. % 9.84/10.07 apply zenon_H75. % 9.84/10.07 rewrite <- zenon_D_pnotp. % 9.84/10.07 exact zenon_H72. % 9.84/10.07 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 9.84/10.07 cut (((a_select2 (rho_defuse) (n2)) = (a_select2 (rho_defuse) zenon_TE_dr))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 9.84/10.07 congruence. % 9.84/10.07 elim (classic ((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr))); [ zenon_intro zenon_H78 | zenon_intro zenon_H79 ]. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr)) = ((a_select2 (rho_defuse) (n2)) = (a_select2 (rho_defuse) zenon_TE_dr))). % 9.84/10.07 intro zenon_D_pnotp. % 9.84/10.07 apply zenon_H7f. % 9.84/10.07 rewrite <- zenon_D_pnotp. % 9.84/10.07 exact zenon_H78. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) zenon_TE_dr))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 9.84/10.07 cut (((a_select2 (rho_defuse) zenon_TE_dr) = (a_select2 (rho_defuse) (n2)))); [idtac | apply NNPP; zenon_intro zenon_H80]. % 9.84/10.07 congruence. % 9.84/10.07 cut ((zenon_TE_dr = (n2))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 9.84/10.07 cut (((rho_defuse) = (rho_defuse))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 9.84/10.07 congruence. % 9.84/10.07 apply zenon_H5c. apply refl_equal. % 9.84/10.07 generalize (finite_domain_2 zenon_TE_dr). zenon_intro zenon_H82. % 9.84/10.07 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 9.84/10.07 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H5e | zenon_intro zenon_H65 ]. % 9.84/10.07 apply (zenon_L2_ zenon_TE_dr); trivial. % 9.84/10.07 apply (zenon_L3_ zenon_TE_dr); trivial. % 9.84/10.07 apply (zenon_or_s _ _ zenon_H83); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 9.84/10.07 exact (zenon_H7b zenon_H86). % 9.84/10.07 apply (zenon_or_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 9.84/10.07 exact (zenon_H7e zenon_H88). % 9.84/10.07 exact (zenon_H81 zenon_H87). % 9.84/10.07 apply zenon_H79. apply refl_equal. % 9.84/10.07 apply zenon_H79. apply refl_equal. % 9.84/10.07 apply zenon_H6a. apply refl_equal. % 9.84/10.07 apply zenon_H79. apply refl_equal. % 9.84/10.07 apply zenon_H79. apply refl_equal. % 9.84/10.07 apply zenon_H6a. apply refl_equal. % 9.84/10.07 apply zenon_H79. apply refl_equal. % 9.84/10.07 apply zenon_H79. apply refl_equal. % 9.84/10.07 apply zenon_H6a. apply refl_equal. % 9.84/10.07 Qed. % 9.84/10.07 % SZS output end Proof % 9.84/10.07 (* END-PROOF *) % 9.84/10.07 nodes searched: 558628 % 9.84/10.07 max branch formulas: 3139 % 9.84/10.07 proof nodes created: 1122 % 9.84/10.07 formulas created: 319329 % 9.84/10.07 %------------------------------------------------------------------------------