↑ Up

nanoCoP---2.0.THM-Prf.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : nanoCoP---2.0
% Problem  : CSR068+2 : TPTP v8.1.2. Released v3.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : nanocop.sh %s %d

% Computer : n025.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 May 19 10:58:47 EDT 2023

% Result   : Theorem 0.42s 1.38s
% Output   : Proof 0.42s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : CSR068+2 : TPTP v8.1.2. Released v3.4.0.
% 0.06/0.12  % Command  : nanocop.sh %s %d
% 0.12/0.33  % Computer : n025.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Fri May 19 00:06:18 EDT 2023
% 0.12/0.34  % CPUTime  : 
% 0.42/1.38  
% 0.42/1.38  /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.42/1.38  Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/1.38  %-----------------------------------------------------
% 0.42/1.38  ncf(matrix, plain, [(5596 ^ _599268) ^ [] : [-(mtvisible(c_tptp_member2356_mt))], (5598 ^ _599268) ^ [] : [tptpofobject(c_theprototypicalfurpelt, f_tptpquantityfn_1(n_328))], (2 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))], (4 ^ _599268) ^ [] : [-(disjointwith(c_intangible, c_partiallytangible))], (6 ^ _599268) ^ [_599473] : [intangible(_599473), partiallytangible(_599473)], (12 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_40430, c_tptpcol_14_40429))], (14 ^ _599268) ^ [_599711] : [tptpcol_15_40430(_599711), -(tptpcol_14_40429(_599711))], (20 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_72710, c_tptpcol_9_72709))], (22 ^ _599268) ^ [_599950] : [tptpcol_10_72710(_599950), -(tptpcol_9_72709(_599950))], (28 ^ _599268) ^ [] : [-(genls(c_inanimateobject, c_partiallytangible))], (30 ^ _599268) ^ [_600189] : [inanimateobject(_600189), -(partiallytangible(_600189))], (36 ^ _599268) ^ [] : [-(microtheory(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)), c_translation_3)))], (38 ^ _599268) ^ [_600456, _600458, _600460] : [-(genlpreds(_600460, _600456)), genlinverse(_600460, _600458), genlinverse(_600458, _600456)], (48 ^ _599268) ^ [] : [-(genlpreds(c_subsetof, c_most))], (50 ^ _599268) ^ [_600818, _600820] : [subsetof(_600820, _600818), -(most(_600820, _600818))], (56 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_93186, c_tptpcol_6_92162))], (58 ^ _599268) ^ [_601067] : [tptpcol_7_93186(_601067), -(tptpcol_6_92162(_601067))], (64 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_40421, c_tptpcol_12_40420))], (66 ^ _599268) ^ [_601306] : [tptpcol_13_40421(_601306), -(tptpcol_12_40420(_601306))], (72 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member2_mt), -(geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l2_x8_y2))], (78 ^ _599268) ^ [] : [-(transitivebinarypredicate(c_genls))], (80 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member2610_mt))], (82 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_22021, c_tptpcol_8_22020))], (84 ^ _599268) ^ [_601770] : [tptpcol_9_22021(_601770), -(tptpcol_8_22020(_601770))], (90 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_16388, c_tptpcol_4_16387))], (92 ^ _599268) ^ [_602009] : [tptpcol_5_16388(_602009), -(tptpcol_4_16387(_602009))], (98 ^ _599268) ^ [] : [mtvisible(c_cyclistsmt), -(ridgeline_topographical(c_tptpridgeline_topographical))], (104 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_72792, c_tptpcol_13_72791))], (106 ^ _599268) ^ [_602367] : [tptpcol_14_72792(_602367), -(tptpcol_13_72791(_602367))], (112 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_20483, c_tptpcol_4_16387))], (114 ^ _599268) ^ [_602606] : [tptpcol_5_20483(_602606), -(tptpcol_4_16387(_602606))], (120 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_22023, c_tptpcol_10_22022))], (122 ^ _599268) ^ [_602845] : [tptpcol_11_22023(_602845), -(tptpcol_10_22022(_602845))], (128 ^ _599268) ^ [] : [-(genls(c_partiallyintangibleindividual, c_individual))], (130 ^ _599268) ^ [_603084] : [partiallyintangibleindividual(_603084), -(individual(_603084))], (136 ^ _599268) ^ [] : [-(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))], (138 ^ _599268) ^ [] : [-(genlmt(c_peopledatamt, c_unitedstatessociallifemt))], (140 ^ _599268) ^ [] : [-(genls(c_trajector_underspecified, c_location_underspecified))], (142 ^ _599268) ^ [_603429] : [trajector_underspecified(_603429), -(location_underspecified(_603429))], (148 ^ _599268) ^ [] : [-(genls(c_partiallytangible, c_enduringthing_localized))], (150 ^ _599268) ^ [_603668] : [partiallytangible(_603668), -(enduringthing_localized(_603668))], (156 ^ _599268) ^ [] : [mtvisible(c_cyclistsmt), -(artsupplies(c_tptpartsupplies))], (162 ^ _599268) ^ [] : [-(genls(c_tptpcol_3_81921, c_tptpcol_2_65537))], (164 ^ _599268) ^ [_604026] : [tptpcol_3_81921(_604026), -(tptpcol_2_65537(_604026))], (170 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_18567, c_tptpcol_9_18439))], (172 ^ _599268) ^ [_604265] : [tptpcol_10_18567(_604265), -(tptpcol_9_18439(_604265))], (178 ^ _599268) ^ [] : [-(genls(c_orderingpredicate, c_transitivebinarypredicate))], (180 ^ _599268) ^ [_604504] : [orderingpredicate(_604504), -(transitivebinarypredicate(_604504))], (186 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_92230, c_tptpcol_10_92166))], (188 ^ _599268) ^ [_604743] : [tptpcol_11_92230(_604743), -(tptpcol_10_92166(_604743))], (194 ^ _599268) ^ [] : [-(genls(c_tptpcol_2_98304, c_tptpcol_1_65536))], (196 ^ _599268) ^ [_604982] : [tptpcol_2_98304(_604982), -(tptpcol_1_65536(_604982))], (202 ^ _599268) ^ [] : [mtvisible(c_tptp_member3356_mt), -(marriagelicensedocument(c_tptpmarriagelicensedocument))], (208 ^ _599268) ^ [] : [-(genlmt(c_miptdatabase19681997_termsmt, c_ldscgeneralcollectormt))], (210 ^ _599268) ^ [] : [-(genlmt(c_ethnicgroupsmt, c_ethnicgroupsvocabularymt))], (212 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_40420, c_tptpcol_11_40388))], (214 ^ _599268) ^ [_605446] : [tptpcol_12_40420(_605446), -(tptpcol_11_40388(_605446))], (220 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_9_693, c_tptptypes_8_692))], (222 ^ _599268) ^ [_605699, _605701] : [tptptypes_9_693(_605701, _605699), -(tptptypes_8_692(_605701, _605699))], (228 ^ _599268) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_miptdatabase19681997_termsmt))], (230 ^ _599268) ^ [] : [-(genlmt(c_ldscdemonstrationspindleheadmt, c_currentworlddatacollectormt_nonhomocentric))], (232 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_8_390, c_tptptypes_7_389))], (234 ^ _599268) ^ [_606068, _606070] : [tptptypes_8_390(_606070, _606068), -(tptptypes_7_389(_606070, _606068))], (240 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)), c_translation_33), c_machinelearningspindleheadmt))], (242 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_member7_mt, c_tptpgeo_spindleheadmt))], (244 ^ _599268) ^ [_606412, _606414, _606416, _606418] : [-(isa(f_relationexistsallfn(_606418, _606414, _606412, _606416), _606412)), isa(_606418, _606416), relationexistsall(_606414, _606412, _606416)], (254 ^ _599268) ^ [] : [-(resultisaarg(c_relationexistsallfn, n_3))], (256 ^ _599268) ^ [] : [-(genlmt(c_nooescapearchitecturemt, c_organizationdatamt))], (258 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwfuntriviacomplayquizcfmqid60926origin)), c_translation_0_885), c_machinelearningspindleheadmt))], (260 ^ _599268) ^ [] : [-(genls(c_tptpcol_4_106497, c_tptpcol_3_98305))], (262 ^ _599268) ^ [_606941] : [tptpcol_4_106497(_606941), -(tptpcol_3_98305(_606941))], (268 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_114690, c_tptpcol_4_114689))], (270 ^ _599268) ^ [_607180] : [tptpcol_5_114690(_607180), -(tptpcol_4_114689(_607180))], (276 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_93765, c_tptpcol_11_93764))], (278 ^ _599268) ^ [_607419] : [tptpcol_12_93765(_607419), -(tptpcol_11_93764(_607419))], (284 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_72708, c_tptpcol_7_72707))], (286 ^ _599268) ^ [_607658] : [tptpcol_8_72708(_607658), -(tptpcol_7_72707(_607658))], (292 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_40324, c_tptpcol_9_40196))], (294 ^ _599268) ^ [_607897] : [tptpcol_10_40324(_607897), -(tptpcol_9_40196(_607897))], (300 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_93766, c_tptpcol_12_93765))], (302 ^ _599268) ^ [_608136] : [tptpcol_13_93766(_608136), -(tptpcol_12_93765(_608136))], (308 ^ _599268) ^ [_608322] : [-(tptpofobject(_608322, f_tptpquantityfn_1(n_328))), mtvisible(c_tptp_spindleheadmt), furpelt(_608322)], (318 ^ _599268) ^ [] : [mtvisible(c_tptp_spindleheadmt), -(relationallinstance(c_tptpofobject, c_furpelt, f_tptpquantityfn_1(n_328)))], (324 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member7_mt), -(inregion(c_geolocation_x53_y74, c_georegion_l4_x53_y74))], (330 ^ _599268) ^ [] : [-(applicationcontext(c_wamt_evalinitial_p14))], (332 ^ _599268) ^ [] : [-(computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))], (334 ^ _599268) ^ [] : [-(genls(c_location_underspecified, c_thing))], (336 ^ _599268) ^ [_608986] : [location_underspecified(_608986), -(thing(_608986))], (342 ^ _599268) ^ [] : [-(genlmt(c_ldscgeneralcollectormt, c_ldscdemonstrationspindleheadmt))], (344 ^ _599268) ^ [] : [-(genlmt(c_patterndetectormt, c_basekb))], (346 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_92262, c_tptpcol_11_92230))], (348 ^ _599268) ^ [_609331] : [tptpcol_12_92262(_609331), -(tptpcol_11_92230(_609331))], (354 ^ _599268) ^ [] : [mtvisible(c_tptp_member1672_mt), -(navypersonnel(c_tptpnavypersonnel_3))], (360 ^ _599268) ^ [] : [-(genlmt(c_universalvocabularymt, c_corecyclmt))], (362 ^ _599268) ^ [] : [-(genlmt(c_tptp_member2831_mt, c_tptp_spindleheadmt))], (364 ^ _599268) ^ [] : [-(executionbyfiringsquad(c_tptpexecutionbyfiringsquad_90))], (366 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_109061, c_tptpcol_9_109060))], (368 ^ _599268) ^ [_609848] : [tptpcol_10_109061(_609848), -(tptpcol_9_109060(_609848))], (374 ^ _599268) ^ [] : [-(shavingrazor_manual(c_theprototypicalshavingrazor_manual))], (376 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_6_388, c_tptptypes_5_387))], (378 ^ _599268) ^ [_610154, _610156] : [tptptypes_6_388(_610156, _610154), -(tptptypes_5_387(_610156, _610154))], (384 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_116738, c_tptpcol_5_114690))], (386 ^ _599268) ^ [_610403] : [tptpcol_6_116738(_610403), -(tptpcol_5_114690(_610403))], (392 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_92268, c_tptpcol_14_92264))], (394 ^ _599268) ^ [_610642] : [tptpcol_15_92268(_610642), -(tptpcol_14_92264(_610642))], (400 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member5_mt), -(borderson(c_georegion_l4_x56_y47, c_georegion_l4_x57_y47))], (406 ^ _599268) ^ [_610947] : [-(tptpofobject(_610947, f_tptpquantityfn_13(n_468))), mtvisible(c_tptp_member235_mt), ridgeline_topographical(_610947)], (416 ^ _599268) ^ [] : [mtvisible(c_tptp_member235_mt), -(relationallinstance(c_tptpofobject, c_ridgeline_topographical, f_tptpquantityfn_13(n_468)))], (422 ^ _599268) ^ [] : [-(genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))], (424 ^ _599268) ^ [_611400, _611402] : [tptptypes_9_401(_611402, _611400), -(tptptypes_8_400(_611400, _611402))], (430 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_18663, c_tptpcol_11_18631))], (432 ^ _599268) ^ [_611649] : [tptpcol_12_18663(_611649), -(tptpcol_11_18631(_611649))], (438 ^ _599268) ^ [] : [-(genls(c_setorcollection, c_mathematicalthing))], (440 ^ _599268) ^ [_611888] : [setorcollection(_611888), -(mathematicalthing(_611888))], (446 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_109173, c_tptpcol_12_109157))], (448 ^ _599268) ^ [_612127] : [tptpcol_13_109173(_612127), -(tptpcol_12_109157(_612127))], (454 ^ _599268) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (456 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_106498, c_tptpcol_4_106497))], (458 ^ _599268) ^ [_612419] : [tptpcol_5_106498(_612419), -(tptpcol_4_106497(_612419))], (464 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_24579, c_tptpcol_4_24578))], (466 ^ _599268) ^ [_612658] : [tptpcol_5_24579(_612658), -(tptpcol_4_24578(_612658))], (472 ^ _599268) ^ [] : [-(transitivebinarypredicate(c_genlpreds))], (474 ^ _599268) ^ [] : [mtvisible(c_worldgeographymt), -(geolevel_3(c_georegion_l3_x4_y13))], (480 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member7_mt), -(borderson(c_georegion_l4_x27_y64, c_georegion_l4_x27_y65))], (486 ^ _599268) ^ [] : [-(genls(c_tptpcol_1_65536, c_tptpcol_0_0))], (488 ^ _599268) ^ [_613188] : [tptpcol_1_65536(_613188), -(tptpcol_0_0(_613188))], (494 ^ _599268) ^ [] : [-(genlmt(c_cyclistsmt, c_hpkbvocabmt))], (496 ^ _599268) ^ [] : [mtvisible(c_englishmt), -(prettystring(f_subcollectionofwithrelationfromtypefn(c_terrorist, c_hasmembers, c_terroristgroup), s_terroristthathasbeenamemberofaterroristorganization))], (502 ^ _599268) ^ [] : [-(genlinverse(c_geographicalsubregions, c_inregion))], (504 ^ _599268) ^ [_613613, _613615] : [geographicalsubregions(_613615, _613613), -(inregion(_613613, _613615))], (510 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_118084, c_tptpcol_10_118020))], (512 ^ _599268) ^ [_613862] : [tptpcol_11_118084(_613862), -(tptpcol_10_118020(_613862))], (518 ^ _599268) ^ [] : [-(genls(c_mathematicalorcomputationalthing, c_intangible))], (520 ^ _599268) ^ [_614101] : [mathematicalorcomputationalthing(_614101), -(intangible(_614101))], (526 ^ _599268) ^ [] : [-(genlmt(c_tptp_member3393_mt, c_tptp_spindleheadmt))], (528 ^ _599268) ^ [] : [-(isa(c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804, f_subcollectionofwithrelationtotypefn(c_issuingaprescription, c_products, c_correctivelensprescription)))], (530 ^ _599268) ^ [] : [-(subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804))], (532 ^ _599268) ^ [] : [-(genlmt(c_generictemporalmt, c_basekb))], (534 ^ _599268) ^ [] : [-(genlmt(c_worldgeographydualistmt, c_worldgeographymt))], (536 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_7_819, c_tptptypes_6_818))], (538 ^ _599268) ^ [_614619, _614621] : [tptptypes_7_819(_614621, _614619), -(tptptypes_6_818(_614621, _614619))], (544 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member1_mt))], (546 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_26919, c_tptpcol_11_26887))], (548 ^ _599268) ^ [_614921] : [tptpcol_12_26919(_614921), -(tptpcol_11_26887(_614921))], (554 ^ _599268) ^ [] : [-(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))], (556 ^ _599268) ^ [_615174, _615176] : [tptptypes_8_692(_615176, _615174), -(tptptypes_7_691(_615174, _615176))], (562 ^ _599268) ^ [] : [-(genls(c_tptpcol_2_2, c_tptpcol_1_1))], (564 ^ _599268) ^ [_615423] : [tptpcol_2_2(_615423), -(tptpcol_1_1(_615423))], (570 ^ _599268) ^ [] : [-(genlmt(c_tptp_member3515_mt, c_tptp_spindleheadmt))], (572 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_92165, c_tptpcol_8_92164))], (574 ^ _599268) ^ [_615715] : [tptpcol_9_92165(_615715), -(tptpcol_8_92164(_615715))], (580 ^ _599268) ^ [] : [-(genls(c_fixedordercollection, c_collection))], (582 ^ _599268) ^ [_615954] : [fixedordercollection(_615954), -(collection(_615954))], (588 ^ _599268) ^ [] : [-(disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536))], (590 ^ _599268) ^ [_616193] : [tptpcol_1_1(_616193), tptpcol_1_65536(_616193)], (596 ^ _599268) ^ [] : [-(genlmt(c_geographymt, c_basekb))], (598 ^ _599268) ^ [] : [-(genls(c_microtheory, c_aspatialinformationstore))], (600 ^ _599268) ^ [_616484] : [microtheory(_616484), -(aspatialinformationstore(_616484))], (606 ^ _599268) ^ [] : [mtvisible(c_tptp_member237_mt), -(tptptypes_9_401(c_pushingababycarriage, c_tptpcol_16_10258))], (612 ^ _599268) ^ [_616789] : [-(tptp_8_875(_616789, f_relationallexistsfn(_616789, c_tptp_8_875, f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval, c_directionoftranslation_throughout, c_movement_translationevent), c_tptpcol_16_31868))), mtvisible(c_tptp_member2610_mt), isa(_616789, f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval, c_directionoftranslation_throughout, c_movement_translationevent))], (622 ^ _599268) ^ [] : [mtvisible(c_tptp_member2610_mt), -(relationallexists(c_tptp_8_875, f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval, c_directionoftranslation_throughout, c_movement_translationevent), c_tptpcol_16_31868))], (628 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_118020, c_tptpcol_9_118019))], (630 ^ _599268) ^ [_617240] : [tptpcol_10_118020(_617240), -(tptpcol_9_118019(_617240))], (636 ^ _599268) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (638 ^ _599268) ^ [] : [mtvisible(c_cyclistsmt), -(runningshorts(c_tptprunningshorts))], (644 ^ _599268) ^ [_617598] : [-(tptp_9_720(_617598, f_relationallexistsfn(_617598, c_tptp_9_720, c_executionbyfiringsquad, c_tptpcol_16_29490))), mtvisible(c_cyclistsmt), executionbyfiringsquad(_617598)], (654 ^ _599268) ^ [] : [mtvisible(c_cyclistsmt), -(relationallexists(c_tptp_9_720, c_executionbyfiringsquad, c_tptpcol_16_29490))], (660 ^ _599268) ^ [] : [-(disjointwith(c_individual, c_setorcollection))], (662 ^ _599268) ^ [_618047] : [individual(_618047), setorcollection(_618047)], (668 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_22055, c_tptpcol_11_22023))], (670 ^ _599268) ^ [_618285] : [tptpcol_12_22055(_618285), -(tptpcol_11_22023(_618285))], (676 ^ _599268) ^ [] : [-(genls(c_applicationcontext, c_microtheory))], (678 ^ _599268) ^ [_618524] : [applicationcontext(_618524), -(microtheory(_618524))], (684 ^ _599268) ^ [] : [-(genlmt(c_tptp_member2089_mt, c_tptp_spindleheadmt))], (686 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_8_400, c_tptptypes_7_396))], (688 ^ _599268) ^ [_618830, _618832] : [tptptypes_8_400(_618832, _618830), -(tptptypes_7_396(_618832, _618830))], (694 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_18631, c_tptpcol_10_18567))], (696 ^ _599268) ^ [_619079] : [tptpcol_11_18631(_619079), -(tptpcol_10_18567(_619079))], (702 ^ _599268) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt))], (704 ^ _599268) ^ [] : [mtvisible(c_tptp_member2668_mt), -(tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector, c_orientation, c_partiallytangible), c_tptpcol_16_8886))], (710 ^ _599268) ^ [] : [-(genls(c_mathematicalthing, c_mathematicalorcomputationalthing))], (712 ^ _599268) ^ [_619490] : [mathematicalthing(_619490), -(mathematicalorcomputationalthing(_619490))], (718 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)), c_translation_14), c_machinelearningspindleheadmt))], (720 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_93775, c_tptpcol_14_93774))], (722 ^ _599268) ^ [_619782] : [tptpcol_15_93775(_619782), -(tptpcol_14_93774(_619782))], (728 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_109059, c_tptpcol_7_108547))], (730 ^ _599268) ^ [_620021] : [tptpcol_8_109059(_620021), -(tptpcol_7_108547(_620021))], (736 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_40429, c_tptpcol_13_40421))], (738 ^ _599268) ^ [_620260] : [tptpcol_14_40429(_620260), -(tptpcol_13_40421(_620260))], (744 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member7_mt), -(geographicalsubregions(c_georegion_l3_x15_y24, c_georegion_l4_x45_y72))], (750 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_22072, c_tptpcol_13_22071))], (752 ^ _599268) ^ [_620618] : [tptpcol_14_22072(_620618), -(tptpcol_13_22071(_620618))], (758 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_93774, c_tptpcol_13_93766))], (760 ^ _599268) ^ [_620857] : [tptpcol_14_93774(_620857), -(tptpcol_13_93766(_620857))], (766 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_22022, c_tptpcol_9_22021))], (768 ^ _599268) ^ [_621096] : [tptpcol_10_22022(_621096), -(tptpcol_9_22021(_621096))], (774 ^ _599268) ^ [] : [-(genls(c_inanimateobject_nonnatural, c_inanimateobject))], (776 ^ _599268) ^ [_621335] : [inanimateobject_nonnatural(_621335), -(inanimateobject(_621335))], (782 ^ _599268) ^ [] : [-(transitivebinarypredicate(c_inregion))], (784 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member237_mt))], (786 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_72709, c_tptpcol_8_72708))], (788 ^ _599268) ^ [_621680] : [tptpcol_9_72709(_621680), -(tptpcol_8_72708(_621680))], (794 ^ _599268) ^ [] : [-(individual(c_xskijump_thegame))], (796 ^ _599268) ^ [_621919] : [-(tptpofobject(_621919, f_tptpquantityfn_14(n_232))), mtvisible(c_tptp_spindleheadmt), supplies(_621919)], (806 ^ _599268) ^ [] : [mtvisible(c_tptp_spindleheadmt), -(relationallinstance(c_tptpofobject, c_supplies, f_tptpquantityfn_14(n_232)))], (812 ^ _599268) ^ [] : [-(genls(c_firstordercollection, c_fixedordercollection))], (814 ^ _599268) ^ [_622358] : [firstordercollection(_622358), -(fixedordercollection(_622358))], (820 ^ _599268) ^ [] : [-(genlmt(c_universalvocabularymt, c_basekb))], (822 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member1_mt), -(borderson(c_georegion_l4_x45_y9, c_georegion_l4_x45_y10))], (828 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_18664, c_tptpcol_12_18663))], (830 ^ _599268) ^ [_622769] : [tptpcol_13_18664(_622769), -(tptpcol_12_18663(_622769))], (836 ^ _599268) ^ [] : [-(genls(c_artifact, c_inanimateobject_nonnatural))], (838 ^ _599268) ^ [_623008] : [artifact(_623008), -(inanimateobject_nonnatural(_623008))], (844 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_member3_mt, c_tptpgeo_spindleheadmt))], (846 ^ _599268) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (848 ^ _599268) ^ [] : [-(genlmt(c_timehasnoendmt, c_generictemporalmt))], (850 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_113665, c_tptpcol_6_112641))], (852 ^ _599268) ^ [_623406] : [tptpcol_7_113665(_623406), -(tptpcol_6_112641(_623406))], (858 ^ _599268) ^ [] : [mtvisible(c_currentworlddatacollectormt_nonhomocentric), -(tptpofobject(f_instancewithrelationtofn(c_airport_physical, c_airporthasiatacode, s_tlh), f_tptpquantityfn_21(n_170)))], (864 ^ _599268) ^ [] : [-(genls(c_geographicalregion, c_partiallytangible))], (866 ^ _599268) ^ [_623764] : [geographicalregion(_623764), -(partiallytangible(_623764))], (872 ^ _599268) ^ [] : [-(genlpreds(c_disjointwith, c_no))], (874 ^ _599268) ^ [_624017, _624019] : [disjointwith(_624019, _624017), -(no(_624019, _624017))], (880 ^ _599268) ^ [] : [-(genls(c_tptpcol_4_24578, c_tptpcol_3_16386))], (882 ^ _599268) ^ [_624266] : [tptpcol_4_24578(_624266), -(tptpcol_3_16386(_624266))], (888 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_69635, c_tptpcol_4_65539))], (890 ^ _599268) ^ [_624505] : [tptpcol_5_69635(_624505), -(tptpcol_4_65539(_624505))], (896 ^ _599268) ^ [] : [-(isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)))], (898 ^ _599268) ^ [] : [-(subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802))], (900 ^ _599268) ^ [] : [-(arg1isa(c_genls, c_collection))], (902 ^ _599268) ^ [_624864, _624866] : [genls(_624866, _624864), -(collection(_624866))], (908 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_22071, c_tptpcol_12_22055))], (910 ^ _599268) ^ [_625111] : [tptpcol_13_22071(_625111), -(tptpcol_12_22055(_625111))], (916 ^ _599268) ^ [] : [-(genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman), c_massmediadatamt))], (918 ^ _599268) ^ [] : [-(genls(c_tptpcol_3_98305, c_tptpcol_2_98304))], (920 ^ _599268) ^ [_625403] : [tptpcol_3_98305(_625403), -(tptpcol_2_98304(_625403))], (926 ^ _599268) ^ [] : [-(genls(c_tptpcol_4_114689, c_tptpcol_3_114688))], (928 ^ _599268) ^ [_625642] : [tptpcol_4_114689(_625642), -(tptpcol_3_114688(_625642))], (934 ^ _599268) ^ [] : [-(genls(c_artsupplies, c_supplies))], (936 ^ _599268) ^ [_625881] : [artsupplies(_625881), -(supplies(_625881))], (942 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_26629, c_tptpcol_7_26628))], (944 ^ _599268) ^ [_626120] : [tptpcol_8_26629(_626120), -(tptpcol_7_26628(_626120))], (950 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_109060, c_tptpcol_8_109059))], (952 ^ _599268) ^ [_626359] : [tptpcol_9_109060(_626359), -(tptpcol_8_109059(_626359))], (958 ^ _599268) ^ [] : [-(genlmt(c_tptp_member3633_mt, c_tptp_spindleheadmt))], (960 ^ _599268) ^ [_626598] : [isa(_626598, f_subcollectionofwithrelationtotypefn(c_issuingaprescription, c_products, c_correctivelensprescription)), -(tptp_8_968(f_relationexistsallfn(_626598, c_tptp_8_968, c_tptpcol_16_7738, f_subcollectionofwithrelationtotypefn(c_issuingaprescription, c_products, c_correctivelensprescription)), _626598))], (966 ^ _599268) ^ [] : [-(relationexistsall(c_tptp_8_968, c_tptpcol_16_7738, f_subcollectionofwithrelationtotypefn(c_issuingaprescription, c_products, c_correctivelensprescription)))], (968 ^ _599268) ^ [] : [-(physicalorderingpredicate(c_geographicalsubregions))], (970 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)), c_translation_0_885), c_machinelearningspindleheadmt))], (972 ^ _599268) ^ [] : [-(genlmt(c_tptp_member974_mt, c_tptp_spindleheadmt))], (974 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member1_mt), -(geographicalsubregions(c_georegion_l3_x11_y2, c_georegion_l4_x35_y7))], (980 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_109181, c_tptpcol_13_109173))], (982 ^ _599268) ^ [_627182] : [tptpcol_14_109181(_627182), -(tptpcol_13_109173(_627182))], (988 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_30972, c_tptpcol_15_30970))], (990 ^ _599268) ^ [_627421] : [tptpcol_16_30972(_627421), -(tptpcol_15_30970(_627421))], (996 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (998 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_18439, c_tptpcol_8_18438))], (1000 ^ _599268) ^ [_627713] : [tptpcol_9_18439(_627713), -(tptpcol_8_18438(_627713))], (1006 ^ _599268) ^ [] : [-(genlmt(c_keinteractionresourcetestmt, c_testvocabularymt))], (1008 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_118116, c_tptpcol_11_118084))], (1010 ^ _599268) ^ [_628005] : [tptpcol_12_118116(_628005), -(tptpcol_11_118084(_628005))], (1016 ^ _599268) ^ [] : [-(furpelt(c_theprototypicalfurpelt))], (1018 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_26628, c_tptpcol_6_26627))], (1020 ^ _599268) ^ [_628297] : [tptpcol_7_26628(_628297), -(tptpcol_6_26627(_628297))], (1026 ^ _599268) ^ [] : [-(arg1isa(c_most, c_setorcollection))], (1028 ^ _599268) ^ [_628550, _628552] : [most(_628552, _628550), -(setorcollection(_628552))], (1034 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_109185, c_tptpcol_14_109181))], (1036 ^ _599268) ^ [_628797] : [tptpcol_15_109185(_628797), -(tptpcol_14_109181(_628797))], (1042 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_92269, c_tptpcol_15_92268))], (1044 ^ _599268) ^ [_629036] : [tptpcol_16_92269(_629036), -(tptpcol_15_92268(_629036))], (1050 ^ _599268) ^ [] : [-(genlmt(c_cycnounlearnermt, c_cycorpproductsmt))], (1052 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_8_823, c_tptptypes_7_819))], (1054 ^ _599268) ^ [_629342, _629344] : [tptptypes_8_823(_629344, _629342), -(tptptypes_7_819(_629344, _629342))], (1060 ^ _599268) ^ [] : [-(genlmt(c_humansociallifemt, c_basekb))], (1062 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt))], (1064 ^ _599268) ^ [] : [-(genlmt(c_knowledgefragmentd3mt, c_basekb))], (1066 ^ _599268) ^ [] : [-(genlmt(c_testvocabularymt, c_nooescapearchitecturemt))], (1068 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member7_mt), -(geographicalsubregions(c_georegion_l2_x5_y8, c_georegion_l3_x15_y24))], (1074 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_26886, c_tptpcol_9_26885))], (1076 ^ _599268) ^ [_629922] : [tptpcol_10_26886(_629922), -(tptpcol_9_26885(_629922))], (1082 ^ _599268) ^ [] : [-(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt))], (1084 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_72793, c_tptpcol_14_72792))], (1086 ^ _599268) ^ [_630214] : [tptpcol_15_72793(_630214), -(tptpcol_14_72792(_630214))], (1092 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member3_mt), -(inregion(c_geolocation_x14_y39, c_georegion_l4_x14_y39))], (1098 ^ _599268) ^ [] : [-(genls(c_navypersonnel, c_militaryperson))], (1100 ^ _599268) ^ [_630572] : [navypersonnel(_630572), -(militaryperson(_630572))], (1106 ^ _599268) ^ [] : [-(genls(c_tptpcol_4_16387, c_tptpcol_3_16386))], (1108 ^ _599268) ^ [_630811] : [tptpcol_4_16387(_630811), -(tptpcol_3_16386(_630811))], (1114 ^ _599268) ^ [] : [-(genls(c_enduringthing_localized, c_spatialthing_nonsituational))], (1116 ^ _599268) ^ [_631050] : [enduringthing_localized(_631050), -(spatialthing_nonsituational(_631050))], (1122 ^ _599268) ^ [_631236] : [collection(_631236), individual(_631236)], (1128 ^ _599268) ^ [] : [-(disjointwith(c_collection, c_individual))], (1130 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member2_mt), -(geographicalsubregions(c_georegion_l2_x8_y2, c_georegion_l3_x25_y7))], (1136 ^ _599268) ^ [] : [mtvisible(c_worldgeographymt), -(geolevel_1(c_georegion_l1_x2_y0))], (1142 ^ _599268) ^ [] : [-(genls(c_physicalorderingpredicate, c_orderingpredicate))], (1144 ^ _599268) ^ [_631765] : [physicalorderingpredicate(_631765), -(orderingpredicate(_631765))], (1150 ^ _599268) ^ [] : [-(arg2isa(c_disjointwith, c_collection))], (1152 ^ _599268) ^ [_632018, _632020] : [disjointwith(_632020, _632018), -(collection(_632018))], (1158 ^ _599268) ^ [_632254, _632256, _632258, _632260] : [-(isa(f_relationallexistsfn(_632260, _632256, _632258, _632254), _632254)), isa(_632260, _632258), relationallexists(_632256, _632258, _632254)], (1168 ^ _599268) ^ [] : [-(resultisaarg(c_relationallexistsfn, n_4))], (1170 ^ _599268) ^ [] : [-(individual(c_tptptptpcol_16_25985))], (1172 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member2_mt), -(geographicalsubregions(c_georegion_l3_x25_y7, c_georegion_l4_x76_y23))], (1178 ^ _599268) ^ [] : [-(genlinverse(c_tptptypes_7_389, c_tptptypes_6_388))], (1180 ^ _599268) ^ [_632863, _632865] : [tptptypes_7_389(_632865, _632863), -(tptptypes_6_388(_632863, _632865))], (1186 ^ _599268) ^ [] : [mtvisible(c_hpkbvocabmt), -(genls(c_state_geopolitical, c_hpkb_subnationalagent))], (1192 ^ _599268) ^ [_633178] : [-(hpkb_subnationalagent(_633178)), mtvisible(c_hpkbvocabmt), state_geopolitical(_633178)], (1202 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_22020, c_tptpcol_7_21508))], (1204 ^ _599268) ^ [_633496] : [tptpcol_8_22020(_633496), -(tptpcol_7_21508(_633496))], (1210 ^ _599268) ^ [] : [-(reflexivebinarypredicate(c_inregion))], (1212 ^ _599268) ^ [_633735] : [-(tptp_9_51(f_relationexistsallfn(_633735, c_tptp_9_51, c_tptpcol_16_27189, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)), _633735)), mtvisible(c_currentworlddatacollectormt_nonhomocentric), isa(_633735, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma))], (1222 ^ _599268) ^ [] : [mtvisible(c_currentworlddatacollectormt_nonhomocentric), -(relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)))], (1228 ^ _599268) ^ [] : [-(genlmt(c_cyclistsmt, c_keinteractionresourcetestmt))], (1230 ^ _599268) ^ [] : [-(genls(c_tptpcol_3_65538, c_tptpcol_2_65537))], (1232 ^ _599268) ^ [_634239] : [tptpcol_3_65538(_634239), -(tptpcol_2_65537(_634239))], (1238 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_26921, c_tptpcol_13_26920))], (1240 ^ _599268) ^ [_634478] : [tptpcol_14_26921(_634478), -(tptpcol_13_26920(_634478))], (1246 ^ _599268) ^ [] : [-(genlmt(c_tptp_member3993_mt, c_tptp_spindleheadmt))], (1248 ^ _599268) ^ [] : [-(isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786, f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval, c_directionoftranslation_throughout, c_movement_translationevent)))], (1250 ^ _599268) ^ [] : [-(subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786))], (1252 ^ _599268) ^ [] : [-(individual(f_citynamedfn(s_agen, c_france)))], (1254 ^ _599268) ^ [] : [-(genls(c_intangibleindividual, c_partiallyintangibleindividual))], (1256 ^ _599268) ^ [_634929] : [intangibleindividual(_634929), -(partiallyintangibleindividual(_634929))], (1262 ^ _599268) ^ [] : [mtvisible(c_worldgeographymt), -(state_geopolitical(c_wanica_districtsuriname))], (1268 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_130924, c_tptpcol_15_130923))], (1270 ^ _599268) ^ [_635287] : [tptpcol_16_130924(_635287), -(tptpcol_15_130923(_635287))], (1276 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_92163, c_tptpcol_6_92162))], (1278 ^ _599268) ^ [_635526] : [tptpcol_7_92163(_635526), -(tptpcol_6_92162(_635526))], (1284 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt))], (1286 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_130933, c_tptpcol_15_130931))], (1288 ^ _599268) ^ [_635818] : [tptpcol_16_130933(_635818), -(tptpcol_15_130931(_635818))], (1294 ^ _599268) ^ [] : [-(genlmt(c_massmediadatamt, c_ethnicgroupsmt))], (1296 ^ _599268) ^ [] : [-(genlpreds(c_no, c_few))], (1298 ^ _599268) ^ [_636124, _636126] : [no(_636126, _636124), -(few(_636126, _636124))], (1304 ^ _599268) ^ [] : [-(genlmt(c_cycorpproductsmt, c_basekb))], (1306 ^ _599268) ^ [] : [-(genlmt(c_reasoningaboutpossibleantecedentsmt, c_humansociallifemt))], (1308 ^ _599268) ^ [] : [-(genlmt(c_worldgeographymt, c_geographymt))], (1310 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_20484, c_tptpcol_5_20483))], (1312 ^ _599268) ^ [_636532] : [tptpcol_6_20484(_636532), -(tptpcol_5_20483(_636532))], (1318 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member3_mt), -(geographicalsubregions(c_georegion_l3_x4_y13, c_georegion_l4_x14_y39))], (1324 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32), c_machinelearningspindleheadmt))], (1326 ^ _599268) ^ [] : [-(genlmt(c_worldcompletedualistgeographymt, c_unitedstatesgeographydualistmt))], (1328 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_108547, c_tptpcol_6_108546))], (1330 ^ _599268) ^ [_636996] : [tptpcol_7_108547(_636996), -(tptpcol_6_108546(_636996))], (1336 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_109125, c_tptpcol_10_109061))], (1338 ^ _599268) ^ [_637235] : [tptpcol_11_109125(_637235), -(tptpcol_10_109061(_637235))], (1344 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member2701_mt))], (1346 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_93698, c_tptpcol_7_93186))], (1348 ^ _599268) ^ [_637527] : [tptpcol_8_93698(_637527), -(tptpcol_7_93186(_637527))], (1354 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)), c_translation_7), c_machinelearningspindleheadmt))], (1356 ^ _599268) ^ [] : [-(genls(c_tptpcol_2_65537, c_tptpcol_1_65536))], (1358 ^ _599268) ^ [_637819] : [tptpcol_2_65537(_637819), -(tptpcol_1_65536(_637819))], (1364 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member2668_mt))], (1366 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_18436, c_tptpcol_5_16388))], (1368 ^ _599268) ^ [_638111] : [tptpcol_6_18436(_638111), -(tptpcol_5_16388(_638111))], (1374 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_18438, c_tptpcol_7_18437))], (1376 ^ _599268) ^ [_638350] : [tptpcol_8_18438(_638350), -(tptpcol_7_18437(_638350))], (1382 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member2_mt), -(inregion(c_geolocation_x76_y23, c_georegion_l4_x76_y23))], (1388 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_117763, c_tptpcol_7_117762))], (1390 ^ _599268) ^ [_638708] : [tptpcol_8_117763(_638708), -(tptpcol_7_117762(_638708))], (1396 ^ _599268) ^ [] : [-(genlmt(c_corecyclmt, c_logicaltruthmt))], (1398 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_109157, c_tptpcol_11_109125))], (1400 ^ _599268) ^ [_639000] : [tptpcol_12_109157(_639000), -(tptpcol_11_109125(_639000))], (1406 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_117762, c_tptpcol_6_116738))], (1408 ^ _599268) ^ [_639239] : [tptpcol_7_117762(_639239), -(tptpcol_6_116738(_639239))], (1414 ^ _599268) ^ [_639453, _639455, _639457] : [isa(_639457, _639455), isa(_639457, _639453), disjointwith(_639455, _639453)], (1424 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member3993_mt))], (1426 ^ _599268) ^ [] : [-(genls(c_aspatialinformationstore, c_aspatialthing))], (1428 ^ _599268) ^ [_639853] : [aspatialinformationstore(_639853), -(aspatialthing(_639853))], (1434 ^ _599268) ^ [] : [-(genlmt(c_ethnicgroupsvocabularymt, c_worldcompletedualistgeographymt))], (1436 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)), c_translation_0_885), c_machinelearningspindleheadmt))], (1438 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt))], (1440 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_93699, c_tptpcol_8_93698))], (1442 ^ _599268) ^ [_640251] : [tptpcol_9_93699(_640251), -(tptpcol_8_93698(_640251))], (1448 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_93764, c_tptpcol_10_93700))], (1450 ^ _599268) ^ [_640490] : [tptpcol_11_93764(_640490), -(tptpcol_10_93700(_640490))], (1456 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_26627, c_tptpcol_5_24579))], (1458 ^ _599268) ^ [_640729] : [tptpcol_6_26627(_640729), -(tptpcol_5_24579(_640729))], (1464 ^ _599268) ^ [] : [-(genls(c_tptpcol_4_90113, c_tptpcol_3_81921))], (1466 ^ _599268) ^ [_640968] : [tptpcol_4_90113(_640968), -(tptpcol_3_81921(_640968))], (1472 ^ _599268) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (1474 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_93700, c_tptpcol_9_93699))], (1476 ^ _599268) ^ [_641260] : [tptpcol_10_93700(_641260), -(tptpcol_9_93699(_641260))], (1482 ^ _599268) ^ [] : [-(genls(c_aspatialinformationstore, c_intangibleindividual))], (1484 ^ _599268) ^ [_641499] : [aspatialinformationstore(_641499), -(intangibleindividual(_641499))], (1490 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member4_mt), -(borderson(c_georegion_l4_x36_y50, c_georegion_l4_x37_y50))], (1496 ^ _599268) ^ [] : [-(genlmt(c_unitedstatesgeographypeoplemt, c_peopledatamt))], (1498 ^ _599268) ^ [] : [-(genls(c_tptpcol_3_16386, c_tptpcol_2_2))], (1500 ^ _599268) ^ [_641910] : [tptpcol_3_16386(_641910), -(tptpcol_2_2(_641910))], (1506 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_118019, c_tptpcol_8_117763))], (1508 ^ _599268) ^ [_642149] : [tptpcol_9_118019(_642149), -(tptpcol_8_117763(_642149))], (1514 ^ _599268) ^ [] : [-(genls(c_individual, c_trajector_underspecified))], (1516 ^ _599268) ^ [_642388] : [individual(_642388), -(trajector_underspecified(_642388))], (1522 ^ _599268) ^ [_642574] : [shavingrazor_manual(_642574), -(tptp_8_271(f_relationexistsallfn(_642574, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual), _642574))], (1528 ^ _599268) ^ [] : [-(relationexistsall(c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual))], (1530 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_112641, c_tptpcol_5_110593))], (1532 ^ _599268) ^ [_642878] : [tptpcol_6_112641(_642878), -(tptpcol_5_110593(_642878))], (1538 ^ _599268) ^ [] : [-(genls(c_tptpcol_12_72775, c_tptpcol_11_72774))], (1540 ^ _599268) ^ [_643117] : [tptpcol_12_72775(_643117), -(tptpcol_11_72774(_643117))], (1546 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_72707, c_tptpcol_6_71683))], (1548 ^ _599268) ^ [_643356] : [tptpcol_7_72707(_643356), -(tptpcol_6_71683(_643356))], (1554 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_50958, c_tptpcol_15_50957))], (1556 ^ _599268) ^ [_643595] : [tptpcol_16_50958(_643595), -(tptpcol_15_50957(_643595))], (1562 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_114177, c_tptpcol_7_113665))], (1564 ^ _599268) ^ [_643834] : [tptpcol_8_114177(_643834), -(tptpcol_7_113665(_643834))], (1570 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_72795, c_tptpcol_15_72793))], (1572 ^ _599268) ^ [_644073] : [tptpcol_16_72795(_644073), -(tptpcol_15_72793(_644073))], (1578 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_71683, c_tptpcol_5_69635))], (1580 ^ _599268) ^ [_644312] : [tptpcol_6_71683(_644312), -(tptpcol_5_69635(_644312))], (1586 ^ _599268) ^ [] : [-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member5_mt))], (1588 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_7_396, c_tptptypes_6_388))], (1590 ^ _599268) ^ [_644618, _644620] : [tptptypes_7_396(_644620, _644618), -(tptptypes_6_388(_644620, _644618))], (1596 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_26885, c_tptpcol_8_26629))], (1598 ^ _599268) ^ [_644867] : [tptpcol_9_26885(_644867), -(tptpcol_8_26629(_644867))], (1604 ^ _599268) ^ [] : [-(genlpreds(c_genls, c_subsetof))], (1606 ^ _599268) ^ [_645120, _645122] : [genls(_645122, _645120), -(subsetof(_645122, _645120))], (1612 ^ _599268) ^ [] : [-(genlmt(c_unitedstatessociallifemt, c_gregoriancalendarmt))], (1614 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_6_818, c_tptptypes_5_802))], (1616 ^ _599268) ^ [_645436, _645438] : [tptptypes_6_818(_645438, _645436), -(tptptypes_5_802(_645438, _645436))], (1622 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_92162, c_tptpcol_5_90114))], (1624 ^ _599268) ^ [_645685] : [tptpcol_6_92162(_645685), -(tptpcol_5_90114(_645685))], (1630 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member235_mt))], (1632 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_92164, c_tptpcol_7_92163))], (1634 ^ _599268) ^ [_645977] : [tptpcol_8_92164(_645977), -(tptpcol_7_92163(_645977))], (1640 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_118117, c_tptpcol_12_118116))], (1642 ^ _599268) ^ [_646216] : [tptpcol_13_118117(_646216), -(tptpcol_12_118116(_646216))], (1648 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_40388, c_tptpcol_10_40324))], (1650 ^ _599268) ^ [_646455] : [tptpcol_11_40388(_646455), -(tptpcol_10_40324(_646455))], (1656 ^ _599268) ^ [] : [-(genlpreds(c_tptptypes_9_824, c_tptptypes_8_823))], (1658 ^ _599268) ^ [_646708, _646710] : [tptptypes_9_824(_646710, _646708), -(tptptypes_8_823(_646710, _646708))], (1664 ^ _599268) ^ [] : [-(individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))], (1666 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_26887, c_tptpcol_10_26886))], (1668 ^ _599268) ^ [_647010] : [tptpcol_11_26887(_647010), -(tptpcol_10_26886(_647010))], (1674 ^ _599268) ^ [] : [-(genls(c_tptpcol_16_26926, c_tptpcol_15_26925))], (1676 ^ _599268) ^ [_647249] : [tptpcol_16_26926(_647249), -(tptpcol_15_26925(_647249))], (1682 ^ _599268) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)), c_translation_21), c_machinelearningspindleheadmt))], (1684 ^ _599268) ^ [] : [-(arg2isa(c_few, c_setorcollection))], (1686 ^ _599268) ^ [_647555, _647557] : [few(_647557, _647555), -(setorcollection(_647555))], (1692 ^ _599268) ^ [] : [-(genls(c_tptpcol_4_65539, c_tptpcol_3_65538))], (1694 ^ _599268) ^ [_647802] : [tptpcol_4_65539(_647802), -(tptpcol_3_65538(_647802))], (1700 ^ _599268) ^ [] : [-(genls(c_tptpcol_8_39940, c_tptpcol_7_39939))], (1702 ^ _599268) ^ [_648041] : [tptpcol_8_39940(_648041), -(tptpcol_7_39939(_648041))], (1708 ^ _599268) ^ [_648227] : [-(tptpofobject(_648227, f_tptpquantityfn_2(n_756))), mtvisible(c_tptp_member2701_mt), runningshorts(_648227)], (1718 ^ _599268) ^ [] : [mtvisible(c_tptp_member2701_mt), -(relationallinstance(c_tptpofobject, c_runningshorts, f_tptpquantityfn_2(n_756)))], (1724 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_22076, c_tptpcol_14_22072))], (1726 ^ _599268) ^ [_648666] : [tptpcol_15_22076(_648666), -(tptpcol_14_22072(_648666))], (1732 ^ _599268) ^ [] : [-(genls(c_tptpcol_0_0, c_individual))], (1734 ^ _599268) ^ [_648905] : [tptpcol_0_0(_648905), -(individual(_648905))], (1740 ^ _599268) ^ [] : [-(genlmt(c_tptp_member2356_mt, c_tptp_spindleheadmt))], (1742 ^ _599268) ^ [] : [-(individual(c_tptptptpcol_16_8398))], (1744 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member698_mt))], (1746 ^ _599268) ^ [] : [-(genls(c_tptpcol_11_72774, c_tptpcol_10_72710))], (1748 ^ _599268) ^ [_649303] : [tptpcol_11_72774(_649303), -(tptpcol_10_72710(_649303))], (1754 ^ _599268) ^ [] : [mtvisible(c_tptp_spindleheadmt), -(tptptypes_7_389(c_pushingwithopenhand, c_tptpcol_16_4451))], (1760 ^ _599268) ^ [] : [mtvisible(c_englishmt), -(prettystring(f_instancewithrelationtofn(c_footballteam, c_affiliatedwith, c_beloitcollege), s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege))], (1766 ^ _599268) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member1672_mt))], (1768 ^ _599268) ^ [] : [-(genlmt(c_unitedstatesgeographydualistmt, c_worldgeographydualistmt))], (1770 ^ _599268) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (1772 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_21508, c_tptpcol_6_20484))], (1774 ^ _599268) ^ [_649939] : [tptpcol_7_21508(_649939), -(tptpcol_6_20484(_649939))], (1780 ^ _599268) ^ [] : [-(genls(c_tptpcol_6_108546, c_tptpcol_5_106498))], (1782 ^ _599268) ^ [_650178] : [tptpcol_6_108546(_650178), -(tptpcol_5_106498(_650178))], (1788 ^ _599268) ^ [] : [mtvisible(c_cyclistsmt), -(tptptypes_8_390(c_pushingwithfingers, c_tptpcol_15_4027))], (1794 ^ _599268) ^ [] : [-(genls(c_geolevel_4, c_geographicalregion))], (1796 ^ _599268) ^ [_650536] : [geolevel_4(_650536), -(geographicalregion(_650536))], (1802 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member1_mt), -(borderson(c_georegion_l4_x38_y24, c_georegion_l4_x39_y24))], (1808 ^ _599268) ^ [] : [mtvisible(c_worldgeographymt), -(geolevel_4(c_georegion_l4_x75_y75))], (1814 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_26920, c_tptpcol_12_26919))], (1816 ^ _599268) ^ [_651013] : [tptpcol_13_26920(_651013), -(tptpcol_12_26919(_651013))], (1822 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_92264, c_tptpcol_13_92263))], (1824 ^ _599268) ^ [_651252] : [tptpcol_14_92264(_651252), -(tptpcol_13_92263(_651252))], (1830 ^ _599268) ^ [] : [-(genlmt(c_gregoriancalendarmt, c_basekb))], (1832 ^ _599268) ^ [] : [-(genls(c_tptpcol_9_40196, c_tptpcol_8_39940))], (1834 ^ _599268) ^ [_651544] : [tptpcol_9_40196(_651544), -(tptpcol_8_39940(_651544))], (1840 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member7_mt), -(geographicalsubregions(c_georegion_l3_x17_y24, c_georegion_l4_x53_y74))], (1846 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_92263, c_tptpcol_12_92262))], (1848 ^ _599268) ^ [_651902] : [tptpcol_13_92263(_651902), -(tptpcol_12_92262(_651902))], (1854 ^ _599268) ^ [] : [-(firstordercollection(c_tptpcol_16_62187))], (1856 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_90114, c_tptpcol_4_90113))], (1858 ^ _599268) ^ [_652194] : [tptpcol_5_90114(_652194), -(tptpcol_4_90113(_652194))], (1864 ^ _599268) ^ [] : [mtvisible(c_worldgeographymt), -(geolevel_3(c_georegion_l3_x17_y24))], (1870 ^ _599268) ^ [] : [-(genlmt(c_tptp_member2862_mt, c_tptp_spindleheadmt))], (1872 ^ _599268) ^ [] : [-(genls(c_tptpcol_15_26925, c_tptpcol_14_26921))], (1874 ^ _599268) ^ [_652605] : [tptpcol_15_26925(_652605), -(tptpcol_14_26921(_652605))], (1880 ^ _599268) ^ [] : [mtvisible(c_currentworlddatacollectormt_nonhomocentric), -(tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma), c_tptpcol_16_26939))], (1886 ^ _599268) ^ [] : [-(genls(c_tptpcol_7_18437, c_tptpcol_6_18436))], (1888 ^ _599268) ^ [_652963] : [tptpcol_7_18437(_652963), -(tptpcol_6_18436(_652963))], (1894 ^ _599268) ^ [] : [mtvisible(c_tptpgeo_member7_mt), -(borderson(c_georegion_l4_x29_y75, c_georegion_l4_x29_y76))], (1900 ^ _599268) ^ [] : [-(genlmt(c_organizationdatamt, f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)))], (1902 ^ _599268) ^ [] : [-(disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688))], (1904 ^ _599268) ^ [_653374] : [tptpcol_3_98305(_653374), tptpcol_3_114688(_653374)], (1910 ^ _599268) ^ [] : [-(genls(c_tptpcol_5_110593, c_tptpcol_4_106497))], (1912 ^ _599268) ^ [_653612] : [tptpcol_5_110593(_653612), -(tptpcol_4_106497(_653612))], (1918 ^ _599268) ^ [] : [-(genls(c_tptpcol_13_72791, c_tptpcol_12_72775))], (1920 ^ _599268) ^ [_653851] : [tptpcol_13_72791(_653851), -(tptpcol_12_72775(_653851))], (1926 ^ _599268) ^ [] : [-(genls(c_computerdataartifact, c_artifact))], (1928 ^ _599268) ^ [_654090] : [computerdataartifact(_654090), -(artifact(_654090))], (1934 ^ _599268) ^ [_654276] : [-(tptpofobject(_654276, f_tptpquantityfn_6(n_414))), mtvisible(c_tptp_member698_mt), militaryperson(_654276)], (1944 ^ _599268) ^ [] : [mtvisible(c_tptp_member698_mt), -(relationallinstance(c_tptpofobject, c_militaryperson, f_tptpquantityfn_6(n_414)))], (1950 ^ _599268) ^ [] : [-(genls(c_tptpcol_10_92166, c_tptpcol_9_92165))], (1952 ^ _599268) ^ [_654715] : [tptpcol_10_92166(_654715), -(tptpcol_9_92165(_654715))], (1958 ^ _599268) ^ [] : [-(genls(c_tptpcol_14_118118, c_tptpcol_13_118117))], (1960 ^ _599268) ^ [_654954] : [tptpcol_14_118118(_654954), -(tptpcol_13_118117(_654954))], (1966 ^ _599268) ^ [_655140] : [isa(_655140, c_tptpcol_14_118118), -(tptpcol_14_118118(_655140))], (1972 ^ _599268) ^ [_655328] : [tptpcol_14_118118(_655328), -(isa(_655328, c_tptpcol_14_118118))], (1978 ^ _599268) ^ [_655501] : [-(natfunction(f_tptpquantityfn_6(_655501), c_tptpquantityfn_6))], (1980 ^ _599268) ^ [_655581] : [-(natargument(f_tptpquantityfn_6(_655581), n_1, _655581))], (1982 ^ _599268) ^ [_655662] : [-(tptpquantity(f_tptpquantityfn_6(_655662)))], (1984 ^ _599268) ^ [_655756] : [isa(_655756, c_tptpcol_16_26939), -(tptpcol_16_26939(_655756))], (1990 ^ _599268) ^ [_655944] : [tptpcol_16_26939(_655944), -(isa(_655944, c_tptpcol_16_26939))], (1996 ^ _599268) ^ [_656132] : [isa(_656132, c_tptpcol_16_62187), -(tptpcol_16_62187(_656132))], (2002 ^ _599268) ^ [_656320] : [tptpcol_16_62187(_656320), -(isa(_656320, c_tptpcol_16_62187))], (2008 ^ _599268) ^ [_656508] : [isa(_656508, c_tptpcol_13_92263), -(tptpcol_13_92263(_656508))], (2014 ^ _599268) ^ [_656696] : [tptpcol_13_92263(_656696), -(isa(_656696, c_tptpcol_13_92263))], (2020 ^ _599268) ^ [_656884] : [isa(_656884, c_geolevel_4), -(geolevel_4(_656884))], (2026 ^ _599268) ^ [_657072] : [geolevel_4(_657072), -(isa(_657072, c_geolevel_4))], (2032 ^ _599268) ^ [_657260] : [isa(_657260, c_tptpcol_15_4027), -(tptpcol_15_4027(_657260))], (2038 ^ _599268) ^ [_657448] : [tptpcol_15_4027(_657448), -(isa(_657448, c_tptpcol_15_4027))], (2044 ^ _599268) ^ [_657636] : [isa(_657636, c_pushingwithfingers), -(pushingwithfingers(_657636))], (2050 ^ _599268) ^ [_657824] : [pushingwithfingers(_657824), -(isa(_657824, c_pushingwithfingers))], (2056 ^ _599268) ^ [_658026, _658028] : [affiliatedwith(_658028, _658026), -(agent_generic(_658026))], (2062 ^ _599268) ^ [_658234, _658236] : [affiliatedwith(_658236, _658234), -(agent_generic(_658236))], (2068 ^ _599268) ^ [_658442, _658444] : [affiliatedwith(_658444, _658442), -(affiliatedwith(_658442, _658444))], (2074 ^ _599268) ^ [_658622] : [affiliatedwith(_658622, _658622)], (2076 ^ _599268) ^ [_658715] : [isa(_658715, c_footballteam), -(footballteam(_658715))], (2082 ^ _599268) ^ [_658903] : [footballteam(_658903), -(isa(_658903, c_footballteam))], (2088 ^ _599268) ^ [_659091] : [isa(_659091, c_tptpcol_16_4451), -(tptpcol_16_4451(_659091))], (2094 ^ _599268) ^ [_659279] : [tptpcol_16_4451(_659279), -(isa(_659279, c_tptpcol_16_4451))], (2100 ^ _599268) ^ [_659467] : [isa(_659467, c_pushingwithopenhand), -(pushingwithopenhand(_659467))], (2106 ^ _599268) ^ [_659655] : [pushingwithopenhand(_659655), -(isa(_659655, c_pushingwithopenhand))], (2112 ^ _599268) ^ [_659843] : [isa(_659843, c_tptpcol_15_22076), -(tptpcol_15_22076(_659843))], (2118 ^ _599268) ^ [_660031] : [tptpcol_15_22076(_660031), -(isa(_660031, c_tptpcol_15_22076))], (2124 ^ _599268) ^ [_660204] : [-(natfunction(f_tptpquantityfn_2(_660204), c_tptpquantityfn_2))], (2126 ^ _599268) ^ [_660284] : [-(natargument(f_tptpquantityfn_2(_660284), n_1, _660284))], (2128 ^ _599268) ^ [_660365] : [-(tptpquantity(f_tptpquantityfn_2(_660365)))], (2130 ^ _599268) ^ [_660459] : [isa(_660459, c_tptpcol_7_39939), -(tptpcol_7_39939(_660459))], (2136 ^ _599268) ^ [_660647] : [tptpcol_7_39939(_660647), -(isa(_660647, c_tptpcol_7_39939))], (2142 ^ _599268) ^ [_660835] : [isa(_660835, c_tptpcol_8_39940), -(tptpcol_8_39940(_660835))], (2148 ^ _599268) ^ [_661023] : [tptpcol_8_39940(_661023), -(isa(_661023, c_tptpcol_8_39940))], (2154 ^ _599268) ^ [_661211] : [isa(_661211, c_tptpcol_15_26925), -(tptpcol_15_26925(_661211))], (2160 ^ _599268) ^ [_661399] : [tptpcol_15_26925(_661399), -(isa(_661399, c_tptpcol_15_26925))], (2166 ^ _599268) ^ [_661587] : [isa(_661587, c_tptpcol_16_26926), -(tptpcol_16_26926(_661587))], (2172 ^ _599268) ^ [_661775] : [tptpcol_16_26926(_661775), -(isa(_661775, c_tptpcol_16_26926))], (2178 ^ _599268) ^ [_661963] : [isa(_661963, c_tptpcol_13_118117), -(tptpcol_13_118117(_661963))], (2184 ^ _599268) ^ [_662151] : [tptpcol_13_118117(_662151), -(isa(_662151, c_tptpcol_13_118117))], (2190 ^ _599268) ^ [_662339] : [isa(_662339, c_tptpcol_5_90114), -(tptpcol_5_90114(_662339))], (2196 ^ _599268) ^ [_662527] : [tptpcol_5_90114(_662527), -(isa(_662527, c_tptpcol_5_90114))], (2202 ^ _599268) ^ [_662729, _662731] : [tptptypes_5_802(_662731, _662729), -(firstordercollection(_662729))], (2208 ^ _599268) ^ [_662937, _662939] : [tptptypes_5_802(_662939, _662937), -(firstordercollection(_662939))], (2214 ^ _599268) ^ [_663131] : [isa(_663131, c_tptpcol_16_72795), -(tptpcol_16_72795(_663131))], (2220 ^ _599268) ^ [_663319] : [tptpcol_16_72795(_663319), -(isa(_663319, c_tptpcol_16_72795))], (2226 ^ _599268) ^ [_663507] : [isa(_663507, c_tptpcol_8_114177), -(tptpcol_8_114177(_663507))], (2232 ^ _599268) ^ [_663695] : [tptpcol_8_114177(_663695), -(isa(_663695, c_tptpcol_8_114177))], (2238 ^ _599268) ^ [_663883] : [isa(_663883, c_tptpcol_15_50957), -(tptpcol_15_50957(_663883))], (2244 ^ _599268) ^ [_664071] : [tptpcol_15_50957(_664071), -(isa(_664071, c_tptpcol_15_50957))], (2250 ^ _599268) ^ [_664259] : [isa(_664259, c_tptpcol_16_50958), -(tptpcol_16_50958(_664259))], (2256 ^ _599268) ^ [_664447] : [tptpcol_16_50958(_664447), -(isa(_664447, c_tptpcol_16_50958))], (2262 ^ _599268) ^ [_664635] : [isa(_664635, c_tptpcol_6_71683), -(tptpcol_6_71683(_664635))], (2268 ^ _599268) ^ [_664823] : [tptpcol_6_71683(_664823), -(isa(_664823, c_tptpcol_6_71683))], (2274 ^ _599268) ^ [_665011] : [isa(_665011, c_tptpcol_11_72774), -(tptpcol_11_72774(_665011))], (2280 ^ _599268) ^ [_665199] : [tptpcol_11_72774(_665199), -(isa(_665199, c_tptpcol_11_72774))], (2286 ^ _599268) ^ [_665387] : [isa(_665387, c_tptpcol_12_72775), -(tptpcol_12_72775(_665387))], (2292 ^ _599268) ^ [_665575] : [tptpcol_12_72775(_665575), -(isa(_665575, c_tptpcol_12_72775))], (2298 ^ _599268) ^ [_665763] : [isa(_665763, c_tptpcol_5_110593), -(tptpcol_5_110593(_665763))], (2304 ^ _599268) ^ [_665951] : [tptpcol_5_110593(_665951), -(isa(_665951, c_tptpcol_5_110593))], (2310 ^ _599268) ^ [_666139] : [isa(_666139, c_tptpcol_16_25972), -(tptpcol_16_25972(_666139))], (2316 ^ _599268) ^ [_666327] : [tptpcol_16_25972(_666327), -(isa(_666327, c_tptpcol_16_25972))], (2322 ^ _599268) ^ [_666529, _666531] : [tptp_8_271(_666531, _666529), -(razor(_666529))], (2328 ^ _599268) ^ [_666737, _666739] : [tptp_8_271(_666739, _666737), -(tptpcol_5_24579(_666739))], (2334 ^ _599268) ^ [_666931] : [isa(_666931, c_tptpcol_4_90113), -(tptpcol_4_90113(_666931))], (2340 ^ _599268) ^ [_667119] : [tptpcol_4_90113(_667119), -(isa(_667119, c_tptpcol_4_90113))], (2346 ^ _599268) ^ [_667307] : [isa(_667307, c_tptpcol_10_93700), -(tptpcol_10_93700(_667307))], (2352 ^ _599268) ^ [_667495] : [tptpcol_10_93700(_667495), -(isa(_667495, c_tptpcol_10_93700))], (2358 ^ _599268) ^ [_667683] : [isa(_667683, c_tptpcol_9_93699), -(tptpcol_9_93699(_667683))], (2364 ^ _599268) ^ [_667871] : [tptpcol_9_93699(_667871), -(isa(_667871, c_tptpcol_9_93699))], (2370 ^ _599268) ^ [_668059] : [isa(_668059, c_aspatialthing), -(aspatialthing(_668059))], (2376 ^ _599268) ^ [_668247] : [aspatialthing(_668247), -(isa(_668247, c_aspatialthing))], (2382 ^ _599268) ^ [_668435] : [isa(_668435, c_tptpcol_7_117762), -(tptpcol_7_117762(_668435))], (2388 ^ _599268) ^ [_668623] : [tptpcol_7_117762(_668623), -(isa(_668623, c_tptpcol_7_117762))], (2394 ^ _599268) ^ [_668811] : [isa(_668811, c_tptpcol_8_117763), -(tptpcol_8_117763(_668811))], (2400 ^ _599268) ^ [_668999] : [tptpcol_8_117763(_668999), -(isa(_668999, c_tptpcol_8_117763))], (2406 ^ _599268) ^ [_669187] : [isa(_669187, c_tptpcol_7_18437), -(tptpcol_7_18437(_669187))], (2412 ^ _599268) ^ [_669375] : [tptpcol_7_18437(_669375), -(isa(_669375, c_tptpcol_7_18437))], (2418 ^ _599268) ^ [_669563] : [isa(_669563, c_tptpcol_6_18436), -(tptpcol_6_18436(_669563))], (2424 ^ _599268) ^ [_669751] : [tptpcol_6_18436(_669751), -(isa(_669751, c_tptpcol_6_18436))], (2430 ^ _599268) ^ [_669939] : [isa(_669939, c_tptpcol_8_93698), -(tptpcol_8_93698(_669939))], (2436 ^ _599268) ^ [_670127] : [tptpcol_8_93698(_670127), -(isa(_670127, c_tptpcol_8_93698))], (2442 ^ _599268) ^ [_670315] : [isa(_670315, c_tptpcol_11_109125), -(tptpcol_11_109125(_670315))], (2448 ^ _599268) ^ [_670503] : [tptpcol_11_109125(_670503), -(isa(_670503, c_tptpcol_11_109125))], (2454 ^ _599268) ^ [_670691] : [isa(_670691, c_tptpcol_6_108546), -(tptpcol_6_108546(_670691))], (2460 ^ _599268) ^ [_670879] : [tptpcol_6_108546(_670879), -(isa(_670879, c_tptpcol_6_108546))], (2466 ^ _599268) ^ [_671067] : [isa(_671067, c_tptpcol_6_20484), -(tptpcol_6_20484(_671067))], (2472 ^ _599268) ^ [_671255] : [tptpcol_6_20484(_671255), -(isa(_671255, c_tptpcol_6_20484))], (2478 ^ _599268) ^ [_671457, _671459] : [few(_671459, _671457), -(setorcollection(_671457))], (2484 ^ _599268) ^ [_671665, _671667] : [few(_671667, _671665), -(setorcollection(_671665))], (2490 ^ _599268) ^ [_671873, _671875] : [few(_671875, _671873), -(setorcollection(_671875))], (2496 ^ _599268) ^ [_672081, _672083] : [few(_672083, _672081), -(setorcollection(_672083))], (2502 ^ _599268) ^ [_672303, _672305, _672307] : [-(few(_672307, _672303)), few(_672307, _672305), subsetof(_672303, _672305)], (2512 ^ _599268) ^ [_672598] : [isa(_672598, c_tptpcol_15_130931), -(tptpcol_15_130931(_672598))], (2518 ^ _599268) ^ [_672786] : [tptpcol_15_130931(_672786), -(isa(_672786, c_tptpcol_15_130931))], (2524 ^ _599268) ^ [_672974] : [isa(_672974, c_tptpcol_16_130933), -(tptpcol_16_130933(_672974))], (2530 ^ _599268) ^ [_673162] : [tptpcol_16_130933(_673162), -(isa(_673162, c_tptpcol_16_130933))], (2536 ^ _599268) ^ [_673350] : [isa(_673350, c_tptpcol_7_92163), -(tptpcol_7_92163(_673350))], (2542 ^ _599268) ^ [_673538] : [tptpcol_7_92163(_673538), -(isa(_673538, c_tptpcol_7_92163))], (2548 ^ _599268) ^ [_673726] : [isa(_673726, c_tptpcol_15_130923), -(tptpcol_15_130923(_673726))], (2554 ^ _599268) ^ [_673914] : [tptpcol_15_130923(_673914), -(isa(_673914, c_tptpcol_15_130923))], (2560 ^ _599268) ^ [_674102] : [isa(_674102, c_tptpcol_16_130924), -(tptpcol_16_130924(_674102))], (2566 ^ _599268) ^ [_674290] : [tptpcol_16_130924(_674290), -(isa(_674290, c_tptpcol_16_130924))], (2572 ^ _599268) ^ [_674478] : [isa(_674478, c_intangibleindividual), -(intangibleindividual(_674478))], (2578 ^ _599268) ^ [_674666] : [intangibleindividual(_674666), -(isa(_674666, c_intangibleindividual))], (2584 ^ _599268) ^ [_674853, _674855] : [-(natfunction(f_citynamedfn(_674855, _674853), c_citynamedfn))], (2586 ^ _599268) ^ [_674950, _674952] : [-(natargument(f_citynamedfn(_674952, _674950), n_1, _674952))], (2588 ^ _599268) ^ [_675048, _675050] : [-(natargument(f_citynamedfn(_675050, _675048), n_2, _675048))], (2590 ^ _599268) ^ [_675146, _675148] : [-(city(f_citynamedfn(_675148, _675146)))], (2592 ^ _599268) ^ [_675243] : [isa(_675243, c_tptpcol_13_26920), -(tptpcol_13_26920(_675243))], (2598 ^ _599268) ^ [_675431] : [tptpcol_13_26920(_675431), -(isa(_675431, c_tptpcol_13_26920))], (2604 ^ _599268) ^ [_675619] : [isa(_675619, c_tptpcol_14_26921), -(tptpcol_14_26921(_675619))], (2610 ^ _599268) ^ [_675807] : [tptpcol_14_26921(_675807), -(isa(_675807, c_tptpcol_14_26921))], (2616 ^ _599268) ^ [_675995] : [isa(_675995, c_tptpcol_3_65538), -(tptpcol_3_65538(_675995))], (2622 ^ _599268) ^ [_676183] : [tptpcol_3_65538(_676183), -(isa(_676183, c_tptpcol_3_65538))], (2628 ^ _599268) ^ [_676371] : [isa(_676371, c_tptpcol_16_27189), -(tptpcol_16_27189(_676371))], (2634 ^ _599268) ^ [_676559] : [tptpcol_16_27189(_676559), -(isa(_676559, c_tptpcol_16_27189))], (2640 ^ _599268) ^ [_676761, _676763] : [tptp_9_51(_676763, _676761), -(subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(_676761))], (2646 ^ _599268) ^ [_676969, _676971] : [tptp_9_51(_676971, _676969), -(tptpcol_7_26628(_676971))], (2652 ^ _599268) ^ [_677163] : [isa(_677163, c_reflexivebinarypredicate), -(reflexivebinarypredicate(_677163))], (2658 ^ _599268) ^ [_677351] : [reflexivebinarypredicate(_677351), -(isa(_677351, c_reflexivebinarypredicate))], (2664 ^ _599268) ^ [_677539] : [isa(_677539, c_tptpcol_7_21508), -(tptpcol_7_21508(_677539))], (2670 ^ _599268) ^ [_677727] : [tptpcol_7_21508(_677727), -(isa(_677727, c_tptpcol_7_21508))], (2676 ^ _599268) ^ [_677915] : [isa(_677915, c_hpkb_subnationalagent), -(hpkb_subnationalagent(_677915))], (2682 ^ _599268) ^ [_678103] : [hpkb_subnationalagent(_678103), -(isa(_678103, c_hpkb_subnationalagent))], (2688 ^ _599268) ^ [_678291] : [isa(_678291, c_state_geopolitical), -(state_geopolitical(_678291))], (2694 ^ _599268) ^ [_678479] : [state_geopolitical(_678479), -(isa(_678479, c_state_geopolitical))], (2700 ^ _599268) ^ [_678694, _678696, _678698, _678700] : [-(natfunction(f_relationallexistsfn(_678700, _678698, _678696, _678694), c_relationallexistsfn))], (2702 ^ _599268) ^ [_678825, _678827, _678829, _678831] : [-(natargument(f_relationallexistsfn(_678831, _678829, _678827, _678825), n_1, _678831))], (2704 ^ _599268) ^ [_678957, _678959, _678961, _678963] : [-(natargument(f_relationallexistsfn(_678963, _678961, _678959, _678957), n_2, _678961))], (2706 ^ _599268) ^ [_679089, _679091, _679093, _679095] : [-(natargument(f_relationallexistsfn(_679095, _679093, _679091, _679089), n_3, _679091))], (2708 ^ _599268) ^ [_679221, _679223, _679225, _679227] : [-(natargument(f_relationallexistsfn(_679227, _679225, _679223, _679221), n_4, _679221))], (2710 ^ _599268) ^ [_679353, _679355, _679357, _679359] : [-(thing(f_relationallexistsfn(_679359, _679357, _679355, _679353)))], (2712 ^ _599268) ^ [_679470, _679472] : [arg2isa(_679472, _679470), -(collection(_679470))], (2718 ^ _599268) ^ [_679678, _679680] : [arg2isa(_679680, _679678), -(relation(_679680))], (2724 ^ _599268) ^ [_679900, _679902, _679904] : [-(arg2isa(_679904, _679900)), arg2isa(_679904, _679902), genls(_679902, _679900)], (2734 ^ _599268) ^ [_680223, _680225, _680227] : [-(arg2isa(_680227, _680223)), arg2isa(_680227, _680225), genls(_680225, _680223)], (2744 ^ _599268) ^ [_680518] : [isa(_680518, c_geolevel_1), -(geolevel_1(_680518))], (2750 ^ _599268) ^ [_680706] : [geolevel_1(_680706), -(isa(_680706, c_geolevel_1))], (2756 ^ _599268) ^ [] : [-(mtvisible(c_logicaltruthmt))], (2758 ^ _599268) ^ [_680947] : [isa(_680947, c_spatialthing_nonsituational), -(spatialthing_nonsituational(_680947))], (2764 ^ _599268) ^ [_681135] : [spatialthing_nonsituational(_681135), -(isa(_681135, c_spatialthing_nonsituational))], (2770 ^ _599268) ^ [_681323] : [isa(_681323, c_militaryperson), -(militaryperson(_681323))], (2776 ^ _599268) ^ [_681511] : [militaryperson(_681511), -(isa(_681511, c_militaryperson))], (2782 ^ _599268) ^ [_681699] : [isa(_681699, c_tptpcol_15_72793), -(tptpcol_15_72793(_681699))], (2788 ^ _599268) ^ [_681887] : [tptpcol_15_72793(_681887), -(isa(_681887, c_tptpcol_15_72793))], (2794 ^ _599268) ^ [_682075] : [isa(_682075, c_tptpcol_9_26885), -(tptpcol_9_26885(_682075))], (2800 ^ _599268) ^ [_682263] : [tptpcol_9_26885(_682263), -(isa(_682263, c_tptpcol_9_26885))], (2806 ^ _599268) ^ [_682451] : [isa(_682451, c_tptpcol_10_26886), -(tptpcol_10_26886(_682451))], (2812 ^ _599268) ^ [_682639] : [tptpcol_10_26886(_682639), -(isa(_682639, c_tptpcol_10_26886))], (2818 ^ _599268) ^ [_682841, _682843] : [tptptypes_8_823(_682843, _682841), -(firstordercollection(_682841))], (2824 ^ _599268) ^ [_683049, _683051] : [tptptypes_8_823(_683051, _683049), -(firstordercollection(_683051))], (2830 ^ _599268) ^ [_683243] : [isa(_683243, c_tptpcol_16_92269), -(tptpcol_16_92269(_683243))], (2836 ^ _599268) ^ [_683431] : [tptpcol_16_92269(_683431), -(isa(_683431, c_tptpcol_16_92269))], (2842 ^ _599268) ^ [_683619] : [isa(_683619, c_tptpcol_15_109185), -(tptpcol_15_109185(_683619))], (2848 ^ _599268) ^ [_683807] : [tptpcol_15_109185(_683807), -(isa(_683807, c_tptpcol_15_109185))], (2854 ^ _599268) ^ [_683995] : [isa(_683995, c_tptpcol_6_26627), -(tptpcol_6_26627(_683995))], (2860 ^ _599268) ^ [_684183] : [tptpcol_6_26627(_684183), -(isa(_684183, c_tptpcol_6_26627))], (2866 ^ _599268) ^ [_684371] : [isa(_684371, c_tptpcol_12_118116), -(tptpcol_12_118116(_684371))], (2872 ^ _599268) ^ [_684559] : [tptpcol_12_118116(_684559), -(isa(_684559, c_tptpcol_12_118116))], (2878 ^ _599268) ^ [_684747] : [isa(_684747, c_tptpcol_8_18438), -(tptpcol_8_18438(_684747))], (2884 ^ _599268) ^ [_684935] : [tptpcol_8_18438(_684935), -(isa(_684935, c_tptpcol_8_18438))], (2890 ^ _599268) ^ [_685123] : [isa(_685123, c_tptpcol_15_30970), -(tptpcol_15_30970(_685123))], (2896 ^ _599268) ^ [_685311] : [tptpcol_15_30970(_685311), -(isa(_685311, c_tptpcol_15_30970))], (2902 ^ _599268) ^ [_685499] : [isa(_685499, c_tptpcol_16_30972), -(tptpcol_16_30972(_685499))], (2908 ^ _599268) ^ [_685687] : [tptpcol_16_30972(_685687), -(isa(_685687, c_tptpcol_16_30972))], (2914 ^ _599268) ^ [_685875] : [isa(_685875, c_tptpcol_14_109181), -(tptpcol_14_109181(_685875))], (2920 ^ _599268) ^ [_686063] : [tptpcol_14_109181(_686063), -(isa(_686063, c_tptpcol_14_109181))], (2926 ^ _599268) ^ [_686251] : [isa(_686251, c_physicalorderingpredicate), -(physicalorderingpredicate(_686251))], (2932 ^ _599268) ^ [_686439] : [physicalorderingpredicate(_686439), -(isa(_686439, c_physicalorderingpredicate))], (2938 ^ _599268) ^ [_686627] : [isa(_686627, c_tptpcol_16_7738), -(tptpcol_16_7738(_686627))], (2944 ^ _599268) ^ [_686815] : [tptpcol_16_7738(_686815), -(isa(_686815, c_tptpcol_16_7738))], (2950 ^ _599268) ^ [_687017, _687019] : [tptp_8_968(_687019, _687017), -(subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(_687017))], (2956 ^ _599268) ^ [_687225, _687227] : [tptp_8_968(_687227, _687225), -(tptpcol_7_7172(_687227))], (2962 ^ _599268) ^ [_687447, _687449, _687451] : [relationexistsall(_687451, _687449, _687447), -(collection(_687447))], (2968 ^ _599268) ^ [_687677, _687679, _687681] : [relationexistsall(_687681, _687679, _687677), -(collection(_687679))], (2974 ^ _599268) ^ [_687907, _687909, _687911] : [relationexistsall(_687911, _687909, _687907), -(binarypredicate(_687911))], (2980 ^ _599268) ^ [_688109] : [isa(_688109, c_tptpcol_7_26628), -(tptpcol_7_26628(_688109))], (2986 ^ _599268) ^ [_688297] : [tptpcol_7_26628(_688297), -(isa(_688297, c_tptpcol_7_26628))], (2992 ^ _599268) ^ [_688485] : [isa(_688485, c_tptpcol_8_26629), -(tptpcol_8_26629(_688485))], (2998 ^ _599268) ^ [_688673] : [tptpcol_8_26629(_688673), -(isa(_688673, c_tptpcol_8_26629))], (3004 ^ _599268) ^ [_688861] : [isa(_688861, c_tptpcol_3_114688), -(tptpcol_3_114688(_688861))], (3010 ^ _599268) ^ [_689049] : [tptpcol_3_114688(_689049), -(isa(_689049, c_tptpcol_3_114688))], (3016 ^ _599268) ^ [_689222] : [-(natfunction(f_contextofpcwfn(_689222), c_contextofpcwfn))], (3018 ^ _599268) ^ [_689302] : [-(natargument(f_contextofpcwfn(_689302), n_1, _689302))], (3020 ^ _599268) ^ [_689383] : [-(microtheory(f_contextofpcwfn(_689383)))], (3022 ^ _599268) ^ [_689491, _689493] : [arg1isa(_689493, _689491), -(collection(_689491))], (3028 ^ _599268) ^ [_689699, _689701] : [arg1isa(_689701, _689699), -(relation(_689701))], (3034 ^ _599268) ^ [_689921, _689923, _689925] : [-(arg1isa(_689925, _689921)), arg1isa(_689925, _689923), genls(_689923, _689921)], (3044 ^ _599268) ^ [_690244, _690246, _690248] : [-(arg1isa(_690248, _690244)), arg1isa(_690248, _690246), genls(_690246, _690244)], (3054 ^ _599268) ^ [_690553, _690555] : [objectfoundinlocation(_690555, _690553), -(spatialthing_nonsituational(_690553))], (3060 ^ _599268) ^ [_690761, _690763] : [objectfoundinlocation(_690763, _690761), -(spatialthing_localized(_690761))], (3066 ^ _599268) ^ [_690969, _690971] : [objectfoundinlocation(_690971, _690969), -(spatialthing_nonsituational(_690971))], (3072 ^ _599268) ^ [_691177, _691179] : [objectfoundinlocation(_691179, _691177), -(spatialthing_localized(_691179))], (3078 ^ _599268) ^ [_691399, _691401, _691403] : [-(objectfoundinlocation(_691403, _691399)), objectfoundinlocation(_691403, _691401), objectfoundinlocation(_691401, _691399)], (3088 ^ _599268) ^ [_691678] : [objectfoundinlocation(_691678, _691678)], (3090 ^ _599268) ^ [_691799, _691801, _691803] : [-(objectfoundinlocation(_691803, _691799)), objectfoundinlocation(_691803, _691801), geopoliticalsubdivision(_691799, _691801)], (3100 ^ _599268) ^ [_692122, _692124, _692126] : [-(objectfoundinlocation(_692126, _692122)), objectfoundinlocation(_692126, _692124), geographicallysubsumes(_692122, _692124)], (3110 ^ _599268) ^ [_692445, _692447, _692449] : [-(objectfoundinlocation(_692449, _692445)), objectfoundinlocation(_692449, _692447), subregions(_692445, _692447)], (3120 ^ _599268) ^ [_692740] : [isa(_692740, c_ship), -(ship(_692740))], (3126 ^ _599268) ^ [_692928] : [ship(_692928), -(isa(_692928, c_ship))], (3132 ^ _599268) ^ [_693129, _693131, _693133] : [-(natfunction(f_subcollectionofwithrelationtofn(_693133, _693131, _693129), c_subcollectionofwithrelationtofn))], (3134 ^ _599268) ^ [_693243, _693245, _693247] : [-(natargument(f_subcollectionofwithrelationtofn(_693247, _693245, _693243), n_1, _693247))], (3136 ^ _599268) ^ [_693358, _693360, _693362] : [-(natargument(f_subcollectionofwithrelationtofn(_693362, _693360, _693358), n_2, _693360))], (3138 ^ _599268) ^ [_693473, _693475, _693477] : [-(natargument(f_subcollectionofwithrelationtofn(_693477, _693475, _693473), n_3, _693473))], (3140 ^ _599268) ^ [_693588, _693590, _693592] : [-(collection(f_subcollectionofwithrelationtofn(_693592, _693590, _693588)))], (3142 ^ _599268) ^ [_693688] : [isa(_693688, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)), -(subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(_693688))], (3148 ^ _599268) ^ [_693876] : [subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(_693876), -(isa(_693876, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)))], (3154 ^ _599268) ^ [_694064] : [isa(_694064, c_tptpcol_4_65539), -(tptpcol_4_65539(_694064))], (3160 ^ _599268) ^ [_694252] : [tptpcol_4_65539(_694252), -(isa(_694252, c_tptpcol_4_65539))], (3166 ^ _599268) ^ [_694440] : [isa(_694440, c_tptpcol_5_69635), -(tptpcol_5_69635(_694440))], (3172 ^ _599268) ^ [_694628] : [tptpcol_5_69635(_694628), -(isa(_694628, c_tptpcol_5_69635))], (3178 ^ _599268) ^ [_694816] : [isa(_694816, c_tptpcol_3_16386), -(tptpcol_3_16386(_694816))], (3184 ^ _599268) ^ [_695004] : [tptpcol_3_16386(_695004), -(isa(_695004, c_tptpcol_3_16386))], (3190 ^ _599268) ^ [_695206, _695208] : [no(_695208, _695206), -(setorcollection(_695206))], (3196 ^ _599268) ^ [_695414, _695416] : [no(_695416, _695414), -(setorcollection(_695416))], (3202 ^ _599268) ^ [_695622, _695624] : [no(_695624, _695622), -(no(_695622, _695624))], (3208 ^ _599268) ^ [_695846, _695848, _695850] : [-(no(_695850, _695846)), no(_695850, _695848), subsetof(_695846, _695848)], (3218 ^ _599268) ^ [_696169, _696171, _696173] : [-(no(_696169, _696171)), no(_696173, _696171), subsetof(_696169, _696173)], (3228 ^ _599268) ^ [_696492, _696494, _696496] : [-(no(_696492, _696494)), no(_696496, _696494), genls(_696492, _696496)], (3238 ^ _599268) ^ [_696815, _696817, _696819] : [-(no(_696819, _696815)), no(_696819, _696817), genls(_696815, _696817)], (3248 ^ _599268) ^ [_697138, _697140, _697142] : [-(no(_697138, _697140)), no(_697142, _697140), subsetof(_697138, _697142)], (3258 ^ _599268) ^ [_697461, _697463, _697465] : [-(no(_697465, _697461)), no(_697465, _697463), subsetof(_697461, _697463)], (3268 ^ _599268) ^ [_697756] : [isa(_697756, c_geographicalregion), -(geographicalregion(_697756))], (3274 ^ _599268) ^ [_697944] : [geographicalregion(_697944), -(isa(_697944, c_geographicalregion))], (3280 ^ _599268) ^ [_698117] : [-(natfunction(f_tptpquantityfn_21(_698117), c_tptpquantityfn_21))], (3282 ^ _599268) ^ [_698197] : [-(natargument(f_tptpquantityfn_21(_698197), n_1, _698197))], (3284 ^ _599268) ^ [_698278] : [-(tptpquantity(f_tptpquantityfn_21(_698278)))], (3286 ^ _599268) ^ [_698386, _698388] : [airporthasiatacode(_698388, _698386), -(stringoflengthfn3(_698386))], (3292 ^ _599268) ^ [_698594, _698596] : [airporthasiatacode(_698596, _698594), -(airport_physical(_698596))], (3298 ^ _599268) ^ [_698788] : [isa(_698788, c_airport_physical), -(airport_physical(_698788))], (3304 ^ _599268) ^ [_698976] : [airport_physical(_698976), -(isa(_698976, c_airport_physical))], (3310 ^ _599268) ^ [_699177, _699179, _699181] : [-(natfunction(f_instancewithrelationtofn(_699181, _699179, _699177), c_instancewithrelationtofn))], (3312 ^ _599268) ^ [_699291, _699293, _699295] : [-(natargument(f_instancewithrelationtofn(_699295, _699293, _699291), n_1, _699295))], (3314 ^ _599268) ^ [_699406, _699408, _699410] : [-(natargument(f_instancewithrelationtofn(_699410, _699408, _699406), n_2, _699408))], (3316 ^ _599268) ^ [_699521, _699523, _699525] : [-(natargument(f_instancewithrelationtofn(_699525, _699523, _699521), n_3, _699521))], (3318 ^ _599268) ^ [_699636, _699638, _699640] : [-(thing(f_instancewithrelationtofn(_699640, _699638, _699636)))], (3320 ^ _599268) ^ [_699736] : [isa(_699736, c_tptpcol_6_112641), -(tptpcol_6_112641(_699736))], (3326 ^ _599268) ^ [_699924] : [tptpcol_6_112641(_699924), -(isa(_699924, c_tptpcol_6_112641))], (3332 ^ _599268) ^ [_700112] : [isa(_700112, c_tptpcol_7_113665), -(tptpcol_7_113665(_700112))], (3338 ^ _599268) ^ [_700300] : [tptpcol_7_113665(_700300), -(isa(_700300, c_tptpcol_7_113665))], (3344 ^ _599268) ^ [_700488] : [isa(_700488, c_artifact), -(artifact(_700488))], (3350 ^ _599268) ^ [_700676] : [artifact(_700676), -(isa(_700676, c_artifact))], (3356 ^ _599268) ^ [_700864] : [isa(_700864, c_tptpcol_13_18664), -(tptpcol_13_18664(_700864))], (3362 ^ _599268) ^ [_701052] : [tptpcol_13_18664(_701052), -(isa(_701052, c_tptpcol_13_18664))], (3368 ^ _599268) ^ [_701240] : [isa(_701240, c_firstordercollection), -(firstordercollection(_701240))], (3374 ^ _599268) ^ [_701428] : [firstordercollection(_701428), -(isa(_701428, c_firstordercollection))], (3380 ^ _599268) ^ [_701601] : [-(natfunction(f_tptpquantityfn_14(_701601), c_tptpquantityfn_14))], (3382 ^ _599268) ^ [_701681] : [-(natargument(f_tptpquantityfn_14(_701681), n_1, _701681))], (3384 ^ _599268) ^ [_701762] : [-(tptpquantity(f_tptpquantityfn_14(_701762)))], (3386 ^ _599268) ^ [_701856] : [isa(_701856, c_supplies), -(supplies(_701856))], (3392 ^ _599268) ^ [_702044] : [supplies(_702044), -(isa(_702044, c_supplies))], (3398 ^ _599268) ^ [_702232] : [isa(_702232, c_inanimateobject_nonnatural), -(inanimateobject_nonnatural(_702232))], (3404 ^ _599268) ^ [_702420] : [inanimateobject_nonnatural(_702420), -(isa(_702420, c_inanimateobject_nonnatural))], (3410 ^ _599268) ^ [_702608] : [isa(_702608, c_tptpcol_13_22071), -(tptpcol_13_22071(_702608))], (3416 ^ _599268) ^ [_702796] : [tptpcol_13_22071(_702796), -(isa(_702796, c_tptpcol_13_22071))], (3422 ^ _599268) ^ [_702984] : [isa(_702984, c_tptpcol_14_22072), -(tptpcol_14_22072(_702984))], (3428 ^ _599268) ^ [_703172] : [tptpcol_14_22072(_703172), -(isa(_703172, c_tptpcol_14_22072))], (3434 ^ _599268) ^ [_703360] : [isa(_703360, c_tptpcol_7_108547), -(tptpcol_7_108547(_703360))], (3440 ^ _599268) ^ [_703548] : [tptpcol_7_108547(_703548), -(isa(_703548, c_tptpcol_7_108547))], (3446 ^ _599268) ^ [_703736] : [isa(_703736, c_tptpcol_8_109059), -(tptpcol_8_109059(_703736))], (3452 ^ _599268) ^ [_703924] : [tptpcol_8_109059(_703924), -(isa(_703924, c_tptpcol_8_109059))], (3458 ^ _599268) ^ [_704112] : [isa(_704112, c_tptpcol_14_93774), -(tptpcol_14_93774(_704112))], (3464 ^ _599268) ^ [_704300] : [tptpcol_14_93774(_704300), -(isa(_704300, c_tptpcol_14_93774))], (3470 ^ _599268) ^ [_704488] : [isa(_704488, c_tptpcol_15_93775), -(tptpcol_15_93775(_704488))], (3476 ^ _599268) ^ [_704676] : [tptpcol_15_93775(_704676), -(isa(_704676, c_tptpcol_15_93775))], (3482 ^ _599268) ^ [_704864] : [isa(_704864, c_tptpcol_16_8886), -(tptpcol_16_8886(_704864))], (3488 ^ _599268) ^ [_705052] : [tptpcol_16_8886(_705052), -(isa(_705052, c_tptpcol_16_8886))], (3494 ^ _599268) ^ [_705254, _705256] : [orientation(_705256, _705254), -(orientationvector(_705254))], (3500 ^ _599268) ^ [_705462, _705464] : [orientation(_705464, _705462), -(spatialthing_localized(_705464))], (3506 ^ _599268) ^ [_705656] : [isa(_705656, c_orientationvector), -(orientationvector(_705656))], (3512 ^ _599268) ^ [_705844] : [orientationvector(_705844), -(isa(_705844, c_orientationvector))], (3518 ^ _599268) ^ [_706032] : [isa(_706032, f_subcollectionofwithrelationfromtypefn(c_orientationvector, c_orientation, c_partiallytangible)), -(subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(_706032))], (3524 ^ _599268) ^ [_706220] : [subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(_706220), -(isa(_706220, f_subcollectionofwithrelationfromtypefn(c_orientationvector, c_orientation, c_partiallytangible)))], (3530 ^ _599268) ^ [_706422, _706424] : [tptptypes_9_824(_706424, _706422), -(firstordercollection(_706422))], (3536 ^ _599268) ^ [_706630, _706632] : [tptptypes_9_824(_706632, _706630), -(firstordercollection(_706632))], (3542 ^ _599268) ^ [_706838, _706840] : [tptptypes_7_396(_706840, _706838), -(firstordercollection(_706838))], (3548 ^ _599268) ^ [_707046, _707048] : [tptptypes_7_396(_707048, _707046), -(firstordercollection(_707048))], (3554 ^ _599268) ^ [_707240] : [isa(_707240, c_tptpcol_12_22055), -(tptpcol_12_22055(_707240))], (3560 ^ _599268) ^ [_707428] : [tptpcol_12_22055(_707428), -(isa(_707428, c_tptpcol_12_22055))], (3566 ^ _599268) ^ [_707616] : [isa(_707616, c_tptpcol_16_29490), -(tptpcol_16_29490(_707616))], (3572 ^ _599268) ^ [_707804] : [tptpcol_16_29490(_707804), -(isa(_707804, c_tptpcol_16_29490))], (3578 ^ _599268) ^ [_708006, _708008] : [tptp_9_720(_708008, _708006), -(tptpcol_5_28674(_708006))], (3584 ^ _599268) ^ [_708214, _708216] : [tptp_9_720(_708216, _708214), -(executionbyfiringsquad(_708216))], (3590 ^ _599268) ^ [_708408] : [isa(_708408, c_runningshorts), -(runningshorts(_708408))], (3596 ^ _599268) ^ [_708596] : [runningshorts(_708596), -(isa(_708596, c_runningshorts))], (3602 ^ _599268) ^ [_708784] : [isa(_708784, c_tptpcol_9_118019), -(tptpcol_9_118019(_708784))], (3608 ^ _599268) ^ [_708972] : [tptpcol_9_118019(_708972), -(isa(_708972, c_tptpcol_9_118019))], (3614 ^ _599268) ^ [_709160] : [isa(_709160, c_tptpcol_16_31868), -(tptpcol_16_31868(_709160))], (3620 ^ _599268) ^ [_709348] : [tptpcol_16_31868(_709348), -(isa(_709348, c_tptpcol_16_31868))], (3626 ^ _599268) ^ [_709536] : [isa(_709536, c_movement_translationevent), -(movement_translationevent(_709536))], (3632 ^ _599268) ^ [_709724] : [movement_translationevent(_709724), -(isa(_709724, c_movement_translationevent))], (3638 ^ _599268) ^ [_709926, _709928] : [directionoftranslation_throughout(_709928, _709926), -(unitvectorinterval(_709926))], (3644 ^ _599268) ^ [_710134, _710136] : [directionoftranslation_throughout(_710136, _710134), -(movement_translationevent(_710136))], (3650 ^ _599268) ^ [_710356, _710358, _710360] : [-(directionoftranslation_throughout(_710356, _710358)), directionoftranslation_throughout(_710360, _710358), subevents(_710360, _710356)], (3660 ^ _599268) ^ [_710651] : [isa(_710651, c_unitvectorinterval), -(unitvectorinterval(_710651))], (3666 ^ _599268) ^ [_710839] : [unitvectorinterval(_710839), -(isa(_710839, c_unitvectorinterval))], (3672 ^ _599268) ^ [_711027] : [isa(_711027, f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval, c_directionoftranslation_throughout, c_movement_translationevent)), -(subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(_711027))], (3678 ^ _599268) ^ [_711215] : [subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(_711215), -(isa(_711215, f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval, c_directionoftranslation_throughout, c_movement_translationevent)))], (3684 ^ _599268) ^ [_711417, _711419] : [tptp_8_875(_711419, _711417), -(tptpcol_4_24578(_711417))], (3690 ^ _599268) ^ [_711625, _711627] : [tptp_8_875(_711627, _711625), -(subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(_711627))], (3696 ^ _599268) ^ [_711847, _711849, _711851] : [relationallexists(_711851, _711849, _711847), -(collection(_711847))], (3702 ^ _599268) ^ [_712077, _712079, _712081] : [relationallexists(_712081, _712079, _712077), -(collection(_712079))], (3708 ^ _599268) ^ [_712307, _712309, _712311] : [relationallexists(_712311, _712309, _712307), -(binarypredicate(_712311))], (3714 ^ _599268) ^ [_712509] : [isa(_712509, c_tptpcol_16_10258), -(tptpcol_16_10258(_712509))], (3720 ^ _599268) ^ [_712697] : [tptpcol_16_10258(_712697), -(isa(_712697, c_tptpcol_16_10258))], (3726 ^ _599268) ^ [_712885] : [isa(_712885, c_pushingababycarriage), -(pushingababycarriage(_712885))], (3732 ^ _599268) ^ [_713073] : [pushingababycarriage(_713073), -(isa(_713073, c_pushingababycarriage))], (3738 ^ _599268) ^ [_713261] : [isa(_713261, c_aspatialinformationstore), -(aspatialinformationstore(_713261))], (3744 ^ _599268) ^ [_713449] : [aspatialinformationstore(_713449), -(isa(_713449, c_aspatialinformationstore))], (3750 ^ _599268) ^ [_713637] : [isa(_713637, c_collection), -(collection(_713637))], (3756 ^ _599268) ^ [_713825] : [collection(_713825), -(isa(_713825, c_collection))], (3762 ^ _599268) ^ [_714013] : [isa(_714013, c_fixedordercollection), -(fixedordercollection(_714013))], (3768 ^ _599268) ^ [_714201] : [fixedordercollection(_714201), -(isa(_714201, c_fixedordercollection))], (3774 ^ _599268) ^ [_714389] : [isa(_714389, c_tptpcol_8_92164), -(tptpcol_8_92164(_714389))], (3780 ^ _599268) ^ [_714577] : [tptpcol_8_92164(_714577), -(isa(_714577, c_tptpcol_8_92164))], (3786 ^ _599268) ^ [_714765] : [isa(_714765, c_tptpcol_9_92165), -(tptpcol_9_92165(_714765))], (3792 ^ _599268) ^ [_714953] : [tptpcol_9_92165(_714953), -(isa(_714953, c_tptpcol_9_92165))], (3798 ^ _599268) ^ [_715141] : [isa(_715141, c_tptpcol_1_1), -(tptpcol_1_1(_715141))], (3804 ^ _599268) ^ [_715329] : [tptpcol_1_1(_715329), -(isa(_715329, c_tptpcol_1_1))], (3810 ^ _599268) ^ [_715517] : [isa(_715517, c_tptpcol_2_2), -(tptpcol_2_2(_715517))], (3816 ^ _599268) ^ [_715705] : [tptpcol_2_2(_715705), -(isa(_715705, c_tptpcol_2_2))], (3822 ^ _599268) ^ [_715907, _715909] : [tptptypes_7_691(_715909, _715907), -(firstordercollection(_715907))], (3828 ^ _599268) ^ [_716115, _716117] : [tptptypes_7_691(_716117, _716115), -(firstordercollection(_716117))], (3834 ^ _599268) ^ [_716309] : [isa(_716309, c_tptpcol_11_26887), -(tptpcol_11_26887(_716309))], (3840 ^ _599268) ^ [_716497] : [tptpcol_11_26887(_716497), -(isa(_716497, c_tptpcol_11_26887))], (3846 ^ _599268) ^ [_716685] : [isa(_716685, c_tptpcol_12_26919), -(tptpcol_12_26919(_716685))], (3852 ^ _599268) ^ [_716873] : [tptpcol_12_26919(_716873), -(isa(_716873, c_tptpcol_12_26919))], (3858 ^ _599268) ^ [_717075, _717077] : [tptptypes_6_818(_717077, _717075), -(firstordercollection(_717075))], (3864 ^ _599268) ^ [_717283, _717285] : [tptptypes_6_818(_717285, _717283), -(firstordercollection(_717285))], (3870 ^ _599268) ^ [_717491, _717493] : [tptptypes_7_819(_717493, _717491), -(firstordercollection(_717491))], (3876 ^ _599268) ^ [_717699, _717701] : [tptptypes_7_819(_717701, _717699), -(firstordercollection(_717701))], (3882 ^ _599268) ^ [_717893] : [isa(_717893, c_correctivelensprescription), -(correctivelensprescription(_717893))], (3888 ^ _599268) ^ [_718081] : [correctivelensprescription(_718081), -(isa(_718081, c_correctivelensprescription))], (3894 ^ _599268) ^ [_718283, _718285] : [products(_718285, _718283), -(artifact(_718283))], (3900 ^ _599268) ^ [_718491, _718493] : [products(_718493, _718491), -(creationordestructionevent(_718493))], (3906 ^ _599268) ^ [_718685] : [isa(_718685, c_issuingaprescription), -(issuingaprescription(_718685))], (3912 ^ _599268) ^ [_718873] : [issuingaprescription(_718873), -(isa(_718873, c_issuingaprescription))], (3918 ^ _599268) ^ [_719074, _719076, _719078] : [-(natfunction(f_subcollectionofwithrelationtotypefn(_719078, _719076, _719074), c_subcollectionofwithrelationtotypefn))], (3920 ^ _599268) ^ [_719188, _719190, _719192] : [-(natargument(f_subcollectionofwithrelationtotypefn(_719192, _719190, _719188), n_1, _719192))], (3922 ^ _599268) ^ [_719303, _719305, _719307] : [-(natargument(f_subcollectionofwithrelationtotypefn(_719307, _719305, _719303), n_2, _719305))], (3924 ^ _599268) ^ [_719418, _719420, _719422] : [-(natargument(f_subcollectionofwithrelationtotypefn(_719422, _719420, _719418), n_3, _719418))], (3926 ^ _599268) ^ [_719533, _719535, _719537] : [-(collection(f_subcollectionofwithrelationtotypefn(_719537, _719535, _719533)))], (3928 ^ _599268) ^ [_719633] : [isa(_719633, f_subcollectionofwithrelationtotypefn(c_issuingaprescription, c_products, c_correctivelensprescription)), -(subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(_719633))], (3934 ^ _599268) ^ [_719821] : [subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(_719821), -(isa(_719821, f_subcollectionofwithrelationtotypefn(c_issuingaprescription, c_products, c_correctivelensprescription)))], (3940 ^ _599268) ^ [_720009] : [isa(_720009, c_mathematicalorcomputationalthing), -(mathematicalorcomputationalthing(_720009))], (3946 ^ _599268) ^ [_720197] : [mathematicalorcomputationalthing(_720197), -(isa(_720197, c_mathematicalorcomputationalthing))], (3952 ^ _599268) ^ [_720385] : [isa(_720385, c_tptpcol_10_118020), -(tptpcol_10_118020(_720385))], (3958 ^ _599268) ^ [_720573] : [tptpcol_10_118020(_720573), -(isa(_720573, c_tptpcol_10_118020))], (3964 ^ _599268) ^ [_720761] : [isa(_720761, c_tptpcol_11_118084), -(tptpcol_11_118084(_720761))], (3970 ^ _599268) ^ [_720949] : [tptpcol_11_118084(_720949), -(isa(_720949, c_tptpcol_11_118084))], (3976 ^ _599268) ^ [_721137] : [isa(_721137, c_terroristgroup), -(terroristgroup(_721137))], (3982 ^ _599268) ^ [_721325] : [terroristgroup(_721325), -(isa(_721325, c_terroristgroup))], (3988 ^ _599268) ^ [_721527, _721529] : [hasmembers(_721529, _721527), -(agent_generic(_721527))], (3994 ^ _599268) ^ [_721735, _721737] : [hasmembers(_721737, _721735), -(organization(_721737))], (4000 ^ _599268) ^ [_721929] : [isa(_721929, c_terrorist), -(terrorist(_721929))], (4006 ^ _599268) ^ [_722117] : [terrorist(_722117), -(isa(_722117, c_terrorist))], (4012 ^ _599268) ^ [_722318, _722320, _722322] : [-(natfunction(f_subcollectionofwithrelationfromtypefn(_722322, _722320, _722318), c_subcollectionofwithrelationfromtypefn))], (4014 ^ _599268) ^ [_722432, _722434, _722436] : [-(natargument(f_subcollectionofwithrelationfromtypefn(_722436, _722434, _722432), n_1, _722436))], (4016 ^ _599268) ^ [_722547, _722549, _722551] : [-(natargument(f_subcollectionofwithrelationfromtypefn(_722551, _722549, _722547), n_2, _722549))], (4018 ^ _599268) ^ [_722662, _722664, _722666] : [-(natargument(f_subcollectionofwithrelationfromtypefn(_722666, _722664, _722662), n_3, _722662))], (4020 ^ _599268) ^ [_722777, _722779, _722781] : [-(collection(f_subcollectionofwithrelationfromtypefn(_722781, _722779, _722777)))], (4022 ^ _599268) ^ [_722877] : [isa(_722877, f_subcollectionofwithrelationfromtypefn(c_terrorist, c_hasmembers, c_terroristgroup)), -(subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(_722877))], (4028 ^ _599268) ^ [_723065] : [subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(_723065), -(isa(_723065, f_subcollectionofwithrelationfromtypefn(c_terrorist, c_hasmembers, c_terroristgroup)))], (4034 ^ _599268) ^ [_723267, _723269] : [prettystring(_723269, _723267), -(controlcharacterfreestring(_723267))], (4040 ^ _599268) ^ [_723475, _723477] : [prettystring(_723477, _723475), -(thing(_723477))], (4046 ^ _599268) ^ [_723669] : [isa(_723669, c_tptpcol_0_0), -(tptpcol_0_0(_723669))], (4052 ^ _599268) ^ [_723857] : [tptpcol_0_0(_723857), -(isa(_723857, c_tptpcol_0_0))], (4058 ^ _599268) ^ [_724045] : [isa(_724045, c_geolevel_3), -(geolevel_3(_724045))], (4064 ^ _599268) ^ [_724233] : [geolevel_3(_724233), -(isa(_724233, c_geolevel_3))], (4070 ^ _599268) ^ [_724421] : [isa(_724421, c_tptpcol_4_24578), -(tptpcol_4_24578(_724421))], (4076 ^ _599268) ^ [_724609] : [tptpcol_4_24578(_724609), -(isa(_724609, c_tptpcol_4_24578))], (4082 ^ _599268) ^ [_724797] : [isa(_724797, c_tptpcol_5_24579), -(tptpcol_5_24579(_724797))], (4088 ^ _599268) ^ [_724985] : [tptpcol_5_24579(_724985), -(isa(_724985, c_tptpcol_5_24579))], (4094 ^ _599268) ^ [_725173] : [isa(_725173, c_tptpcol_5_106498), -(tptpcol_5_106498(_725173))], (4100 ^ _599268) ^ [_725361] : [tptpcol_5_106498(_725361), -(isa(_725361, c_tptpcol_5_106498))], (4106 ^ _599268) ^ [_725549] : [isa(_725549, c_tptpcol_12_109157), -(tptpcol_12_109157(_725549))], (4112 ^ _599268) ^ [_725737] : [tptpcol_12_109157(_725737), -(isa(_725737, c_tptpcol_12_109157))], (4118 ^ _599268) ^ [_725925] : [isa(_725925, c_tptpcol_13_109173), -(tptpcol_13_109173(_725925))], (4124 ^ _599268) ^ [_726113] : [tptpcol_13_109173(_726113), -(isa(_726113, c_tptpcol_13_109173))], (4130 ^ _599268) ^ [_726301] : [isa(_726301, c_mathematicalthing), -(mathematicalthing(_726301))], (4136 ^ _599268) ^ [_726489] : [mathematicalthing(_726489), -(isa(_726489, c_mathematicalthing))], (4142 ^ _599268) ^ [_726677] : [isa(_726677, c_setorcollection), -(setorcollection(_726677))], (4148 ^ _599268) ^ [_726865] : [setorcollection(_726865), -(isa(_726865, c_setorcollection))], (4154 ^ _599268) ^ [_727053] : [isa(_727053, c_tptpcol_11_18631), -(tptpcol_11_18631(_727053))], (4160 ^ _599268) ^ [_727241] : [tptpcol_11_18631(_727241), -(isa(_727241, c_tptpcol_11_18631))], (4166 ^ _599268) ^ [_727429] : [isa(_727429, c_tptpcol_12_18663), -(tptpcol_12_18663(_727429))], (4172 ^ _599268) ^ [_727617] : [tptpcol_12_18663(_727617), -(isa(_727617, c_tptpcol_12_18663))], (4178 ^ _599268) ^ [_727819, _727821] : [tptptypes_8_400(_727821, _727819), -(firstordercollection(_727819))], (4184 ^ _599268) ^ [_728027, _728029] : [tptptypes_8_400(_728029, _728027), -(firstordercollection(_728029))], (4190 ^ _599268) ^ [_728235, _728237] : [tptptypes_9_401(_728237, _728235), -(firstordercollection(_728235))], (4196 ^ _599268) ^ [_728443, _728445] : [tptptypes_9_401(_728445, _728443), -(firstordercollection(_728445))], (4202 ^ _599268) ^ [_728622] : [-(natfunction(f_tptpquantityfn_13(_728622), c_tptpquantityfn_13))], (4204 ^ _599268) ^ [_728702] : [-(natargument(f_tptpquantityfn_13(_728702), n_1, _728702))], (4206 ^ _599268) ^ [_728783] : [-(tptpquantity(f_tptpquantityfn_13(_728783)))], (4208 ^ _599268) ^ [_728891, _728893] : [borderson(_728893, _728891), -(geographicalregion(_728891))], (4214 ^ _599268) ^ [_729099, _729101] : [borderson(_729101, _729099), -(geographicalregion(_729101))], (4220 ^ _599268) ^ [_729307, _729309] : [borderson(_729309, _729307), -(borderson(_729307, _729309))], (4226 ^ _599268) ^ [_729487] : [borderson(_729487, _729487)], (4228 ^ _599268) ^ [_729580] : [isa(_729580, c_tptpcol_14_92264), -(tptpcol_14_92264(_729580))], (4234 ^ _599268) ^ [_729768] : [tptpcol_14_92264(_729768), -(isa(_729768, c_tptpcol_14_92264))], (4240 ^ _599268) ^ [_729956] : [isa(_729956, c_tptpcol_15_92268), -(tptpcol_15_92268(_729956))], (4246 ^ _599268) ^ [_730144] : [tptpcol_15_92268(_730144), -(isa(_730144, c_tptpcol_15_92268))], (4252 ^ _599268) ^ [_730332] : [isa(_730332, c_tptpcol_6_116738), -(tptpcol_6_116738(_730332))], (4258 ^ _599268) ^ [_730520] : [tptpcol_6_116738(_730520), -(isa(_730520, c_tptpcol_6_116738))], (4264 ^ _599268) ^ [_730722, _730724] : [tptptypes_5_387(_730724, _730722), -(firstordercollection(_730722))], (4270 ^ _599268) ^ [_730930, _730932] : [tptptypes_5_387(_730932, _730930), -(firstordercollection(_730932))], (4276 ^ _599268) ^ [_731138, _731140] : [tptptypes_6_388(_731140, _731138), -(firstordercollection(_731138))], (4282 ^ _599268) ^ [_731346, _731348] : [tptptypes_6_388(_731348, _731346), -(firstordercollection(_731348))], (4288 ^ _599268) ^ [_731540] : [isa(_731540, c_shavingrazor_manual), -(shavingrazor_manual(_731540))], (4294 ^ _599268) ^ [_731728] : [shavingrazor_manual(_731728), -(isa(_731728, c_shavingrazor_manual))], (4300 ^ _599268) ^ [_731916] : [isa(_731916, c_tptpcol_9_109060), -(tptpcol_9_109060(_731916))], (4306 ^ _599268) ^ [_732104] : [tptpcol_9_109060(_732104), -(isa(_732104, c_tptpcol_9_109060))], (4312 ^ _599268) ^ [_732292] : [isa(_732292, c_tptpcol_10_109061), -(tptpcol_10_109061(_732292))], (4318 ^ _599268) ^ [_732480] : [tptpcol_10_109061(_732480), -(isa(_732480, c_tptpcol_10_109061))], (4324 ^ _599268) ^ [_732668] : [isa(_732668, c_executionbyfiringsquad), -(executionbyfiringsquad(_732668))], (4330 ^ _599268) ^ [_732856] : [executionbyfiringsquad(_732856), -(isa(_732856, c_executionbyfiringsquad))], (4336 ^ _599268) ^ [] : [-(mtvisible(c_corecyclmt))], (4338 ^ _599268) ^ [_733097] : [isa(_733097, c_navypersonnel), -(navypersonnel(_733097))], (4344 ^ _599268) ^ [_733285] : [navypersonnel(_733285), -(isa(_733285, c_navypersonnel))], (4350 ^ _599268) ^ [_733473] : [isa(_733473, c_tptpcol_12_92262), -(tptpcol_12_92262(_733473))], (4356 ^ _599268) ^ [_733661] : [tptpcol_12_92262(_733661), -(isa(_733661, c_tptpcol_12_92262))], (4362 ^ _599268) ^ [_733849] : [isa(_733849, c_thing), -(thing(_733849))], (4368 ^ _599268) ^ [_734037] : [thing(_734037), -(isa(_734037, c_thing))], (4374 ^ _599268) ^ [_734225] : [isa(_734225, c_computerdataartifact), -(computerdataartifact(_734225))], (4380 ^ _599268) ^ [_734413] : [computerdataartifact(_734413), -(isa(_734413, c_computerdataartifact))], (4386 ^ _599268) ^ [_734601] : [isa(_734601, c_applicationcontext), -(applicationcontext(_734601))], (4392 ^ _599268) ^ [_734789] : [applicationcontext(_734789), -(isa(_734789, c_applicationcontext))], (4398 ^ _599268) ^ [_734991, _734993] : [inregion(_734993, _734991), -(spatialthing_nonsituational(_734991))], (4404 ^ _599268) ^ [_735199, _735201] : [inregion(_735201, _735199), -(spatialthing_nonsituational(_735201))], (4410 ^ _599268) ^ [_735421, _735423, _735425] : [-(inregion(_735425, _735421)), inregion(_735425, _735423), inregion(_735423, _735421)], (4420 ^ _599268) ^ [_735716] : [spatialthing_nonsituational(_735716), -(inregion(_735716, _735716))], (4426 ^ _599268) ^ [_735889] : [-(natfunction(f_tptpquantityfn_1(_735889), c_tptpquantityfn_1))], (4428 ^ _599268) ^ [_735969] : [-(natargument(f_tptpquantityfn_1(_735969), n_1, _735969))], (4430 ^ _599268) ^ [_736050] : [-(tptpquantity(f_tptpquantityfn_1(_736050)))], (4432 ^ _599268) ^ [_736144] : [isa(_736144, c_furpelt), -(furpelt(_736144))], (4438 ^ _599268) ^ [_736332] : [furpelt(_736332), -(isa(_736332, c_furpelt))], (4444 ^ _599268) ^ [_736534, _736536] : [tptpofobject(_736536, _736534), -(tptpquantity(_736534))], (4450 ^ _599268) ^ [_736742, _736744] : [tptpofobject(_736744, _736742), -(partiallytangible(_736744))], (4456 ^ _599268) ^ [_736964, _736966, _736968] : [relationallinstance(_736968, _736966, _736964), -(thing(_736964))], (4462 ^ _599268) ^ [_737194, _737196, _737198] : [relationallinstance(_737198, _737196, _737194), -(collection(_737196))], (4468 ^ _599268) ^ [_737424, _737426, _737428] : [relationallinstance(_737428, _737426, _737424), -(binarypredicate(_737428))], (4474 ^ _599268) ^ [_737626] : [isa(_737626, c_tptpcol_13_93766), -(tptpcol_13_93766(_737626))], (4480 ^ _599268) ^ [_737814] : [tptpcol_13_93766(_737814), -(isa(_737814, c_tptpcol_13_93766))], (4486 ^ _599268) ^ [_738002] : [isa(_738002, c_tptpcol_9_40196), -(tptpcol_9_40196(_738002))], (4492 ^ _599268) ^ [_738190] : [tptpcol_9_40196(_738190), -(isa(_738190, c_tptpcol_9_40196))], (4498 ^ _599268) ^ [_738378] : [isa(_738378, c_tptpcol_10_40324), -(tptpcol_10_40324(_738378))], (4504 ^ _599268) ^ [_738566] : [tptpcol_10_40324(_738566), -(isa(_738566, c_tptpcol_10_40324))], (4510 ^ _599268) ^ [_738754] : [isa(_738754, c_tptpcol_7_72707), -(tptpcol_7_72707(_738754))], (4516 ^ _599268) ^ [_738942] : [tptpcol_7_72707(_738942), -(isa(_738942, c_tptpcol_7_72707))], (4522 ^ _599268) ^ [_739130] : [isa(_739130, c_tptpcol_8_72708), -(tptpcol_8_72708(_739130))], (4528 ^ _599268) ^ [_739318] : [tptpcol_8_72708(_739318), -(isa(_739318, c_tptpcol_8_72708))], (4534 ^ _599268) ^ [_739506] : [isa(_739506, c_tptpcol_11_93764), -(tptpcol_11_93764(_739506))], (4540 ^ _599268) ^ [_739694] : [tptpcol_11_93764(_739694), -(isa(_739694, c_tptpcol_11_93764))], (4546 ^ _599268) ^ [_739882] : [isa(_739882, c_tptpcol_12_93765), -(tptpcol_12_93765(_739882))], (4552 ^ _599268) ^ [_740070] : [tptpcol_12_93765(_740070), -(isa(_740070, c_tptpcol_12_93765))], (4558 ^ _599268) ^ [_740258] : [isa(_740258, c_tptpcol_4_114689), -(tptpcol_4_114689(_740258))], (4564 ^ _599268) ^ [_740446] : [tptpcol_4_114689(_740446), -(isa(_740446, c_tptpcol_4_114689))], (4570 ^ _599268) ^ [_740634] : [isa(_740634, c_tptpcol_5_114690), -(tptpcol_5_114690(_740634))], (4576 ^ _599268) ^ [_740822] : [tptpcol_5_114690(_740822), -(isa(_740822, c_tptpcol_5_114690))], (4582 ^ _599268) ^ [_741010] : [isa(_741010, c_tptpcol_3_98305), -(tptpcol_3_98305(_741010))], (4588 ^ _599268) ^ [_741198] : [tptpcol_3_98305(_741198), -(isa(_741198, c_tptpcol_3_98305))], (4594 ^ _599268) ^ [_741386] : [isa(_741386, c_tptpcol_4_106497), -(tptpcol_4_106497(_741386))], (4600 ^ _599268) ^ [_741574] : [tptpcol_4_106497(_741574), -(isa(_741574, c_tptpcol_4_106497))], (4606 ^ _599268) ^ [_741789, _741791, _741793, _741795] : [-(natfunction(f_relationexistsallfn(_741795, _741793, _741791, _741789), c_relationexistsallfn))], (4608 ^ _599268) ^ [_741920, _741922, _741924, _741926] : [-(natargument(f_relationexistsallfn(_741926, _741924, _741922, _741920), n_1, _741926))], (4610 ^ _599268) ^ [_742052, _742054, _742056, _742058] : [-(natargument(f_relationexistsallfn(_742058, _742056, _742054, _742052), n_2, _742056))], (4612 ^ _599268) ^ [_742184, _742186, _742188, _742190] : [-(natargument(f_relationexistsallfn(_742190, _742188, _742186, _742184), n_3, _742186))], (4614 ^ _599268) ^ [_742316, _742318, _742320, _742322] : [-(natargument(f_relationexistsallfn(_742322, _742320, _742318, _742316), n_4, _742316))], (4616 ^ _599268) ^ [_742448, _742450, _742452, _742454] : [-(thing(f_relationexistsallfn(_742454, _742452, _742450, _742448)))], (4618 ^ _599268) ^ [_742565, _742567] : [resultisaarg(_742567, _742565), -(positiveinteger(_742565))], (4624 ^ _599268) ^ [_742773, _742775] : [resultisaarg(_742775, _742773), -(function_denotational(_742775))], (4630 ^ _599268) ^ [_742981, _742983] : [tptptypes_7_389(_742983, _742981), -(firstordercollection(_742981))], (4636 ^ _599268) ^ [_743189, _743191] : [tptptypes_7_389(_743191, _743189), -(firstordercollection(_743191))], (4642 ^ _599268) ^ [_743397, _743399] : [tptptypes_8_390(_743399, _743397), -(firstordercollection(_743397))], (4648 ^ _599268) ^ [_743605, _743607] : [tptptypes_8_390(_743607, _743605), -(firstordercollection(_743607))], (4654 ^ _599268) ^ [_743813, _743815] : [tptptypes_8_692(_743815, _743813), -(firstordercollection(_743813))], (4660 ^ _599268) ^ [_744021, _744023] : [tptptypes_8_692(_744023, _744021), -(firstordercollection(_744023))], (4666 ^ _599268) ^ [_744229, _744231] : [tptptypes_9_693(_744231, _744229), -(firstordercollection(_744229))], (4672 ^ _599268) ^ [_744437, _744439] : [tptptypes_9_693(_744439, _744437), -(firstordercollection(_744439))], (4678 ^ _599268) ^ [_744631] : [isa(_744631, c_tptpcol_11_40388), -(tptpcol_11_40388(_744631))], (4684 ^ _599268) ^ [_744819] : [tptpcol_11_40388(_744819), -(isa(_744819, c_tptpcol_11_40388))], (4690 ^ _599268) ^ [_745007] : [isa(_745007, c_marriagelicensedocument), -(marriagelicensedocument(_745007))], (4696 ^ _599268) ^ [_745195] : [marriagelicensedocument(_745195), -(isa(_745195, c_marriagelicensedocument))], (4702 ^ _599268) ^ [_745383] : [isa(_745383, c_tptpcol_1_65536), -(tptpcol_1_65536(_745383))], (4708 ^ _599268) ^ [_745571] : [tptpcol_1_65536(_745571), -(isa(_745571, c_tptpcol_1_65536))], (4714 ^ _599268) ^ [_745759] : [isa(_745759, c_tptpcol_2_98304), -(tptpcol_2_98304(_745759))], (4720 ^ _599268) ^ [_745947] : [tptpcol_2_98304(_745947), -(isa(_745947, c_tptpcol_2_98304))], (4726 ^ _599268) ^ [_746135] : [isa(_746135, c_tptpcol_10_92166), -(tptpcol_10_92166(_746135))], (4732 ^ _599268) ^ [_746323] : [tptpcol_10_92166(_746323), -(isa(_746323, c_tptpcol_10_92166))], (4738 ^ _599268) ^ [_746511] : [isa(_746511, c_tptpcol_11_92230), -(tptpcol_11_92230(_746511))], (4744 ^ _599268) ^ [_746699] : [tptpcol_11_92230(_746699), -(isa(_746699, c_tptpcol_11_92230))], (4750 ^ _599268) ^ [_746887] : [isa(_746887, c_orderingpredicate), -(orderingpredicate(_746887))], (4756 ^ _599268) ^ [_747075] : [orderingpredicate(_747075), -(isa(_747075, c_orderingpredicate))], (4762 ^ _599268) ^ [_747263] : [isa(_747263, c_tptpcol_9_18439), -(tptpcol_9_18439(_747263))], (4768 ^ _599268) ^ [_747451] : [tptpcol_9_18439(_747451), -(isa(_747451, c_tptpcol_9_18439))], (4774 ^ _599268) ^ [_747639] : [isa(_747639, c_tptpcol_10_18567), -(tptpcol_10_18567(_747639))], (4780 ^ _599268) ^ [_747827] : [tptpcol_10_18567(_747827), -(isa(_747827, c_tptpcol_10_18567))], (4786 ^ _599268) ^ [_748015] : [isa(_748015, c_tptpcol_2_65537), -(tptpcol_2_65537(_748015))], (4792 ^ _599268) ^ [_748203] : [tptpcol_2_65537(_748203), -(isa(_748203, c_tptpcol_2_65537))], (4798 ^ _599268) ^ [_748391] : [isa(_748391, c_tptpcol_3_81921), -(tptpcol_3_81921(_748391))], (4804 ^ _599268) ^ [_748579] : [tptpcol_3_81921(_748579), -(isa(_748579, c_tptpcol_3_81921))], (4810 ^ _599268) ^ [_748767] : [isa(_748767, c_artsupplies), -(artsupplies(_748767))], (4816 ^ _599268) ^ [_748955] : [artsupplies(_748955), -(isa(_748955, c_artsupplies))], (4822 ^ _599268) ^ [_749143] : [isa(_749143, c_enduringthing_localized), -(enduringthing_localized(_749143))], (4828 ^ _599268) ^ [_749331] : [enduringthing_localized(_749331), -(isa(_749331, c_enduringthing_localized))], (4834 ^ _599268) ^ [_749519] : [isa(_749519, c_location_underspecified), -(location_underspecified(_749519))], (4840 ^ _599268) ^ [_749707] : [location_underspecified(_749707), -(isa(_749707, c_location_underspecified))], (4846 ^ _599268) ^ [_749895] : [isa(_749895, c_trajector_underspecified), -(trajector_underspecified(_749895))], (4852 ^ _599268) ^ [_750083] : [trajector_underspecified(_750083), -(isa(_750083, c_trajector_underspecified))], (4858 ^ _599268) ^ [_750271] : [isa(_750271, c_individual), -(individual(_750271))], (4864 ^ _599268) ^ [_750459] : [individual(_750459), -(isa(_750459, c_individual))], (4870 ^ _599268) ^ [_750647] : [isa(_750647, c_partiallyintangibleindividual), -(partiallyintangibleindividual(_750647))], (4876 ^ _599268) ^ [_750835] : [partiallyintangibleindividual(_750835), -(isa(_750835, c_partiallyintangibleindividual))], (4882 ^ _599268) ^ [_751023] : [isa(_751023, c_tptpcol_10_22022), -(tptpcol_10_22022(_751023))], (4888 ^ _599268) ^ [_751211] : [tptpcol_10_22022(_751211), -(isa(_751211, c_tptpcol_10_22022))], (4894 ^ _599268) ^ [_751399] : [isa(_751399, c_tptpcol_11_22023), -(tptpcol_11_22023(_751399))], (4900 ^ _599268) ^ [_751587] : [tptpcol_11_22023(_751587), -(isa(_751587, c_tptpcol_11_22023))], (4906 ^ _599268) ^ [_751775] : [isa(_751775, c_tptpcol_5_20483), -(tptpcol_5_20483(_751775))], (4912 ^ _599268) ^ [_751963] : [tptpcol_5_20483(_751963), -(isa(_751963, c_tptpcol_5_20483))], (4918 ^ _599268) ^ [_752151] : [isa(_752151, c_tptpcol_13_72791), -(tptpcol_13_72791(_752151))], (4924 ^ _599268) ^ [_752339] : [tptpcol_13_72791(_752339), -(isa(_752339, c_tptpcol_13_72791))], (4930 ^ _599268) ^ [_752527] : [isa(_752527, c_tptpcol_14_72792), -(tptpcol_14_72792(_752527))], (4936 ^ _599268) ^ [_752715] : [tptpcol_14_72792(_752715), -(isa(_752715, c_tptpcol_14_72792))], (4942 ^ _599268) ^ [_752903] : [isa(_752903, c_ridgeline_topographical), -(ridgeline_topographical(_752903))], (4948 ^ _599268) ^ [_753091] : [ridgeline_topographical(_753091), -(isa(_753091, c_ridgeline_topographical))], (4954 ^ _599268) ^ [_753279] : [isa(_753279, c_tptpcol_4_16387), -(tptpcol_4_16387(_753279))], (4960 ^ _599268) ^ [_753467] : [tptpcol_4_16387(_753467), -(isa(_753467, c_tptpcol_4_16387))], (4966 ^ _599268) ^ [_753655] : [isa(_753655, c_tptpcol_5_16388), -(tptpcol_5_16388(_753655))], (4972 ^ _599268) ^ [_753843] : [tptpcol_5_16388(_753843), -(isa(_753843, c_tptpcol_5_16388))], (4978 ^ _599268) ^ [_754031] : [isa(_754031, c_tptpcol_8_22020), -(tptpcol_8_22020(_754031))], (4984 ^ _599268) ^ [_754219] : [tptpcol_8_22020(_754219), -(isa(_754219, c_tptpcol_8_22020))], (4990 ^ _599268) ^ [_754407] : [isa(_754407, c_tptpcol_9_22021), -(tptpcol_9_22021(_754407))], (4996 ^ _599268) ^ [_754595] : [tptpcol_9_22021(_754595), -(isa(_754595, c_tptpcol_9_22021))], (5002 ^ _599268) ^ [_754783] : [isa(_754783, c_transitivebinarypredicate), -(transitivebinarypredicate(_754783))], (5008 ^ _599268) ^ [_754971] : [transitivebinarypredicate(_754971), -(isa(_754971, c_transitivebinarypredicate))], (5014 ^ _599268) ^ [_755173, _755175] : [geographicalsubregions(_755175, _755173), -(geographicalregion(_755173))], (5020 ^ _599268) ^ [_755381, _755383] : [geographicalsubregions(_755383, _755381), -(geographicalregion(_755383))], (5026 ^ _599268) ^ [_755603, _755605, _755607] : [-(geographicalsubregions(_755607, _755603)), geographicalsubregions(_755607, _755605), geographicalsubregions(_755605, _755603)], (5036 ^ _599268) ^ [_755898] : [geographicalregion(_755898), -(geographicalsubregions(_755898, _755898))], (5042 ^ _599268) ^ [_756086] : [isa(_756086, c_tptpcol_12_40420), -(tptpcol_12_40420(_756086))], (5048 ^ _599268) ^ [_756274] : [tptpcol_12_40420(_756274), -(isa(_756274, c_tptpcol_12_40420))], (5054 ^ _599268) ^ [_756462] : [isa(_756462, c_tptpcol_13_40421), -(tptpcol_13_40421(_756462))], (5060 ^ _599268) ^ [_756650] : [tptpcol_13_40421(_756650), -(isa(_756650, c_tptpcol_13_40421))], (5066 ^ _599268) ^ [_756838] : [isa(_756838, c_tptpcol_6_92162), -(tptpcol_6_92162(_756838))], (5072 ^ _599268) ^ [_757026] : [tptpcol_6_92162(_757026), -(isa(_757026, c_tptpcol_6_92162))], (5078 ^ _599268) ^ [_757214] : [isa(_757214, c_tptpcol_7_93186), -(tptpcol_7_93186(_757214))], (5084 ^ _599268) ^ [_757402] : [tptpcol_7_93186(_757402), -(isa(_757402, c_tptpcol_7_93186))], (5090 ^ _599268) ^ [_757604, _757606] : [most(_757606, _757604), -(setorcollection(_757604))], (5096 ^ _599268) ^ [_757812, _757814] : [most(_757814, _757812), -(setorcollection(_757812))], (5102 ^ _599268) ^ [_758020, _758022] : [most(_758022, _758020), -(setorcollection(_758022))], (5108 ^ _599268) ^ [_758228, _758230] : [most(_758230, _758228), -(setorcollection(_758230))], (5114 ^ _599268) ^ [_758422] : [setorcollection(_758422), -(most(_758422, _758422))], (5120 ^ _599268) ^ [_758610] : [setorcollection(_758610), -(most(_758610, _758610))], (5126 ^ _599268) ^ [_758826, _758828, _758830] : [-(most(_758830, _758826)), most(_758830, _758828), subsetof(_758828, _758826)], (5136 ^ _599268) ^ [_759149, _759151, _759153] : [-(most(_759153, _759149)), most(_759153, _759151), subsetof(_759151, _759149)], (5146 ^ _599268) ^ [_759458, _759460] : [subsetof(_759460, _759458), -(setorcollection(_759458))], (5152 ^ _599268) ^ [_759666, _759668] : [subsetof(_759668, _759666), -(setorcollection(_759668))], (5158 ^ _599268) ^ [_759888, _759890, _759892] : [-(subsetof(_759892, _759888)), subsetof(_759892, _759890), subsetof(_759890, _759888)], (5168 ^ _599268) ^ [_760183] : [setorcollection(_760183), -(subsetof(_760183, _760183))], (5174 ^ _599268) ^ [_760399, _760401, _760403] : [-(subsetof(_760399, _760401)), subsetof(_760403, _760401), subsetof(_760399, _760403)], (5184 ^ _599268) ^ [_760722, _760724, _760726] : [-(subsetof(_760726, _760722)), subsetof(_760726, _760724), subsetof(_760724, _760722)], (5194 ^ _599268) ^ [_761045, _761047, _761049] : [-(subsetof(_761049, _761045)), subsetof(_761049, _761047), subsetof(_761047, _761045)], (5204 ^ _599268) ^ [_761354, _761356] : [genlpreds(_761356, _761354), -(predicate(_761354))], (5210 ^ _599268) ^ [_761562, _761564] : [genlpreds(_761564, _761562), -(predicate(_761562))], (5216 ^ _599268) ^ [_761770, _761772] : [genlpreds(_761772, _761770), -(predicate(_761772))], (5222 ^ _599268) ^ [_761978, _761980] : [genlpreds(_761980, _761978), -(predicate(_761980))], (5228 ^ _599268) ^ [_762200, _762202, _762204] : [-(genlpreds(_762204, _762200)), genlpreds(_762204, _762202), genlpreds(_762202, _762200)], (5238 ^ _599268) ^ [_762495] : [predicate(_762495), -(genlpreds(_762495, _762495))], (5244 ^ _599268) ^ [_762683] : [predicate(_762683), -(genlpreds(_762683, _762683))], (5250 ^ _599268) ^ [_762885, _762887] : [genlinverse(_762887, _762885), -(binarypredicate(_762885))], (5256 ^ _599268) ^ [_763093, _763095] : [genlinverse(_763095, _763093), -(binarypredicate(_763095))], (5262 ^ _599268) ^ [_763315, _763317, _763319] : [-(genlinverse(_763315, _763317)), genlinverse(_763319, _763317), genlpreds(_763315, _763319)], (5272 ^ _599268) ^ [_763638, _763640, _763642] : [-(genlinverse(_763642, _763638)), genlinverse(_763642, _763640), genlpreds(_763640, _763638)], (5282 ^ _599268) ^ [] : [-(mtvisible(c_basekb))], (5284 ^ _599268) ^ [_763986] : [isa(_763986, c_microtheory), -(microtheory(_763986))], (5290 ^ _599268) ^ [_764174] : [microtheory(_764174), -(isa(_764174, c_microtheory))], (5296 ^ _599268) ^ [_764347] : [-(natfunction(f_urlfn(_764347), c_urlfn))], (5298 ^ _599268) ^ [_764427] : [-(natargument(f_urlfn(_764427), n_1, _764427))], (5300 ^ _599268) ^ [_764508] : [-(uniformresourcelocator(f_urlfn(_764508)))], (5302 ^ _599268) ^ [_764587] : [-(natfunction(f_urlreferentfn(_764587), c_urlreferentfn))], (5304 ^ _599268) ^ [_764667] : [-(natargument(f_urlreferentfn(_764667), n_1, _764667))], (5306 ^ _599268) ^ [_764748] : [-(computerdataartifact(f_urlreferentfn(_764748)))], (5308 ^ _599268) ^ [_764841, _764843] : [-(natfunction(f_contentmtofcdafromeventfn(_764843, _764841), c_contentmtofcdafromeventfn))], (5310 ^ _599268) ^ [_764938, _764940] : [-(natargument(f_contentmtofcdafromeventfn(_764940, _764938), n_1, _764940))], (5312 ^ _599268) ^ [_765036, _765038] : [-(natargument(f_contentmtofcdafromeventfn(_765038, _765036), n_2, _765036))], (5314 ^ _599268) ^ [_765134, _765136] : [-(microtheory(f_contentmtofcdafromeventfn(_765136, _765134)))], (5316 ^ _599268) ^ [_765245, _765247] : [isa(_765247, _765245), -(collection(_765245))], (5322 ^ _599268) ^ [_765453, _765455] : [isa(_765455, _765453), -(collection(_765453))], (5328 ^ _599268) ^ [_765661, _765663] : [isa(_765663, _765661), -(thing(_765663))], (5334 ^ _599268) ^ [_765869, _765871] : [isa(_765871, _765869), -(thing(_765871))], (5340 ^ _599268) ^ [_766091, _766093, _766095] : [-(isa(_766095, _766091)), isa(_766095, _766093), genls(_766093, _766091)], (5350 ^ _599268) ^ [_766386] : [isa(_766386, c_inanimateobject), -(inanimateobject(_766386))], (5356 ^ _599268) ^ [_766574] : [inanimateobject(_766574), -(isa(_766574, c_inanimateobject))], (5362 ^ _599268) ^ [_766762] : [isa(_766762, c_tptpcol_9_72709), -(tptpcol_9_72709(_766762))], (5368 ^ _599268) ^ [_766950] : [tptpcol_9_72709(_766950), -(isa(_766950, c_tptpcol_9_72709))], (5374 ^ _599268) ^ [_767138] : [isa(_767138, c_tptpcol_10_72710), -(tptpcol_10_72710(_767138))], (5380 ^ _599268) ^ [_767326] : [tptpcol_10_72710(_767326), -(isa(_767326, c_tptpcol_10_72710))], (5386 ^ _599268) ^ [_767514] : [isa(_767514, c_tptpcol_14_40429), -(tptpcol_14_40429(_767514))], (5392 ^ _599268) ^ [_767702] : [tptpcol_14_40429(_767702), -(isa(_767702, c_tptpcol_14_40429))], (5398 ^ _599268) ^ [_767890] : [isa(_767890, c_tptpcol_15_40430), -(tptpcol_15_40430(_767890))], (5404 ^ _599268) ^ [_768078] : [tptpcol_15_40430(_768078), -(isa(_768078, c_tptpcol_15_40430))], (5410 ^ _599268) ^ [_768280, _768282] : [genls(_768282, _768280), -(collection(_768280))], (5416 ^ _599268) ^ [_768488, _768490] : [genls(_768490, _768488), -(collection(_768488))], (5422 ^ _599268) ^ [_768696, _768698] : [genls(_768698, _768696), -(collection(_768698))], (5428 ^ _599268) ^ [_768904, _768906] : [genls(_768906, _768904), -(collection(_768906))], (5434 ^ _599268) ^ [_769126, _769128, _769130] : [-(genls(_769130, _769126)), genls(_769130, _769128), genls(_769128, _769126)], (5444 ^ _599268) ^ [_769421] : [collection(_769421), -(genls(_769421, _769421))], (5450 ^ _599268) ^ [_769609] : [collection(_769609), -(genls(_769609, _769609))], (5456 ^ _599268) ^ [_769825, _769827, _769829] : [-(genls(_769825, _769827)), genls(_769829, _769827), genls(_769825, _769829)], (5466 ^ _599268) ^ [_770148, _770150, _770152] : [-(genls(_770152, _770148)), genls(_770152, _770150), genls(_770150, _770148)], (5476 ^ _599268) ^ [_770443] : [isa(_770443, c_partiallytangible), -(partiallytangible(_770443))], (5482 ^ _599268) ^ [_770631] : [partiallytangible(_770631), -(isa(_770631, c_partiallytangible))], (5488 ^ _599268) ^ [_770819] : [isa(_770819, c_intangible), -(intangible(_770819))], (5494 ^ _599268) ^ [_771007] : [intangible(_771007), -(isa(_771007, c_intangible))], (5500 ^ _599268) ^ [_771209, _771211] : [disjointwith(_771211, _771209), -(collection(_771209))], (5506 ^ _599268) ^ [_771417, _771419] : [disjointwith(_771419, _771417), -(collection(_771419))], (5512 ^ _599268) ^ [_771625, _771627] : [disjointwith(_771627, _771625), -(disjointwith(_771625, _771627))], (5518 ^ _599268) ^ [_771849, _771851, _771853] : [-(disjointwith(_771853, _771849)), disjointwith(_771853, _771851), genls(_771849, _771851)], (5528 ^ _599268) ^ [_772172, _772174, _772176] : [-(disjointwith(_772172, _772174)), disjointwith(_772176, _772174), genls(_772172, _772176)], (5538 ^ _599268) ^ [_772481, _772483] : [-(mtvisible(_772481)), mtvisible(_772483), genlmt(_772483, _772481)], (5548 ^ _599268) ^ [_772776, _772778] : [genlmt(_772778, _772776), -(microtheory(_772776))], (5554 ^ _599268) ^ [_772984, _772986] : [genlmt(_772986, _772984), -(microtheory(_772984))], (5560 ^ _599268) ^ [_773192, _773194] : [genlmt(_773194, _773192), -(microtheory(_773194))], (5566 ^ _599268) ^ [_773400, _773402] : [genlmt(_773402, _773400), -(microtheory(_773402))], (5572 ^ _599268) ^ [_773622, _773624, _773626] : [-(genlmt(_773626, _773622)), genlmt(_773626, _773624), genlmt(_773624, _773622)], (5582 ^ _599268) ^ [_773917] : [microtheory(_773917), -(genlmt(_773917, _773917))], (5594 ^ _599268) ^ [] : [-(mtvisible(c_universalvocabularymt))], (5588 ^ _599268) ^ [_774105] : [microtheory(_774105), -(genlmt(_774105, _774105))]], input).
% 0.42/1.38  ncf('1',plain,[tptpofobject(c_theprototypicalfurpelt, f_tptpquantityfn_1(n_328))],start(5598 ^ 0)).
% 0.42/1.38  ncf('1.1',plain,[-(tptpofobject(c_theprototypicalfurpelt, f_tptpquantityfn_1(n_328))), mtvisible(c_tptp_spindleheadmt), furpelt(c_theprototypicalfurpelt)],extension(308 ^ 1,bind([[_608322], [c_theprototypicalfurpelt]]))).
% 0.42/1.38  ncf('1.1.1',plain,[-(mtvisible(c_tptp_spindleheadmt)), mtvisible(c_tptp_member2356_mt), genlmt(c_tptp_member2356_mt, c_tptp_spindleheadmt)],extension(5538 ^ 2,bind([[_772481, _772483], [c_tptp_spindleheadmt, c_tptp_member2356_mt]]))).
% 0.42/1.38  ncf('1.1.1.1',plain,[-(mtvisible(c_tptp_member2356_mt))],extension(5596 ^ 3)).
% 0.42/1.38  ncf('1.1.1.2',plain,[-(genlmt(c_tptp_member2356_mt, c_tptp_spindleheadmt))],extension(1740 ^ 3)).
% 0.42/1.38  ncf('1.1.2',plain,[-(furpelt(c_theprototypicalfurpelt))],extension(1016 ^ 2)).
% 0.42/1.38  %-----------------------------------------------------
% 0.42/1.38  End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------