%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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:08 PM UTC 2026 % Result : Theorem 19.13s 19.34s % Output : Proof 19.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.16/0.33 % Computer : n028.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 07:53:30 EDT 2026 % 0.16/0.33 % CPUTime : % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__9231 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__9233 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23525 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23529 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__22798 : zenon_U) in $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__421 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__424 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__21852 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__21855 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.48/0.65 Zenon warning: unused variable (Vvar__5___24Anonymous__13556 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.48/0.65 Zenon warning: unused variable (Vvar__5___24Anonymous__13562 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__29187 : zenon_U) in $_discrim_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__9240 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__9241 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__9236 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.48/0.65 Zenon warning: unused variable (Vvar__1___24Anonymous__9237 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23536 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23537 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23552 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23553 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23544 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__23545 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__18067 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.48/0.65 Zenon warning: unused variable (Vvar__3___24Anonymous__18068 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.48/0.65 Zenon warning: unused variable (Vvar__4___24Anonymous__22721 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.48/0.65 Zenon warning: unused variable (Vvar__4___24Anonymous__22722 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.48/0.65 Zenon warning: unused variable (Vvar__5___24Anonymous__22723 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.48/0.65 Zenon warning: unused variable (Vvar__5___24Anonymous__22724 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__22809 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__22810 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__429 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__430 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__435 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.48/0.65 Zenon warning: unused variable (Vvar__2___24Anonymous__436 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.48/0.65 Zenon warning: unused variable (Vvar__1__cond__nonzero__23724 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 0.48/0.65 Zenon warning: unused variable (Vvar__1__cond__nonzero__23725 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 19.13/19.34 Zenon warning: unused variable (Vvar__2___24Anonymous__21870 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 19.13/19.34 Zenon warning: unused variable (Vvar__2___24Anonymous__21871 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 19.13/19.34 Zenon warning: unused variable (Vvar__1___24Anonymous__21858 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 19.13/19.34 Zenon warning: unused variable (Vvar__1___24Anonymous__21859 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 19.13/19.34 Zenon warning: unused variable (Vvar__2___24Anonymous__21864 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 19.13/19.34 Zenon warning: unused variable (Vvar__2___24Anonymous__21865 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__13585 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__13586 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__13597 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__13598 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__13573 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__13574 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__8988 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__8989 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 19.13/19.34 Zenon warning: unused variable (Vvar__6___24Anonymous__8990 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 19.13/19.34 Zenon warning: unused variable (Vvar__6___24Anonymous__8991 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 19.13/19.34 Zenon warning: unused variable (Vvar__4___24Anonymous__29429 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 19.13/19.34 Zenon warning: unused variable (Vvar__4___24Anonymous__29430 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__29431 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 19.13/19.34 Zenon warning: unused variable (Vvar__5___24Anonymous__29432 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 19.13/19.34 Zenon warning: unused variable (Vvar__6___24Anonymous__29433 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 19.13/19.34 Zenon warning: unused variable (Vvar__6___24Anonymous__29434 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 19.13/19.34 Zenon warning: unused variable (Vvar__3___24Anonymous__29194 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 19.13/19.34 Zenon warning: unused variable (Vvar__3___24Anonymous__29195 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 19.13/19.34 Zenon warning: unused variable (Vvar__17___24Anonymous__29230 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 19.13/19.34 Zenon warning: unused variable (Vvar__17___24Anonymous__29231 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 19.13/19.34 (* PROOF-FOUND *) % 19.13/19.34 % SZS status Theorem % 19.13/19.34 (* BEGIN-PROOF *) % 19.13/19.34 % SZS output start Proof % 19.13/19.34 Theorem _HAMMER_GOAL : (forall V0__P : zenon_U, ((cProp___24t V0__P)->(forall V1__Q : zenon_U, ((cProp___24t V1__Q)->((V0__P = V1__Q)->((p V0__P)->(p V1__Q))))))). % 19.13/19.34 Proof. % 19.13/19.34 apply NNPP. intro zenon_G. % 19.13/19.34 apply (zenon_notallex_s (fun V0__P : zenon_U => ((cProp___24t V0__P)->(forall V1__Q : zenon_U, ((cProp___24t V1__Q)->((V0__P = V1__Q)->((p V0__P)->(p V1__Q))))))) zenon_G); [ zenon_intro zenon_H9ba; idtac ]. % 19.13/19.34 elim zenon_H9ba. zenon_intro zenon_TV0__P_drv. zenon_intro zenon_H9bc. % 19.13/19.34 apply (zenon_notimply_s _ _ zenon_H9bc). zenon_intro zenon_H9be. zenon_intro zenon_H9bd. % 19.13/19.34 apply (zenon_notallex_s (fun V1__Q : zenon_U => ((cProp___24t V1__Q)->((zenon_TV0__P_drv = V1__Q)->((p zenon_TV0__P_drv)->(p V1__Q))))) zenon_H9bd); [ zenon_intro zenon_H9bf; idtac ]. % 19.13/19.34 elim zenon_H9bf. zenon_intro zenon_TV1__Q_dsa. zenon_intro zenon_H9c1. % 19.13/19.34 apply (zenon_notimply_s _ _ zenon_H9c1). zenon_intro zenon_H9c3. zenon_intro zenon_H9c2. % 19.13/19.34 apply (zenon_notimply_s _ _ zenon_H9c2). zenon_intro zenon_H9c5. zenon_intro zenon_H9c4. % 19.13/19.36 apply (zenon_notimply_s _ _ zenon_H9c4). zenon_intro zenon_H9c7. zenon_intro zenon_H9c6. % 19.13/19.36 cut ((p zenon_TV0__P_drv) = (p zenon_TV1__Q_dsa)). % 19.13/19.36 intro zenon_D_pnotp. % 19.13/19.36 apply zenon_H9c6. % 19.13/19.36 rewrite <- zenon_D_pnotp. % 19.13/19.36 exact zenon_H9c7. % 19.13/19.36 cut ((zenon_TV0__P_drv = zenon_TV1__Q_dsa)); [idtac | apply NNPP; zenon_intro zenon_H9c8]. % 19.13/19.36 congruence. % 19.13/19.36 exact (zenon_H9c8 zenon_H9c5). % 19.13/19.36 Qed. % 19.13/19.36 % SZS output end Proof % 19.13/19.36 (* END-PROOF *) % 19.13/19.36 nodes searched: 110113 % 19.13/19.36 max branch formulas: 61395 % 19.13/19.36 proof nodes created: 76 % 19.13/19.36 formulas created: 2488684 % 19.13/19.36 %------------------------------------------------------------------------------