%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR050+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n011.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:13 PM UTC 2025 % Result : Theorem 5.35s 5.55s % Output : Proof 5.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR050+1 : TPTP v9.2.0. Released v3.4.0. % 0.12/0.14 % Command : duper %s % 0.14/0.35 % Computer : n011.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 20:00:08 EDT 2025 % 0.14/0.35 % CPUTime : % 5.35/5.55 SZS status Theorem for theBenchmark.p % 5.35/5.55 SZS output start Proof for theBenchmark.p % 5.35/5.55 Clause #0 (by assumption #[]): Eq (genlmt c_ldscdemonstrationspindleheadmt c_currentworlddatacollectormt_nonhomocentric) True % 5.35/5.55 Clause #3 (by assumption #[]): Eq % 5.35/5.55 (genlmt % 5.35/5.55 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.55 c_translation_32) % 5.35/5.55 c_machinelearningspindleheadmt) % 5.35/5.55 True % 5.35/5.55 Clause #4 (by assumption #[]): Eq (genlmt c_machinelearningspindleheadmt c_miptdatabase19681997_termsmt) True % 5.35/5.55 Clause #5 (by assumption #[]): Eq (genlmt c_miptdatabase19681997_termsmt c_ldscgeneralcollectormt) True % 5.35/5.55 Clause #6 (by assumption #[]): Eq (genlmt c_ldscgeneralcollectormt c_ldscdemonstrationspindleheadmt) True % 5.35/5.55 Clause #11 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), tptptypes_8_692 ARG1 ARG2 → tptptypes_7_691 ARG2 ARG1) True % 5.35/5.55 Clause #13 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), tptptypes_9_693 ARG1 ARG2 → tptptypes_8_692 ARG1 ARG2) True % 5.35/5.55 Clause #14 (by assumption #[]): Eq % 5.35/5.55 (mtvisible c_currentworlddatacollectormt_nonhomocentric → % 5.35/5.55 tptptypes_9_693 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma) % 5.35/5.55 c_tptpcol_16_26939) % 5.35/5.55 True % 5.35/5.55 Clause #72 (by assumption #[]): Eq (∀ (SPECMT GENLMT : Iota), And (mtvisible SPECMT) (genlmt SPECMT GENLMT) → mtvisible GENLMT) True % 5.35/5.55 Clause #75 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genlmt X Y) (genlmt Y Z) → genlmt X Z) True % 5.35/5.55 Clause #78 (by assumption #[]): Eq % 5.35/5.55 (Not % 5.35/5.55 (mtvisible % 5.35/5.55 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.55 c_translation_32) → % 5.35/5.55 tptptypes_7_691 c_tptpcol_16_26939 % 5.35/5.55 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma))) % 5.35/5.55 True % 5.35/5.55 Clause #84 (by clausification #[11]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), tptptypes_8_692 a ARG2 → tptptypes_7_691 ARG2 a) True % 5.35/5.55 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), Eq (tptptypes_8_692 a a_1 → tptptypes_7_691 a_1 a) True % 5.35/5.55 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (tptptypes_8_692 a a_1) False) (Eq (tptptypes_7_691 a_1 a) True) % 5.35/5.55 Clause #96 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), tptptypes_9_693 a ARG2 → tptptypes_8_692 a ARG2) True % 5.35/5.55 Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota), Eq (tptptypes_9_693 a a_1 → tptptypes_8_692 a a_1) True % 5.35/5.55 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), Or (Eq (tptptypes_9_693 a a_1) False) (Eq (tptptypes_8_692 a a_1) True) % 5.35/5.55 Clause #114 (by clausification #[14]): Or (Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) False) % 5.35/5.55 (Eq % 5.35/5.55 (tptptypes_9_693 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma) % 5.35/5.55 c_tptpcol_16_26939) % 5.35/5.55 True) % 5.35/5.55 Clause #149 (by clausification #[72]): ∀ (a : Iota), Eq (∀ (GENLMT : Iota), And (mtvisible a) (genlmt a GENLMT) → mtvisible GENLMT) True % 5.35/5.55 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), Eq (And (mtvisible a) (genlmt a a_1) → mtvisible a_1) True % 5.35/5.55 Clause #151 (by clausification #[150]): ∀ (a a_1 : Iota), Or (Eq (And (mtvisible a) (genlmt a a_1)) False) (Eq (mtvisible a_1) True) % 5.35/5.55 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), Or (Eq (mtvisible a) True) (Or (Eq (mtvisible a_1) False) (Eq (genlmt a_1 a) False)) % 5.35/5.55 Clause #318 (by clausification #[75]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genlmt a Y) (genlmt Y Z) → genlmt a Z) True % 5.35/5.55 Clause #319 (by clausification #[318]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genlmt a a_1) (genlmt a_1 Z) → genlmt a Z) True % 5.35/5.55 Clause #320 (by clausification #[319]): ∀ (a a_1 a_2 : Iota), Eq (And (genlmt a a_1) (genlmt a_1 a_2) → genlmt a a_2) True % 5.35/5.55 Clause #321 (by clausification #[320]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (genlmt a a_1) (genlmt a_1 a_2)) False) (Eq (genlmt a a_2) True) % 5.35/5.55 Clause #322 (by clausification #[321]): ∀ (a a_1 a_2 : Iota), Or (Eq (genlmt a a_1) True) (Or (Eq (genlmt a a_2) False) (Eq (genlmt a_2 a_1) False)) % 5.35/5.55 Clause #323 (by superposition #[322, 5]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (genlmt c_miptdatabase19681997_termsmt a) True) % 5.35/5.57 (Or (Eq (genlmt c_ldscgeneralcollectormt a) False) (Eq False True)) % 5.35/5.57 Clause #324 (by superposition #[322, 4]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) % 5.35/5.57 (Or (Eq (genlmt c_miptdatabase19681997_termsmt a) False) (Eq False True)) % 5.35/5.57 Clause #329 (by superposition #[322, 3]): ∀ (a : Iota), % 5.35/5.57 Or % 5.35/5.57 (Eq % 5.35/5.57 (genlmt % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) % 5.35/5.57 a) % 5.35/5.57 True) % 5.35/5.57 (Or (Eq (genlmt c_machinelearningspindleheadmt a) False) (Eq False True)) % 5.35/5.57 Clause #351 (by clausification #[78]): Eq % 5.35/5.57 (mtvisible % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) → % 5.35/5.57 tptptypes_7_691 c_tptpcol_16_26939 % 5.35/5.57 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 5.35/5.57 False % 5.35/5.57 Clause #352 (by clausification #[351]): Eq % 5.35/5.57 (mtvisible % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32)) % 5.35/5.57 True % 5.35/5.57 Clause #353 (by clausification #[351]): Eq % 5.35/5.57 (tptptypes_7_691 c_tptpcol_16_26939 % 5.35/5.57 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 5.35/5.57 False % 5.35/5.57 Clause #354 (by superposition #[352, 152]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (mtvisible a) True) % 5.35/5.57 (Or (Eq True False) % 5.35/5.57 (Eq % 5.35/5.57 (genlmt % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) % 5.35/5.57 a) % 5.35/5.57 False)) % 5.35/5.57 Clause #402 (by clausification #[323]): ∀ (a : Iota), Or (Eq (genlmt c_miptdatabase19681997_termsmt a) True) (Eq (genlmt c_ldscgeneralcollectormt a) False) % 5.35/5.57 Clause #403 (by superposition #[402, 6]): Or (Eq (genlmt c_miptdatabase19681997_termsmt c_ldscdemonstrationspindleheadmt) True) (Eq False True) % 5.35/5.57 Clause #406 (by clausification #[403]): Eq (genlmt c_miptdatabase19681997_termsmt c_ldscdemonstrationspindleheadmt) True % 5.35/5.57 Clause #409 (by clausification #[324]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) (Eq (genlmt c_miptdatabase19681997_termsmt a) False) % 5.35/5.57 Clause #412 (by superposition #[409, 406]): Or (Eq (genlmt c_machinelearningspindleheadmt c_ldscdemonstrationspindleheadmt) True) (Eq False True) % 5.35/5.57 Clause #413 (by clausification #[412]): Eq (genlmt c_machinelearningspindleheadmt c_ldscdemonstrationspindleheadmt) True % 5.35/5.57 Clause #414 (by superposition #[413, 322]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) % 5.35/5.57 (Or (Eq True False) (Eq (genlmt c_ldscdemonstrationspindleheadmt a) False)) % 5.35/5.57 Clause #417 (by clausification #[414]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) (Eq (genlmt c_ldscdemonstrationspindleheadmt a) False) % 5.35/5.57 Clause #418 (by superposition #[417, 0]): Or (Eq (genlmt c_machinelearningspindleheadmt c_currentworlddatacollectormt_nonhomocentric) True) (Eq False True) % 5.35/5.57 Clause #419 (by clausification #[418]): Eq (genlmt c_machinelearningspindleheadmt c_currentworlddatacollectormt_nonhomocentric) True % 5.35/5.57 Clause #447 (by clausification #[329]): ∀ (a : Iota), % 5.35/5.57 Or % 5.35/5.57 (Eq % 5.35/5.57 (genlmt % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) % 5.35/5.57 a) % 5.35/5.57 True) % 5.35/5.57 (Eq (genlmt c_machinelearningspindleheadmt a) False) % 5.35/5.57 Clause #453 (by superposition #[447, 419]): Or % 5.35/5.57 (Eq % 5.35/5.57 (genlmt % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) % 5.35/5.57 c_currentworlddatacollectormt_nonhomocentric) % 5.35/5.57 True) % 5.35/5.57 (Eq False True) % 5.35/5.57 Clause #454 (by clausification #[453]): Eq % 5.35/5.57 (genlmt % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) % 5.35/5.57 c_currentworlddatacollectormt_nonhomocentric) % 5.35/5.57 True % 5.35/5.57 Clause #499 (by clausification #[354]): ∀ (a : Iota), % 5.35/5.57 Or (Eq (mtvisible a) True) % 5.35/5.57 (Eq % 5.35/5.57 (genlmt % 5.35/5.57 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_memberstripodcomindygalfordtriviahtm)) % 5.35/5.57 c_translation_32) % 5.35/5.57 a) % 5.35/5.57 False) % 5.35/5.57 Clause #502 (by superposition #[499, 454]): Or (Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) True) (Eq False True) % 5.35/5.57 Clause #519 (by clausification #[502]): Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) True % 5.35/5.57 Clause #520 (by backward demodulation #[519, 114]): Or (Eq True False) % 5.35/5.57 (Eq % 5.35/5.57 (tptptypes_9_693 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma) % 5.35/5.57 c_tptpcol_16_26939) % 5.35/5.57 True) % 5.35/5.57 Clause #528 (by clausification #[520]): Eq % 5.35/5.57 (tptptypes_9_693 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma) % 5.35/5.57 c_tptpcol_16_26939) % 5.35/5.57 True % 5.35/5.57 Clause #529 (by superposition #[528, 98]): Or (Eq True False) % 5.35/5.57 (Eq % 5.35/5.57 (tptptypes_8_692 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma) % 5.35/5.57 c_tptpcol_16_26939) % 5.35/5.57 True) % 5.35/5.57 Clause #534 (by clausification #[529]): Eq % 5.35/5.57 (tptptypes_8_692 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma) % 5.35/5.57 c_tptpcol_16_26939) % 5.35/5.57 True % 5.35/5.57 Clause #535 (by superposition #[534, 86]): Or (Eq True False) % 5.35/5.57 (Eq % 5.35/5.57 (tptptypes_7_691 c_tptpcol_16_26939 % 5.35/5.57 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 5.35/5.57 True) % 5.35/5.57 Clause #537 (by clausification #[535]): Eq % 5.35/5.57 (tptptypes_7_691 c_tptpcol_16_26939 % 5.35/5.57 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 5.35/5.57 True % 5.35/5.57 Clause #538 (by superposition #[537, 353]): Eq True False % 5.35/5.57 Clause #539 (by clausification #[538]): False % 5.35/5.57 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------