%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV678+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n014.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:09 PM UTC 2026 % Result : Theorem 24.34s 24.59s % Output : Proof 24.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV678+1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.13 % Command : run_zenon %s %d % 0.18/0.34 % Computer : n014.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue May 5 08:24:36 EDT 2026 % 0.18/0.35 % CPUTime : % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__92264 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__92266 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112854 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112858 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__308 : zenon_U) in $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__265 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__268 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__113356 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__113359 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.54/0.76 Zenon warning: unused variable (Vvar__5___24Anonymous__90920 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.54/0.76 Zenon warning: unused variable (Vvar__5___24Anonymous__90926 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__92273 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__92274 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__92269 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__92270 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112865 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112866 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112881 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112882 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112873 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__112874 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__78070 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.54/0.76 Zenon warning: unused variable (Vvar__3___24Anonymous__78071 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__319 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__320 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__273 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__274 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__279 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__280 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__113374 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__113375 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__113362 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 0.54/0.76 Zenon warning: unused variable (Vvar__1___24Anonymous__113363 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__113368 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 0.54/0.76 Zenon warning: unused variable (Vvar__2___24Anonymous__113369 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 0.54/0.76 Zenon warning: unused variable (Vvar__5___24Anonymous__90949 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 24.34/24.59 Zenon warning: unused variable (Vvar__5___24Anonymous__90950 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 24.34/24.59 Zenon warning: unused variable (Vvar__5___24Anonymous__90961 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 24.34/24.59 Zenon warning: unused variable (Vvar__5___24Anonymous__90962 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 24.34/24.59 Zenon warning: unused variable (Vvar__5___24Anonymous__90937 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 24.34/24.59 Zenon warning: unused variable (Vvar__5___24Anonymous__90938 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 24.34/24.59 (* PROOF-FOUND *) % 24.34/24.59 % SZS status Theorem % 24.34/24.59 (* BEGIN-PROOF *) % 24.34/24.59 % SZS output start Proof % 24.34/24.59 Theorem _HAMMER_GOAL : ((forall V0__x : zenon_U, ((cCoq_2eInit_2eDatatypes_2enat___24t V0__x)->(cUseAuto_2eP___24a1 V0__x)))->(p (cUseAuto_2emyFact))). % 24.34/24.59 Proof. % 24.34/24.59 apply NNPP. intro zenon_G. % 24.34/24.59 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_Hb4f. zenon_intro zenon_Hb4e. % 24.34/24.59 apply (zenon_equiv_s _ _ $_def_UseAuto.myFact); [ zenon_intro zenon_Hb4e; zenon_intro zenon_Hb52 | zenon_intro zenon_Hb51; zenon_intro zenon_Hb50 ]. % 24.34/24.59 apply (zenon_notallex_s (fun V0__x : zenon_U => ((cCoq_2eInit_2eDatatypes_2enat___24t V0__x)->((cCoq_2eInit_2ePeano_2ele___24a2 V0__x (cCoq_2eInit_2eDatatypes_2eS___24a1 (cCoq_2eInit_2eDatatypes_2eS___24a1 (cCoq_2eInit_2eDatatypes_2eS___24a1 (cCoq_2eInit_2eDatatypes_2eO)))))->(cUseAuto_2eP___24a1 V0__x)))) zenon_Hb52); [ zenon_intro zenon_Hb53; idtac ]. % 24.34/24.59 elim zenon_Hb53. zenon_intro zenon_TV0__x_eho. zenon_intro zenon_Hb55. % 24.34/24.59 apply (zenon_notimply_s _ _ zenon_Hb55). zenon_intro zenon_Hb57. zenon_intro zenon_Hb56. % 24.34/24.59 apply (zenon_notimply_s _ _ zenon_Hb56). zenon_intro zenon_Hb59. zenon_intro zenon_Hb58. % 24.34/24.59 generalize ($tdef_Coq.Init.Datatypes.nat zenon_TV0__x_eho). zenon_intro zenon_Hb5a. % 24.34/24.59 apply (zenon_equiv_s _ _ zenon_Hb5a); [ zenon_intro zenon_Hb5d; zenon_intro zenon_Hb5c | zenon_intro zenon_Hb57; zenon_intro zenon_Hb5b ]. % 24.34/24.59 exact (zenon_Hb5d zenon_Hb57). % 24.34/24.59 generalize (zenon_Hb4f zenon_TV0__x_eho). zenon_intro zenon_Hb5e. % 24.34/24.59 apply (zenon_imply_s _ _ zenon_Hb5e); [ zenon_intro zenon_Hb5d | zenon_intro zenon_Hb5f ]. % 24.34/24.59 generalize ($tdef_Coq.Init.Datatypes.nat zenon_TV0__x_eho). zenon_intro zenon_Hb5a. % 24.34/24.59 apply (zenon_equiv_s _ _ zenon_Hb5a); [ zenon_intro zenon_Hb5d; zenon_intro zenon_Hb5c | zenon_intro zenon_Hb57; zenon_intro zenon_Hb5b ]. % 24.34/24.59 exact (zenon_Hb5c zenon_Hb5b). % 24.34/24.59 exact (zenon_Hb5d zenon_Hb57). % 24.34/24.59 exact (zenon_Hb58 zenon_Hb5f). % 24.34/24.59 exact (zenon_Hb4e zenon_Hb51). % 24.34/24.59 Qed. % 24.34/24.59 % SZS output end Proof % 24.34/24.59 (* END-PROOF *) % 24.34/24.59 nodes searched: 135043 % 24.34/24.59 max branch formulas: 68727 % 24.34/24.59 proof nodes created: 36 % 24.34/24.59 formulas created: 2921790 % 24.34/24.59 %------------------------------------------------------------------------------