%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV672+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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.62s 0.88s % Output : Proof 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SEV672+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.09 % Command : run_zenon %s %d % 0.10/0.28 % Computer : n026.cluster.edu % 0.10/0.28 % Model : x86_64 x86_64 % 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.28 % Memory : 8042.1875MB % 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.28 % CPULimit : 300 % 0.10/0.28 % WCLimit : 300 % 0.10/0.28 % DateTime : Tue May 5 08:12:53 EDT 2026 % 0.10/0.29 % CPUTime : % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__12 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__14 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142035 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142039 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__141406 : zenon_U) in $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__30235 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__30238 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__139544 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__139547 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.44/0.67 Zenon warning: unused variable (Vvar__5___24Anonymous__31838 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.44/0.67 Zenon warning: unused variable (Vvar__5___24Anonymous__31844 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__141237 : zenon_U) in $_discrim_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__21 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__22 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__17 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.44/0.67 Zenon warning: unused variable (Vvar__1___24Anonymous__18 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142046 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142047 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142062 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142063 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142054 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__142055 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__102869 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.44/0.67 Zenon warning: unused variable (Vvar__3___24Anonymous__102870 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.44/0.67 Zenon warning: unused variable (Vvar__4___24Anonymous__102933 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.44/0.67 Zenon warning: unused variable (Vvar__4___24Anonymous__102934 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.44/0.67 Zenon warning: unused variable (Vvar__5___24Anonymous__102935 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.44/0.67 Zenon warning: unused variable (Vvar__5___24Anonymous__102936 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__141417 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__141418 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__30243 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__30244 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__30249 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.44/0.67 Zenon warning: unused variable (Vvar__2___24Anonymous__30250 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.44/0.67 Zenon warning: unused variable (Vvar__1__cond__neg__139466 : zenon_U) in $_inj_Coq.Reals.RIneq.mknegreal % 0.44/0.67 Zenon warning: unused variable (Vvar__1__cond__neg__139467 : zenon_U) in $_inj_Coq.Reals.RIneq.mknegreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__nonneg__127929 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonnegreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__nonneg__127930 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonnegreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__nonpos__139459 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonposreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__nonpos__139460 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonposreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__nonzero__139473 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__nonzero__139474 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__pos__139452 : zenon_U) in $_inj_Coq.Reals.RIneq.mkposreal % 0.62/0.88 Zenon warning: unused variable (Vvar__1__cond__pos__139453 : zenon_U) in $_inj_Coq.Reals.RIneq.mkposreal % 0.62/0.88 Zenon warning: unused variable (Vvar__2___24Anonymous__139562 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 0.62/0.88 Zenon warning: unused variable (Vvar__2___24Anonymous__139563 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 0.62/0.88 Zenon warning: unused variable (Vvar__1___24Anonymous__139550 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 0.62/0.88 Zenon warning: unused variable (Vvar__1___24Anonymous__139551 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 0.62/0.88 Zenon warning: unused variable (Vvar__2___24Anonymous__139556 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 0.62/0.88 Zenon warning: unused variable (Vvar__2___24Anonymous__139557 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__31867 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__31868 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__31879 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__31880 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__31855 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__31856 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__141583 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__141584 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.62/0.88 Zenon warning: unused variable (Vvar__6___24Anonymous__141585 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.62/0.88 Zenon warning: unused variable (Vvar__6___24Anonymous__141586 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 0.62/0.88 Zenon warning: unused variable (Vvar__4___24Anonymous__149414 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.62/0.88 Zenon warning: unused variable (Vvar__4___24Anonymous__149415 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__149416 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.62/0.88 Zenon warning: unused variable (Vvar__5___24Anonymous__149417 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.62/0.88 Zenon warning: unused variable (Vvar__6___24Anonymous__149418 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.62/0.88 Zenon warning: unused variable (Vvar__6___24Anonymous__149419 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 0.62/0.88 Zenon warning: unused variable (Vvar__3___24Anonymous__141244 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 0.62/0.88 Zenon warning: unused variable (Vvar__3___24Anonymous__141245 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 0.62/0.88 Zenon warning: unused variable (Vvar__17___24Anonymous__141280 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 0.62/0.88 Zenon warning: unused variable (Vvar__17___24Anonymous__141281 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 0.62/0.88 (* PROOF-FOUND *) % 0.62/0.88 % SZS status Theorem % 0.62/0.88 (* BEGIN-PROOF *) % 0.62/0.88 % SZS output start Proof % 0.62/0.88 Theorem _HAMMER_GOAL : (cPLF_2eSmallstep_2emulti___24a4 (cStlc_2eSTLC_2etm) (cStlc_2eSTLC_2estep) (cStlc_2eSTLC_2eapp___24a2 (cStlc_2eSTLC_2eabs___24a3 (cStlc_2eSTLC_2ex) (cStlc_2eSTLC_2eArrow___24a2 (cStlc_2eSTLC_2eBool) (cStlc_2eSTLC_2eBool)) (cStlc_2eSTLC_2evar___24a1 (cStlc_2eSTLC_2ex))) (cStlc_2eSTLC_2eabs___24a3 (cStlc_2eSTLC_2ex) (cStlc_2eSTLC_2eBool) (cStlc_2eSTLC_2evar___24a1 (cStlc_2eSTLC_2ex)))) (cStlc_2eSTLC_2eabs___24a3 (cStlc_2eSTLC_2ex) (cStlc_2eSTLC_2eBool) (cStlc_2eSTLC_2evar___24a1 (cStlc_2eSTLC_2ex)))). % 0.62/0.89 Proof. % 0.62/0.89 apply NNPP. intro zenon_G. % 0.62/0.89 exact (zenon_G Stlc.STLC.step_example1). % 0.62/0.89 Qed. % 0.62/0.89 % SZS output end Proof % 0.62/0.89 (* END-PROOF *) % 0.62/0.89 nodes searched: 420 % 0.62/0.89 max branch formulas: 3318 % 0.62/0.89 proof nodes created: 1 % 0.62/0.89 formulas created: 75574 % 0.62/0.89 %------------------------------------------------------------------------------