%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEV608+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 : n020.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:47 PM UTC 2026 % Result : Theorem 8.57s 8.88s % Output : Proof 8.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.16/0.34 % Computer : n020.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 05:26:04 EDT 2026 % 0.16/0.34 % CPUTime : % 8.57/8.88 % SZS status Theorem % 8.57/8.88 (* PROOF-FOUND *) % 8.57/8.88 (* BEGIN-PROOF *) % 8.57/8.88 % SZS output start Proof % 8.57/8.88 1. (-. (All V0__K, ((cCoq_2eInit_2eDatatypes_2enat___24t V0__K) => (All V1__g, ((cColor_2egraph___24t V1__g) => (All V2__n, ((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)))))))))) (All V0__K, ((cCoq_2eInit_2eDatatypes_2enat___24t V0__K) => (All V1__g, ((cColor_2egraph___24t V1__g) => (All V2__n, ((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))))))))) ### Axiom % 8.57/8.88 % SZS output end Proof % 8.57/8.88 (* END-PROOF *) %------------------------------------------------------------------------------