%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR060+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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:17 PM UTC 2025 % Result : Theorem 4.82s 4.98s % Output : Proof 4.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : CSR060+1 : TPTP v9.2.0. Released v3.4.0. % 0.08/0.13 % Command : duper %s % 0.13/0.34 % Computer : n008.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 19:59:38 EDT 2025 % 0.13/0.34 % CPUTime : % 4.82/4.98 SZS status Theorem for theBenchmark.p % 4.82/4.98 SZS output start Proof for theBenchmark.p % 4.82/4.98 Clause #0 (by assumption #[]): Eq (genlmt c_ldscdemonstrationspindleheadmt c_currentworlddatacollectormt_nonhomocentric) True % 4.82/4.98 Clause #3 (by assumption #[]): Eq % 4.82/4.98 (genlmt % 4.82/4.98 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/4.98 c_translation_0_885) % 4.82/4.98 c_machinelearningspindleheadmt) % 4.82/4.98 True % 4.82/4.98 Clause #4 (by assumption #[]): Eq (genlmt c_machinelearningspindleheadmt c_miptdatabase19681997_termsmt) True % 4.82/4.98 Clause #5 (by assumption #[]): Eq % 4.82/4.98 (∀ (TERM INDEPCOL PRED DEPCOL : Iota), % 4.82/4.98 And (isa TERM INDEPCOL) (relationexistsall PRED DEPCOL INDEPCOL) → % 4.82/4.98 isa (f_relationexistsallfn TERM PRED DEPCOL INDEPCOL) DEPCOL) % 4.82/4.98 True % 4.82/4.98 Clause #7 (by assumption #[]): Eq (genlmt c_miptdatabase19681997_termsmt c_ldscgeneralcollectormt) True % 4.82/4.98 Clause #8 (by assumption #[]): Eq (genlmt c_ldscgeneralcollectormt c_ldscdemonstrationspindleheadmt) True % 4.82/4.98 Clause #12 (by assumption #[]): Eq % 4.82/4.98 (∀ (TERM : Iota), % 4.82/4.98 And (mtvisible c_currentworlddatacollectormt_nonhomocentric) % 4.82/4.98 (isa TERM (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) → % 4.82/4.98 tptp_9_51 % 4.82/4.98 (f_relationexistsallfn TERM c_tptp_9_51 c_tptpcol_16_27189 % 4.82/4.98 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/4.98 TERM) % 4.82/4.98 True % 4.82/4.98 Clause #13 (by assumption #[]): Eq % 4.82/4.98 (mtvisible c_currentworlddatacollectormt_nonhomocentric → % 4.82/4.98 relationexistsall c_tptp_9_51 c_tptpcol_16_27189 % 4.82/4.98 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/4.98 True % 4.82/4.98 Clause #14 (by assumption #[]): Eq % 4.82/4.98 (isa c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 % 4.82/4.98 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/4.98 True % 4.82/4.98 Clause #49 (by assumption #[]): Eq (∀ (X : Iota), isa X c_tptpcol_16_27189 → tptpcol_16_27189 X) True % 4.82/4.98 Clause #80 (by assumption #[]): Eq (∀ (SPECMT GENLMT : Iota), And (mtvisible SPECMT) (genlmt SPECMT GENLMT) → mtvisible GENLMT) True % 4.82/4.98 Clause #83 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genlmt X Y) (genlmt Y Z) → genlmt X Z) True % 4.82/4.98 Clause #86 (by assumption #[]): Eq % 4.82/4.98 (Not % 4.82/4.98 (Exists fun X => % 4.82/4.98 mtvisible % 4.82/4.98 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/4.98 c_translation_0_885) → % 4.82/4.98 And (tptp_9_51 X c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 4.82/4.98 (tptpcol_16_27189 X))) % 4.82/4.98 True % 4.82/4.98 Clause #95 (by clausification #[49]): ∀ (a : Iota), Eq (isa a c_tptpcol_16_27189 → tptpcol_16_27189 a) True % 4.82/4.98 Clause #96 (by clausification #[95]): ∀ (a : Iota), Or (Eq (isa a c_tptpcol_16_27189) False) (Eq (tptpcol_16_27189 a) True) % 4.82/4.98 Clause #105 (by clausification #[5]): ∀ (a : Iota), % 4.82/4.98 Eq % 4.82/4.98 (∀ (INDEPCOL PRED DEPCOL : Iota), % 4.82/4.98 And (isa a INDEPCOL) (relationexistsall PRED DEPCOL INDEPCOL) → % 4.82/4.98 isa (f_relationexistsallfn a PRED DEPCOL INDEPCOL) DEPCOL) % 4.82/4.98 True % 4.82/4.98 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 4.82/4.98 Eq % 4.82/4.98 (∀ (PRED DEPCOL : Iota), % 4.82/4.98 And (isa a a_1) (relationexistsall PRED DEPCOL a_1) → isa (f_relationexistsallfn a PRED DEPCOL a_1) DEPCOL) % 4.82/4.98 True % 4.82/4.98 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 4.82/4.98 Eq % 4.82/4.98 (∀ (DEPCOL : Iota), % 4.82/4.98 And (isa a a_1) (relationexistsall a_2 DEPCOL a_1) → isa (f_relationexistsallfn a a_2 DEPCOL a_1) DEPCOL) % 4.82/4.98 True % 4.82/4.98 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 4.82/4.98 Eq (And (isa a a_1) (relationexistsall a_2 a_3 a_1) → isa (f_relationexistsallfn a a_2 a_3 a_1) a_3) True % 4.82/4.98 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : Iota), % 4.82/4.98 Or (Eq (And (isa a a_1) (relationexistsall a_2 a_3 a_1)) False) % 4.82/4.98 (Eq (isa (f_relationexistsallfn a a_2 a_3 a_1) a_3) True) % 4.82/4.98 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 4.82/4.98 Or (Eq (isa (f_relationexistsallfn a a_1 a_2 a_3) a_2) True) % 4.82/4.98 (Or (Eq (isa a a_3) False) (Eq (relationexistsall a_1 a_2 a_3) False)) % 4.82/5.00 Clause #131 (by clausification #[12]): ∀ (a : Iota), % 4.82/5.00 Eq % 4.82/5.00 (And (mtvisible c_currentworlddatacollectormt_nonhomocentric) % 4.82/5.00 (isa a (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) → % 4.82/5.00 tptp_9_51 % 4.82/5.00 (f_relationexistsallfn a c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.00 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.00 a) % 4.82/5.00 True % 4.82/5.00 Clause #132 (by clausification #[131]): ∀ (a : Iota), % 4.82/5.00 Or % 4.82/5.00 (Eq % 4.82/5.00 (And (mtvisible c_currentworlddatacollectormt_nonhomocentric) % 4.82/5.00 (isa a (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma))) % 4.82/5.00 False) % 4.82/5.00 (Eq % 4.82/5.00 (tptp_9_51 % 4.82/5.00 (f_relationexistsallfn a c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.00 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.00 a) % 4.82/5.00 True) % 4.82/5.00 Clause #133 (by clausification #[132]): ∀ (a : Iota), % 4.82/5.00 Or % 4.82/5.00 (Eq % 4.82/5.00 (tptp_9_51 % 4.82/5.00 (f_relationexistsallfn a c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.00 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.00 a) % 4.82/5.00 True) % 4.82/5.00 (Or (Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) False) % 4.82/5.00 (Eq (isa a (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) False)) % 4.82/5.00 Clause #139 (by clausification #[13]): Or (Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) False) % 4.82/5.00 (Eq % 4.82/5.00 (relationexistsall c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.00 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.00 True) % 4.82/5.00 Clause #148 (by clausification #[80]): ∀ (a : Iota), Eq (∀ (GENLMT : Iota), And (mtvisible a) (genlmt a GENLMT) → mtvisible GENLMT) True % 4.82/5.00 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), Eq (And (mtvisible a) (genlmt a a_1) → mtvisible a_1) True % 4.82/5.00 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), Or (Eq (And (mtvisible a) (genlmt a a_1)) False) (Eq (mtvisible a_1) True) % 4.82/5.00 Clause #151 (by clausification #[150]): ∀ (a a_1 : Iota), Or (Eq (mtvisible a) True) (Or (Eq (mtvisible a_1) False) (Eq (genlmt a_1 a) False)) % 4.82/5.00 Clause #155 (by superposition #[14, 110]): ∀ (a a_1 : Iota), % 4.82/5.00 Or % 4.82/5.00 (Eq % 4.82/5.00 (isa % 4.82/5.00 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 a a_1 % 4.82/5.00 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.00 a_1) % 4.82/5.00 True) % 4.82/5.00 (Or % 4.82/5.00 (Eq (relationexistsall a a_1 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.00 False) % 4.82/5.00 (Eq False True)) % 4.82/5.00 Clause #325 (by clausification #[83]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genlmt a Y) (genlmt Y Z) → genlmt a Z) True % 4.82/5.00 Clause #326 (by clausification #[325]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genlmt a a_1) (genlmt a_1 Z) → genlmt a Z) True % 4.82/5.00 Clause #327 (by clausification #[326]): ∀ (a a_1 a_2 : Iota), Eq (And (genlmt a a_1) (genlmt a_1 a_2) → genlmt a a_2) True % 4.82/5.00 Clause #328 (by clausification #[327]): ∀ (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) % 4.82/5.00 Clause #329 (by clausification #[328]): ∀ (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)) % 4.82/5.00 Clause #330 (by superposition #[329, 8]): ∀ (a : Iota), % 4.82/5.00 Or (Eq (genlmt c_ldscgeneralcollectormt a) True) % 4.82/5.00 (Or (Eq (genlmt c_ldscdemonstrationspindleheadmt a) False) (Eq False True)) % 4.82/5.00 Clause #335 (by superposition #[329, 4]): ∀ (a : Iota), % 4.82/5.00 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) % 4.82/5.00 (Or (Eq (genlmt c_miptdatabase19681997_termsmt a) False) (Eq False True)) % 4.82/5.00 Clause #392 (by clausification #[330]): ∀ (a : Iota), Or (Eq (genlmt c_ldscgeneralcollectormt a) True) (Eq (genlmt c_ldscdemonstrationspindleheadmt a) False) % 4.82/5.00 Clause #393 (by superposition #[392, 0]): Or (Eq (genlmt c_ldscgeneralcollectormt c_currentworlddatacollectormt_nonhomocentric) True) (Eq False True) % 4.82/5.00 Clause #395 (by clausification #[393]): Eq (genlmt c_ldscgeneralcollectormt c_currentworlddatacollectormt_nonhomocentric) True % 4.82/5.01 Clause #405 (by clausification #[335]): ∀ (a : Iota), % 4.82/5.01 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) (Eq (genlmt c_miptdatabase19681997_termsmt a) False) % 4.82/5.01 Clause #406 (by superposition #[405, 7]): Or (Eq (genlmt c_machinelearningspindleheadmt c_ldscgeneralcollectormt) True) (Eq False True) % 4.82/5.01 Clause #408 (by clausification #[406]): Eq (genlmt c_machinelearningspindleheadmt c_ldscgeneralcollectormt) True % 4.82/5.01 Clause #409 (by superposition #[408, 329]): ∀ (a : Iota), % 4.82/5.01 Or (Eq (genlmt c_machinelearningspindleheadmt a) True) % 4.82/5.01 (Or (Eq True False) (Eq (genlmt c_ldscgeneralcollectormt a) False)) % 4.82/5.01 Clause #414 (by clausification #[409]): ∀ (a : Iota), Or (Eq (genlmt c_machinelearningspindleheadmt a) True) (Eq (genlmt c_ldscgeneralcollectormt a) False) % 4.82/5.01 Clause #416 (by superposition #[414, 395]): Or (Eq (genlmt c_machinelearningspindleheadmt c_currentworlddatacollectormt_nonhomocentric) True) (Eq False True) % 4.82/5.01 Clause #417 (by clausification #[416]): Eq (genlmt c_machinelearningspindleheadmt c_currentworlddatacollectormt_nonhomocentric) True % 4.82/5.01 Clause #470 (by clausification #[86]): Eq % 4.82/5.01 (Exists fun X => % 4.82/5.01 mtvisible % 4.82/5.01 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/5.01 c_translation_0_885) → % 4.82/5.01 And (tptp_9_51 X c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 4.82/5.01 (tptpcol_16_27189 X)) % 4.82/5.01 False % 4.82/5.01 Clause #471 (by clausification #[470]): ∀ (a : Iota), % 4.82/5.01 Eq % 4.82/5.01 (mtvisible % 4.82/5.01 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/5.01 c_translation_0_885) → % 4.82/5.01 And (tptp_9_51 a c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 4.82/5.01 (tptpcol_16_27189 a)) % 4.82/5.01 False % 4.82/5.01 Clause #472 (by clausification #[471]): Eq % 4.82/5.01 (mtvisible % 4.82/5.01 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/5.01 c_translation_0_885)) % 4.82/5.01 True % 4.82/5.01 Clause #473 (by clausification #[471]): ∀ (a : Iota), % 4.82/5.01 Eq % 4.82/5.01 (And (tptp_9_51 a c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 4.82/5.01 (tptpcol_16_27189 a)) % 4.82/5.01 False % 4.82/5.01 Clause #474 (by superposition #[472, 151]): ∀ (a : Iota), % 4.82/5.01 Or (Eq (mtvisible a) True) % 4.82/5.01 (Or (Eq True False) % 4.82/5.01 (Eq % 4.82/5.01 (genlmt % 4.82/5.01 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/5.01 c_translation_0_885) % 4.82/5.01 a) % 4.82/5.01 False)) % 4.82/5.01 Clause #481 (by clausification #[473]): ∀ (a : Iota), % 4.82/5.01 Or (Eq (tptp_9_51 a c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) False) % 4.82/5.01 (Eq (tptpcol_16_27189 a) False) % 4.82/5.01 Clause #483 (by clausification #[155]): ∀ (a a_1 : Iota), % 4.82/5.01 Or % 4.82/5.01 (Eq % 4.82/5.01 (isa % 4.82/5.01 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 a a_1 % 4.82/5.01 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.01 a_1) % 4.82/5.01 True) % 4.82/5.01 (Eq (relationexistsall a a_1 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.01 False) % 4.82/5.01 Clause #493 (by clausification #[474]): ∀ (a : Iota), % 4.82/5.01 Or (Eq (mtvisible a) True) % 4.82/5.01 (Eq % 4.82/5.01 (genlmt % 4.82/5.01 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)) % 4.82/5.01 c_translation_0_885) % 4.82/5.01 a) % 4.82/5.01 False) % 4.82/5.01 Clause #494 (by superposition #[493, 3]): Or (Eq (mtvisible c_machinelearningspindleheadmt) True) (Eq False True) % 4.82/5.01 Clause #496 (by clausification #[494]): Eq (mtvisible c_machinelearningspindleheadmt) True % 4.82/5.01 Clause #497 (by superposition #[496, 151]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Or (Eq True False) (Eq (genlmt c_machinelearningspindleheadmt a) False)) % 4.82/5.01 Clause #499 (by clausification #[497]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Eq (genlmt c_machinelearningspindleheadmt a) False) % 4.82/5.01 Clause #503 (by superposition #[499, 417]): Or (Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) True) (Eq False True) % 4.82/5.02 Clause #510 (by clausification #[503]): Eq (mtvisible c_currentworlddatacollectormt_nonhomocentric) True % 4.82/5.02 Clause #511 (by backward demodulation #[510, 133]): ∀ (a : Iota), % 4.82/5.02 Or % 4.82/5.02 (Eq % 4.82/5.02 (tptp_9_51 % 4.82/5.02 (f_relationexistsallfn a c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 a) % 4.82/5.02 True) % 4.82/5.02 (Or (Eq True False) % 4.82/5.02 (Eq (isa a (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) False)) % 4.82/5.02 Clause #512 (by backward demodulation #[510, 139]): Or (Eq True False) % 4.82/5.02 (Eq % 4.82/5.02 (relationexistsall c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 True) % 4.82/5.02 Clause #537 (by clausification #[512]): Eq % 4.82/5.02 (relationexistsall c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 True % 4.82/5.02 Clause #538 (by superposition #[537, 483]): Or % 4.82/5.02 (Eq % 4.82/5.02 (isa % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 % 4.82/5.02 c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 c_tptpcol_16_27189) % 4.82/5.02 True) % 4.82/5.02 (Eq True False) % 4.82/5.02 Clause #543 (by clausification #[511]): ∀ (a : Iota), % 4.82/5.02 Or % 4.82/5.02 (Eq % 4.82/5.02 (tptp_9_51 % 4.82/5.02 (f_relationexistsallfn a c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 a) % 4.82/5.02 True) % 4.82/5.02 (Eq (isa a (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) False) % 4.82/5.02 Clause #544 (by superposition #[543, 14]): Or % 4.82/5.02 (Eq % 4.82/5.02 (tptp_9_51 % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 % 4.82/5.02 c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 4.82/5.02 True) % 4.82/5.02 (Eq False True) % 4.82/5.02 Clause #571 (by clausification #[538]): Eq % 4.82/5.02 (isa % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 c_tptp_9_51 % 4.82/5.02 c_tptpcol_16_27189 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 c_tptpcol_16_27189) % 4.82/5.02 True % 4.82/5.02 Clause #572 (by superposition #[571, 96]): Or (Eq True False) % 4.82/5.02 (Eq % 4.82/5.02 (tptpcol_16_27189 % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 % 4.82/5.02 c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma))) % 4.82/5.02 True) % 4.82/5.02 Clause #577 (by clausification #[572]): Eq % 4.82/5.02 (tptpcol_16_27189 % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 c_tptp_9_51 % 4.82/5.02 c_tptpcol_16_27189 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma))) % 4.82/5.02 True % 4.82/5.02 Clause #579 (by clausification #[544]): Eq % 4.82/5.02 (tptp_9_51 % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 c_tptp_9_51 % 4.82/5.02 c_tptpcol_16_27189 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma)) % 4.82/5.02 c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 4.82/5.02 True % 4.82/5.02 Clause #580 (by superposition #[579, 481]): Or (Eq True False) % 4.82/5.02 (Eq % 4.82/5.02 (tptpcol_16_27189 % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 % 4.82/5.02 c_tptp_9_51 c_tptpcol_16_27189 % 4.82/5.02 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma))) % 4.82/5.02 False) % 4.82/5.02 Clause #584 (by clausification #[580]): Eq % 4.82/5.02 (tptpcol_16_27189 % 4.82/5.02 (f_relationexistsallfn c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 c_tptp_9_51 % 4.82/5.02 c_tptpcol_16_27189 (f_subcollectionofwithrelationtofn c_ship c_objectfoundinlocation c_cityofbostonma))) % 4.82/5.02 False % 4.82/5.02 Clause #585 (by superposition #[584, 577]): Eq False True % 4.82/5.02 Clause #586 (by clausification #[585]): False % 4.82/5.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------