%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR057+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %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 : Fri Oct 3 07:46:16 PM UTC 2025 % Result : Theorem 4.54s 4.74s % Output : Proof 4.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : CSR057+1 : TPTP v9.2.0. Released v3.4.0. % 0.08/0.14 % Command : duper %s % 0.13/0.36 % Computer : n020.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Thu Oct 2 20:15:38 EDT 2025 % 0.13/0.36 % CPUTime : % 4.54/4.74 SZS status Theorem for theBenchmark.p % 4.54/4.74 SZS output start Proof for theBenchmark.p % 4.54/4.74 Clause #5 (by assumption #[]): Eq (genlmt c_tptpgeo_spindleheadmt c_worldgeographymt) True % 4.54/4.74 Clause #6 (by assumption #[]): Eq (genlmt c_tptpgeo_member8_mt c_tptpgeo_spindleheadmt) True % 4.54/4.74 Clause #9 (by assumption #[]): Eq (mtvisible c_worldgeographymt → geolevel_4 c_georegion_l4_x75_y75) True % 4.54/4.74 Clause #11 (by assumption #[]): Eq (∀ (OBJ : Iota), geolevel_4 OBJ → geographicalregion OBJ) True % 4.54/4.74 Clause #13 (by assumption #[]): Eq (∀ (OBJ : Iota), enduringthing_localized OBJ → spatialthing_nonsituational OBJ) True % 4.54/4.74 Clause #15 (by assumption #[]): Eq (∀ (OBJ : Iota), partiallytangible OBJ → enduringthing_localized OBJ) True % 4.54/4.74 Clause #17 (by assumption #[]): Eq (∀ (OBJ : Iota), geographicalregion OBJ → partiallytangible OBJ) True % 4.54/4.74 Clause #51 (by assumption #[]): Eq (∀ (X : Iota), spatialthing_nonsituational X → inregion X X) True % 4.54/4.74 Clause #58 (by assumption #[]): Eq (∀ (SPECMT GENLMT : Iota), And (mtvisible SPECMT) (genlmt SPECMT GENLMT) → mtvisible GENLMT) True % 4.54/4.74 Clause #64 (by assumption #[]): Eq (Not (Exists fun X => mtvisible c_tptpgeo_member8_mt → inregion X c_georegion_l4_x75_y75)) True % 4.54/4.74 Clause #70 (by clausification #[9]): Or (Eq (mtvisible c_worldgeographymt) False) (Eq (geolevel_4 c_georegion_l4_x75_y75) True) % 4.54/4.74 Clause #71 (by clausification #[17]): ∀ (a : Iota), Eq (geographicalregion a → partiallytangible a) True % 4.54/4.74 Clause #72 (by clausification #[71]): ∀ (a : Iota), Or (Eq (geographicalregion a) False) (Eq (partiallytangible a) True) % 4.54/4.74 Clause #87 (by clausification #[13]): ∀ (a : Iota), Eq (enduringthing_localized a → spatialthing_nonsituational a) True % 4.54/4.74 Clause #88 (by clausification #[87]): ∀ (a : Iota), Or (Eq (enduringthing_localized a) False) (Eq (spatialthing_nonsituational a) True) % 4.54/4.74 Clause #89 (by clausification #[15]): ∀ (a : Iota), Eq (partiallytangible a → enduringthing_localized a) True % 4.54/4.74 Clause #90 (by clausification #[89]): ∀ (a : Iota), Or (Eq (partiallytangible a) False) (Eq (enduringthing_localized a) True) % 4.54/4.74 Clause #91 (by clausification #[11]): ∀ (a : Iota), Eq (geolevel_4 a → geographicalregion a) True % 4.54/4.74 Clause #92 (by clausification #[91]): ∀ (a : Iota), Or (Eq (geolevel_4 a) False) (Eq (geographicalregion a) True) % 4.54/4.74 Clause #99 (by clausification #[51]): ∀ (a : Iota), Eq (spatialthing_nonsituational a → inregion a a) True % 4.54/4.74 Clause #100 (by clausification #[99]): ∀ (a : Iota), Or (Eq (spatialthing_nonsituational a) False) (Eq (inregion a a) True) % 4.54/4.74 Clause #245 (by clausification #[58]): ∀ (a : Iota), Eq (∀ (GENLMT : Iota), And (mtvisible a) (genlmt a GENLMT) → mtvisible GENLMT) True % 4.54/4.74 Clause #246 (by clausification #[245]): ∀ (a a_1 : Iota), Eq (And (mtvisible a) (genlmt a a_1) → mtvisible a_1) True % 4.54/4.74 Clause #247 (by clausification #[246]): ∀ (a a_1 : Iota), Or (Eq (And (mtvisible a) (genlmt a a_1)) False) (Eq (mtvisible a_1) True) % 4.54/4.74 Clause #248 (by clausification #[247]): ∀ (a a_1 : Iota), Or (Eq (mtvisible a) True) (Or (Eq (mtvisible a_1) False) (Eq (genlmt a_1 a) False)) % 4.54/4.74 Clause #325 (by clausification #[64]): Eq (Exists fun X => mtvisible c_tptpgeo_member8_mt → inregion X c_georegion_l4_x75_y75) False % 4.54/4.74 Clause #326 (by clausification #[325]): ∀ (a : Iota), Eq (mtvisible c_tptpgeo_member8_mt → inregion a c_georegion_l4_x75_y75) False % 4.54/4.74 Clause #327 (by clausification #[326]): Eq (mtvisible c_tptpgeo_member8_mt) True % 4.54/4.74 Clause #328 (by clausification #[326]): ∀ (a : Iota), Eq (inregion a c_georegion_l4_x75_y75) False % 4.54/4.74 Clause #329 (by superposition #[327, 248]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Or (Eq True False) (Eq (genlmt c_tptpgeo_member8_mt a) False)) % 4.54/4.74 Clause #330 (by clausification #[329]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Eq (genlmt c_tptpgeo_member8_mt a) False) % 4.54/4.74 Clause #331 (by superposition #[330, 6]): Or (Eq (mtvisible c_tptpgeo_spindleheadmt) True) (Eq False True) % 4.54/4.74 Clause #333 (by clausification #[331]): Eq (mtvisible c_tptpgeo_spindleheadmt) True % 4.54/4.74 Clause #334 (by superposition #[333, 248]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Or (Eq True False) (Eq (genlmt c_tptpgeo_spindleheadmt a) False)) % 4.54/4.75 Clause #335 (by clausification #[334]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Eq (genlmt c_tptpgeo_spindleheadmt a) False) % 4.54/4.75 Clause #336 (by superposition #[335, 5]): Or (Eq (mtvisible c_worldgeographymt) True) (Eq False True) % 4.54/4.75 Clause #340 (by clausification #[336]): Eq (mtvisible c_worldgeographymt) True % 4.54/4.75 Clause #341 (by backward demodulation #[340, 70]): Or (Eq True False) (Eq (geolevel_4 c_georegion_l4_x75_y75) True) % 4.54/4.75 Clause #343 (by clausification #[341]): Eq (geolevel_4 c_georegion_l4_x75_y75) True % 4.54/4.75 Clause #344 (by superposition #[343, 92]): Or (Eq True False) (Eq (geographicalregion c_georegion_l4_x75_y75) True) % 4.54/4.75 Clause #346 (by clausification #[344]): Eq (geographicalregion c_georegion_l4_x75_y75) True % 4.54/4.75 Clause #347 (by superposition #[346, 72]): Or (Eq True False) (Eq (partiallytangible c_georegion_l4_x75_y75) True) % 4.54/4.75 Clause #349 (by clausification #[347]): Eq (partiallytangible c_georegion_l4_x75_y75) True % 4.54/4.75 Clause #350 (by superposition #[349, 90]): Or (Eq True False) (Eq (enduringthing_localized c_georegion_l4_x75_y75) True) % 4.54/4.75 Clause #352 (by clausification #[350]): Eq (enduringthing_localized c_georegion_l4_x75_y75) True % 4.54/4.75 Clause #353 (by superposition #[352, 88]): Or (Eq True False) (Eq (spatialthing_nonsituational c_georegion_l4_x75_y75) True) % 4.54/4.75 Clause #357 (by clausification #[353]): Eq (spatialthing_nonsituational c_georegion_l4_x75_y75) True % 4.54/4.75 Clause #358 (by superposition #[357, 100]): Or (Eq True False) (Eq (inregion c_georegion_l4_x75_y75 c_georegion_l4_x75_y75) True) % 4.54/4.75 Clause #364 (by clausification #[358]): Eq (inregion c_georegion_l4_x75_y75 c_georegion_l4_x75_y75) True % 4.54/4.75 Clause #365 (by superposition #[364, 328]): Eq True False % 4.54/4.75 Clause #367 (by clausification #[365]): False % 4.54/4.75 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------