%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n010.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 0.85s 1.10s % Output : Proof 0.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.14 % Command : run_zenon %s %d % 0.18/0.36 % Computer : n010.cluster.edu % 0.18/0.36 % Model : x86_64 x86_64 % 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.36 % Memory : 8042.1875MB % 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.36 % CPULimit : 300 % 0.18/0.36 % WCLimit : 300 % 0.18/0.36 % DateTime : Tue May 5 05:25:21 EDT 2026 % 0.18/0.36 % CPUTime : % 0.85/1.10 Zenon warning: unused variable (Vvar__1___24Anonymous__30054 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.85/1.10 Zenon warning: unused variable (Vvar__1___24Anonymous__30056 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2763 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2767 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26875 : zenon_U) in $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26832 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26835 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__202 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__208 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.85/1.10 Zenon warning: unused variable (Vvar__1___24Anonymous__30063 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.85/1.10 Zenon warning: unused variable (Vvar__1___24Anonymous__30064 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.85/1.10 Zenon warning: unused variable (Vvar__1___24Anonymous__30059 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.85/1.10 Zenon warning: unused variable (Vvar__1___24Anonymous__30060 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2774 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2775 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2790 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2791 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2782 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__2783 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__30918 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.85/1.10 Zenon warning: unused variable (Vvar__3___24Anonymous__30919 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26886 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26887 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26840 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26841 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26846 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.85/1.10 Zenon warning: unused variable (Vvar__2___24Anonymous__26847 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__231 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__232 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__243 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__244 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__219 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 0.85/1.10 Zenon warning: unused variable (Vvar__5___24Anonymous__220 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 0.85/1.10 (* PROOF-FOUND *) % 0.85/1.10 % SZS status Theorem % 0.85/1.10 (* BEGIN-PROOF *) % 0.85/1.10 % SZS output start Proof % 0.85/1.10 Theorem _HAMMER_GOAL : (forall V0__K : zenon_U, ((cCoq_2eInit_2eDatatypes_2enat___24t V0__K)->(forall V1__g : zenon_U, ((cColor_2egraph___24t V1__g)->(forall V2__n : zenon_U, ((cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t V2__n)->(((cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1 (cColor_2esubset__nodes___24a2 (cColor_2elow__deg___24a1 V0__K) V1__g)) = (cCoq_2eInit_2eDatatypes_2eSome___24a2 (cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt) V2__n))->(cCoq_2eInit_2ePeano_2elt___24a2 (cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2 (cColor_2enodeset) (cColor_2eremove__node___24a2 V2__n V1__g)) (cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2 (cColor_2enodeset) V1__g))))))))). % 0.85/1.10 Proof. % 0.85/1.10 apply NNPP. intro zenon_G. % 0.85/1.10 exact (zenon_G Color.select_terminates). % 0.85/1.10 Qed. % 0.85/1.10 % SZS output end Proof % 0.85/1.10 (* END-PROOF *) % 0.85/1.10 nodes searched: 305 % 0.85/1.10 max branch formulas: 2979 % 0.85/1.10 proof nodes created: 1 % 0.85/1.10 formulas created: 79444 % 0.85/1.10 %------------------------------------------------------------------------------