%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n003.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 0.74s 0.91s % Output : Proof 0.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_zenon %s %d % 0.15/0.33 % Computer : n003.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue May 5 08:27:11 EDT 2026 % 0.15/0.33 % CPUTime : % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__92264 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__92266 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112854 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112858 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__308 : zenon_U) in $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__265 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__268 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__113356 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__113359 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.53/0.73 Zenon warning: unused variable (Vvar__5___24Anonymous__90920 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.53/0.73 Zenon warning: unused variable (Vvar__5___24Anonymous__90926 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__85860 : zenon_U) in $_discrim_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__92273 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__92274 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__92269 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.53/0.73 Zenon warning: unused variable (Vvar__1___24Anonymous__92270 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112865 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112866 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112881 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112882 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112873 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__112874 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__78070 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.53/0.73 Zenon warning: unused variable (Vvar__3___24Anonymous__78071 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.53/0.73 Zenon warning: unused variable (Vvar__4___24Anonymous__91832 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.53/0.73 Zenon warning: unused variable (Vvar__4___24Anonymous__91833 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.53/0.73 Zenon warning: unused variable (Vvar__5___24Anonymous__91834 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.53/0.73 Zenon warning: unused variable (Vvar__5___24Anonymous__91835 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__319 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__320 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__273 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__274 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__279 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.53/0.73 Zenon warning: unused variable (Vvar__2___24Anonymous__280 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.53/0.73 Zenon warning: unused variable (Vvar__1__cond__neg__85545 : zenon_U) in $_inj_Coq.Reals.RIneq.mknegreal % 0.53/0.73 Zenon warning: unused variable (Vvar__1__cond__neg__85546 : zenon_U) in $_inj_Coq.Reals.RIneq.mknegreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__nonneg__90968 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonnegreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__nonneg__90969 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonnegreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__nonpos__85538 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonposreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__nonpos__85539 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonposreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__nonzero__87824 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__nonzero__87825 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__pos__90975 : zenon_U) in $_inj_Coq.Reals.RIneq.mkposreal % 0.74/0.91 Zenon warning: unused variable (Vvar__1__cond__pos__90976 : zenon_U) in $_inj_Coq.Reals.RIneq.mkposreal % 0.74/0.91 Zenon warning: unused variable (Vvar__2___24Anonymous__113374 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 0.74/0.91 Zenon warning: unused variable (Vvar__2___24Anonymous__113375 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 0.74/0.91 Zenon warning: unused variable (Vvar__1___24Anonymous__113362 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 0.74/0.91 Zenon warning: unused variable (Vvar__1___24Anonymous__113363 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 0.74/0.91 Zenon warning: unused variable (Vvar__2___24Anonymous__113368 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 0.74/0.91 Zenon warning: unused variable (Vvar__2___24Anonymous__113369 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__90949 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__90950 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__90961 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__90962 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__90937 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__90938 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__113524 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__113525 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.74/0.91 Zenon warning: unused variable (Vvar__6___24Anonymous__113526 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.74/0.91 Zenon warning: unused variable (Vvar__6___24Anonymous__113527 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.74/0.91 Zenon warning: unused variable (Vvar__4___24Anonymous__113570 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.74/0.91 Zenon warning: unused variable (Vvar__4___24Anonymous__113571 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__113572 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.74/0.91 Zenon warning: unused variable (Vvar__5___24Anonymous__113573 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.74/0.91 Zenon warning: unused variable (Vvar__6___24Anonymous__113574 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.74/0.91 Zenon warning: unused variable (Vvar__6___24Anonymous__113575 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.74/0.91 Zenon warning: unused variable (Vvar__3___24Anonymous__85867 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 0.74/0.91 Zenon warning: unused variable (Vvar__3___24Anonymous__85868 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 0.74/0.91 Zenon warning: unused variable (Vvar__17___24Anonymous__85903 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 0.74/0.91 Zenon warning: unused variable (Vvar__17___24Anonymous__85904 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 0.74/0.91 (* PROOF-FOUND *) % 0.74/0.91 % SZS status Theorem % 0.74/0.91 (* BEGIN-PROOF *) % 0.74/0.91 % SZS output start Proof % 0.74/0.91 Theorem _HAMMER_GOAL : (forall V0__ST : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t V0__ST)->(forall V1__t : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2etm___24t V1__t)->(forall V2__t_27 : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2etm___24t V2__t_27)->(forall V3__T : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2ety___24t V3__T)->(forall V4__st : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2estore___24t V4__st)->(forall V5__st_27 : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2estore___24t V5__st_27)->((cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4 (cPLF_2eMaps_2eempty___24a1 (cPLF_2eReferences_2eSTLCRef_2ety)) V0__ST V1__t V3__T)->((cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2 V0__ST V4__st)->((cPLF_2eReferences_2eSTLCRef_2estep___24a2 (cCoq_2eInit_2eDatatypes_2epair___24a4 (cPLF_2eReferences_2eSTLCRef_2etm) (cPLF_2eReferences_2eSTLCRef_2estore) V1__t V4__st) (cCoq_2eInit_2eDatatypes_2epair___24a4 (cPLF_2eReferences_2eSTLCRef_2etm) (cPLF_2eReferences_2eSTLCRef_2estore) V2__t_27 V5__st_27))->(exists V9__ST_27 : zenon_U, ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t V9__ST_27)/\((cPLF_2eReferences_2eSTLCRef_2eextends___24a2 V9__ST_27 V0__ST)/\((cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4 (cPLF_2eMaps_2eempty___24a1 (cPLF_2eReferences_2eSTLCRef_2ety)) V9__ST_27 V2__t_27 V3__T)/\(cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2 V9__ST_27 V5__st_27)))))))))))))))))))). % 0.74/0.91 Proof. % 0.74/0.91 apply NNPP. intro zenon_G. % 0.74/0.91 exact (zenon_G PLF.References.STLCRef.preservation). % 0.74/0.91 Qed. % 0.74/0.91 % SZS output end Proof % 0.74/0.91 (* END-PROOF *) % 0.74/0.91 nodes searched: 352 % 0.74/0.91 max branch formulas: 3477 % 0.74/0.91 proof nodes created: 1 % 0.74/0.91 formulas created: 87283 % 0.74/0.91 %------------------------------------------------------------------------------