%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV064+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.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:50 EDT 2022 % Result : Theorem 0.18s 0.50s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV064+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n017.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:57:40 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.50 (* PROOF-FOUND *) % 0.18/0.50 % SZS status Theorem % 0.18/0.50 (* BEGIN-PROOF *) % 0.18/0.50 % SZS output start Proof % 0.18/0.50 Theorem cl5_nebula_array_0005 : (((leq (n0) (pv10))/\((leq (n0) (pv53))/\((leq (n0) (pv54))/\((leq (pv10) (minus (n135300) (n1)))/\((leq (pv53) (minus (n5) (n1)))/\(leq (pv54) (minus (n5) (n1))))))))->((leq (n0) (n0))/\((leq (n0) (pv10))/\((leq (n0) (pv53))/\((leq (n0) (pv54))/\((leq (pv10) (minus (n135300) (n1)))/\((leq (pv53) (minus (n5) (n1)))/\(leq (pv54) (minus (n5) (n1)))))))))). % 0.18/0.50 Proof. % 0.18/0.50 apply NNPP. intro zenon_G. % 0.18/0.50 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.18/0.50 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.18/0.50 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H61. zenon_intro zenon_H60. % 0.18/0.50 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.18/0.50 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.18/0.50 apply (zenon_and_s _ _ zenon_H64). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.18/0.50 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H68. % 0.18/0.50 generalize (zenon_H68 (pv10)). zenon_intro zenon_H69. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H6c; zenon_intro zenon_H6b | zenon_intro zenon_H5f; zenon_intro zenon_H6a ]. % 0.18/0.50 exact (zenon_H6c zenon_H5f). % 0.18/0.50 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H68. % 0.18/0.50 generalize (zenon_H68 (pv53)). zenon_intro zenon_H6d. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H6d); [ zenon_intro zenon_H70; zenon_intro zenon_H6f | zenon_intro zenon_H61; zenon_intro zenon_H6e ]. % 0.18/0.50 exact (zenon_H70 zenon_H61). % 0.18/0.50 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H68. % 0.18/0.50 generalize (zenon_H68 (pv54)). zenon_intro zenon_H71. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H71); [ zenon_intro zenon_H74; zenon_intro zenon_H73 | zenon_intro zenon_H63; zenon_intro zenon_H72 ]. % 0.18/0.50 exact (zenon_H74 zenon_H63). % 0.18/0.50 generalize (leq_succ_gt_equiv (pv10)). zenon_intro zenon_H75. % 0.18/0.50 generalize (zenon_H75 (minus (n135300) (n1))). zenon_intro zenon_H76. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H76); [ zenon_intro zenon_H79; zenon_intro zenon_H78 | zenon_intro zenon_H65; zenon_intro zenon_H77 ]. % 0.18/0.50 exact (zenon_H79 zenon_H65). % 0.18/0.50 generalize (leq_succ_gt_equiv (pv53)). zenon_intro zenon_H7a. % 0.18/0.50 generalize (zenon_H7a (minus (n5) (n1))). zenon_intro zenon_H7b. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H7b); [ zenon_intro zenon_H7e; zenon_intro zenon_H7d | zenon_intro zenon_H67; zenon_intro zenon_H7c ]. % 0.18/0.50 exact (zenon_H7e zenon_H67). % 0.18/0.50 generalize (leq_succ_gt_equiv (pv54)). zenon_intro zenon_H7f. % 0.18/0.50 generalize (zenon_H7f (minus (n5) (n1))). zenon_intro zenon_H80. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H80); [ zenon_intro zenon_H83; zenon_intro zenon_H82 | zenon_intro zenon_H66; zenon_intro zenon_H81 ]. % 0.18/0.50 exact (zenon_H83 zenon_H66). % 0.18/0.50 apply (zenon_notand_s _ _ zenon_H5c); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 0.18/0.50 generalize (reflexivity_leq (n0)). zenon_intro zenon_H86. % 0.18/0.50 exact (zenon_H85 zenon_H86). % 0.18/0.50 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H6c | zenon_intro zenon_H87 ]. % 0.18/0.50 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H68. % 0.18/0.50 generalize (zenon_H68 (pv10)). zenon_intro zenon_H69. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H6c; zenon_intro zenon_H6b | zenon_intro zenon_H5f; zenon_intro zenon_H6a ]. % 0.18/0.50 exact (zenon_H6b zenon_H6a). % 0.18/0.50 exact (zenon_H6c zenon_H5f). % 0.18/0.50 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H70 | zenon_intro zenon_H88 ]. % 0.18/0.50 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H68. % 0.18/0.50 generalize (zenon_H68 (pv53)). zenon_intro zenon_H6d. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H6d); [ zenon_intro zenon_H70; zenon_intro zenon_H6f | zenon_intro zenon_H61; zenon_intro zenon_H6e ]. % 0.18/0.50 exact (zenon_H6f zenon_H6e). % 0.18/0.50 exact (zenon_H70 zenon_H61). % 0.18/0.50 apply (zenon_notand_s _ _ zenon_H88); [ zenon_intro zenon_H74 | zenon_intro zenon_H89 ]. % 0.18/0.50 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H68. % 0.18/0.50 generalize (zenon_H68 (pv54)). zenon_intro zenon_H71. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H71); [ zenon_intro zenon_H74; zenon_intro zenon_H73 | zenon_intro zenon_H63; zenon_intro zenon_H72 ]. % 0.18/0.50 exact (zenon_H73 zenon_H72). % 0.18/0.50 exact (zenon_H74 zenon_H63). % 0.18/0.50 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H79 | zenon_intro zenon_H8a ]. % 0.18/0.50 generalize (leq_succ_gt_equiv (pv10)). zenon_intro zenon_H75. % 0.18/0.50 generalize (zenon_H75 (minus (n135300) (n1))). zenon_intro zenon_H76. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H76); [ zenon_intro zenon_H79; zenon_intro zenon_H78 | zenon_intro zenon_H65; zenon_intro zenon_H77 ]. % 0.18/0.50 exact (zenon_H78 zenon_H77). % 0.18/0.50 exact (zenon_H79 zenon_H65). % 0.18/0.50 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H7e | zenon_intro zenon_H83 ]. % 0.18/0.50 generalize (leq_succ_gt_equiv (pv53)). zenon_intro zenon_H7a. % 0.18/0.50 generalize (zenon_H7a (minus (n5) (n1))). zenon_intro zenon_H7b. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H7b); [ zenon_intro zenon_H7e; zenon_intro zenon_H7d | zenon_intro zenon_H67; zenon_intro zenon_H7c ]. % 0.18/0.50 exact (zenon_H7d zenon_H7c). % 0.18/0.50 exact (zenon_H7e zenon_H67). % 0.18/0.50 generalize (leq_succ_gt_equiv (pv54)). zenon_intro zenon_H7f. % 0.18/0.50 generalize (zenon_H7f (minus (n5) (n1))). zenon_intro zenon_H80. % 0.18/0.50 apply (zenon_equiv_s _ _ zenon_H80); [ zenon_intro zenon_H83; zenon_intro zenon_H82 | zenon_intro zenon_H66; zenon_intro zenon_H81 ]. % 0.18/0.50 exact (zenon_H82 zenon_H81). % 0.18/0.50 exact (zenon_H83 zenon_H66). % 0.18/0.50 Qed. % 0.18/0.50 % SZS output end Proof % 0.18/0.50 (* END-PROOF *) % 0.18/0.50 nodes searched: 22 % 0.18/0.50 max branch formulas: 101 % 0.18/0.50 proof nodes created: 21 % 0.18/0.50 formulas created: 1838 % 0.18/0.50 %------------------------------------------------------------------------------