%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n016.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:55:51 PM UTC 2026 % Result : Theorem 11.13s 11.31s % Output : Proof 11.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.10 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.30 % Computer : n016.cluster.edu % 0.13/0.30 % Model : x86_64 x86_64 % 0.13/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.30 % Memory : 8042.1875MB % 0.13/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.30 % CPULimit : 300 % 0.13/0.30 % WCLimit : 300 % 0.13/0.30 % DateTime : Tue May 5 08:27:36 EDT 2026 % 0.13/0.31 % CPUTime : % 11.13/11.31 % SZS status Theorem % 11.13/11.31 (* PROOF-FOUND *) % 11.13/11.31 (* BEGIN-PROOF *) % 11.13/11.31 % SZS output start Proof % 11.13/11.31 1. (-. (All V0__ST, ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t V0__ST) => (All V1__t, ((cPLF_2eReferences_2eSTLCRef_2etm___24t V1__t) => (All V2__t_27, ((cPLF_2eReferences_2eSTLCRef_2etm___24t V2__t_27) => (All V3__T, ((cPLF_2eReferences_2eSTLCRef_2ety___24t V3__T) => (All V4__st, ((cPLF_2eReferences_2eSTLCRef_2estore___24t V4__st) => (All V5__st_27, ((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)) => (Ex V9__ST_27, ((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))))))))))))))))))))) (All V0__ST, ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t V0__ST) => (All V1__t, ((cPLF_2eReferences_2eSTLCRef_2etm___24t V1__t) => (All V2__t_27, ((cPLF_2eReferences_2eSTLCRef_2etm___24t V2__t_27) => (All V3__T, ((cPLF_2eReferences_2eSTLCRef_2ety___24t V3__T) => (All V4__st, ((cPLF_2eReferences_2eSTLCRef_2estore___24t V4__st) => (All V5__st_27, ((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)) => (Ex V9__ST_27, ((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)))))))))))))))))))) ### Axiom % 11.13/11.31 % SZS output end Proof % 11.13/11.31 (* END-PROOF *) %------------------------------------------------------------------------------