%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM306+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n013.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:47 EDT 2022 % Result : Theorem 27.70s 27.87s % Output : Proof 27.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM306+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n013.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 : Tue Jul 5 12:07:29 EDT 2022 % 0.12/0.33 % CPUTime : % 27.70/27.87 (* PROOF-FOUND *) % 27.70/27.87 % SZS status Theorem % 27.70/27.87 (* BEGIN-PROOF *) % 27.70/27.87 % SZS output start Proof % 27.70/27.87 Theorem sum_n23_n34_n57 : (sum (n23) (n34) (n57)). % 27.70/27.87 Proof. % 27.70/27.87 assert (zenon_L1_ : (~(rdn_non_zero (rdnn (n2)))) -> False). % 27.70/27.87 do 0 intro. intros zenon_H192. % 27.70/27.87 generalize (rdn_non_zero_by_digit (n2)). zenon_intro zenon_H193. % 27.70/27.87 apply (zenon_imply_s _ _ zenon_H193); [ zenon_intro zenon_H195 | zenon_intro zenon_H194 ]. % 27.70/27.87 exact (zenon_H195 rdn_digit2). % 27.70/27.87 exact (zenon_H192 zenon_H194). % 27.70/27.87 (* end of lemma zenon_L1_ *) % 27.70/27.87 assert (zenon_L2_ : (~(rdn_non_zero (rdnn (n3)))) -> False). % 27.70/27.87 do 0 intro. intros zenon_H196. % 27.70/27.87 generalize (rdn_non_zero_by_digit (n3)). zenon_intro zenon_H197. % 27.70/27.87 apply (zenon_imply_s _ _ zenon_H197); [ zenon_intro zenon_H199 | zenon_intro zenon_H198 ]. % 27.70/27.87 exact (zenon_H199 rdn_digit3). % 27.70/27.87 exact (zenon_H196 zenon_H198). % 27.70/27.87 (* end of lemma zenon_L2_ *) % 27.70/27.87 assert (zenon_L3_ : (~(rdn_non_zero (rdnn (n5)))) -> False). % 27.70/27.87 do 0 intro. intros zenon_H19a. % 27.70/27.87 generalize (rdn_non_zero_by_digit (n5)). zenon_intro zenon_H19b. % 27.70/27.87 apply (zenon_imply_s _ _ zenon_H19b); [ zenon_intro zenon_H19d | zenon_intro zenon_H19c ]. % 27.70/27.87 exact (zenon_H19d rdn_digit5). % 27.70/27.87 exact (zenon_H19a zenon_H19c). % 27.70/27.87 (* end of lemma zenon_L3_ *) % 27.70/27.87 assert (zenon_L4_ : (forall RC : zenon_U, (((rdn_digit_add (rdnn (n3)) (rdnn (n4)) (rdnn (n7)) (rdnn (n0)))/\((rdn_digit_add (rdnn (n7)) (rdnn (n0)) (rdnn (n7)) (rdnn (n0)))/\((rdn_digit_add (rdnn (n0)) (rdnn (n0)) (rdnn RC) (rdnn (n0)))/\((rdn_add_with_carry (rdnn RC) (rdnn (n2)) (rdnn (n3)) (rdnn (n5)))/\((rdn_non_zero (rdnn (n2)))/\((rdn_non_zero (rdnn (n3)))/\(rdn_non_zero (rdnn (n5)))))))))->(rdn_add_with_carry (rdnn (n0)) (rdn (rdnn (n3)) (rdnn (n2))) (rdn (rdnn (n4)) (rdnn (n3))) (rdn (rdnn (n7)) (rdnn (n5)))))) -> (rdn_add_with_carry (rdnn (n0)) (rdnn (n2)) (rdnn (n3)) (rdnn (n5))) -> (~(rdn_add_with_carry (rdnn (n0)) (rdn (rdnn (n3)) (rdnn (n2))) (rdn (rdnn (n4)) (rdnn (n3))) (rdn (rdnn (n7)) (rdnn (n5))))) -> False). % 27.70/27.87 do 0 intro. intros zenon_H19e zenon_H19f zenon_H1a0. % 27.70/27.87 generalize (zenon_H19e (n0)). zenon_intro zenon_H1a1. % 27.70/27.87 apply (zenon_imply_s _ _ zenon_H1a1); [ zenon_intro zenon_H1a3 | zenon_intro zenon_H1a2 ]. % 27.70/27.87 apply (zenon_notand_s _ _ zenon_H1a3); [ zenon_intro zenon_H1a5 | zenon_intro zenon_H1a4 ]. % 27.70/27.87 exact (zenon_H1a5 rdn_digit_add_n3_n4_n7_n0). % 27.70/27.87 apply (zenon_notand_s _ _ zenon_H1a4); [ zenon_intro zenon_H1a7 | zenon_intro zenon_H1a6 ]. % 27.70/27.87 exact (zenon_H1a7 rdn_digit_add_n7_n0_n7_n0). % 27.70/27.87 apply (zenon_notand_s _ _ zenon_H1a6); [ zenon_intro zenon_H1a9 | zenon_intro zenon_H1a8 ]. % 27.70/27.87 exact (zenon_H1a9 rdn_digit_add_n0_n0_n0_n0). % 27.70/27.87 apply (zenon_notand_s _ _ zenon_H1a8); [ zenon_intro zenon_H1ab | zenon_intro zenon_H1aa ]. % 27.70/27.87 exact (zenon_H1ab zenon_H19f). % 27.70/27.87 apply (zenon_notand_s _ _ zenon_H1aa); [ zenon_intro zenon_H192 | zenon_intro zenon_H1ac ]. % 27.70/27.87 apply (zenon_L1_); trivial. % 27.70/27.87 apply (zenon_notand_s _ _ zenon_H1ac); [ zenon_intro zenon_H196 | zenon_intro zenon_H19a ]. % 27.70/27.87 apply (zenon_L2_); trivial. % 27.70/27.87 apply (zenon_L3_); trivial. % 27.70/27.87 exact (zenon_H1a0 zenon_H1a2). % 27.70/27.87 (* end of lemma zenon_L4_ *) % 27.70/27.87 assert (zenon_L5_ : (sum (n23) (n34) (n57)) -> (~(difference (n57) (n23) (n34))) -> False). % 27.70/27.87 do 0 intro. intros zenon_H1ad zenon_H1ae. % 27.70/27.87 generalize (minus_entry_point (n57)). zenon_intro zenon_H1af. % 27.70/27.87 generalize (zenon_H1af (n23)). zenon_intro zenon_H1b0. % 27.70/27.87 generalize (zenon_H1b0 (n34)). zenon_intro zenon_H1b1. % 27.70/27.87 apply (zenon_equiv_s _ _ zenon_H1b1); [ zenon_intro zenon_G; zenon_intro zenon_H1ae | zenon_intro zenon_H1ad; zenon_intro zenon_H1b2 ]. % 27.70/27.87 exact (zenon_G zenon_H1ad). % 27.70/27.87 exact (zenon_H1ae zenon_H1b2). % 27.70/27.87 (* end of lemma zenon_L5_ *) % 27.70/27.87 apply NNPP. intro zenon_G. % 27.70/27.87 generalize (minus_entry_point (n57)). zenon_intro zenon_H1af. % 27.70/27.87 generalize (zenon_H1af (n23)). zenon_intro zenon_H1b0. % 27.70/27.87 generalize (zenon_H1b0 (n34)). zenon_intro zenon_H1b1. % 27.70/27.87 apply (zenon_equiv_s _ _ zenon_H1b1); [ zenon_intro zenon_G; zenon_intro zenon_H1ae | zenon_intro zenon_H1ad; zenon_intro zenon_H1b2 ]. % 27.70/27.87 generalize (sum_entry_point_pos_pos (n23)). zenon_intro zenon_H1b3. % 27.70/27.87 generalize (zenon_H1b3 (n34)). zenon_intro zenon_H1b4. % 27.70/27.87 generalize (zenon_H1b4 (n57)). zenon_intro zenon_H1b5. % 27.70/27.87 generalize (zenon_H1b5 (rdn (rdnn (n3)) (rdnn (n2)))). zenon_intro zenon_H1b6. % 27.70/27.87 generalize (zenon_H1b6 (rdn (rdnn (n4)) (rdnn (n3)))). zenon_intro zenon_H1b7. % 27.70/27.88 generalize (zenon_H1b7 (rdn (rdnn (n7)) (rdnn (n5)))). zenon_intro zenon_H1b8. % 27.70/27.88 apply (zenon_imply_s _ _ zenon_H1b8); [ zenon_intro zenon_H1b9 | zenon_intro zenon_H1ad ]. % 27.70/27.88 apply (zenon_notand_s _ _ zenon_H1b9); [ zenon_intro zenon_H1bb | zenon_intro zenon_H1ba ]. % 27.70/27.88 exact (zenon_H1bb rdn23). % 27.70/27.88 apply (zenon_notand_s _ _ zenon_H1ba); [ zenon_intro zenon_H1bd | zenon_intro zenon_H1bc ]. % 27.70/27.88 exact (zenon_H1bd rdn34). % 27.70/27.88 apply (zenon_notand_s _ _ zenon_H1bc); [ zenon_intro zenon_H1a0 | zenon_intro zenon_H1be ]. % 27.70/27.88 generalize (add_rdn_rdn_rdn (n0)). zenon_intro zenon_H1bf. % 27.70/27.88 generalize (zenon_H1bf (n3)). zenon_intro zenon_H1c0. % 27.70/27.88 generalize (zenon_H1c0 (rdnn (n2))). zenon_intro zenon_H1c1. % 27.70/27.88 generalize (zenon_H1c1 (n4)). zenon_intro zenon_H1c2. % 27.70/27.88 generalize (zenon_H1c2 (rdnn (n3))). zenon_intro zenon_H1c3. % 27.70/27.88 generalize (zenon_H1c3 (n7)). zenon_intro zenon_H1c4. % 27.70/27.88 generalize (zenon_H1c4 (rdnn (n5))). zenon_intro zenon_H1c5. % 27.70/27.88 generalize (zenon_H1c5 (n7)). zenon_intro zenon_H1c6. % 27.70/27.88 generalize (zenon_H1c6 (n0)). zenon_intro zenon_H1c7. % 27.70/27.88 generalize (zenon_H1c7 (n0)). zenon_intro zenon_H19e. % 27.70/27.88 generalize (add_digit_digit_digit (n0)). zenon_intro zenon_H1c8. % 27.70/27.88 generalize (zenon_H1c8 (n2)). zenon_intro zenon_H1c9. % 27.70/27.88 generalize (zenon_H1c9 (n3)). zenon_intro zenon_H1ca. % 27.70/27.88 generalize (zenon_H1ca (n5)). zenon_intro zenon_H1cb. % 27.70/27.88 generalize (zenon_H1cb (n5)). zenon_intro zenon_H1cc. % 27.70/27.88 apply (zenon_imply_s _ _ zenon_H1cc); [ zenon_intro zenon_H1cd | zenon_intro zenon_H19f ]. % 27.70/27.88 apply (zenon_notand_s _ _ zenon_H1cd); [ zenon_intro zenon_H1cf | zenon_intro zenon_H1ce ]. % 27.70/27.88 exact (zenon_H1cf rdn_digit_add_n2_n3_n5_n0). % 27.70/27.88 exact (zenon_H1ce rdn_digit_add_n5_n0_n5_n0). % 27.70/27.88 apply (zenon_L4_); trivial. % 27.70/27.88 exact (zenon_H1be rdn57). % 27.70/27.88 apply (zenon_L5_); trivial. % 27.70/27.88 exact (zenon_G zenon_H1ad). % 27.70/27.88 Qed. % 27.70/27.88 % SZS output end Proof % 27.70/27.88 (* END-PROOF *) % 27.70/27.88 nodes searched: 798203 % 27.70/27.88 max branch formulas: 88143 % 27.70/27.88 proof nodes created: 16857 % 27.70/27.88 formulas created: 3226897 % 27.70/27.88 %------------------------------------------------------------------------------