%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV067+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n006.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:02:51 EDT 2022 % Result : Theorem 0.38s 0.60s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SWV067+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n006.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 : Tue Jun 14 21:26:41 EDT 2022 % 0.12/0.33 % CPUTime : % 0.38/0.60 (* PROOF-FOUND *) % 0.38/0.60 % SZS status Theorem % 0.38/0.60 (* BEGIN-PROOF *) % 0.38/0.60 % SZS output start Proof % 0.38/0.60 Theorem cl5_nebula_array_0008 : (((leq (n0) (pv10))/\((leq (n1) (pv63))/\((leq (pv10) (minus (n135300) (n1)))/\(leq (pv63) (minus (n5) (n1))))))->((leq (n0) (pv10))/\((leq (n0) (pv63))/\((leq (pv10) (minus (n135300) (n1)))/\((leq (pv63) (minus (n5) (n1)))/\(((~(gt (a_select3 (q) (pv10) (pv63)) (pv78)))->((leq (n0) (pv10))/\(leq (pv10) (minus (n135300) (n1)))))/\((gt (a_select3 (q) (pv10) (pv63)) (pv78))->((leq (n0) (pv10))/\(leq (pv10) (minus (n135300) (n1))))))))))). % 0.38/0.60 Proof. % 0.38/0.60 assert (zenon_L1_ : (gt (succ (pv10)) (n0)) -> (~(leq (n0) (pv10))) -> False). % 0.38/0.60 do 0 intro. intros zenon_H5c zenon_H5d. % 0.38/0.60 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H5e. % 0.38/0.60 generalize (zenon_H5e (pv10)). zenon_intro zenon_H5f. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H5f); [ zenon_intro zenon_H5d; zenon_intro zenon_H61 | zenon_intro zenon_H60; zenon_intro zenon_H5c ]. % 0.38/0.60 exact (zenon_H61 zenon_H5c). % 0.38/0.60 exact (zenon_H5d zenon_H60). % 0.38/0.60 (* end of lemma zenon_L1_ *) % 0.38/0.60 assert (zenon_L2_ : (~((n0) = (n0))) -> False). % 0.38/0.60 do 0 intro. intros zenon_H62. % 0.38/0.60 apply zenon_H62. apply refl_equal. % 0.38/0.60 (* end of lemma zenon_L2_ *) % 0.38/0.60 assert (zenon_L3_ : (gt (succ (minus (n135300) (n1))) (pv10)) -> (~(leq (pv10) (minus (n135300) (n1)))) -> False). % 0.38/0.60 do 0 intro. intros zenon_H63 zenon_H64. % 0.38/0.60 generalize (leq_succ_gt_equiv (pv10)). zenon_intro zenon_H65. % 0.38/0.60 generalize (zenon_H65 (minus (n135300) (n1))). zenon_intro zenon_H66. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H66); [ zenon_intro zenon_H64; zenon_intro zenon_H68 | zenon_intro zenon_H67; zenon_intro zenon_H63 ]. % 0.38/0.60 exact (zenon_H68 zenon_H63). % 0.38/0.60 exact (zenon_H64 zenon_H67). % 0.38/0.60 (* end of lemma zenon_L3_ *) % 0.38/0.60 assert (zenon_L4_ : (~((leq (n0) (pv10))/\(leq (pv10) (minus (n135300) (n1))))) -> (gt (succ (minus (n135300) (n1))) (pv10)) -> (gt (succ (pv10)) (n0)) -> False). % 0.38/0.60 do 0 intro. intros zenon_H69 zenon_H63 zenon_H5c. % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H69); [ zenon_intro zenon_H5d | zenon_intro zenon_H64 ]. % 0.38/0.60 apply (zenon_L1_); trivial. % 0.38/0.60 apply (zenon_L3_); trivial. % 0.38/0.60 (* end of lemma zenon_L4_ *) % 0.38/0.60 apply NNPP. intro zenon_G. % 0.38/0.60 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z))))))); [ zenon_intro zenon_H6a | zenon_intro zenon_H6b ]. % 0.38/0.60 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.38/0.60 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H60. zenon_intro zenon_H6e. % 0.38/0.60 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.38/0.60 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H67. zenon_intro zenon_H71. % 0.38/0.60 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H5e. % 0.38/0.60 generalize (zenon_H5e (pv10)). zenon_intro zenon_H5f. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H5f); [ zenon_intro zenon_H5d; zenon_intro zenon_H61 | zenon_intro zenon_H60; zenon_intro zenon_H5c ]. % 0.38/0.60 exact (zenon_H5d zenon_H60). % 0.38/0.60 generalize (leq_succ_gt_equiv (n1)). zenon_intro zenon_H72. % 0.38/0.60 generalize (zenon_H72 (pv63)). zenon_intro zenon_H73. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H76; zenon_intro zenon_H75 | zenon_intro zenon_H70; zenon_intro zenon_H74 ]. % 0.38/0.60 exact (zenon_H76 zenon_H70). % 0.38/0.60 generalize (leq_succ_gt_equiv (pv10)). zenon_intro zenon_H65. % 0.38/0.60 generalize (zenon_H65 (minus (n135300) (n1))). zenon_intro zenon_H66. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H66); [ zenon_intro zenon_H64; zenon_intro zenon_H68 | zenon_intro zenon_H67; zenon_intro zenon_H63 ]. % 0.38/0.60 exact (zenon_H64 zenon_H67). % 0.38/0.60 generalize (leq_succ_gt_equiv (pv63)). zenon_intro zenon_H77. % 0.38/0.60 generalize (zenon_H77 (minus (n5) (n1))). zenon_intro zenon_H78. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H78); [ zenon_intro zenon_H7b; zenon_intro zenon_H7a | zenon_intro zenon_H71; zenon_intro zenon_H79 ]. % 0.38/0.60 exact (zenon_H7b zenon_H71). % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H5d | zenon_intro zenon_H7c ]. % 0.38/0.60 apply (zenon_L1_); trivial. % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 0.38/0.60 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H5e. % 0.38/0.60 generalize (zenon_H5e (pv63)). zenon_intro zenon_H7f. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H7f); [ zenon_intro zenon_H7e; zenon_intro zenon_H82 | zenon_intro zenon_H81; zenon_intro zenon_H80 ]. % 0.38/0.60 elim (classic ((~((succ (pv63)) = (n1)))/\(~(gt (succ (pv63)) (n1))))); [ zenon_intro zenon_H83 | zenon_intro zenon_H84 ]. % 0.38/0.60 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H85. zenon_intro zenon_H75. % 0.38/0.60 exact (zenon_H75 zenon_H74). % 0.38/0.60 cut ((gt (n1) (n0)) = (gt (succ (pv63)) (n0))). % 0.38/0.60 intro zenon_D_pnotp. % 0.38/0.60 apply zenon_H82. % 0.38/0.60 rewrite <- zenon_D_pnotp. % 0.38/0.60 exact gt_1_0. % 0.38/0.60 cut (((n0) = (n0))); [idtac | apply NNPP; zenon_intro zenon_H62]. % 0.38/0.60 cut (((n1) = (succ (pv63)))); [idtac | apply NNPP; zenon_intro zenon_H86]. % 0.38/0.60 congruence. % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.38/0.60 apply zenon_H88. zenon_intro zenon_H89. % 0.38/0.60 elim (classic ((succ (pv63)) = (succ (pv63)))); [ zenon_intro zenon_H8a | zenon_intro zenon_H8b ]. % 0.38/0.60 cut (((succ (pv63)) = (succ (pv63))) = ((n1) = (succ (pv63)))). % 0.38/0.60 intro zenon_D_pnotp. % 0.38/0.60 apply zenon_H86. % 0.38/0.60 rewrite <- zenon_D_pnotp. % 0.38/0.60 exact zenon_H8a. % 0.38/0.60 cut (((succ (pv63)) = (succ (pv63)))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 0.38/0.60 cut (((succ (pv63)) = (n1))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 0.38/0.60 congruence. % 0.38/0.60 exact (zenon_H85 zenon_H89). % 0.38/0.60 apply zenon_H8b. apply refl_equal. % 0.38/0.60 apply zenon_H8b. apply refl_equal. % 0.38/0.60 apply zenon_H87. zenon_intro zenon_H74. % 0.38/0.60 generalize (zenon_H6a (succ (pv63))). zenon_intro zenon_H8c. % 0.38/0.60 generalize (zenon_H8c (n1)). zenon_intro zenon_H8d. % 0.38/0.60 generalize (zenon_H8d (n0)). zenon_intro zenon_H8e. % 0.38/0.60 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H75 | zenon_intro zenon_H8f ]. % 0.38/0.60 exact (zenon_H75 zenon_H74). % 0.38/0.60 apply (zenon_imply_s _ _ zenon_H8f); [ zenon_intro zenon_H90 | zenon_intro zenon_H80 ]. % 0.38/0.60 exact (zenon_H90 gt_1_0). % 0.38/0.60 exact (zenon_H82 zenon_H80). % 0.38/0.60 apply zenon_H62. apply refl_equal. % 0.38/0.60 exact (zenon_H7e zenon_H81). % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H7d); [ zenon_intro zenon_H64 | zenon_intro zenon_H91 ]. % 0.38/0.60 apply (zenon_L3_); trivial. % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H91); [ zenon_intro zenon_H7b | zenon_intro zenon_H92 ]. % 0.38/0.60 generalize (leq_succ_gt_equiv (pv63)). zenon_intro zenon_H77. % 0.38/0.60 generalize (zenon_H77 (minus (n5) (n1))). zenon_intro zenon_H78. % 0.38/0.60 apply (zenon_equiv_s _ _ zenon_H78); [ zenon_intro zenon_H7b; zenon_intro zenon_H7a | zenon_intro zenon_H71; zenon_intro zenon_H79 ]. % 0.38/0.60 exact (zenon_H7a zenon_H79). % 0.38/0.60 exact (zenon_H7b zenon_H71). % 0.38/0.60 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_H94 | zenon_intro zenon_H93 ]. % 0.38/0.60 apply (zenon_notimply_s _ _ zenon_H94). zenon_intro zenon_H95. zenon_intro zenon_H69. % 0.38/0.60 apply (zenon_L4_); trivial. % 0.38/0.60 apply (zenon_notimply_s _ _ zenon_H93). zenon_intro zenon_H96. zenon_intro zenon_H69. % 0.38/0.60 apply (zenon_L4_); trivial. % 0.38/0.60 apply zenon_H6b. zenon_intro zenon_Tx_fv. apply NNPP. zenon_intro zenon_H98. % 0.38/0.60 apply zenon_H98. zenon_intro zenon_Ty_fx. apply NNPP. zenon_intro zenon_H9a. % 0.38/0.60 apply zenon_H9a. zenon_intro zenon_Tz_fz. apply NNPP. zenon_intro zenon_H9c. % 0.38/0.60 apply (zenon_notimply_s _ _ zenon_H9c). zenon_intro zenon_H9e. zenon_intro zenon_H9d. % 0.38/0.60 apply (zenon_notimply_s _ _ zenon_H9d). zenon_intro zenon_Ha0. zenon_intro zenon_H9f. % 0.38/0.60 generalize (transitivity_gt zenon_Tx_fv). zenon_intro zenon_Ha1. % 0.38/0.60 generalize (zenon_Ha1 zenon_Ty_fx). zenon_intro zenon_Ha2. % 0.38/0.60 generalize (zenon_Ha2 zenon_Tz_fz). zenon_intro zenon_Ha3. % 0.38/0.60 apply (zenon_imply_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.38/0.60 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.38/0.60 exact (zenon_Ha7 zenon_H9e). % 0.38/0.60 exact (zenon_Ha6 zenon_Ha0). % 0.38/0.60 exact (zenon_H9f zenon_Ha4). % 0.38/0.60 Qed. % 0.38/0.60 % SZS output end Proof % 0.38/0.60 (* END-PROOF *) % 0.38/0.60 nodes searched: 3793 % 0.38/0.60 max branch formulas: 834 % 0.38/0.60 proof nodes created: 21 % 0.38/0.60 formulas created: 13644 % 0.38/0.60 %------------------------------------------------------------------------------