%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV162+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n016.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:10 EDT 2022 % Result : Theorem 18.56s 18.77s % Output : Proof 18.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWV162+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.04/0.13 % Command : run_zenon %s %d % 0.14/0.34 % Computer : n016.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Thu Jun 16 04:54:18 EDT 2022 % 0.14/0.34 % CPUTime : % 18.56/18.77 (* PROOF-FOUND *) % 18.56/18.77 % SZS status Theorem % 18.56/18.77 (* BEGIN-PROOF *) % 18.56/18.77 % SZS output start Proof % 18.56/18.77 Theorem cl5_nebula_norm_0012 : ((((sum (n0) (n4) (a_select3 (q) (pv10) (tptp_sum_index))) = (n1))/\((leq (n0) (pv10))/\((leq (pv10) (n135299))/\(forall A : zenon_U, (((leq (n0) A)/\(leq A (pred (pv10))))->((sum (n0) (n4) (a_select3 (q) A (tptp_sum_index))) = (n1)))))))->(forall B : zenon_U, (((leq (n0) B)/\(leq B (pv10)))->((sum (n0) (n4) (a_select3 (q) B (tptp_sum_index))) = (n1))))). % 18.56/18.77 Proof. % 18.56/18.77 assert (zenon_L1_ : (~((n0) = (n0))) -> False). % 18.56/18.77 do 0 intro. intros zenon_H5c. % 18.56/18.77 apply zenon_H5c. apply refl_equal. % 18.56/18.77 (* end of lemma zenon_L1_ *) % 18.56/18.77 assert (zenon_L2_ : (~((n4) = (n4))) -> False). % 18.56/18.77 do 0 intro. intros zenon_H5d. % 18.56/18.77 apply zenon_H5d. apply refl_equal. % 18.56/18.77 (* end of lemma zenon_L2_ *) % 18.56/18.77 assert (zenon_L3_ : (~((q) = (q))) -> False). % 18.56/18.77 do 0 intro. intros zenon_H5e. % 18.56/18.77 apply zenon_H5e. apply refl_equal. % 18.56/18.77 (* end of lemma zenon_L3_ *) % 18.56/18.77 assert (zenon_L4_ : forall (zenon_TB_dt : zenon_U), (gt (succ zenon_TB_dt) (n0)) -> (~(leq (n0) zenon_TB_dt)) -> False). % 18.56/18.77 do 1 intro. intros zenon_H5f zenon_H60. % 18.56/18.77 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H62. % 18.56/18.77 generalize (zenon_H62 zenon_TB_dt). zenon_intro zenon_H63. % 18.56/18.77 apply (zenon_equiv_s _ _ zenon_H63); [ zenon_intro zenon_H60; zenon_intro zenon_H65 | zenon_intro zenon_H64; zenon_intro zenon_H5f ]. % 18.56/18.77 exact (zenon_H65 zenon_H5f). % 18.56/18.77 exact (zenon_H60 zenon_H64). % 18.56/18.77 (* end of lemma zenon_L4_ *) % 18.56/18.77 assert (zenon_L5_ : forall (zenon_TB_dt : zenon_U), (forall Y : zenon_U, (((leq zenon_TB_dt Y)/\(~(zenon_TB_dt = Y)))->(gt Y zenon_TB_dt))) -> (gt (succ (pv10)) zenon_TB_dt) -> (~(zenon_TB_dt = (pv10))) -> (~(gt (pv10) zenon_TB_dt)) -> False). % 18.56/18.77 do 1 intro. intros zenon_H66 zenon_H67 zenon_H68 zenon_H69. % 18.56/18.77 generalize (zenon_H66 (pv10)). zenon_intro zenon_H6a. % 18.56/18.77 apply (zenon_imply_s _ _ zenon_H6a); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 18.56/18.77 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 18.56/18.77 generalize (leq_succ_gt_equiv zenon_TB_dt). zenon_intro zenon_H6f. % 18.56/18.77 generalize (zenon_H6f (pv10)). zenon_intro zenon_H70. % 18.56/18.77 apply (zenon_equiv_s _ _ zenon_H70); [ zenon_intro zenon_H6e; zenon_intro zenon_H72 | zenon_intro zenon_H71; zenon_intro zenon_H67 ]. % 18.56/18.77 exact (zenon_H72 zenon_H67). % 18.56/18.77 exact (zenon_H6e zenon_H71). % 18.56/18.77 exact (zenon_H6d zenon_H68). % 18.56/18.77 exact (zenon_H69 zenon_H6b). % 18.56/18.77 (* end of lemma zenon_L5_ *) % 18.56/18.77 assert (zenon_L6_ : (~((tptp_sum_index) = (tptp_sum_index))) -> False). % 18.56/18.77 do 0 intro. intros zenon_H73. % 18.56/18.77 apply zenon_H73. apply refl_equal. % 18.56/18.77 (* end of lemma zenon_L6_ *) % 18.56/18.77 assert (zenon_L7_ : (~((n1) = (n1))) -> False). % 18.56/18.77 do 0 intro. intros zenon_H74. % 18.56/18.77 apply zenon_H74. apply refl_equal. % 18.56/18.77 (* end of lemma zenon_L7_ *) % 18.56/18.77 apply NNPP. intro zenon_G. % 18.56/18.77 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H76. zenon_intro zenon_H75. % 18.56/18.77 apply (zenon_and_s _ _ zenon_H76). zenon_intro zenon_H78. zenon_intro zenon_H77. % 18.56/18.77 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 18.56/18.77 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 18.56/18.77 apply (zenon_notallex_s (fun B : zenon_U => (((leq (n0) B)/\(leq B (pv10)))->((sum (n0) (n4) (a_select3 (q) B (tptp_sum_index))) = (n1)))) zenon_H75); [ zenon_intro zenon_H7d; idtac ]. % 18.56/18.77 elim zenon_H7d. zenon_intro zenon_TB_dt. zenon_intro zenon_H7e. % 18.56/18.77 apply (zenon_notimply_s _ _ zenon_H7e). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 18.56/18.77 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H64. zenon_intro zenon_H71. % 18.56/18.77 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H62. % 18.56/18.77 generalize (zenon_H62 zenon_TB_dt). zenon_intro zenon_H63. % 18.56/18.77 apply (zenon_equiv_s _ _ zenon_H63); [ zenon_intro zenon_H60; zenon_intro zenon_H65 | zenon_intro zenon_H64; zenon_intro zenon_H5f ]. % 18.56/18.77 exact (zenon_H60 zenon_H64). % 18.56/18.77 generalize (leq_succ_gt_equiv zenon_TB_dt). zenon_intro zenon_H6f. % 18.56/18.77 generalize (zenon_H6f (pv10)). zenon_intro zenon_H70. % 18.56/18.77 apply (zenon_equiv_s _ _ zenon_H70); [ zenon_intro zenon_H6e; zenon_intro zenon_H72 | zenon_intro zenon_H71; zenon_intro zenon_H67 ]. % 18.56/18.77 exact (zenon_H6e zenon_H71). % 18.56/18.77 cut (((sum (n0) (n4) (a_select3 (q) (pv10) (tptp_sum_index))) = (n1)) = ((sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))) = (n1))). % 18.56/18.78 intro zenon_D_pnotp. % 18.56/18.78 apply zenon_H7f. % 18.56/18.78 rewrite <- zenon_D_pnotp. % 18.56/18.78 exact zenon_H78. % 18.56/18.78 cut (((n1) = (n1))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 18.56/18.78 cut (((sum (n0) (n4) (a_select3 (q) (pv10) (tptp_sum_index))) = (sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 18.56/18.78 congruence. % 18.56/18.78 elim (classic ((sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))) = (sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 18.56/18.78 cut (((sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))) = (sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index)))) = ((sum (n0) (n4) (a_select3 (q) (pv10) (tptp_sum_index))) = (sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))))). % 18.56/18.78 intro zenon_D_pnotp. % 18.56/18.78 apply zenon_H81. % 18.56/18.78 rewrite <- zenon_D_pnotp. % 18.56/18.78 exact zenon_H82. % 18.56/18.78 cut (((sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))) = (sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 18.56/18.78 cut (((sum (n0) (n4) (a_select3 (q) zenon_TB_dt (tptp_sum_index))) = (sum (n0) (n4) (a_select3 (q) (pv10) (tptp_sum_index))))); [idtac | apply NNPP; zenon_intro zenon_H84]. % 18.56/18.78 congruence. % 18.56/18.78 cut (((a_select3 (q) zenon_TB_dt (tptp_sum_index)) = (a_select3 (q) (pv10) (tptp_sum_index)))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 18.56/18.78 cut (((n4) = (n4))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 18.56/18.78 cut (((n0) = (n0))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 18.56/18.78 congruence. % 18.56/18.78 apply zenon_H5c. apply refl_equal. % 18.56/18.78 apply zenon_H5d. apply refl_equal. % 18.56/18.78 cut (((tptp_sum_index) = (tptp_sum_index))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 18.56/18.78 cut ((zenon_TB_dt = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 18.56/18.78 cut (((q) = (q))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 18.56/18.78 congruence. % 18.56/18.78 apply zenon_H5e. apply refl_equal. % 18.56/18.78 generalize (succ_pred (pv10)). zenon_intro zenon_H86. % 18.56/18.78 generalize (leq_gt2 zenon_TB_dt). zenon_intro zenon_H66. % 18.56/18.78 generalize (zenon_H7b zenon_TB_dt). zenon_intro zenon_H87. % 18.56/18.78 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 18.56/18.78 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H60 | zenon_intro zenon_H8a ]. % 18.56/18.78 apply (zenon_L4_ zenon_TB_dt); trivial. % 18.56/18.78 generalize (leq_succ_gt_equiv zenon_TB_dt). zenon_intro zenon_H6f. % 18.56/18.78 generalize (zenon_H6f (pred (pv10))). zenon_intro zenon_H8b. % 18.56/18.78 apply (zenon_equiv_s _ _ zenon_H8b); [ zenon_intro zenon_H8a; zenon_intro zenon_H8e | zenon_intro zenon_H8d; zenon_intro zenon_H8c ]. % 18.56/18.78 elim (classic (gt (pv10) zenon_TB_dt)); [ zenon_intro zenon_H6b | zenon_intro zenon_H69 ]. % 18.56/18.78 cut ((gt (pv10) zenon_TB_dt) = (gt (succ (pred (pv10))) zenon_TB_dt)). % 18.56/18.78 intro zenon_D_pnotp. % 18.56/18.78 apply zenon_H8e. % 18.56/18.78 rewrite <- zenon_D_pnotp. % 18.56/18.78 exact zenon_H6b. % 18.56/18.78 cut ((zenon_TB_dt = zenon_TB_dt)); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 18.56/18.78 cut (((pv10) = (succ (pred (pv10))))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 18.56/18.78 congruence. % 18.56/18.78 elim (classic ((succ (pred (pv10))) = (succ (pred (pv10))))); [ zenon_intro zenon_H91 | zenon_intro zenon_H92 ]. % 18.56/18.78 cut (((succ (pred (pv10))) = (succ (pred (pv10)))) = ((pv10) = (succ (pred (pv10))))). % 18.56/18.78 intro zenon_D_pnotp. % 18.56/18.78 apply zenon_H90. % 18.56/18.78 rewrite <- zenon_D_pnotp. % 18.56/18.78 exact zenon_H91. % 18.56/18.78 cut (((succ (pred (pv10))) = (succ (pred (pv10))))); [idtac | apply NNPP; zenon_intro zenon_H92]. % 18.56/18.78 cut (((succ (pred (pv10))) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H93]. % 18.56/18.78 congruence. % 18.56/18.78 exact (zenon_H93 zenon_H86). % 18.56/18.78 apply zenon_H92. apply refl_equal. % 18.56/18.78 apply zenon_H92. apply refl_equal. % 18.56/18.78 apply zenon_H8f. apply refl_equal. % 18.56/18.78 apply (zenon_L5_ zenon_TB_dt); trivial. % 18.56/18.78 exact (zenon_H8a zenon_H8d). % 18.56/18.78 exact (zenon_H7f zenon_H88). % 18.56/18.78 apply zenon_H73. apply refl_equal. % 18.56/18.78 apply zenon_H83. apply refl_equal. % 18.56/18.78 apply zenon_H83. apply refl_equal. % 18.56/18.78 apply zenon_H74. apply refl_equal. % 18.56/18.78 Qed. % 18.56/18.78 % SZS output end Proof % 18.56/18.78 (* END-PROOF *) % 18.56/18.78 nodes searched: 1326434 % 18.56/18.78 max branch formulas: 18747 % 18.56/18.78 proof nodes created: 5317 % 18.56/18.78 formulas created: 439288 % 18.56/18.78 %------------------------------------------------------------------------------