%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV065+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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.21s 0.52s % Output : Proof 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SWV065+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.11/0.13 % Command : run_zenon %s %d % 0.12/0.35 % Computer : n005.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Wed Jun 15 09:36:54 EDT 2022 % 0.12/0.35 % CPUTime : % 0.21/0.52 (* PROOF-FOUND *) % 0.21/0.52 % SZS status Theorem % 0.21/0.52 (* BEGIN-PROOF *) % 0.21/0.52 % SZS output start Proof % 0.21/0.52 Theorem cl5_nebula_array_0006 : (((leq (n0) (pv10))/\((leq (n0) (pv53))/\((leq (pv10) (minus (n135300) (n1)))/\(leq (pv53) (minus (n5) (n1))))))->((leq (n0) (n0))/\((leq (n0) (pv10))/\((leq (n0) (pv53))/\((leq (pv10) (minus (n135300) (n1)))/\(leq (pv53) (minus (n5) (n1)))))))). % 0.21/0.52 Proof. % 0.21/0.52 apply NNPP. intro zenon_G. % 0.21/0.52 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.21/0.52 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.21/0.52 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H61. zenon_intro zenon_H60. % 0.21/0.52 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.21/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H64. % 0.21/0.52 generalize (zenon_H64 (pv10)). zenon_intro zenon_H65. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H68; zenon_intro zenon_H67 | zenon_intro zenon_H5f; zenon_intro zenon_H66 ]. % 0.21/0.52 exact (zenon_H68 zenon_H5f). % 0.21/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H64. % 0.21/0.52 generalize (zenon_H64 (pv53)). zenon_intro zenon_H69. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H6c; zenon_intro zenon_H6b | zenon_intro zenon_H61; zenon_intro zenon_H6a ]. % 0.21/0.52 exact (zenon_H6c zenon_H61). % 0.21/0.52 generalize (leq_succ_gt_equiv (pv10)). zenon_intro zenon_H6d. % 0.21/0.52 generalize (zenon_H6d (minus (n135300) (n1))). zenon_intro zenon_H6e. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H6e); [ zenon_intro zenon_H71; zenon_intro zenon_H70 | zenon_intro zenon_H63; zenon_intro zenon_H6f ]. % 0.21/0.52 exact (zenon_H71 zenon_H63). % 0.21/0.52 generalize (leq_succ_gt_equiv (pv53)). zenon_intro zenon_H72. % 0.21/0.52 generalize (zenon_H72 (minus (n5) (n1))). zenon_intro zenon_H73. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H76; zenon_intro zenon_H75 | zenon_intro zenon_H62; zenon_intro zenon_H74 ]. % 0.21/0.52 exact (zenon_H76 zenon_H62). % 0.21/0.52 apply (zenon_notand_s _ _ zenon_H5c); [ zenon_intro zenon_H78 | zenon_intro zenon_H77 ]. % 0.21/0.52 generalize (reflexivity_leq (n0)). zenon_intro zenon_H79. % 0.21/0.52 exact (zenon_H78 zenon_H79). % 0.21/0.52 apply (zenon_notand_s _ _ zenon_H77); [ zenon_intro zenon_H68 | zenon_intro zenon_H7a ]. % 0.21/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H64. % 0.21/0.52 generalize (zenon_H64 (pv10)). zenon_intro zenon_H65. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H68; zenon_intro zenon_H67 | zenon_intro zenon_H5f; zenon_intro zenon_H66 ]. % 0.21/0.52 exact (zenon_H67 zenon_H66). % 0.21/0.52 exact (zenon_H68 zenon_H5f). % 0.21/0.52 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H6c | zenon_intro zenon_H7b ]. % 0.21/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H64. % 0.21/0.52 generalize (zenon_H64 (pv53)). zenon_intro zenon_H69. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H6c; zenon_intro zenon_H6b | zenon_intro zenon_H61; zenon_intro zenon_H6a ]. % 0.21/0.52 exact (zenon_H6b zenon_H6a). % 0.21/0.52 exact (zenon_H6c zenon_H61). % 0.21/0.52 apply (zenon_notand_s _ _ zenon_H7b); [ zenon_intro zenon_H71 | zenon_intro zenon_H76 ]. % 0.21/0.52 generalize (leq_succ_gt_equiv (pv10)). zenon_intro zenon_H6d. % 0.21/0.52 generalize (zenon_H6d (minus (n135300) (n1))). zenon_intro zenon_H6e. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H6e); [ zenon_intro zenon_H71; zenon_intro zenon_H70 | zenon_intro zenon_H63; zenon_intro zenon_H6f ]. % 0.21/0.52 exact (zenon_H70 zenon_H6f). % 0.21/0.52 exact (zenon_H71 zenon_H63). % 0.21/0.52 generalize (leq_succ_gt_equiv (pv53)). zenon_intro zenon_H72. % 0.21/0.52 generalize (zenon_H72 (minus (n5) (n1))). zenon_intro zenon_H73. % 0.21/0.52 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H76; zenon_intro zenon_H75 | zenon_intro zenon_H62; zenon_intro zenon_H74 ]. % 0.21/0.52 exact (zenon_H75 zenon_H74). % 0.21/0.52 exact (zenon_H76 zenon_H62). % 0.21/0.52 Qed. % 0.21/0.52 % SZS output end Proof % 0.21/0.52 (* END-PROOF *) % 0.21/0.52 nodes searched: 16 % 0.21/0.52 max branch formulas: 97 % 0.21/0.52 proof nodes created: 15 % 0.21/0.52 formulas created: 1657 % 0.21/0.52 %------------------------------------------------------------------------------