%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM925+1 : TPTP v8.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.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 16:00:29 EDT 2022 % Result : Theorem 137.73s 137.92s % Output : Proof 137.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM925+1 : TPTP v8.1.0. Released v5.3.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 5 06:58:57 EDT 2022 % 0.13/0.34 % CPUTime : % 137.73/137.92 (* PROOF-FOUND *) % 137.73/137.92 % SZS status Theorem % 137.73/137.92 (* BEGIN-PROOF *) % 137.73/137.92 % SZS output start Proof % 137.73/137.92 Theorem conj_0 : (~((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int))). % 137.73/137.92 Proof. % 137.73/137.92 assert (zenon_L1_ : (~((zero_zero_int) = (zero_zero_int))) -> False). % 137.73/137.92 do 0 intro. intros zenon_H60. % 137.73/137.92 apply zenon_H60. apply refl_equal. % 137.73/137.92 (* end of lemma zenon_L1_ *) % 137.73/137.92 assert (zenon_L2_ : (~((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (power_power_int (zero_zero_int) (number_number_of_nat (bit0 (bit1 (pls))))))) -> ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) -> False). % 137.73/137.92 do 0 intro. intros zenon_H61 zenon_H62. % 137.73/137.92 cut (((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (zero_zero_int)) = ((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (power_power_int (zero_zero_int) (number_number_of_nat (bit0 (bit1 (pls))))))). % 137.73/137.92 intro zenon_D_pnotp. % 137.73/137.92 apply zenon_H61. % 137.73/137.92 rewrite <- zenon_D_pnotp. % 137.73/137.92 exact zenon_H62. % 137.73/137.92 cut (((zero_zero_int) = (power_power_int (zero_zero_int) (number_number_of_nat (bit0 (bit1 (pls))))))); [idtac | apply NNPP; zenon_intro zenon_H63]. % 137.73/137.92 cut (((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 137.73/137.92 congruence. % 137.73/137.92 apply zenon_H64. apply refl_equal. % 137.73/137.92 apply zenon_H63. apply sym_equal. exact fact_5_zero__power2. % 137.73/137.92 (* end of lemma zenon_L2_ *) % 137.73/137.92 apply NNPP. intro zenon_G. % 137.73/137.92 apply zenon_G. zenon_intro zenon_H62. % 137.73/137.92 generalize (fact_103_zero__less__power2 (zero_zero_int)). zenon_intro zenon_H65. % 137.73/137.92 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H68; zenon_intro zenon_H67 | zenon_intro zenon_H66; zenon_intro zenon_H60 ]. % 137.73/137.92 cut ((ord_less_int (zero_zero_int) (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))) = (ord_less_int (pls) (zero_zero_int))). % 137.73/137.92 intro zenon_D_pnotp. % 137.73/137.92 apply fact_62_bin__less__0__simps_I1_J. % 137.73/137.92 rewrite <- zenon_D_pnotp. % 137.73/137.92 exact fact_0_n1pos. % 137.73/137.92 cut (((plus_plus_int (one_one_int) (semiri1621563631at_int (n))) = (zero_zero_int))); [idtac | apply NNPP; zenon_intro zenon_H69]. % 137.73/137.92 cut (((zero_zero_int) = (pls))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 137.73/137.92 congruence. % 137.73/137.92 apply zenon_H6a. apply sym_equal. exact fact_78_Pls__def. % 137.73/137.92 generalize (fact_103_zero__less__power2 (plus_plus_int (one_one_int) (semiri1621563631at_int (n)))). zenon_intro zenon_H6b. % 137.73/137.92 apply (zenon_equiv_s _ _ zenon_H6b); [ zenon_intro zenon_H6e; zenon_intro zenon_H6d | zenon_intro zenon_H6c; zenon_intro zenon_H69 ]. % 137.73/137.92 exact (zenon_H6d zenon_H69). % 137.73/137.92 cut ((ord_less_int (zero_zero_int) (power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls)))))) = (ord_less_int (zero_zero_int) (power_power_int (zero_zero_int) (number_number_of_nat (bit0 (bit1 (pls))))))). % 137.73/137.92 intro zenon_D_pnotp. % 137.73/137.92 apply zenon_H68. % 137.73/137.92 rewrite <- zenon_D_pnotp. % 137.73/137.92 exact zenon_H6c. % 137.73/137.92 cut (((power_power_int (plus_plus_int (one_one_int) (semiri1621563631at_int (n))) (number_number_of_nat (bit0 (bit1 (pls))))) = (power_power_int (zero_zero_int) (number_number_of_nat (bit0 (bit1 (pls))))))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 137.73/137.92 cut (((zero_zero_int) = (zero_zero_int))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 137.73/137.92 congruence. % 137.73/137.92 apply zenon_H60. apply refl_equal. % 137.73/137.92 apply (zenon_L2_); trivial. % 137.73/137.92 apply zenon_H60. apply refl_equal. % 137.73/137.92 Qed. % 137.73/137.92 % SZS output end Proof % 137.73/137.92 (* END-PROOF *) % 137.73/137.92 nodes searched: 825011 % 137.73/137.92 max branch formulas: 14971 % 137.73/137.92 proof nodes created: 18210 % 137.73/137.92 formulas created: 2684925 % 137.73/137.92 %------------------------------------------------------------------------------