%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM316+1 : TPTP v8.1.0. Released v3.1.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 : Mon Jul 18 15:54:50 EDT 2022 % Result : Theorem 1.58s 1.77s % Output : Proof 1.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : NUM316+1 : TPTP v8.1.0. Released v3.1.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 : Thu Jul 7 02:11:14 EDT 2022 % 0.12/0.33 % CPUTime : % 1.58/1.77 (* PROOF-FOUND *) % 1.58/1.77 % SZS status Theorem % 1.58/1.77 (* BEGIN-PROOF *) % 1.58/1.77 % SZS output start Proof % 1.58/1.77 Theorem sum_n2_nn5_nn3 : (sum (n2) (nn5) (nn3)). % 1.58/1.77 Proof. % 1.58/1.77 assert (zenon_L1_ : (~(rdn_positive_less (rdnn (n3)) (rdnn (n5)))) -> False). % 1.58/1.77 do 0 intro. intros zenon_H192. % 1.58/1.77 generalize (rdn_positive_less_transitivity (n3)). zenon_intro zenon_H193. % 1.58/1.77 generalize (zenon_H193 (n4)). zenon_intro zenon_H194. % 1.58/1.77 generalize (zenon_H194 (n5)). zenon_intro zenon_H195. % 1.58/1.77 apply (zenon_imply_s _ _ zenon_H195); [ zenon_intro zenon_H197 | zenon_intro zenon_H196 ]. % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H197); [ zenon_intro zenon_H199 | zenon_intro zenon_H198 ]. % 1.58/1.77 exact (zenon_H199 rdn_positive_less34). % 1.58/1.77 exact (zenon_H198 rdn_positive_less45). % 1.58/1.77 exact (zenon_H192 zenon_H196). % 1.58/1.77 (* end of lemma zenon_L1_ *) % 1.58/1.77 assert (zenon_L2_ : (sum (n2) (nn5) (nn3)) -> (~(difference (nn3) (n2) (nn5))) -> False). % 1.58/1.77 do 0 intro. intros zenon_H19a zenon_H19b. % 1.58/1.77 generalize (minus_entry_point (nn3)). zenon_intro zenon_H19c. % 1.58/1.77 generalize (zenon_H19c (n2)). zenon_intro zenon_H19d. % 1.58/1.77 generalize (zenon_H19d (nn5)). zenon_intro zenon_H19e. % 1.58/1.77 apply (zenon_equiv_s _ _ zenon_H19e); [ zenon_intro zenon_G; zenon_intro zenon_H19b | zenon_intro zenon_H19a; zenon_intro zenon_H19f ]. % 1.58/1.77 exact (zenon_G zenon_H19a). % 1.58/1.77 exact (zenon_H19b zenon_H19f). % 1.58/1.77 (* end of lemma zenon_L2_ *) % 1.58/1.77 assert (zenon_L3_ : (forall RDN_Y : zenon_U, (forall RDN_Z : zenon_U, (((rdn_translate (n2) (rdn_pos (rdnn (n2))))/\((rdn_translate (nn5) (rdn_neg RDN_Y))/\((rdn_positive_less (rdnn (n2)) RDN_Y)/\((rdn_add_with_carry (rdnn (n0)) (rdnn (n2)) RDN_Z RDN_Y)/\(rdn_translate (nn3) (rdn_neg RDN_Z))))))->(sum (n2) (nn5) (nn3))))) -> (~(difference (nn3) (n2) (nn5))) -> (rdn_positive_less (rdnn (n2)) (rdnn (n5))) -> False). % 1.58/1.77 do 0 intro. intros zenon_H1a0 zenon_H19b zenon_H1a1. % 1.58/1.77 generalize (zenon_H1a0 (rdnn (n5))). zenon_intro zenon_H1a2. % 1.58/1.77 generalize (zenon_H1a2 (rdnn (n3))). zenon_intro zenon_H1a3. % 1.58/1.77 apply (zenon_imply_s _ _ zenon_H1a3); [ zenon_intro zenon_H1a4 | zenon_intro zenon_H19a ]. % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H1a4); [ zenon_intro zenon_H1a6 | zenon_intro zenon_H1a5 ]. % 1.58/1.77 exact (zenon_H1a6 rdn2). % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H1a5); [ zenon_intro zenon_H1a8 | zenon_intro zenon_H1a7 ]. % 1.58/1.77 exact (zenon_H1a8 rdnn5). % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H1a7); [ zenon_intro zenon_H1aa | zenon_intro zenon_H1a9 ]. % 1.58/1.77 exact (zenon_H1aa zenon_H1a1). % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H1a9); [ zenon_intro zenon_H1ac | zenon_intro zenon_H1ab ]. % 1.58/1.77 generalize (add_digit_digit_digit (n0)). zenon_intro zenon_H1ad. % 1.58/1.77 generalize (zenon_H1ad (n2)). zenon_intro zenon_H1ae. % 1.58/1.77 generalize (zenon_H1ae (n3)). zenon_intro zenon_H1af. % 1.58/1.77 generalize (zenon_H1af (n5)). zenon_intro zenon_H1b0. % 1.58/1.77 generalize (zenon_H1b0 (n5)). zenon_intro zenon_H1b1. % 1.58/1.77 apply (zenon_imply_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b3 | zenon_intro zenon_H1b2 ]. % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H1b3); [ zenon_intro zenon_H1b5 | zenon_intro zenon_H1b4 ]. % 1.58/1.77 exact (zenon_H1b5 rdn_digit_add_n2_n3_n5_n0). % 1.58/1.77 exact (zenon_H1b4 rdn_digit_add_n5_n0_n5_n0). % 1.58/1.77 exact (zenon_H1ac zenon_H1b2). % 1.58/1.77 exact (zenon_H1ab rdnn3). % 1.58/1.77 apply (zenon_L2_); trivial. % 1.58/1.77 (* end of lemma zenon_L3_ *) % 1.58/1.77 assert (zenon_L4_ : (forall RDN_X : zenon_U, (forall RDN_Y : zenon_U, (forall RDN_Z : zenon_U, (((rdn_translate (n2) (rdn_pos RDN_X))/\((rdn_translate (nn5) (rdn_neg RDN_Y))/\((rdn_positive_less RDN_X RDN_Y)/\((rdn_add_with_carry (rdnn (n0)) RDN_X RDN_Z RDN_Y)/\(rdn_translate (nn3) (rdn_neg RDN_Z))))))->(sum (n2) (nn5) (nn3)))))) -> (rdn_positive_less (rdnn (n2)) (rdnn (n5))) -> (~(difference (nn3) (n2) (nn5))) -> False). % 1.58/1.77 do 0 intro. intros zenon_H1b6 zenon_H1a1 zenon_H19b. % 1.58/1.77 generalize (zenon_H1b6 (rdnn (n2))). zenon_intro zenon_H1a0. % 1.58/1.77 apply (zenon_L3_); trivial. % 1.58/1.77 (* end of lemma zenon_L4_ *) % 1.58/1.77 apply NNPP. intro zenon_G. % 1.58/1.77 generalize (minus_entry_point (nn3)). zenon_intro zenon_H19c. % 1.58/1.77 generalize (zenon_H19c (n2)). zenon_intro zenon_H19d. % 1.58/1.77 generalize (zenon_H19d (nn5)). zenon_intro zenon_H19e. % 1.58/1.77 apply (zenon_equiv_s _ _ zenon_H19e); [ zenon_intro zenon_G; zenon_intro zenon_H19b | zenon_intro zenon_H19a; zenon_intro zenon_H19f ]. % 1.58/1.77 generalize (sum_entry_point_pos_neg_1 (n2)). zenon_intro zenon_H1b7. % 1.58/1.77 generalize (zenon_H1b7 (nn5)). zenon_intro zenon_H1b8. % 1.58/1.77 generalize (zenon_H1b8 (nn3)). zenon_intro zenon_H1b6. % 1.58/1.77 generalize (rdn_positive_less_transitivity (n2)). zenon_intro zenon_H1b9. % 1.58/1.77 generalize (zenon_H1b9 (n3)). zenon_intro zenon_H1ba. % 1.58/1.77 generalize (zenon_H1ba (n5)). zenon_intro zenon_H1bb. % 1.58/1.77 apply (zenon_imply_s _ _ zenon_H1bb); [ zenon_intro zenon_H1bc | zenon_intro zenon_H1a1 ]. % 1.58/1.77 apply (zenon_notand_s _ _ zenon_H1bc); [ zenon_intro zenon_H1bd | zenon_intro zenon_H192 ]. % 1.58/1.77 exact (zenon_H1bd rdn_positive_less23). % 1.58/1.77 apply (zenon_L1_); trivial. % 1.58/1.77 apply (zenon_L4_); trivial. % 1.58/1.77 exact (zenon_G zenon_H19a). % 1.58/1.77 Qed. % 1.58/1.77 % SZS output end Proof % 1.58/1.77 (* END-PROOF *) % 1.58/1.77 nodes searched: 209145 % 1.58/1.77 max branch formulas: 4481 % 1.58/1.77 proof nodes created: 3296 % 1.58/1.77 formulas created: 238806 % 1.58/1.77 %------------------------------------------------------------------------------