%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV139+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:03:05 EDT 2022 % Result : Theorem 81.62s 81.85s % Output : Proof 81.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV139+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.06/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 : Wed Jun 15 20:12:26 EDT 2022 % 0.12/0.33 % CPUTime : % 81.62/81.85 (* PROOF-FOUND *) % 81.62/81.85 % SZS status Theorem % 81.62/81.85 (* BEGIN-PROOF *) % 81.62/81.85 % SZS output start Proof % 81.62/81.85 Theorem gauss_array_0009 : (((leq (tptp_float_0_001) (pv1341))/\((leq (n1) (loopcounter))/\(((~(leq (tptp_float_0_001) (pv1341)))->(leq (n0) (s_best7)))/\(((~(leq (tptp_float_0_001) (pv1341)))->(leq (n0) (s_sworst7)))/\(((~(leq (tptp_float_0_001) (pv1341)))->(leq (n0) (s_worst7)))/\(((~(leq (tptp_float_0_001) (pv1341)))->(leq (s_best7) (n3)))/\(((~(leq (tptp_float_0_001) (pv1341)))->(leq (s_sworst7) (n3)))/\(((~(leq (tptp_float_0_001) (pv1341)))->(leq (s_worst7) (n3)))/\(((gt (loopcounter) (n0))->(leq (n0) (s_best7)))/\(((gt (loopcounter) (n0))->(leq (n0) (s_sworst7)))/\(((gt (loopcounter) (n0))->(leq (n0) (s_worst7)))/\(((gt (loopcounter) (n0))->(leq (s_best7) (n3)))/\(((gt (loopcounter) (n0))->(leq (s_sworst7) (n3)))/\((gt (loopcounter) (n0))->(leq (s_worst7) (n3))))))))))))))))->(leq (n0) (s_best7))). % 81.62/81.85 Proof. % 81.62/81.85 assert (zenon_L1_ : (~((n0) = (n0))) -> False). % 81.62/81.85 do 0 intro. intros zenon_H55. % 81.62/81.85 apply zenon_H55. apply refl_equal. % 81.62/81.85 (* end of lemma zenon_L1_ *) % 81.62/81.85 assert (zenon_L2_ : (leq (n0) (s_best7)) -> (~(gt (succ (s_best7)) (n0))) -> False). % 81.62/81.85 do 0 intro. intros zenon_H56 zenon_H57. % 81.62/81.85 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H58. % 81.62/81.85 generalize (zenon_H58 (s_best7)). zenon_intro zenon_H59. % 81.62/81.85 apply (zenon_equiv_s _ _ zenon_H59); [ zenon_intro zenon_H5b; zenon_intro zenon_H57 | zenon_intro zenon_H56; zenon_intro zenon_H5a ]. % 81.62/81.85 exact (zenon_H5b zenon_H56). % 81.62/81.85 exact (zenon_H57 zenon_H5a). % 81.62/81.85 (* end of lemma zenon_L2_ *) % 81.62/81.85 apply NNPP. intro zenon_G. % 81.62/81.85 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_H5c | zenon_intro zenon_H5d ]. % 81.62/81.85 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H5e. zenon_intro zenon_H5b. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H62. zenon_intro zenon_H61. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 81.62/81.85 generalize (leq_succ_gt_equiv (n1)). zenon_intro zenon_H71. % 81.62/81.85 generalize (zenon_H71 (loopcounter)). zenon_intro zenon_H72. % 81.62/81.85 apply (zenon_equiv_s _ _ zenon_H72); [ zenon_intro zenon_H75; zenon_intro zenon_H74 | zenon_intro zenon_H62; zenon_intro zenon_H73 ]. % 81.62/81.85 exact (zenon_H75 zenon_H62). % 81.62/81.85 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H58. % 81.62/81.85 generalize (zenon_H58 (s_best7)). zenon_intro zenon_H59. % 81.62/81.85 apply (zenon_equiv_s _ _ zenon_H59); [ zenon_intro zenon_H5b; zenon_intro zenon_H57 | zenon_intro zenon_H56; zenon_intro zenon_H5a ]. % 81.62/81.85 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H76 | zenon_intro zenon_H56 ]. % 81.62/81.85 elim (classic ((~((loopcounter) = (n1)))/\(~(gt (loopcounter) (n1))))); [ zenon_intro zenon_H77 | zenon_intro zenon_H78 ]. % 81.62/81.85 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 81.62/81.85 generalize (leq_gt2 (n1)). zenon_intro zenon_H7b. % 81.62/81.85 generalize (zenon_H7b (loopcounter)). zenon_intro zenon_H7c. % 81.62/81.85 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 81.62/81.85 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H75 | zenon_intro zenon_H7f ]. % 81.62/81.85 generalize (leq_succ_gt_equiv (n1)). zenon_intro zenon_H71. % 81.62/81.85 generalize (zenon_H71 (loopcounter)). zenon_intro zenon_H72. % 81.62/81.85 apply (zenon_equiv_s _ _ zenon_H72); [ zenon_intro zenon_H75; zenon_intro zenon_H74 | zenon_intro zenon_H62; zenon_intro zenon_H73 ]. % 81.62/81.85 exact (zenon_H74 zenon_H73). % 81.62/81.85 exact (zenon_H75 zenon_H62). % 81.62/81.85 apply zenon_H7f. zenon_intro zenon_H80. % 81.62/81.85 apply zenon_H7a. apply sym_equal. exact zenon_H80. % 81.62/81.85 exact (zenon_H79 zenon_H7d). % 81.62/81.85 cut ((gt (n1) (n0)) = (gt (loopcounter) (n0))). % 81.70/81.88 intro zenon_D_pnotp. % 81.70/81.88 apply zenon_H76. % 81.70/81.88 rewrite <- zenon_D_pnotp. % 81.70/81.88 exact gt_1_0. % 81.70/81.88 cut (((n0) = (n0))); [idtac | apply NNPP; zenon_intro zenon_H55]. % 81.70/81.88 cut (((n1) = (loopcounter))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 81.70/81.88 congruence. % 81.70/81.88 apply (zenon_notand_s _ _ zenon_H78); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 81.70/81.88 apply zenon_H83. zenon_intro zenon_H84. % 81.70/81.88 elim (classic ((loopcounter) = (loopcounter))); [ zenon_intro zenon_H85 | zenon_intro zenon_H86 ]. % 81.70/81.88 cut (((loopcounter) = (loopcounter)) = ((n1) = (loopcounter))). % 81.70/81.88 intro zenon_D_pnotp. % 81.70/81.88 apply zenon_H81. % 81.70/81.88 rewrite <- zenon_D_pnotp. % 81.70/81.88 exact zenon_H85. % 81.70/81.88 cut (((loopcounter) = (loopcounter))); [idtac | apply NNPP; zenon_intro zenon_H86]. % 81.70/81.88 cut (((loopcounter) = (n1))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 81.70/81.88 congruence. % 81.70/81.88 exact (zenon_H7a zenon_H84). % 81.70/81.88 apply zenon_H86. apply refl_equal. % 81.70/81.88 apply zenon_H86. apply refl_equal. % 81.70/81.88 apply zenon_H82. zenon_intro zenon_H7d. % 81.70/81.88 generalize (zenon_H5c (loopcounter)). zenon_intro zenon_H87. % 81.70/81.88 generalize (zenon_H87 (n1)). zenon_intro zenon_H88. % 81.70/81.88 generalize (zenon_H88 (n0)). zenon_intro zenon_H89. % 81.70/81.88 apply (zenon_imply_s _ _ zenon_H89); [ zenon_intro zenon_H79 | zenon_intro zenon_H8a ]. % 81.70/81.88 exact (zenon_H79 zenon_H7d). % 81.70/81.88 apply (zenon_imply_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 81.70/81.88 exact (zenon_H8c gt_1_0). % 81.70/81.88 exact (zenon_H76 zenon_H8b). % 81.70/81.88 apply zenon_H55. apply refl_equal. % 81.70/81.88 apply (zenon_L2_); trivial. % 81.70/81.88 exact (zenon_H5b zenon_H56). % 81.70/81.88 apply zenon_H5d. zenon_intro zenon_Tx_fl. apply NNPP. zenon_intro zenon_H8e. % 81.70/81.88 apply zenon_H8e. zenon_intro zenon_Ty_fn. apply NNPP. zenon_intro zenon_H90. % 81.70/81.88 apply zenon_H90. zenon_intro zenon_Tz_fp. apply NNPP. zenon_intro zenon_H92. % 81.70/81.88 apply (zenon_notimply_s _ _ zenon_H92). zenon_intro zenon_H94. zenon_intro zenon_H93. % 81.70/81.88 apply (zenon_notimply_s _ _ zenon_H93). zenon_intro zenon_H96. zenon_intro zenon_H95. % 81.70/81.88 generalize (transitivity_gt zenon_Tx_fl). zenon_intro zenon_H97. % 81.70/81.88 generalize (zenon_H97 zenon_Ty_fn). zenon_intro zenon_H98. % 81.70/81.88 generalize (zenon_H98 zenon_Tz_fp). zenon_intro zenon_H99. % 81.70/81.88 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 81.70/81.88 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H9d | zenon_intro zenon_H9c ]. % 81.70/81.88 exact (zenon_H9d zenon_H94). % 81.70/81.88 exact (zenon_H9c zenon_H96). % 81.70/81.88 exact (zenon_H95 zenon_H9a). % 81.70/81.88 Qed. % 81.70/81.88 % SZS output end Proof % 81.70/81.88 (* END-PROOF *) % 81.70/81.88 nodes searched: 6231101 % 81.70/81.88 max branch formulas: 33772 % 81.70/81.88 proof nodes created: 8440 % 81.70/81.88 formulas created: 1040635 % 81.70/81.88 %------------------------------------------------------------------------------