%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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 : 300s % DateTime : Tue May 5 06:56:05 PM UTC 2026 % Result : Theorem 31.35s 31.51s % Output : Proof 31.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : run_zenon %s %d % 0.17/0.33 % Computer : n027.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Tue May 5 05:21:04 EDT 2026 % 0.17/0.33 % CPUTime : % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__121 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__124 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 31.35/31.51 Zenon warning: unused variable (Vvar__1___24Anonymous__32109 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__32112 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 31.35/31.51 Zenon warning: unused variable (Vvar__3___24Anonymous__105 : zenon_U) in $_inj_Coq.Init.Specif.exist % 31.35/31.51 Zenon warning: unused variable (Vvar__3___24Anonymous__106 : zenon_U) in $_inj_Coq.Init.Specif.exist % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__129 : zenon_U) in $_inj_Coq.Init.Specif.left % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__130 : zenon_U) in $_inj_Coq.Init.Specif.left % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__135 : zenon_U) in $_inj_Coq.Init.Specif.right % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__136 : zenon_U) in $_inj_Coq.Init.Specif.right % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__32127 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__32128 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 31.35/31.51 Zenon warning: unused variable (Vvar__1___24Anonymous__32115 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 31.35/31.51 Zenon warning: unused variable (Vvar__1___24Anonymous__32116 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__32121 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 31.35/31.51 Zenon warning: unused variable (Vvar__2___24Anonymous__32122 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 31.35/31.51 Zenon warning: unused variable (Vvar__5___24Anonymous__16828 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 31.35/31.51 Zenon warning: unused variable (Vvar__5___24Anonymous__16829 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 31.35/31.51 Zenon warning: unused variable (Vvar__6___24Anonymous__16830 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 31.35/31.51 Zenon warning: unused variable (Vvar__6___24Anonymous__16831 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 31.35/31.51 Zenon warning: unused variable (Vvar__4___24Anonymous__18845 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 31.35/31.51 Zenon warning: unused variable (Vvar__4___24Anonymous__18846 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 31.35/31.51 Zenon warning: unused variable (Vvar__5___24Anonymous__18847 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 31.35/31.51 Zenon warning: unused variable (Vvar__5___24Anonymous__18848 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 31.35/31.51 Zenon warning: unused variable (Vvar__6___24Anonymous__18849 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 31.35/31.51 Zenon warning: unused variable (Vvar__6___24Anonymous__18850 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 31.35/31.51 (* PROOF-FOUND *) % 31.35/31.51 % SZS status Theorem % 31.35/31.51 (* BEGIN-PROOF *) % 31.35/31.51 % SZS output start Proof % 31.35/31.51 Theorem _HAMMER_GOAL : (forall V0__n : zenon_U, ((cCoq_2eNumbers_2eBinNums_2eZ___24t V0__n)->(forall V1__m : zenon_U, ((cCoq_2eNumbers_2eBinNums_2eZ___24t V1__m)->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eNumbers_2eBinNums_2eZ0) V0__n))->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eNumbers_2eBinNums_2eZ0) V1__m))->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2 V1__m V1__m) (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2 V0__n V0__n)))->(p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 V1__m V0__n))))))))). % 31.35/31.51 Proof. % 31.35/31.51 assert (zenon_L1_ : forall (zenon_TV1__m_cmv : zenon_U), (t zenon_TV1__m_cmv (cCoq_2eNumbers_2eBinNums_2eZ)) -> (~(cCoq_2eNumbers_2eBinNums_2eZ___24t zenon_TV1__m_cmv)) -> False). % 31.35/31.51 do 1 intro. intros zenon_H693 zenon_H694. % 31.35/31.51 generalize ($tdef_Coq.Numbers.BinNums.Z zenon_TV1__m_cmv). zenon_intro zenon_H696. % 31.35/31.51 apply (zenon_equiv_s _ _ zenon_H696); [ zenon_intro zenon_H694; zenon_intro zenon_H698 | zenon_intro zenon_H697; zenon_intro zenon_H693 ]. % 31.35/31.51 exact (zenon_H698 zenon_H693). % 31.35/31.51 exact (zenon_H694 zenon_H697). % 31.35/31.54 (* end of lemma zenon_L1_ *) % 31.35/31.54 assert (zenon_L2_ : forall (zenon_TV0__n_cnb : zenon_U), (t zenon_TV0__n_cnb (cCoq_2eNumbers_2eBinNums_2eZ)) -> (~(cCoq_2eNumbers_2eBinNums_2eZ___24t zenon_TV0__n_cnb)) -> False). % 31.35/31.54 do 1 intro. intros zenon_H699 zenon_H69a. % 31.35/31.54 generalize ($tdef_Coq.Numbers.BinNums.Z zenon_TV0__n_cnb). zenon_intro zenon_H69c. % 31.35/31.54 apply (zenon_equiv_s _ _ zenon_H69c); [ zenon_intro zenon_H69a; zenon_intro zenon_H69e | zenon_intro zenon_H69d; zenon_intro zenon_H699 ]. % 31.35/31.54 exact (zenon_H69e zenon_H699). % 31.35/31.54 exact (zenon_H69a zenon_H69d). % 31.35/31.54 (* end of lemma zenon_L2_ *) % 31.35/31.54 apply NNPP. intro zenon_G. % 31.35/31.54 apply (zenon_notallex_s (fun V0__n : zenon_U => ((cCoq_2eNumbers_2eBinNums_2eZ___24t V0__n)->(forall V1__m : zenon_U, ((cCoq_2eNumbers_2eBinNums_2eZ___24t V1__m)->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eNumbers_2eBinNums_2eZ0) V0__n))->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eNumbers_2eBinNums_2eZ0) V1__m))->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2 V1__m V1__m) (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2 V0__n V0__n)))->(p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 V1__m V0__n))))))))) zenon_G); [ zenon_intro zenon_H69f; idtac ]. % 31.35/31.54 elim zenon_H69f. zenon_intro zenon_TV0__n_cnb. zenon_intro zenon_H6a0. % 31.35/31.54 apply (zenon_notimply_s _ _ zenon_H6a0). zenon_intro zenon_H69d. zenon_intro zenon_H6a1. % 31.35/31.54 generalize ($tdef_Coq.Numbers.BinNums.Z zenon_TV0__n_cnb). zenon_intro zenon_H69c. % 31.35/31.54 apply (zenon_equiv_s _ _ zenon_H69c); [ zenon_intro zenon_H69a; zenon_intro zenon_H69e | zenon_intro zenon_H69d; zenon_intro zenon_H699 ]. % 31.35/31.54 exact (zenon_H69a zenon_H69d). % 31.35/31.54 apply (zenon_notallex_s (fun V1__m : zenon_U => ((cCoq_2eNumbers_2eBinNums_2eZ___24t V1__m)->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eNumbers_2eBinNums_2eZ0) zenon_TV0__n_cnb))->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eNumbers_2eBinNums_2eZ0) V1__m))->((p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2 V1__m V1__m) (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2 zenon_TV0__n_cnb zenon_TV0__n_cnb)))->(p (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2 V1__m zenon_TV0__n_cnb))))))) zenon_H6a1); [ zenon_intro zenon_H6a2; idtac ]. % 31.35/31.54 elim zenon_H6a2. zenon_intro zenon_TV1__m_cmv. zenon_intro zenon_H6a3. % 31.35/31.54 apply (zenon_notimply_s _ _ zenon_H6a3). zenon_intro zenon_H697. zenon_intro zenon_H6a4. % 31.35/31.54 apply (zenon_notimply_s _ _ zenon_H6a4). zenon_intro zenon_H6a6. zenon_intro zenon_H6a5. % 31.35/31.54 apply (zenon_notimply_s _ _ zenon_H6a5). zenon_intro zenon_H6a8. zenon_intro zenon_H6a7. % 31.35/31.54 apply (zenon_notimply_s _ _ zenon_H6a7). zenon_intro zenon_H6aa. zenon_intro zenon_H6a9. % 31.35/31.54 generalize ($tdef_Coq.Numbers.BinNums.Z zenon_TV1__m_cmv). zenon_intro zenon_H696. % 31.35/31.54 apply (zenon_equiv_s _ _ zenon_H696); [ zenon_intro zenon_H694; zenon_intro zenon_H698 | zenon_intro zenon_H697; zenon_intro zenon_H693 ]. % 31.35/31.54 exact (zenon_H694 zenon_H697). % 31.35/31.54 generalize (Coq.ZArith.BinInt.Z.square_le_simpl_nonneg zenon_TV1__m_cmv). zenon_intro zenon_H6ab. % 31.35/31.54 apply (zenon_imply_s _ _ zenon_H6ab); [ zenon_intro zenon_H694 | zenon_intro zenon_H6ac ]. % 31.35/31.54 apply (zenon_L1_ zenon_TV1__m_cmv); trivial. % 31.35/31.54 generalize (zenon_H6ac zenon_TV0__n_cnb). zenon_intro zenon_H6ad. % 31.35/31.54 apply (zenon_imply_s _ _ zenon_H6ad); [ zenon_intro zenon_H69a | zenon_intro zenon_H6ae ]. % 31.35/31.54 apply (zenon_L2_ zenon_TV0__n_cnb); trivial. % 31.35/31.54 apply (zenon_imply_s _ _ zenon_H6ae); [ zenon_intro zenon_H6b0 | zenon_intro zenon_H6af ]. % 31.35/31.54 exact (zenon_H6b0 zenon_H6a6). % 31.35/31.54 apply (zenon_imply_s _ _ zenon_H6af); [ zenon_intro zenon_H6b2 | zenon_intro zenon_H6b1 ]. % 31.35/31.54 exact (zenon_H6b2 zenon_H6aa). % 31.35/31.54 exact (zenon_H6a9 zenon_H6b1). % 31.35/31.54 Qed. % 31.35/31.54 % SZS output end Proof % 31.35/31.54 (* END-PROOF *) % 31.35/31.54 nodes searched: 175146 % 31.35/31.54 max branch formulas: 101958 % 31.35/31.54 proof nodes created: 1757 % 31.35/31.54 formulas created: 1976852 % 31.35/31.54 %------------------------------------------------------------------------------