%------------------------------------------------------------------------------ % File : CSR002+1 : TPTP v6.4.0. Released v3.4.0. % Domain : Common Sense Reasoning % Axioms : 1131 axioms from Cyc % Version : Especial. % English : % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem % Source : [RS+] % Names : % Status : Satisfiable % Syntax : Number of formulae : 1131 ( 346 unit) % Number of atoms : 1964 ( 0 equality) % Maximal formula depth : 7 ( 3 average) % Number of connectives : 842 ( 9 ~ ; 0 |; 54 &) % ( 0 <=>; 779 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 269 ( 0 propositional; 1-3 arity) % Number of functors : 413 ( 396 constant; 0-4 arity) % Number of variables : 1121 ( 0 singleton;1121 !; 0 ?) % Maximal term depth : 4 ( 1 average) % SPC : % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin, % TX, USA. All rights reserved. % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc., % Austin, TX, USA. All rights reserved. % : A superset of CSR002+0.ax % : It is known that there are some duplicate axioms. %------------------------------------------------------------------------------ % Cyc Assertion #2463166: fof(ax1_1,axiom,( genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt) )). % Cyc Assertion #670314: fof(ax1_2,axiom,( disjointwith(c_intangible,c_partiallytangible) )). fof(ax1_3,axiom,( ! [OBJ] : ~ ( intangible(OBJ) & partiallytangible(OBJ) ) )). % Cyc Assertion #1923815: fof(ax1_4,axiom,( genls(c_tptpcol_15_40430,c_tptpcol_14_40429) )). fof(ax1_5,axiom,( ! [OBJ] : ( tptpcol_15_40430(OBJ) => tptpcol_14_40429(OBJ) ) )). % Cyc Assertion #2004520: fof(ax1_6,axiom,( genls(c_tptpcol_10_72710,c_tptpcol_9_72709) )). fof(ax1_7,axiom,( ! [OBJ] : ( tptpcol_10_72710(OBJ) => tptpcol_9_72709(OBJ) ) )). % Cyc Assertion #1694819: fof(ax1_8,axiom,( genls(c_inanimateobject,c_partiallytangible) )). fof(ax1_9,axiom,( ! [OBJ] : ( inanimateobject(OBJ) => partiallytangible(OBJ) ) )). % Cyc Assertion #1443960: fof(ax1_10,axiom,( microtheory(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3)) )). % Cyc Assertion #831913: fof(ax1_11,axiom,( ! [SPECPRED,PRED,GENLPRED] : ( ( genlinverse(SPECPRED,PRED) & genlinverse(PRED,GENLPRED) ) => genlpreds(SPECPRED,GENLPRED) ) )). % Cyc Assertion #606520: fof(ax1_12,axiom,( genlpreds(c_subsetof,c_most) )). fof(ax1_13,axiom,( ! [ARG1,ARG2] : ( subsetof(ARG1,ARG2) => most(ARG1,ARG2) ) )). % Cyc Assertion #2055711: fof(ax1_14,axiom,( genls(c_tptpcol_7_93186,c_tptpcol_6_92162) )). fof(ax1_15,axiom,( ! [OBJ] : ( tptpcol_7_93186(OBJ) => tptpcol_6_92162(OBJ) ) )). % Cyc Assertion #1923794: fof(ax1_16,axiom,( genls(c_tptpcol_13_40421,c_tptpcol_12_40420) )). fof(ax1_17,axiom,( ! [OBJ] : ( tptpcol_13_40421(OBJ) => tptpcol_12_40420(OBJ) ) )). % Cyc Assertion #2491146: fof(ax1_18,axiom, ( mtvisible(c_tptpgeo_member2_mt) => geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2) )). % Cyc Assertion #455528: fof(ax1_19,axiom,( transitivebinarypredicate(c_genls) )). % Cyc Assertion #2181376: fof(ax1_20,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt) )). % Cyc Assertion #1877798: fof(ax1_21,axiom,( genls(c_tptpcol_9_22021,c_tptpcol_8_22020) )). fof(ax1_22,axiom,( ! [OBJ] : ( tptpcol_9_22021(OBJ) => tptpcol_8_22020(OBJ) ) )). % Cyc Assertion #1863719: fof(ax1_23,axiom,( genls(c_tptpcol_5_16388,c_tptpcol_4_16387) )). fof(ax1_24,axiom,( ! [OBJ] : ( tptpcol_5_16388(OBJ) => tptpcol_4_16387(OBJ) ) )). % Cyc Assertion #2352863: fof(ax1_25,axiom, ( mtvisible(c_cyclistsmt) => ridgeline_topographical(c_tptpridgeline_topographical) )). % Cyc Assertion #2004722: fof(ax1_26,axiom,( genls(c_tptpcol_14_72792,c_tptpcol_13_72791) )). fof(ax1_27,axiom,( ! [OBJ] : ( tptpcol_14_72792(OBJ) => tptpcol_13_72791(OBJ) ) )). % Cyc Assertion #1873956: fof(ax1_28,axiom,( genls(c_tptpcol_5_20483,c_tptpcol_4_16387) )). fof(ax1_29,axiom,( ! [OBJ] : ( tptpcol_5_20483(OBJ) => tptpcol_4_16387(OBJ) ) )). % Cyc Assertion #1877802: fof(ax1_30,axiom,( genls(c_tptpcol_11_22023,c_tptpcol_10_22022) )). fof(ax1_31,axiom,( ! [OBJ] : ( tptpcol_11_22023(OBJ) => tptpcol_10_22022(OBJ) ) )). % Cyc Assertion #1117993: fof(ax1_32,axiom,( genls(c_partiallyintangibleindividual,c_individual) )). fof(ax1_33,axiom,( ! [OBJ] : ( partiallyintangibleindividual(OBJ) => individual(OBJ) ) )). % Cyc Assertion #2183755: fof(ax1_34,axiom,( genlmt(c_tptp_member3205_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #1785295: fof(ax1_35,axiom,( genlmt(c_peopledatamt,c_unitedstatessociallifemt) )). % Cyc Assertion #638580: fof(ax1_36,axiom,( genls(c_trajector_underspecified,c_location_underspecified) )). fof(ax1_37,axiom,( ! [OBJ] : ( trajector_underspecified(OBJ) => location_underspecified(OBJ) ) )). % Cyc Assertion #1610132: fof(ax1_38,axiom,( genls(c_partiallytangible,c_enduringthing_localized) )). fof(ax1_39,axiom,( ! [OBJ] : ( partiallytangible(OBJ) => enduringthing_localized(OBJ) ) )). % Cyc Assertion #2410426: fof(ax1_40,axiom, ( mtvisible(c_cyclistsmt) => artsupplies(c_tptpartsupplies) )). % Cyc Assertion #2027552: fof(ax1_41,axiom,( genls(c_tptpcol_3_81921,c_tptpcol_2_65537) )). fof(ax1_42,axiom,( ! [OBJ] : ( tptpcol_3_81921(OBJ) => tptpcol_2_65537(OBJ) ) )). % Cyc Assertion #1869163: fof(ax1_43,axiom,( genls(c_tptpcol_10_18567,c_tptpcol_9_18439) )). fof(ax1_44,axiom,( ! [OBJ] : ( tptpcol_10_18567(OBJ) => tptpcol_9_18439(OBJ) ) )). % Cyc Assertion #697202: fof(ax1_45,axiom,( genls(c_orderingpredicate,c_transitivebinarypredicate) )). fof(ax1_46,axiom,( ! [OBJ] : ( orderingpredicate(OBJ) => transitivebinarypredicate(OBJ) ) )). % Cyc Assertion #2053319: fof(ax1_47,axiom,( genls(c_tptpcol_11_92230,c_tptpcol_10_92166) )). fof(ax1_48,axiom,( ! [OBJ] : ( tptpcol_11_92230(OBJ) => tptpcol_10_92166(OBJ) ) )). % Cyc Assertion #2068510: fof(ax1_49,axiom,( genls(c_tptpcol_2_98304,c_tptpcol_1_65536) )). fof(ax1_50,axiom,( ! [OBJ] : ( tptpcol_2_98304(OBJ) => tptpcol_1_65536(OBJ) ) )). % Cyc Assertion #2401366: fof(ax1_51,axiom, ( mtvisible(c_tptp_member3356_mt) => marriagelicensedocument(c_tptpmarriagelicensedocument) )). % Cyc Assertion #1028120: fof(ax1_52,axiom,( genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt) )). % Cyc Assertion #1545258: fof(ax1_53,axiom,( genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt) )). % Cyc Assertion #1923792: fof(ax1_54,axiom,( genls(c_tptpcol_12_40420,c_tptpcol_11_40388) )). fof(ax1_55,axiom,( ! [OBJ] : ( tptpcol_12_40420(OBJ) => tptpcol_11_40388(OBJ) ) )). % Cyc Assertion #2155285: fof(ax1_56,axiom,( genlpreds(c_tptptypes_9_693,c_tptptypes_8_692) )). fof(ax1_57,axiom,( ! [ARG1,ARG2] : ( tptptypes_9_693(ARG1,ARG2) => tptptypes_8_692(ARG1,ARG2) ) )). % Cyc Assertion #964779: fof(ax1_58,axiom,( genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt) )). % Cyc Assertion #518539: fof(ax1_59,axiom,( genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric) )). % Cyc Assertion #2153164: fof(ax1_60,axiom,( genlpreds(c_tptptypes_8_390,c_tptptypes_7_389) )). fof(ax1_61,axiom,( ! [ARG1,ARG2] : ( tptptypes_8_390(ARG1,ARG2) => tptptypes_7_389(ARG1,ARG2) ) )). % Cyc Assertion #829544: fof(ax1_62,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33),c_machinelearningspindleheadmt) )). % Cyc Assertion #2463162: fof(ax1_63,axiom,( genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt) )). % Cyc Assertion #976441: fof(ax1_64,axiom,( ! [TERM,INDEPCOL,PRED,DEPCOL] : ( ( isa(TERM,INDEPCOL) & relationexistsall(PRED,DEPCOL,INDEPCOL) ) => isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL) ) )). fof(ax1_65,axiom,( resultisaarg(c_relationexistsallfn,n_3) )). % Cyc Assertion #583547: fof(ax1_66,axiom,( genlmt(c_nooescapearchitecturemt,c_organizationdatamt) )). % Cyc Assertion #1290103: fof(ax1_67,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwfuntriviacomplayquizcfmqid60926origin)),c_translation_0_885),c_machinelearningspindleheadmt) )). % Cyc Assertion #2088991: fof(ax1_68,axiom,( genls(c_tptpcol_4_106497,c_tptpcol_3_98305) )). fof(ax1_69,axiom,( ! [OBJ] : ( tptpcol_4_106497(OBJ) => tptpcol_3_98305(OBJ) ) )). % Cyc Assertion #2109473: fof(ax1_70,axiom,( genls(c_tptpcol_5_114690,c_tptpcol_4_114689) )). fof(ax1_71,axiom,( ! [OBJ] : ( tptpcol_5_114690(OBJ) => tptpcol_4_114689(OBJ) ) )). % Cyc Assertion #2057155: fof(ax1_72,axiom,( genls(c_tptpcol_12_93765,c_tptpcol_11_93764) )). fof(ax1_73,axiom,( ! [OBJ] : ( tptpcol_12_93765(OBJ) => tptpcol_11_93764(OBJ) ) )). % Cyc Assertion #2004516: fof(ax1_74,axiom,( genls(c_tptpcol_8_72708,c_tptpcol_7_72707) )). fof(ax1_75,axiom,( ! [OBJ] : ( tptpcol_8_72708(OBJ) => tptpcol_7_72707(OBJ) ) )). % Cyc Assertion #1923554: fof(ax1_76,axiom,( genls(c_tptpcol_10_40324,c_tptpcol_9_40196) )). fof(ax1_77,axiom,( ! [OBJ] : ( tptpcol_10_40324(OBJ) => tptpcol_9_40196(OBJ) ) )). % Cyc Assertion #2057157: fof(ax1_78,axiom,( genls(c_tptpcol_13_93766,c_tptpcol_12_93765) )). fof(ax1_79,axiom,( ! [OBJ] : ( tptpcol_13_93766(OBJ) => tptpcol_12_93765(OBJ) ) )). % Cyc Assertion #2357194: fof(ax1_80,axiom,( ! [INS] : ( ( mtvisible(c_tptp_spindleheadmt) & furpelt(INS) ) => tptpofobject(INS,f_tptpquantityfn_1(n_328)) ) )). fof(ax1_81,axiom, ( mtvisible(c_tptp_spindleheadmt) => relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328)) )). % Cyc Assertion #2502810: fof(ax1_82,axiom, ( mtvisible(c_tptpgeo_member7_mt) => inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74) )). % Cyc Assertion #438063: fof(ax1_83,axiom,( applicationcontext(c_wamt_evalinitial_p14) )). % Cyc Assertion #385707: fof(ax1_84,axiom,( computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) )). % Cyc Assertion #753566: fof(ax1_85,axiom,( genls(c_location_underspecified,c_thing) )). fof(ax1_86,axiom,( ! [OBJ] : ( location_underspecified(OBJ) => thing(OBJ) ) )). % Cyc Assertion #1103756: fof(ax1_87,axiom,( genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt) )). % Cyc Assertion #1795454: fof(ax1_88,axiom,( genlmt(c_patterndetectormt,c_basekb) )). % Cyc Assertion #2053398: fof(ax1_89,axiom,( genls(c_tptpcol_12_92262,c_tptpcol_11_92230) )). fof(ax1_90,axiom,( ! [OBJ] : ( tptpcol_12_92262(OBJ) => tptpcol_11_92230(OBJ) ) )). % Cyc Assertion #2418340: fof(ax1_91,axiom, ( mtvisible(c_tptp_member1672_mt) => navypersonnel(c_tptpnavypersonnel_3) )). % Cyc Assertion #954903: fof(ax1_92,axiom,( genlmt(c_universalvocabularymt,c_corecyclmt) )). % Cyc Assertion #2182259: fof(ax1_93,axiom,( genlmt(c_tptp_member2831_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2246811: fof(ax1_94,axiom,( executionbyfiringsquad(c_tptpexecutionbyfiringsquad_90) )). % Cyc Assertion #2095397: fof(ax1_95,axiom,( genls(c_tptpcol_10_109061,c_tptpcol_9_109060) )). fof(ax1_96,axiom,( ! [OBJ] : ( tptpcol_10_109061(OBJ) => tptpcol_9_109060(OBJ) ) )). % Cyc Assertion #2207952: fof(ax1_97,axiom,( shavingrazor_manual(c_theprototypicalshavingrazor_manual) )). % Cyc Assertion #2153150: fof(ax1_98,axiom,( genlpreds(c_tptptypes_6_388,c_tptptypes_5_387) )). fof(ax1_99,axiom,( ! [ARG1,ARG2] : ( tptptypes_6_388(ARG1,ARG2) => tptptypes_5_387(ARG1,ARG2) ) )). % Cyc Assertion #2114592: fof(ax1_100,axiom,( genls(c_tptpcol_6_116738,c_tptpcol_5_114690) )). fof(ax1_101,axiom,( ! [OBJ] : ( tptpcol_6_116738(OBJ) => tptpcol_5_114690(OBJ) ) )). % Cyc Assertion #2053411: fof(ax1_102,axiom,( genls(c_tptpcol_15_92268,c_tptpcol_14_92264) )). fof(ax1_103,axiom,( ! [OBJ] : ( tptpcol_15_92268(OBJ) => tptpcol_14_92264(OBJ) ) )). % Cyc Assertion #2515333: fof(ax1_104,axiom, ( mtvisible(c_tptpgeo_member5_mt) => borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47) )). % Cyc Assertion #2359224: fof(ax1_105,axiom,( ! [INS] : ( ( mtvisible(c_tptp_member235_mt) & ridgeline_topographical(INS) ) => tptpofobject(INS,f_tptpquantityfn_13(n_468)) ) )). fof(ax1_106,axiom, ( mtvisible(c_tptp_member235_mt) => relationallinstance(c_tptpofobject,c_ridgeline_topographical,f_tptpquantityfn_13(n_468)) )). % Cyc Assertion #2153241: fof(ax1_107,axiom,( genlinverse(c_tptptypes_9_401,c_tptptypes_8_400) )). fof(ax1_108,axiom,( ! [ARG1,ARG2] : ( tptptypes_9_401(ARG1,ARG2) => tptptypes_8_400(ARG2,ARG1) ) )). % Cyc Assertion #1869401: fof(ax1_109,axiom,( genls(c_tptpcol_12_18663,c_tptpcol_11_18631) )). fof(ax1_110,axiom,( ! [OBJ] : ( tptpcol_12_18663(OBJ) => tptpcol_11_18631(OBJ) ) )). % Cyc Assertion #294201: fof(ax1_111,axiom,( genls(c_setorcollection,c_mathematicalthing) )). fof(ax1_112,axiom,( ! [OBJ] : ( setorcollection(OBJ) => mathematicalthing(OBJ) ) )). % Cyc Assertion #2095674: fof(ax1_113,axiom,( genls(c_tptpcol_13_109173,c_tptpcol_12_109157) )). fof(ax1_114,axiom,( ! [OBJ] : ( tptpcol_13_109173(OBJ) => tptpcol_12_109157(OBJ) ) )). % Cyc Assertion #1706514: fof(ax1_115,axiom,( genlmt(c_cyclistsmt,c_calendarsmt) )). % Cyc Assertion #2088993: fof(ax1_116,axiom,( genls(c_tptpcol_5_106498,c_tptpcol_4_106497) )). fof(ax1_117,axiom,( ! [OBJ] : ( tptpcol_5_106498(OBJ) => tptpcol_4_106497(OBJ) ) )). % Cyc Assertion #1884196: fof(ax1_118,axiom,( genls(c_tptpcol_5_24579,c_tptpcol_4_24578) )). fof(ax1_119,axiom,( ! [OBJ] : ( tptpcol_5_24579(OBJ) => tptpcol_4_24578(OBJ) ) )). % Cyc Assertion #849068: fof(ax1_120,axiom,( transitivebinarypredicate(c_genlpreds) )). % Cyc Assertion #2477332: fof(ax1_121,axiom, ( mtvisible(c_worldgeographymt) => geolevel_3(c_georegion_l3_x4_y13) )). % Cyc Assertion #2510694: fof(ax1_122,axiom, ( mtvisible(c_tptpgeo_member7_mt) => borderson(c_georegion_l4_x27_y64,c_georegion_l4_x27_y65) )). % Cyc Assertion #1986591: fof(ax1_123,axiom,( genls(c_tptpcol_1_65536,c_tptpcol_0_0) )). fof(ax1_124,axiom,( ! [OBJ] : ( tptpcol_1_65536(OBJ) => tptpcol_0_0(OBJ) ) )). % Cyc Assertion #566511: fof(ax1_125,axiom,( genlmt(c_cyclistsmt,c_hpkbvocabmt) )). % Cyc Assertion #1623378: fof(ax1_126,axiom, ( mtvisible(c_englishmt) => prettystring(f_subcollectionofwithrelationfromtypefn(c_terrorist,c_hasmembers,c_terroristgroup),s_terroristthathasbeenamemberofaterroristorganization) )). % Cyc Assertion #1144679: fof(ax1_127,axiom,( genlinverse(c_geographicalsubregions,c_inregion) )). fof(ax1_128,axiom,( ! [ARG1,ARG2] : ( geographicalsubregions(ARG1,ARG2) => inregion(ARG2,ARG1) ) )). % Cyc Assertion #2117953: fof(ax1_129,axiom,( genls(c_tptpcol_11_118084,c_tptpcol_10_118020) )). fof(ax1_130,axiom,( ! [OBJ] : ( tptpcol_11_118084(OBJ) => tptpcol_10_118020(OBJ) ) )). % Cyc Assertion #642174: fof(ax1_131,axiom,( genls(c_mathematicalorcomputationalthing,c_intangible) )). fof(ax1_132,axiom,( ! [OBJ] : ( mathematicalorcomputationalthing(OBJ) => intangible(OBJ) ) )). % Cyc Assertion #2184507: fof(ax1_133,axiom,( genlmt(c_tptp_member3393_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2341860: fof(ax1_134,axiom,( isa(c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)) )). fof(ax1_135,axiom,( subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) )). % Cyc Assertion #1462275: fof(ax1_136,axiom,( genlmt(c_generictemporalmt,c_basekb) )). % Cyc Assertion #190772: fof(ax1_137,axiom,( genlmt(c_worldgeographydualistmt,c_worldgeographymt) )). % Cyc Assertion #2156167: fof(ax1_138,axiom,( genlpreds(c_tptptypes_7_819,c_tptptypes_6_818) )). fof(ax1_139,axiom,( ! [ARG1,ARG2] : ( tptptypes_7_819(ARG1,ARG2) => tptptypes_6_818(ARG1,ARG2) ) )). % Cyc Assertion #2463139: fof(ax1_140,axiom,( genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt) )). % Cyc Assertion #1890041: fof(ax1_141,axiom,( genls(c_tptpcol_12_26919,c_tptpcol_11_26887) )). fof(ax1_142,axiom,( ! [OBJ] : ( tptpcol_12_26919(OBJ) => tptpcol_11_26887(OBJ) ) )). % Cyc Assertion #2155278: fof(ax1_143,axiom,( genlinverse(c_tptptypes_8_692,c_tptptypes_7_691) )). fof(ax1_144,axiom,( ! [ARG1,ARG2] : ( tptptypes_8_692(ARG1,ARG2) => tptptypes_7_691(ARG2,ARG1) ) )). % Cyc Assertion #1822756: fof(ax1_145,axiom,( genls(c_tptpcol_2_2,c_tptpcol_1_1) )). fof(ax1_146,axiom,( ! [OBJ] : ( tptpcol_2_2(OBJ) => tptpcol_1_1(OBJ) ) )). % Cyc Assertion #2184995: fof(ax1_147,axiom,( genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2053158: fof(ax1_148,axiom,( genls(c_tptpcol_9_92165,c_tptpcol_8_92164) )). fof(ax1_149,axiom,( ! [OBJ] : ( tptpcol_9_92165(OBJ) => tptpcol_8_92164(OBJ) ) )). % Cyc Assertion #1778144: fof(ax1_150,axiom,( genls(c_fixedordercollection,c_collection) )). fof(ax1_151,axiom,( ! [OBJ] : ( fixedordercollection(OBJ) => collection(OBJ) ) )). % Cyc Assertion #2150427: fof(ax1_152,axiom,( disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) )). fof(ax1_153,axiom,( ! [OBJ] : ~ ( tptpcol_1_1(OBJ) & tptpcol_1_65536(OBJ) ) )). % Cyc Assertion #253062: fof(ax1_154,axiom,( genlmt(c_geographymt,c_basekb) )). % Cyc Assertion #733764: fof(ax1_155,axiom,( genls(c_microtheory,c_aspatialinformationstore) )). fof(ax1_156,axiom,( ! [OBJ] : ( microtheory(OBJ) => aspatialinformationstore(OBJ) ) )). % Cyc Assertion #2188349: fof(ax1_157,axiom, ( mtvisible(c_tptp_member237_mt) => tptptypes_9_401(c_pushingababycarriage,c_tptpcol_16_10258) )). % Cyc Assertion #2194401: fof(ax1_158,axiom,( ! [TERM] : ( ( mtvisible(c_tptp_member2610_mt) & isa(TERM,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) ) => tptp_8_875(TERM,f_relationallexistsfn(TERM,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)) ) )). fof(ax1_159,axiom, ( mtvisible(c_tptp_member2610_mt) => relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868) )). % Cyc Assertion #2117794: fof(ax1_160,axiom,( genls(c_tptpcol_10_118020,c_tptpcol_9_118019) )). fof(ax1_161,axiom,( ! [OBJ] : ( tptpcol_10_118020(OBJ) => tptpcol_9_118019(OBJ) ) )). % Cyc Assertion #1746783: fof(ax1_162,axiom,( genlmt(c_calendarsvocabularymt,c_basekb) )). % Cyc Assertion #2375063: fof(ax1_163,axiom, ( mtvisible(c_cyclistsmt) => runningshorts(c_tptprunningshorts) )). % Cyc Assertion #2191631: fof(ax1_164,axiom,( ! [TERM] : ( ( mtvisible(c_cyclistsmt) & executionbyfiringsquad(TERM) ) => tptp_9_720(TERM,f_relationallexistsfn(TERM,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)) ) )). fof(ax1_165,axiom, ( mtvisible(c_cyclistsmt) => relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490) )). % Cyc Assertion #1419921: fof(ax1_166,axiom,( disjointwith(c_individual,c_setorcollection) )). fof(ax1_167,axiom,( ! [OBJ] : ~ ( individual(OBJ) & setorcollection(OBJ) ) )). % Cyc Assertion #1877881: fof(ax1_168,axiom,( genls(c_tptpcol_12_22055,c_tptpcol_11_22023) )). fof(ax1_169,axiom,( ! [OBJ] : ( tptpcol_12_22055(OBJ) => tptpcol_11_22023(OBJ) ) )). % Cyc Assertion #1385317: fof(ax1_170,axiom,( genls(c_applicationcontext,c_microtheory) )). fof(ax1_171,axiom,( ! [OBJ] : ( applicationcontext(OBJ) => microtheory(OBJ) ) )). % Cyc Assertion #2179291: fof(ax1_172,axiom,( genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2153234: fof(ax1_173,axiom,( genlpreds(c_tptptypes_8_400,c_tptptypes_7_396) )). fof(ax1_174,axiom,( ! [ARG1,ARG2] : ( tptptypes_8_400(ARG1,ARG2) => tptptypes_7_396(ARG1,ARG2) ) )). % Cyc Assertion #1869322: fof(ax1_175,axiom,( genls(c_tptpcol_11_18631,c_tptpcol_10_18567) )). fof(ax1_176,axiom,( ! [OBJ] : ( tptpcol_11_18631(OBJ) => tptpcol_10_18567(OBJ) ) )). % Cyc Assertion #1614635: fof(ax1_177,axiom,( genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt) )). % Cyc Assertion #2190761: fof(ax1_178,axiom, ( mtvisible(c_tptp_member2668_mt) => tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886) )). % Cyc Assertion #913648: fof(ax1_179,axiom,( genls(c_mathematicalthing,c_mathematicalorcomputationalthing) )). fof(ax1_180,axiom,( ! [OBJ] : ( mathematicalthing(OBJ) => mathematicalorcomputationalthing(OBJ) ) )). % Cyc Assertion #146206: fof(ax1_181,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14),c_machinelearningspindleheadmt) )). % Cyc Assertion #2057178: fof(ax1_182,axiom,( genls(c_tptpcol_15_93775,c_tptpcol_14_93774) )). fof(ax1_183,axiom,( ! [OBJ] : ( tptpcol_15_93775(OBJ) => tptpcol_14_93774(OBJ) ) )). % Cyc Assertion #2095393: fof(ax1_184,axiom,( genls(c_tptpcol_8_109059,c_tptpcol_7_108547) )). fof(ax1_185,axiom,( ! [OBJ] : ( tptpcol_8_109059(OBJ) => tptpcol_7_108547(OBJ) ) )). % Cyc Assertion #1923813: fof(ax1_186,axiom,( genls(c_tptpcol_14_40429,c_tptpcol_13_40421) )). fof(ax1_187,axiom,( ! [OBJ] : ( tptpcol_14_40429(OBJ) => tptpcol_13_40421(OBJ) ) )). % Cyc Assertion #2495599: fof(ax1_188,axiom, ( mtvisible(c_tptpgeo_member7_mt) => geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72) )). % Cyc Assertion #1877922: fof(ax1_189,axiom,( genls(c_tptpcol_14_22072,c_tptpcol_13_22071) )). fof(ax1_190,axiom,( ! [OBJ] : ( tptpcol_14_22072(OBJ) => tptpcol_13_22071(OBJ) ) )). % Cyc Assertion #2057176: fof(ax1_191,axiom,( genls(c_tptpcol_14_93774,c_tptpcol_13_93766) )). fof(ax1_192,axiom,( ! [OBJ] : ( tptpcol_14_93774(OBJ) => tptpcol_13_93766(OBJ) ) )). % Cyc Assertion #1877800: fof(ax1_193,axiom,( genls(c_tptpcol_10_22022,c_tptpcol_9_22021) )). fof(ax1_194,axiom,( ! [OBJ] : ( tptpcol_10_22022(OBJ) => tptpcol_9_22021(OBJ) ) )). % Cyc Assertion #1643131: fof(ax1_195,axiom,( genls(c_inanimateobject_nonnatural,c_inanimateobject) )). fof(ax1_196,axiom,( ! [OBJ] : ( inanimateobject_nonnatural(OBJ) => inanimateobject(OBJ) ) )). % Cyc Assertion #536720: fof(ax1_197,axiom,( transitivebinarypredicate(c_inregion) )). % Cyc Assertion #2171884: fof(ax1_198,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member237_mt) )). % Cyc Assertion #2004518: fof(ax1_199,axiom,( genls(c_tptpcol_9_72709,c_tptpcol_8_72708) )). fof(ax1_200,axiom,( ! [OBJ] : ( tptpcol_9_72709(OBJ) => tptpcol_8_72708(OBJ) ) )). % Cyc Assertion #640909: fof(ax1_201,axiom,( individual(c_xskijump_thegame) )). % Cyc Assertion #2363011: fof(ax1_202,axiom,( ! [INS] : ( ( mtvisible(c_tptp_spindleheadmt) & supplies(INS) ) => tptpofobject(INS,f_tptpquantityfn_14(n_232)) ) )). fof(ax1_203,axiom, ( mtvisible(c_tptp_spindleheadmt) => relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232)) )). % Cyc Assertion #595427: fof(ax1_204,axiom,( genls(c_firstordercollection,c_fixedordercollection) )). fof(ax1_205,axiom,( ! [OBJ] : ( firstordercollection(OBJ) => fixedordercollection(OBJ) ) )). % Cyc Assertion #985685: fof(ax1_206,axiom,( genlmt(c_universalvocabularymt,c_basekb) )). % Cyc Assertion #2513432: fof(ax1_207,axiom, ( mtvisible(c_tptpgeo_member1_mt) => borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10) )). % Cyc Assertion #1869403: fof(ax1_208,axiom,( genls(c_tptpcol_13_18664,c_tptpcol_12_18663) )). fof(ax1_209,axiom,( ! [OBJ] : ( tptpcol_13_18664(OBJ) => tptpcol_12_18663(OBJ) ) )). % Cyc Assertion #1591255: fof(ax1_210,axiom,( genls(c_artifact,c_inanimateobject_nonnatural) )). fof(ax1_211,axiom,( ! [OBJ] : ( artifact(OBJ) => inanimateobject_nonnatural(OBJ) ) )). % Cyc Assertion #2463146: fof(ax1_212,axiom,( genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt) )). % Cyc Assertion #1322220: fof(ax1_213,axiom,( transitivebinarypredicate(c_genlmt) )). % Cyc Assertion #1473451: fof(ax1_214,axiom,( genlmt(c_timehasnoendmt,c_generictemporalmt) )). % Cyc Assertion #2106908: fof(ax1_215,axiom,( genls(c_tptpcol_7_113665,c_tptpcol_6_112641) )). fof(ax1_216,axiom,( ! [OBJ] : ( tptpcol_7_113665(OBJ) => tptpcol_6_112641(OBJ) ) )). % Cyc Assertion #2440265: fof(ax1_217,axiom, ( mtvisible(c_currentworlddatacollectormt_nonhomocentric) => tptpofobject(f_instancewithrelationtofn(c_airport_physical,c_airporthasiatacode,s_tlh),f_tptpquantityfn_21(n_170)) )). % Cyc Assertion #612894: fof(ax1_218,axiom,( genls(c_geographicalregion,c_partiallytangible) )). fof(ax1_219,axiom,( ! [OBJ] : ( geographicalregion(OBJ) => partiallytangible(OBJ) ) )). % Cyc Assertion #649807: fof(ax1_220,axiom,( genlpreds(c_disjointwith,c_no) )). fof(ax1_221,axiom,( ! [ARG1,ARG2] : ( disjointwith(ARG1,ARG2) => no(ARG1,ARG2) ) )). % Cyc Assertion #1884194: fof(ax1_222,axiom,( genls(c_tptpcol_4_24578,c_tptpcol_3_16386) )). fof(ax1_223,axiom,( ! [OBJ] : ( tptpcol_4_24578(OBJ) => tptpcol_3_16386(OBJ) ) )). % Cyc Assertion #1996836: fof(ax1_224,axiom,( genls(c_tptpcol_5_69635,c_tptpcol_4_65539) )). fof(ax1_225,axiom,( ! [OBJ] : ( tptpcol_5_69635(OBJ) => tptpcol_4_65539(OBJ) ) )). % Cyc Assertion #2283540: fof(ax1_226,axiom,( isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )). fof(ax1_227,axiom,( subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) )). % Cyc Assertion #961669: fof(ax1_228,axiom,( arg1isa(c_genls,c_collection) )). fof(ax1_229,axiom,( ! [ARG1,ARG2] : ( genls(ARG1,ARG2) => collection(ARG1) ) )). % Cyc Assertion #1877920: fof(ax1_230,axiom,( genls(c_tptpcol_13_22071,c_tptpcol_12_22055) )). fof(ax1_231,axiom,( ! [OBJ] : ( tptpcol_13_22071(OBJ) => tptpcol_12_22055(OBJ) ) )). % Cyc Assertion #1757575: fof(ax1_232,axiom,( genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt) )). % Cyc Assertion #2068512: fof(ax1_233,axiom,( genls(c_tptpcol_3_98305,c_tptpcol_2_98304) )). fof(ax1_234,axiom,( ! [OBJ] : ( tptpcol_3_98305(OBJ) => tptpcol_2_98304(OBJ) ) )). % Cyc Assertion #2109471: fof(ax1_235,axiom,( genls(c_tptpcol_4_114689,c_tptpcol_3_114688) )). fof(ax1_236,axiom,( ! [OBJ] : ( tptpcol_4_114689(OBJ) => tptpcol_3_114688(OBJ) ) )). % Cyc Assertion #767498: fof(ax1_237,axiom,( genls(c_artsupplies,c_supplies) )). fof(ax1_238,axiom,( ! [OBJ] : ( artsupplies(OBJ) => supplies(OBJ) ) )). % Cyc Assertion #1889319: fof(ax1_239,axiom,( genls(c_tptpcol_8_26629,c_tptpcol_7_26628) )). fof(ax1_240,axiom,( ! [OBJ] : ( tptpcol_8_26629(OBJ) => tptpcol_7_26628(OBJ) ) )). % Cyc Assertion #2095395: fof(ax1_241,axiom,( genls(c_tptpcol_9_109060,c_tptpcol_8_109059) )). fof(ax1_242,axiom,( ! [OBJ] : ( tptpcol_9_109060(OBJ) => tptpcol_8_109059(OBJ) ) )). % Cyc Assertion #2185467: fof(ax1_243,axiom,( genlmt(c_tptp_member3633_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2190508: fof(ax1_244,axiom,( ! [TERM] : ( isa(TERM,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)) => tptp_8_968(f_relationexistsallfn(TERM,c_tptp_8_968,c_tptpcol_16_7738,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)),TERM) ) )). fof(ax1_245,axiom,( relationexistsall(c_tptp_8_968,c_tptpcol_16_7738,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)) )). % Cyc Assertion #1679221: fof(ax1_246,axiom,( physicalorderingpredicate(c_geographicalsubregions) )). % Cyc Assertion #665043: fof(ax1_247,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt) )). % Cyc Assertion #2174831: fof(ax1_248,axiom,( genlmt(c_tptp_member974_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2494724: fof(ax1_249,axiom, ( mtvisible(c_tptpgeo_member1_mt) => geographicalsubregions(c_georegion_l3_x11_y2,c_georegion_l4_x35_y7) )). % Cyc Assertion #2095693: fof(ax1_250,axiom,( genls(c_tptpcol_14_109181,c_tptpcol_13_109173) )). fof(ax1_251,axiom,( ! [OBJ] : ( tptpcol_14_109181(OBJ) => tptpcol_13_109173(OBJ) ) )). % Cyc Assertion #1900169: fof(ax1_252,axiom,( genls(c_tptpcol_16_30972,c_tptpcol_15_30970) )). fof(ax1_253,axiom,( ! [OBJ] : ( tptpcol_16_30972(OBJ) => tptpcol_15_30970(OBJ) ) )). % Cyc Assertion #2170932: fof(ax1_254,axiom,( genlmt(c_tptp_spindleheadmt,c_cyclistsmt) )). % Cyc Assertion #1868844: fof(ax1_255,axiom,( genls(c_tptpcol_9_18439,c_tptpcol_8_18438) )). fof(ax1_256,axiom,( ! [OBJ] : ( tptpcol_9_18439(OBJ) => tptpcol_8_18438(OBJ) ) )). % Cyc Assertion #1038166: fof(ax1_257,axiom,( genlmt(c_keinteractionresourcetestmt,c_testvocabularymt) )). % Cyc Assertion #2118032: fof(ax1_258,axiom,( genls(c_tptpcol_12_118116,c_tptpcol_11_118084) )). fof(ax1_259,axiom,( ! [OBJ] : ( tptpcol_12_118116(OBJ) => tptpcol_11_118084(OBJ) ) )). % Cyc Assertion #2289027: fof(ax1_260,axiom,( furpelt(c_theprototypicalfurpelt) )). % Cyc Assertion #1889317: fof(ax1_261,axiom,( genls(c_tptpcol_7_26628,c_tptpcol_6_26627) )). fof(ax1_262,axiom,( ! [OBJ] : ( tptpcol_7_26628(OBJ) => tptpcol_6_26627(OBJ) ) )). % Cyc Assertion #1243931: fof(ax1_263,axiom,( arg1isa(c_most,c_setorcollection) )). fof(ax1_264,axiom,( ! [ARG1,ARG2] : ( most(ARG1,ARG2) => setorcollection(ARG1) ) )). % Cyc Assertion #2095702: fof(ax1_265,axiom,( genls(c_tptpcol_15_109185,c_tptpcol_14_109181) )). fof(ax1_266,axiom,( ! [OBJ] : ( tptpcol_15_109185(OBJ) => tptpcol_14_109181(OBJ) ) )). % Cyc Assertion #2053413: fof(ax1_267,axiom,( genls(c_tptpcol_16_92269,c_tptpcol_15_92268) )). fof(ax1_268,axiom,( ! [OBJ] : ( tptpcol_16_92269(OBJ) => tptpcol_15_92268(OBJ) ) )). % Cyc Assertion #600900: fof(ax1_269,axiom,( genlmt(c_cycnounlearnermt,c_cycorpproductsmt) )). % Cyc Assertion #2156195: fof(ax1_270,axiom,( genlpreds(c_tptptypes_8_823,c_tptptypes_7_819) )). fof(ax1_271,axiom,( ! [ARG1,ARG2] : ( tptptypes_8_823(ARG1,ARG2) => tptptypes_7_819(ARG1,ARG2) ) )). % Cyc Assertion #899762: fof(ax1_272,axiom,( genlmt(c_humansociallifemt,c_basekb) )). % Cyc Assertion #2463143: fof(ax1_273,axiom,( genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt) )). % Cyc Assertion #1312404: fof(ax1_274,axiom,( genlmt(c_knowledgefragmentd3mt,c_basekb) )). % Cyc Assertion #591557: fof(ax1_275,axiom,( genlmt(c_testvocabularymt,c_nooescapearchitecturemt) )). % Cyc Assertion #2491582: fof(ax1_276,axiom, ( mtvisible(c_tptpgeo_member7_mt) => geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24) )). % Cyc Assertion #1889960: fof(ax1_277,axiom,( genls(c_tptpcol_10_26886,c_tptpcol_9_26885) )). fof(ax1_278,axiom,( ! [OBJ] : ( tptpcol_10_26886(OBJ) => tptpcol_9_26885(OBJ) ) )). % Cyc Assertion #2185803: fof(ax1_279,axiom,( genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2004724: fof(ax1_280,axiom,( genls(c_tptpcol_15_72793,c_tptpcol_14_72792) )). fof(ax1_281,axiom,( ! [OBJ] : ( tptpcol_15_72793(OBJ) => tptpcol_14_72792(OBJ) ) )). % Cyc Assertion #2499616: fof(ax1_282,axiom, ( mtvisible(c_tptpgeo_member3_mt) => inregion(c_geolocation_x14_y39,c_georegion_l4_x14_y39) )). % Cyc Assertion #665347: fof(ax1_283,axiom,( genls(c_navypersonnel,c_militaryperson) )). fof(ax1_284,axiom,( ! [OBJ] : ( navypersonnel(OBJ) => militaryperson(OBJ) ) )). % Cyc Assertion #1863717: fof(ax1_285,axiom,( genls(c_tptpcol_4_16387,c_tptpcol_3_16386) )). fof(ax1_286,axiom,( ! [OBJ] : ( tptpcol_4_16387(OBJ) => tptpcol_3_16386(OBJ) ) )). % Cyc Assertion #1639598: fof(ax1_287,axiom,( genls(c_enduringthing_localized,c_spatialthing_nonsituational) )). fof(ax1_288,axiom,( ! [OBJ] : ( enduringthing_localized(OBJ) => spatialthing_nonsituational(OBJ) ) )). % Cyc Assertion #1558442: fof(ax1_289,axiom,( ! [OBJ] : ~ ( collection(OBJ) & individual(OBJ) ) )). fof(ax1_290,axiom,( disjointwith(c_collection,c_individual) )). % Cyc Assertion #2491835: fof(ax1_291,axiom, ( mtvisible(c_tptpgeo_member2_mt) => geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7) )). % Cyc Assertion #2477127: fof(ax1_292,axiom, ( mtvisible(c_worldgeographymt) => geolevel_1(c_georegion_l1_x2_y0) )). % Cyc Assertion #1199541: fof(ax1_293,axiom,( genls(c_physicalorderingpredicate,c_orderingpredicate) )). fof(ax1_294,axiom,( ! [OBJ] : ( physicalorderingpredicate(OBJ) => orderingpredicate(OBJ) ) )). % Cyc Assertion #352680: fof(ax1_295,axiom,( arg2isa(c_disjointwith,c_collection) )). fof(ax1_296,axiom,( ! [ARG1,ARG2] : ( disjointwith(ARG1,ARG2) => collection(ARG2) ) )). % Cyc Assertion #1008490: fof(ax1_297,axiom,( ! [TERM,INDEPCOL,PRED,DEPCOL] : ( ( isa(TERM,INDEPCOL) & relationallexists(PRED,INDEPCOL,DEPCOL) ) => isa(f_relationallexistsfn(TERM,PRED,INDEPCOL,DEPCOL),DEPCOL) ) )). fof(ax1_298,axiom,( resultisaarg(c_relationallexistsfn,n_4) )). % Cyc Assertion #2226304: fof(ax1_299,axiom,( individual(c_tptptptpcol_16_25985) )). % Cyc Assertion #2498061: fof(ax1_300,axiom, ( mtvisible(c_tptpgeo_member2_mt) => geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23) )). % Cyc Assertion #2153157: fof(ax1_301,axiom,( genlinverse(c_tptptypes_7_389,c_tptptypes_6_388) )). fof(ax1_302,axiom,( ! [ARG1,ARG2] : ( tptptypes_7_389(ARG1,ARG2) => tptptypes_6_388(ARG2,ARG1) ) )). % Cyc Assertion #797186: fof(ax1_303,axiom, ( mtvisible(c_hpkbvocabmt) => genls(c_state_geopolitical,c_hpkb_subnationalagent) )). fof(ax1_304,axiom,( ! [OBJ] : ( ( mtvisible(c_hpkbvocabmt) & state_geopolitical(OBJ) ) => hpkb_subnationalagent(OBJ) ) )). % Cyc Assertion #1877796: fof(ax1_305,axiom,( genls(c_tptpcol_8_22020,c_tptpcol_7_21508) )). fof(ax1_306,axiom,( ! [OBJ] : ( tptpcol_8_22020(OBJ) => tptpcol_7_21508(OBJ) ) )). % Cyc Assertion #1494491: fof(ax1_307,axiom,( reflexivebinarypredicate(c_inregion) )). % Cyc Assertion #2188322: fof(ax1_308,axiom,( ! [TERM] : ( ( mtvisible(c_currentworlddatacollectormt_nonhomocentric) & isa(TERM,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ) => tptp_9_51(f_relationexistsallfn(TERM,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),TERM) ) )). fof(ax1_309,axiom, ( mtvisible(c_currentworlddatacollectormt_nonhomocentric) => relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )). % Cyc Assertion #1030084: fof(ax1_310,axiom,( genlmt(c_cyclistsmt,c_keinteractionresourcetestmt) )). % Cyc Assertion #1986595: fof(ax1_311,axiom,( genls(c_tptpcol_3_65538,c_tptpcol_2_65537) )). fof(ax1_312,axiom,( ! [OBJ] : ( tptpcol_3_65538(OBJ) => tptpcol_2_65537(OBJ) ) )). % Cyc Assertion #1890045: fof(ax1_313,axiom,( genls(c_tptpcol_14_26921,c_tptpcol_13_26920) )). fof(ax1_314,axiom,( ! [OBJ] : ( tptpcol_14_26921(OBJ) => tptpcol_13_26920(OBJ) ) )). % Cyc Assertion #2186907: fof(ax1_315,axiom,( genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2287217: fof(ax1_316,axiom,( isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) )). fof(ax1_317,axiom,( subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786) )). % Cyc Assertion #426678: fof(ax1_318,axiom,( individual(f_citynamedfn(s_agen,c_france)) )). % Cyc Assertion #1012294: fof(ax1_319,axiom,( genls(c_intangibleindividual,c_partiallyintangibleindividual) )). fof(ax1_320,axiom,( ! [OBJ] : ( intangibleindividual(OBJ) => partiallyintangibleindividual(OBJ) ) )). % Cyc Assertion #1508031: fof(ax1_321,axiom, ( mtvisible(c_worldgeographymt) => state_geopolitical(c_wanica_districtsuriname) )). % Cyc Assertion #2150048: fof(ax1_322,axiom,( genls(c_tptpcol_16_130924,c_tptpcol_15_130923) )). fof(ax1_323,axiom,( ! [OBJ] : ( tptpcol_16_130924(OBJ) => tptpcol_15_130923(OBJ) ) )). % Cyc Assertion #2053154: fof(ax1_324,axiom,( genls(c_tptpcol_7_92163,c_tptpcol_6_92162) )). fof(ax1_325,axiom,( ! [OBJ] : ( tptpcol_7_92163(OBJ) => tptpcol_6_92162(OBJ) ) )). % Cyc Assertion #2463131: fof(ax1_326,axiom,( genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt) )). % Cyc Assertion #2150070: fof(ax1_327,axiom,( genls(c_tptpcol_16_130933,c_tptpcol_15_130931) )). fof(ax1_328,axiom,( ! [OBJ] : ( tptpcol_16_130933(OBJ) => tptpcol_15_130931(OBJ) ) )). % Cyc Assertion #1262542: fof(ax1_329,axiom,( genlmt(c_massmediadatamt,c_ethnicgroupsmt) )). % Cyc Assertion #1263090: fof(ax1_330,axiom,( genlpreds(c_no,c_few) )). fof(ax1_331,axiom,( ! [ARG1,ARG2] : ( no(ARG1,ARG2) => few(ARG1,ARG2) ) )). % Cyc Assertion #592971: fof(ax1_332,axiom,( genlmt(c_cycorpproductsmt,c_basekb) )). % Cyc Assertion #1408590: fof(ax1_333,axiom,( genlmt(c_reasoningaboutpossibleantecedentsmt,c_humansociallifemt) )). % Cyc Assertion #631445: fof(ax1_334,axiom,( genlmt(c_worldgeographymt,c_geographymt) )). % Cyc Assertion #1873958: fof(ax1_335,axiom,( genls(c_tptpcol_6_20484,c_tptpcol_5_20483) )). fof(ax1_336,axiom,( ! [OBJ] : ( tptpcol_6_20484(OBJ) => tptpcol_5_20483(OBJ) ) )). % Cyc Assertion #2493055: fof(ax1_337,axiom, ( mtvisible(c_tptpgeo_member3_mt) => geographicalsubregions(c_georegion_l3_x4_y13,c_georegion_l4_x14_y39) )). % Cyc Assertion #880523: fof(ax1_338,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32),c_machinelearningspindleheadmt) )). % Cyc Assertion #1132949: fof(ax1_339,axiom,( genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt) )). % Cyc Assertion #2094114: fof(ax1_340,axiom,( genls(c_tptpcol_7_108547,c_tptpcol_6_108546) )). fof(ax1_341,axiom,( ! [OBJ] : ( tptpcol_7_108547(OBJ) => tptpcol_6_108546(OBJ) ) )). % Cyc Assertion #2095556: fof(ax1_342,axiom,( genls(c_tptpcol_11_109125,c_tptpcol_10_109061) )). fof(ax1_343,axiom,( ! [OBJ] : ( tptpcol_11_109125(OBJ) => tptpcol_10_109061(OBJ) ) )). % Cyc Assertion #2181740: fof(ax1_344,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt) )). % Cyc Assertion #2056990: fof(ax1_345,axiom,( genls(c_tptpcol_8_93698,c_tptpcol_7_93186) )). fof(ax1_346,axiom,( ! [OBJ] : ( tptpcol_8_93698(OBJ) => tptpcol_7_93186(OBJ) ) )). % Cyc Assertion #1439735: fof(ax1_347,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7),c_machinelearningspindleheadmt) )). % Cyc Assertion #1986593: fof(ax1_348,axiom,( genls(c_tptpcol_2_65537,c_tptpcol_1_65536) )). fof(ax1_349,axiom,( ! [OBJ] : ( tptpcol_2_65537(OBJ) => tptpcol_1_65536(OBJ) ) )). % Cyc Assertion #2181608: fof(ax1_350,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member2668_mt) )). % Cyc Assertion #1868838: fof(ax1_351,axiom,( genls(c_tptpcol_6_18436,c_tptpcol_5_16388) )). fof(ax1_352,axiom,( ! [OBJ] : ( tptpcol_6_18436(OBJ) => tptpcol_5_16388(OBJ) ) )). % Cyc Assertion #1868842: fof(ax1_353,axiom,( genls(c_tptpcol_8_18438,c_tptpcol_7_18437) )). fof(ax1_354,axiom,( ! [OBJ] : ( tptpcol_8_18438(OBJ) => tptpcol_7_18437(OBJ) ) )). % Cyc Assertion #2504622: fof(ax1_355,axiom, ( mtvisible(c_tptpgeo_member2_mt) => inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23) )). % Cyc Assertion #2117153: fof(ax1_356,axiom,( genls(c_tptpcol_8_117763,c_tptpcol_7_117762) )). fof(ax1_357,axiom,( ! [OBJ] : ( tptpcol_8_117763(OBJ) => tptpcol_7_117762(OBJ) ) )). % Cyc Assertion #1326245: fof(ax1_358,axiom,( genlmt(c_corecyclmt,c_logicaltruthmt) )). % Cyc Assertion #2095635: fof(ax1_359,axiom,( genls(c_tptpcol_12_109157,c_tptpcol_11_109125) )). fof(ax1_360,axiom,( ! [OBJ] : ( tptpcol_12_109157(OBJ) => tptpcol_11_109125(OBJ) ) )). % Cyc Assertion #2117151: fof(ax1_361,axiom,( genls(c_tptpcol_7_117762,c_tptpcol_6_116738) )). fof(ax1_362,axiom,( ! [OBJ] : ( tptpcol_7_117762(OBJ) => tptpcol_6_116738(OBJ) ) )). % Cyc Assertion #398814: fof(ax1_363,axiom,( ! [OBJ,COL1,COL2] : ~ ( isa(OBJ,COL1) & isa(OBJ,COL2) & disjointwith(COL1,COL2) ) )). % Cyc Assertion #2186908: fof(ax1_364,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt) )). % Cyc Assertion #356096: fof(ax1_365,axiom,( genls(c_aspatialinformationstore,c_aspatialthing) )). fof(ax1_366,axiom,( ! [OBJ] : ( aspatialinformationstore(OBJ) => aspatialthing(OBJ) ) )). % Cyc Assertion #233936: fof(ax1_367,axiom,( genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt) )). % Cyc Assertion #1484562: fof(ax1_368,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885),c_machinelearningspindleheadmt) )). % Cyc Assertion #2463167: fof(ax1_369,axiom,( genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member8_mt) )). % Cyc Assertion #2056992: fof(ax1_370,axiom,( genls(c_tptpcol_9_93699,c_tptpcol_8_93698) )). fof(ax1_371,axiom,( ! [OBJ] : ( tptpcol_9_93699(OBJ) => tptpcol_8_93698(OBJ) ) )). % Cyc Assertion #2057153: fof(ax1_372,axiom,( genls(c_tptpcol_11_93764,c_tptpcol_10_93700) )). fof(ax1_373,axiom,( ! [OBJ] : ( tptpcol_11_93764(OBJ) => tptpcol_10_93700(OBJ) ) )). % Cyc Assertion #1889315: fof(ax1_374,axiom,( genls(c_tptpcol_6_26627,c_tptpcol_5_24579) )). fof(ax1_375,axiom,( ! [OBJ] : ( tptpcol_6_26627(OBJ) => tptpcol_5_24579(OBJ) ) )). % Cyc Assertion #2048031: fof(ax1_376,axiom,( genls(c_tptpcol_4_90113,c_tptpcol_3_81921) )). fof(ax1_377,axiom,( ! [OBJ] : ( tptpcol_4_90113(OBJ) => tptpcol_3_81921(OBJ) ) )). % Cyc Assertion #1077444: fof(ax1_378,axiom,( genlmt(c_calendarsmt,c_calendarsvocabularymt) )). % Cyc Assertion #2056994: fof(ax1_379,axiom,( genls(c_tptpcol_10_93700,c_tptpcol_9_93699) )). fof(ax1_380,axiom,( ! [OBJ] : ( tptpcol_10_93700(OBJ) => tptpcol_9_93699(OBJ) ) )). % Cyc Assertion #1074241: fof(ax1_381,axiom,( genls(c_aspatialinformationstore,c_intangibleindividual) )). fof(ax1_382,axiom,( ! [OBJ] : ( aspatialinformationstore(OBJ) => intangibleindividual(OBJ) ) )). % Cyc Assertion #2512240: fof(ax1_383,axiom, ( mtvisible(c_tptpgeo_member4_mt) => borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50) )). % Cyc Assertion #935028: fof(ax1_384,axiom,( genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt) )). % Cyc Assertion #1863715: fof(ax1_385,axiom,( genls(c_tptpcol_3_16386,c_tptpcol_2_2) )). fof(ax1_386,axiom,( ! [OBJ] : ( tptpcol_3_16386(OBJ) => tptpcol_2_2(OBJ) ) )). % Cyc Assertion #2117792: fof(ax1_387,axiom,( genls(c_tptpcol_9_118019,c_tptpcol_8_117763) )). fof(ax1_388,axiom,( ! [OBJ] : ( tptpcol_9_118019(OBJ) => tptpcol_8_117763(OBJ) ) )). % Cyc Assertion #1610244: fof(ax1_389,axiom,( genls(c_individual,c_trajector_underspecified) )). fof(ax1_390,axiom,( ! [OBJ] : ( individual(OBJ) => trajector_underspecified(OBJ) ) )). % Cyc Assertion #2198037: fof(ax1_391,axiom,( ! [TERM] : ( shavingrazor_manual(TERM) => tptp_8_271(f_relationexistsallfn(TERM,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),TERM) ) )). fof(ax1_392,axiom,( relationexistsall(c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual) )). % Cyc Assertion #2104349: fof(ax1_393,axiom,( genls(c_tptpcol_6_112641,c_tptpcol_5_110593) )). fof(ax1_394,axiom,( ! [OBJ] : ( tptpcol_6_112641(OBJ) => tptpcol_5_110593(OBJ) ) )). % Cyc Assertion #2004681: fof(ax1_395,axiom,( genls(c_tptpcol_12_72775,c_tptpcol_11_72774) )). fof(ax1_396,axiom,( ! [OBJ] : ( tptpcol_12_72775(OBJ) => tptpcol_11_72774(OBJ) ) )). % Cyc Assertion #2004514: fof(ax1_397,axiom,( genls(c_tptpcol_7_72707,c_tptpcol_6_71683) )). fof(ax1_398,axiom,( ! [OBJ] : ( tptpcol_7_72707(OBJ) => tptpcol_6_71683(OBJ) ) )). % Cyc Assertion #1950136: fof(ax1_399,axiom,( genls(c_tptpcol_16_50958,c_tptpcol_15_50957) )). fof(ax1_400,axiom,( ! [OBJ] : ( tptpcol_16_50958(OBJ) => tptpcol_15_50957(OBJ) ) )). % Cyc Assertion #2108187: fof(ax1_401,axiom,( genls(c_tptpcol_8_114177,c_tptpcol_7_113665) )). fof(ax1_402,axiom,( ! [OBJ] : ( tptpcol_8_114177(OBJ) => tptpcol_7_113665(OBJ) ) )). % Cyc Assertion #2004728: fof(ax1_403,axiom,( genls(c_tptpcol_16_72795,c_tptpcol_15_72793) )). fof(ax1_404,axiom,( ! [OBJ] : ( tptpcol_16_72795(OBJ) => tptpcol_15_72793(OBJ) ) )). % Cyc Assertion #2001955: fof(ax1_405,axiom,( genls(c_tptpcol_6_71683,c_tptpcol_5_69635) )). fof(ax1_406,axiom,( ! [OBJ] : ( tptpcol_6_71683(OBJ) => tptpcol_5_69635(OBJ) ) )). % Cyc Assertion #2463155: fof(ax1_407,axiom,( genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt) )). % Cyc Assertion #2153206: fof(ax1_408,axiom,( genlpreds(c_tptptypes_7_396,c_tptptypes_6_388) )). fof(ax1_409,axiom,( ! [ARG1,ARG2] : ( tptptypes_7_396(ARG1,ARG2) => tptptypes_6_388(ARG1,ARG2) ) )). % Cyc Assertion #1889958: fof(ax1_410,axiom,( genls(c_tptpcol_9_26885,c_tptpcol_8_26629) )). fof(ax1_411,axiom,( ! [OBJ] : ( tptpcol_9_26885(OBJ) => tptpcol_8_26629(OBJ) ) )). % Cyc Assertion #1738068: fof(ax1_412,axiom,( genlpreds(c_genls,c_subsetof) )). fof(ax1_413,axiom,( ! [ARG1,ARG2] : ( genls(ARG1,ARG2) => subsetof(ARG1,ARG2) ) )). % Cyc Assertion #1315163: fof(ax1_414,axiom,( genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt) )). % Cyc Assertion #2156160: fof(ax1_415,axiom,( genlpreds(c_tptptypes_6_818,c_tptptypes_5_802) )). fof(ax1_416,axiom,( ! [ARG1,ARG2] : ( tptptypes_6_818(ARG1,ARG2) => tptptypes_5_802(ARG1,ARG2) ) )). % Cyc Assertion #2053152: fof(ax1_417,axiom,( genls(c_tptpcol_6_92162,c_tptpcol_5_90114) )). fof(ax1_418,axiom,( ! [OBJ] : ( tptpcol_6_92162(OBJ) => tptpcol_5_90114(OBJ) ) )). % Cyc Assertion #2171876: fof(ax1_419,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member235_mt) )). % Cyc Assertion #2053156: fof(ax1_420,axiom,( genls(c_tptpcol_8_92164,c_tptpcol_7_92163) )). fof(ax1_421,axiom,( ! [OBJ] : ( tptpcol_8_92164(OBJ) => tptpcol_7_92163(OBJ) ) )). % Cyc Assertion #2118034: fof(ax1_422,axiom,( genls(c_tptpcol_13_118117,c_tptpcol_12_118116) )). fof(ax1_423,axiom,( ! [OBJ] : ( tptpcol_13_118117(OBJ) => tptpcol_12_118116(OBJ) ) )). % Cyc Assertion #1923713: fof(ax1_424,axiom,( genls(c_tptpcol_11_40388,c_tptpcol_10_40324) )). fof(ax1_425,axiom,( ! [OBJ] : ( tptpcol_11_40388(OBJ) => tptpcol_10_40324(OBJ) ) )). % Cyc Assertion #2156202: fof(ax1_426,axiom,( genlpreds(c_tptptypes_9_824,c_tptptypes_8_823) )). fof(ax1_427,axiom,( ! [ARG1,ARG2] : ( tptptypes_9_824(ARG1,ARG2) => tptptypes_8_823(ARG1,ARG2) ) )). % Cyc Assertion #1668072: fof(ax1_428,axiom,( individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) )). % Cyc Assertion #1889962: fof(ax1_429,axiom,( genls(c_tptpcol_11_26887,c_tptpcol_10_26886) )). fof(ax1_430,axiom,( ! [OBJ] : ( tptpcol_11_26887(OBJ) => tptpcol_10_26886(OBJ) ) )). % Cyc Assertion #1890056: fof(ax1_431,axiom,( genls(c_tptpcol_16_26926,c_tptpcol_15_26925) )). fof(ax1_432,axiom,( ! [OBJ] : ( tptpcol_16_26926(OBJ) => tptpcol_15_26925(OBJ) ) )). % Cyc Assertion #767368: fof(ax1_433,axiom,( genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21),c_machinelearningspindleheadmt) )). % Cyc Assertion #1255218: fof(ax1_434,axiom,( arg2isa(c_few,c_setorcollection) )). fof(ax1_435,axiom,( ! [ARG1,ARG2] : ( few(ARG1,ARG2) => setorcollection(ARG2) ) )). % Cyc Assertion #1986597: fof(ax1_436,axiom,( genls(c_tptpcol_4_65539,c_tptpcol_3_65538) )). fof(ax1_437,axiom,( ! [OBJ] : ( tptpcol_4_65539(OBJ) => tptpcol_3_65538(OBJ) ) )). % Cyc Assertion #1922596: fof(ax1_438,axiom,( genls(c_tptpcol_8_39940,c_tptpcol_7_39939) )). fof(ax1_439,axiom,( ! [OBJ] : ( tptpcol_8_39940(OBJ) => tptpcol_7_39939(OBJ) ) )). % Cyc Assertion #2360289: fof(ax1_440,axiom,( ! [INS] : ( ( mtvisible(c_tptp_member2701_mt) & runningshorts(INS) ) => tptpofobject(INS,f_tptpquantityfn_2(n_756)) ) )). fof(ax1_441,axiom, ( mtvisible(c_tptp_member2701_mt) => relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756)) )). % Cyc Assertion #1877931: fof(ax1_442,axiom,( genls(c_tptpcol_15_22076,c_tptpcol_14_22072) )). fof(ax1_443,axiom,( ! [OBJ] : ( tptpcol_15_22076(OBJ) => tptpcol_14_22072(OBJ) ) )). % Cyc Assertion #1822752: fof(ax1_444,axiom,( genls(c_tptpcol_0_0,c_individual) )). fof(ax1_445,axiom,( ! [OBJ] : ( tptpcol_0_0(OBJ) => individual(OBJ) ) )). % Cyc Assertion #2180359: fof(ax1_446,axiom,( genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #2230906: fof(ax1_447,axiom,( individual(c_tptptptpcol_16_8398) )). % Cyc Assertion #2173728: fof(ax1_448,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt) )). % Cyc Assertion #2004679: fof(ax1_449,axiom,( genls(c_tptpcol_11_72774,c_tptpcol_10_72710) )). fof(ax1_450,axiom,( ! [OBJ] : ( tptpcol_11_72774(OBJ) => tptpcol_10_72710(OBJ) ) )). % Cyc Assertion #2188543: fof(ax1_451,axiom, ( mtvisible(c_tptp_spindleheadmt) => tptptypes_7_389(c_pushingwithopenhand,c_tptpcol_16_4451) )). % Cyc Assertion #1697211: fof(ax1_452,axiom, ( mtvisible(c_englishmt) => prettystring(f_instancewithrelationtofn(c_footballteam,c_affiliatedwith,c_beloitcollege),s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege) )). % Cyc Assertion #2177624: fof(ax1_453,axiom,( genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt) )). % Cyc Assertion #974757: fof(ax1_454,axiom,( genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt) )). % Cyc Assertion #1650755: fof(ax1_455,axiom,( genlmt(c_basekb,c_universalvocabularymt) )). % Cyc Assertion #1876517: fof(ax1_456,axiom,( genls(c_tptpcol_7_21508,c_tptpcol_6_20484) )). fof(ax1_457,axiom,( ! [OBJ] : ( tptpcol_7_21508(OBJ) => tptpcol_6_20484(OBJ) ) )). % Cyc Assertion #2094112: fof(ax1_458,axiom,( genls(c_tptpcol_6_108546,c_tptpcol_5_106498) )). fof(ax1_459,axiom,( ! [OBJ] : ( tptpcol_6_108546(OBJ) => tptpcol_5_106498(OBJ) ) )). % Cyc Assertion #2189225: fof(ax1_460,axiom, ( mtvisible(c_cyclistsmt) => tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027) )). % Cyc Assertion #2463177: fof(ax1_461,axiom,( genls(c_geolevel_4,c_geographicalregion) )). fof(ax1_462,axiom,( ! [OBJ] : ( geolevel_4(OBJ) => geographicalregion(OBJ) ) )). % Cyc Assertion #2512507: fof(ax1_463,axiom, ( mtvisible(c_tptpgeo_member1_mt) => borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24) )). % Cyc Assertion #2484090: fof(ax1_464,axiom, ( mtvisible(c_worldgeographymt) => geolevel_4(c_georegion_l4_x75_y75) )). % Cyc Assertion #1890043: fof(ax1_465,axiom,( genls(c_tptpcol_13_26920,c_tptpcol_12_26919) )). fof(ax1_466,axiom,( ! [OBJ] : ( tptpcol_13_26920(OBJ) => tptpcol_12_26919(OBJ) ) )). % Cyc Assertion #2053402: fof(ax1_467,axiom,( genls(c_tptpcol_14_92264,c_tptpcol_13_92263) )). fof(ax1_468,axiom,( ! [OBJ] : ( tptpcol_14_92264(OBJ) => tptpcol_13_92263(OBJ) ) )). % Cyc Assertion #752062: fof(ax1_469,axiom,( genlmt(c_gregoriancalendarmt,c_basekb) )). % Cyc Assertion #1923235: fof(ax1_470,axiom,( genls(c_tptpcol_9_40196,c_tptpcol_8_39940) )). fof(ax1_471,axiom,( ! [OBJ] : ( tptpcol_9_40196(OBJ) => tptpcol_8_39940(OBJ) ) )). % Cyc Assertion #2496249: fof(ax1_472,axiom, ( mtvisible(c_tptpgeo_member7_mt) => geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74) )). % Cyc Assertion #2053400: fof(ax1_473,axiom,( genls(c_tptpcol_13_92263,c_tptpcol_12_92262) )). fof(ax1_474,axiom,( ! [OBJ] : ( tptpcol_13_92263(OBJ) => tptpcol_12_92262(OBJ) ) )). % Cyc Assertion #1978206: fof(ax1_475,axiom,( firstordercollection(c_tptpcol_16_62187) )). % Cyc Assertion #2048033: fof(ax1_476,axiom,( genls(c_tptpcol_5_90114,c_tptpcol_4_90113) )). fof(ax1_477,axiom,( ! [OBJ] : ( tptpcol_5_90114(OBJ) => tptpcol_4_90113(OBJ) ) )). % Cyc Assertion #2477694: fof(ax1_478,axiom, ( mtvisible(c_worldgeographymt) => geolevel_3(c_georegion_l3_x17_y24) )). % Cyc Assertion #2182383: fof(ax1_479,axiom,( genlmt(c_tptp_member2862_mt,c_tptp_spindleheadmt) )). % Cyc Assertion #1890054: fof(ax1_480,axiom,( genls(c_tptpcol_15_26925,c_tptpcol_14_26921) )). fof(ax1_481,axiom,( ! [OBJ] : ( tptpcol_15_26925(OBJ) => tptpcol_14_26921(OBJ) ) )). % Cyc Assertion #2189688: fof(ax1_482,axiom, ( mtvisible(c_currentworlddatacollectormt_nonhomocentric) => tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939) )). % Cyc Assertion #1868840: fof(ax1_483,axiom,( genls(c_tptpcol_7_18437,c_tptpcol_6_18436) )). fof(ax1_484,axiom,( ! [OBJ] : ( tptpcol_7_18437(OBJ) => tptpcol_6_18436(OBJ) ) )). % Cyc Assertion #2511018: fof(ax1_485,axiom, ( mtvisible(c_tptpgeo_member7_mt) => borderson(c_georegion_l4_x29_y75,c_georegion_l4_x29_y76) )). % Cyc Assertion #1753642: fof(ax1_486,axiom,( genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) )). % Cyc Assertion #2150425: fof(ax1_487,axiom,( disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688) )). fof(ax1_488,axiom,( ! [OBJ] : ~ ( tptpcol_3_98305(OBJ) & tptpcol_3_114688(OBJ) ) )). % Cyc Assertion #2099230: fof(ax1_489,axiom,( genls(c_tptpcol_5_110593,c_tptpcol_4_106497) )). fof(ax1_490,axiom,( ! [OBJ] : ( tptpcol_5_110593(OBJ) => tptpcol_4_106497(OBJ) ) )). % Cyc Assertion #2004720: fof(ax1_491,axiom,( genls(c_tptpcol_13_72791,c_tptpcol_12_72775) )). fof(ax1_492,axiom,( ! [OBJ] : ( tptpcol_13_72791(OBJ) => tptpcol_12_72775(OBJ) ) )). % Cyc Assertion #833751: fof(ax1_493,axiom,( genls(c_computerdataartifact,c_artifact) )). fof(ax1_494,axiom,( ! [OBJ] : ( computerdataartifact(OBJ) => artifact(OBJ) ) )). % Cyc Assertion #2362336: fof(ax1_495,axiom,( ! [INS] : ( ( mtvisible(c_tptp_member698_mt) & militaryperson(INS) ) => tptpofobject(INS,f_tptpquantityfn_6(n_414)) ) )). fof(ax1_496,axiom, ( mtvisible(c_tptp_member698_mt) => relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414)) )). % Cyc Assertion #2053160: fof(ax1_497,axiom,( genls(c_tptpcol_10_92166,c_tptpcol_9_92165) )). fof(ax1_498,axiom,( ! [OBJ] : ( tptpcol_10_92166(OBJ) => tptpcol_9_92165(OBJ) ) )). % Cyc Assertion #2118036: fof(ax1_499,axiom,( genls(c_tptpcol_14_118118,c_tptpcol_13_118117) )). fof(ax1_500,axiom,( ! [OBJ] : ( tptpcol_14_118118(OBJ) => tptpcol_13_118117(OBJ) ) )). % Cyc Constant #247715: fof(ax1_501,axiom,( ! [X] : ( isa(X,c_tptpcol_14_118118) => tptpcol_14_118118(X) ) )). fof(ax1_502,axiom,( ! [X] : ( tptpcol_14_118118(X) => isa(X,c_tptpcol_14_118118) ) )). % Cyc Constant #347762: fof(ax1_503,axiom,( ! [ARG1] : natfunction(f_tptpquantityfn_6(ARG1),c_tptpquantityfn_6) )). fof(ax1_504,axiom,( ! [ARG1] : natargument(f_tptpquantityfn_6(ARG1),n_1,ARG1) )). fof(ax1_505,axiom,( ! [ARG1] : tptpquantity(f_tptpquantityfn_6(ARG1)) )). % Cyc Constant #156536: fof(ax1_506,axiom,( ! [X] : ( isa(X,c_tptpcol_16_26939) => tptpcol_16_26939(X) ) )). fof(ax1_507,axiom,( ! [X] : ( tptpcol_16_26939(X) => isa(X,c_tptpcol_16_26939) ) )). % Cyc Constant #191784: fof(ax1_508,axiom,( ! [X] : ( isa(X,c_tptpcol_16_62187) => tptpcol_16_62187(X) ) )). fof(ax1_509,axiom,( ! [X] : ( tptpcol_16_62187(X) => isa(X,c_tptpcol_16_62187) ) )). % Cyc Constant #221860: fof(ax1_510,axiom,( ! [X] : ( isa(X,c_tptpcol_13_92263) => tptpcol_13_92263(X) ) )). fof(ax1_511,axiom,( ! [X] : ( tptpcol_13_92263(X) => isa(X,c_tptpcol_13_92263) ) )). % Cyc Constant #380146: fof(ax1_512,axiom,( ! [X] : ( isa(X,c_geolevel_4) => geolevel_4(X) ) )). fof(ax1_513,axiom,( ! [X] : ( geolevel_4(X) => isa(X,c_geolevel_4) ) )). % Cyc Constant #133624: fof(ax1_514,axiom,( ! [X] : ( isa(X,c_tptpcol_15_4027) => tptpcol_15_4027(X) ) )). fof(ax1_515,axiom,( ! [X] : ( tptpcol_15_4027(X) => isa(X,c_tptpcol_15_4027) ) )). % Cyc Constant #38356: fof(ax1_516,axiom,( ! [X] : ( isa(X,c_pushingwithfingers) => pushingwithfingers(X) ) )). fof(ax1_517,axiom,( ! [X] : ( pushingwithfingers(X) => isa(X,c_pushingwithfingers) ) )). % Cyc Constant #53946: fof(ax1_518,axiom,( ! [ARG1,INS] : ( affiliatedwith(ARG1,INS) => agent_generic(INS) ) )). fof(ax1_519,axiom,( ! [INS,ARG2] : ( affiliatedwith(INS,ARG2) => agent_generic(INS) ) )). fof(ax1_520,axiom,( ! [X,Y] : ( affiliatedwith(X,Y) => affiliatedwith(Y,X) ) )). fof(ax1_521,axiom,( ! [X] : ~ affiliatedwith(X,X) )). % Cyc Constant #21892: fof(ax1_522,axiom,( ! [X] : ( isa(X,c_footballteam) => footballteam(X) ) )). fof(ax1_523,axiom,( ! [X] : ( footballteam(X) => isa(X,c_footballteam) ) )). % Cyc Constant #134048: fof(ax1_524,axiom,( ! [X] : ( isa(X,c_tptpcol_16_4451) => tptpcol_16_4451(X) ) )). fof(ax1_525,axiom,( ! [X] : ( tptpcol_16_4451(X) => isa(X,c_tptpcol_16_4451) ) )). % Cyc Constant #33419: fof(ax1_526,axiom,( ! [X] : ( isa(X,c_pushingwithopenhand) => pushingwithopenhand(X) ) )). fof(ax1_527,axiom,( ! [X] : ( pushingwithopenhand(X) => isa(X,c_pushingwithopenhand) ) )). % Cyc Constant #151673: fof(ax1_528,axiom,( ! [X] : ( isa(X,c_tptpcol_15_22076) => tptpcol_15_22076(X) ) )). fof(ax1_529,axiom,( ! [X] : ( tptpcol_15_22076(X) => isa(X,c_tptpcol_15_22076) ) )). % Cyc Constant #347758: fof(ax1_530,axiom,( ! [ARG1] : natfunction(f_tptpquantityfn_2(ARG1),c_tptpquantityfn_2) )). fof(ax1_531,axiom,( ! [ARG1] : natargument(f_tptpquantityfn_2(ARG1),n_1,ARG1) )). fof(ax1_532,axiom,( ! [ARG1] : tptpquantity(f_tptpquantityfn_2(ARG1)) )). % Cyc Constant #169536: fof(ax1_533,axiom,( ! [X] : ( isa(X,c_tptpcol_7_39939) => tptpcol_7_39939(X) ) )). fof(ax1_534,axiom,( ! [X] : ( tptpcol_7_39939(X) => isa(X,c_tptpcol_7_39939) ) )). % Cyc Constant #169537: fof(ax1_535,axiom,( ! [X] : ( isa(X,c_tptpcol_8_39940) => tptpcol_8_39940(X) ) )). fof(ax1_536,axiom,( ! [X] : ( tptpcol_8_39940(X) => isa(X,c_tptpcol_8_39940) ) )). % Cyc Constant #156522: fof(ax1_537,axiom,( ! [X] : ( isa(X,c_tptpcol_15_26925) => tptpcol_15_26925(X) ) )). fof(ax1_538,axiom,( ! [X] : ( tptpcol_15_26925(X) => isa(X,c_tptpcol_15_26925) ) )). % Cyc Constant #156523: fof(ax1_539,axiom,( ! [X] : ( isa(X,c_tptpcol_16_26926) => tptpcol_16_26926(X) ) )). fof(ax1_540,axiom,( ! [X] : ( tptpcol_16_26926(X) => isa(X,c_tptpcol_16_26926) ) )). % Cyc Constant #247714: fof(ax1_541,axiom,( ! [X] : ( isa(X,c_tptpcol_13_118117) => tptpcol_13_118117(X) ) )). fof(ax1_542,axiom,( ! [X] : ( tptpcol_13_118117(X) => isa(X,c_tptpcol_13_118117) ) )). % Cyc Constant #219711: fof(ax1_543,axiom,( ! [X] : ( isa(X,c_tptpcol_5_90114) => tptpcol_5_90114(X) ) )). fof(ax1_544,axiom,( ! [X] : ( tptpcol_5_90114(X) => isa(X,c_tptpcol_5_90114) ) )). % Cyc Constant #261471: fof(ax1_545,axiom,( ! [ARG1,INS] : ( tptptypes_5_802(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_546,axiom,( ! [INS,ARG2] : ( tptptypes_5_802(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #202392: fof(ax1_547,axiom,( ! [X] : ( isa(X,c_tptpcol_16_72795) => tptpcol_16_72795(X) ) )). fof(ax1_548,axiom,( ! [X] : ( tptpcol_16_72795(X) => isa(X,c_tptpcol_16_72795) ) )). % Cyc Constant #243774: fof(ax1_549,axiom,( ! [X] : ( isa(X,c_tptpcol_8_114177) => tptpcol_8_114177(X) ) )). fof(ax1_550,axiom,( ! [X] : ( tptpcol_8_114177(X) => isa(X,c_tptpcol_8_114177) ) )). % Cyc Constant #180554: fof(ax1_551,axiom,( ! [X] : ( isa(X,c_tptpcol_15_50957) => tptpcol_15_50957(X) ) )). fof(ax1_552,axiom,( ! [X] : ( tptpcol_15_50957(X) => isa(X,c_tptpcol_15_50957) ) )). % Cyc Constant #180555: fof(ax1_553,axiom,( ! [X] : ( isa(X,c_tptpcol_16_50958) => tptpcol_16_50958(X) ) )). fof(ax1_554,axiom,( ! [X] : ( tptpcol_16_50958(X) => isa(X,c_tptpcol_16_50958) ) )). % Cyc Constant #201280: fof(ax1_555,axiom,( ! [X] : ( isa(X,c_tptpcol_6_71683) => tptpcol_6_71683(X) ) )). fof(ax1_556,axiom,( ! [X] : ( tptpcol_6_71683(X) => isa(X,c_tptpcol_6_71683) ) )). % Cyc Constant #202371: fof(ax1_557,axiom,( ! [X] : ( isa(X,c_tptpcol_11_72774) => tptpcol_11_72774(X) ) )). fof(ax1_558,axiom,( ! [X] : ( tptpcol_11_72774(X) => isa(X,c_tptpcol_11_72774) ) )). % Cyc Constant #202372: fof(ax1_559,axiom,( ! [X] : ( isa(X,c_tptpcol_12_72775) => tptpcol_12_72775(X) ) )). fof(ax1_560,axiom,( ! [X] : ( tptpcol_12_72775(X) => isa(X,c_tptpcol_12_72775) ) )). % Cyc Constant #240190: fof(ax1_561,axiom,( ! [X] : ( isa(X,c_tptpcol_5_110593) => tptpcol_5_110593(X) ) )). fof(ax1_562,axiom,( ! [X] : ( tptpcol_5_110593(X) => isa(X,c_tptpcol_5_110593) ) )). % Cyc Constant #155569: fof(ax1_563,axiom,( ! [X] : ( isa(X,c_tptpcol_16_25972) => tptpcol_16_25972(X) ) )). fof(ax1_564,axiom,( ! [X] : ( tptpcol_16_25972(X) => isa(X,c_tptpcol_16_25972) ) )). % Cyc Constant #262618: fof(ax1_565,axiom,( ! [ARG1,INS] : ( tptp_8_271(ARG1,INS) => razor(INS) ) )). fof(ax1_566,axiom,( ! [INS,ARG2] : ( tptp_8_271(INS,ARG2) => tptpcol_5_24579(INS) ) )). % Cyc Constant #219710: fof(ax1_567,axiom,( ! [X] : ( isa(X,c_tptpcol_4_90113) => tptpcol_4_90113(X) ) )). fof(ax1_568,axiom,( ! [X] : ( tptpcol_4_90113(X) => isa(X,c_tptpcol_4_90113) ) )). % Cyc Constant #223297: fof(ax1_569,axiom,( ! [X] : ( isa(X,c_tptpcol_10_93700) => tptpcol_10_93700(X) ) )). fof(ax1_570,axiom,( ! [X] : ( tptpcol_10_93700(X) => isa(X,c_tptpcol_10_93700) ) )). % Cyc Constant #223296: fof(ax1_571,axiom,( ! [X] : ( isa(X,c_tptpcol_9_93699) => tptpcol_9_93699(X) ) )). fof(ax1_572,axiom,( ! [X] : ( tptpcol_9_93699(X) => isa(X,c_tptpcol_9_93699) ) )). % Cyc Constant #16302: fof(ax1_573,axiom,( ! [X] : ( isa(X,c_aspatialthing) => aspatialthing(X) ) )). fof(ax1_574,axiom,( ! [X] : ( aspatialthing(X) => isa(X,c_aspatialthing) ) )). % Cyc Constant #247359: fof(ax1_575,axiom,( ! [X] : ( isa(X,c_tptpcol_7_117762) => tptpcol_7_117762(X) ) )). fof(ax1_576,axiom,( ! [X] : ( tptpcol_7_117762(X) => isa(X,c_tptpcol_7_117762) ) )). % Cyc Constant #247360: fof(ax1_577,axiom,( ! [X] : ( isa(X,c_tptpcol_8_117763) => tptpcol_8_117763(X) ) )). fof(ax1_578,axiom,( ! [X] : ( tptpcol_8_117763(X) => isa(X,c_tptpcol_8_117763) ) )). % Cyc Constant #148034: fof(ax1_579,axiom,( ! [X] : ( isa(X,c_tptpcol_7_18437) => tptpcol_7_18437(X) ) )). fof(ax1_580,axiom,( ! [X] : ( tptpcol_7_18437(X) => isa(X,c_tptpcol_7_18437) ) )). % Cyc Constant #148033: fof(ax1_581,axiom,( ! [X] : ( isa(X,c_tptpcol_6_18436) => tptpcol_6_18436(X) ) )). fof(ax1_582,axiom,( ! [X] : ( tptpcol_6_18436(X) => isa(X,c_tptpcol_6_18436) ) )). % Cyc Constant #223295: fof(ax1_583,axiom,( ! [X] : ( isa(X,c_tptpcol_8_93698) => tptpcol_8_93698(X) ) )). fof(ax1_584,axiom,( ! [X] : ( tptpcol_8_93698(X) => isa(X,c_tptpcol_8_93698) ) )). % Cyc Constant #238722: fof(ax1_585,axiom,( ! [X] : ( isa(X,c_tptpcol_11_109125) => tptpcol_11_109125(X) ) )). fof(ax1_586,axiom,( ! [X] : ( tptpcol_11_109125(X) => isa(X,c_tptpcol_11_109125) ) )). % Cyc Constant #238143: fof(ax1_587,axiom,( ! [X] : ( isa(X,c_tptpcol_6_108546) => tptpcol_6_108546(X) ) )). fof(ax1_588,axiom,( ! [X] : ( tptpcol_6_108546(X) => isa(X,c_tptpcol_6_108546) ) )). % Cyc Constant #150081: fof(ax1_589,axiom,( ! [X] : ( isa(X,c_tptpcol_6_20484) => tptpcol_6_20484(X) ) )). fof(ax1_590,axiom,( ! [X] : ( tptpcol_6_20484(X) => isa(X,c_tptpcol_6_20484) ) )). % Cyc Constant #72033: fof(ax1_591,axiom,( ! [ARG1,INS] : ( few(ARG1,INS) => setorcollection(INS) ) )). fof(ax1_592,axiom,( ! [ARG1,INS] : ( few(ARG1,INS) => setorcollection(INS) ) )). fof(ax1_593,axiom,( ! [INS,ARG2] : ( few(INS,ARG2) => setorcollection(INS) ) )). fof(ax1_594,axiom,( ! [INS,ARG2] : ( few(INS,ARG2) => setorcollection(INS) ) )). fof(ax1_595,axiom,( ! [ARG1,OLD,NEW] : ( ( few(ARG1,OLD) & subsetof(NEW,OLD) ) => few(ARG1,NEW) ) )). % Cyc Constant #260528: fof(ax1_596,axiom,( ! [X] : ( isa(X,c_tptpcol_15_130931) => tptpcol_15_130931(X) ) )). fof(ax1_597,axiom,( ! [X] : ( tptpcol_15_130931(X) => isa(X,c_tptpcol_15_130931) ) )). % Cyc Constant #260530: fof(ax1_598,axiom,( ! [X] : ( isa(X,c_tptpcol_16_130933) => tptpcol_16_130933(X) ) )). fof(ax1_599,axiom,( ! [X] : ( tptpcol_16_130933(X) => isa(X,c_tptpcol_16_130933) ) )). % Cyc Constant #221760: fof(ax1_600,axiom,( ! [X] : ( isa(X,c_tptpcol_7_92163) => tptpcol_7_92163(X) ) )). fof(ax1_601,axiom,( ! [X] : ( tptpcol_7_92163(X) => isa(X,c_tptpcol_7_92163) ) )). % Cyc Constant #260520: fof(ax1_602,axiom,( ! [X] : ( isa(X,c_tptpcol_15_130923) => tptpcol_15_130923(X) ) )). fof(ax1_603,axiom,( ! [X] : ( tptpcol_15_130923(X) => isa(X,c_tptpcol_15_130923) ) )). % Cyc Constant #260521: fof(ax1_604,axiom,( ! [X] : ( isa(X,c_tptpcol_16_130924) => tptpcol_16_130924(X) ) )). fof(ax1_605,axiom,( ! [X] : ( tptpcol_16_130924(X) => isa(X,c_tptpcol_16_130924) ) )). % Cyc Constant #73655: fof(ax1_606,axiom,( ! [X] : ( isa(X,c_intangibleindividual) => intangibleindividual(X) ) )). fof(ax1_607,axiom,( ! [X] : ( intangibleindividual(X) => isa(X,c_intangibleindividual) ) )). % Cyc Constant #97068: fof(ax1_608,axiom,( ! [ARG1,ARG2] : natfunction(f_citynamedfn(ARG1,ARG2),c_citynamedfn) )). fof(ax1_609,axiom,( ! [ARG1,ARG2] : natargument(f_citynamedfn(ARG1,ARG2),n_1,ARG1) )). fof(ax1_610,axiom,( ! [ARG1,ARG2] : natargument(f_citynamedfn(ARG1,ARG2),n_2,ARG2) )). fof(ax1_611,axiom,( ! [ARG1,ARG2] : city(f_citynamedfn(ARG1,ARG2)) )). % Cyc Constant #156517: fof(ax1_612,axiom,( ! [X] : ( isa(X,c_tptpcol_13_26920) => tptpcol_13_26920(X) ) )). fof(ax1_613,axiom,( ! [X] : ( tptpcol_13_26920(X) => isa(X,c_tptpcol_13_26920) ) )). % Cyc Constant #156518: fof(ax1_614,axiom,( ! [X] : ( isa(X,c_tptpcol_14_26921) => tptpcol_14_26921(X) ) )). fof(ax1_615,axiom,( ! [X] : ( tptpcol_14_26921(X) => isa(X,c_tptpcol_14_26921) ) )). % Cyc Constant #195135: fof(ax1_616,axiom,( ! [X] : ( isa(X,c_tptpcol_3_65538) => tptpcol_3_65538(X) ) )). fof(ax1_617,axiom,( ! [X] : ( tptpcol_3_65538(X) => isa(X,c_tptpcol_3_65538) ) )). % Cyc Constant #156786: fof(ax1_618,axiom,( ! [X] : ( isa(X,c_tptpcol_16_27189) => tptpcol_16_27189(X) ) )). fof(ax1_619,axiom,( ! [X] : ( tptpcol_16_27189(X) => isa(X,c_tptpcol_16_27189) ) )). % Cyc Constant #262034: fof(ax1_620,axiom,( ! [ARG1,INS] : ( tptp_9_51(ARG1,INS) => subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(INS) ) )). fof(ax1_621,axiom,( ! [INS,ARG2] : ( tptp_9_51(INS,ARG2) => tptpcol_7_26628(INS) ) )). % Cyc Constant #1988: fof(ax1_622,axiom,( ! [X] : ( isa(X,c_reflexivebinarypredicate) => reflexivebinarypredicate(X) ) )). fof(ax1_623,axiom,( ! [X] : ( reflexivebinarypredicate(X) => isa(X,c_reflexivebinarypredicate) ) )). % Cyc Constant #151105: fof(ax1_624,axiom,( ! [X] : ( isa(X,c_tptpcol_7_21508) => tptpcol_7_21508(X) ) )). fof(ax1_625,axiom,( ! [X] : ( tptpcol_7_21508(X) => isa(X,c_tptpcol_7_21508) ) )). % Cyc Constant #105210: fof(ax1_626,axiom,( ! [X] : ( isa(X,c_hpkb_subnationalagent) => hpkb_subnationalagent(X) ) )). fof(ax1_627,axiom,( ! [X] : ( hpkb_subnationalagent(X) => isa(X,c_hpkb_subnationalagent) ) )). % Cyc Constant #123012: fof(ax1_628,axiom,( ! [X] : ( isa(X,c_state_geopolitical) => state_geopolitical(X) ) )). fof(ax1_629,axiom,( ! [X] : ( state_geopolitical(X) => isa(X,c_state_geopolitical) ) )). % Cyc Constant #104318: fof(ax1_630,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natfunction(f_relationallexistsfn(ARG1,ARG2,ARG3,ARG4),c_relationallexistsfn) )). fof(ax1_631,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationallexistsfn(ARG1,ARG2,ARG3,ARG4),n_1,ARG1) )). fof(ax1_632,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationallexistsfn(ARG1,ARG2,ARG3,ARG4),n_2,ARG2) )). fof(ax1_633,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationallexistsfn(ARG1,ARG2,ARG3,ARG4),n_3,ARG3) )). fof(ax1_634,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationallexistsfn(ARG1,ARG2,ARG3,ARG4),n_4,ARG4) )). fof(ax1_635,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : thing(f_relationallexistsfn(ARG1,ARG2,ARG3,ARG4)) )). % Cyc Constant #59425: fof(ax1_636,axiom,( ! [ARG1,INS] : ( arg2isa(ARG1,INS) => collection(INS) ) )). fof(ax1_637,axiom,( ! [INS,ARG2] : ( arg2isa(INS,ARG2) => relation(INS) ) )). fof(ax1_638,axiom,( ! [ARG1,OLD,NEW] : ( ( arg2isa(ARG1,OLD) & genls(OLD,NEW) ) => arg2isa(ARG1,NEW) ) )). fof(ax1_639,axiom,( ! [ARG1,OLD,NEW] : ( ( arg2isa(ARG1,OLD) & genls(OLD,NEW) ) => arg2isa(ARG1,NEW) ) )). % Cyc Constant #380143: fof(ax1_640,axiom,( ! [X] : ( isa(X,c_geolevel_1) => geolevel_1(X) ) )). fof(ax1_641,axiom,( ! [X] : ( geolevel_1(X) => isa(X,c_geolevel_1) ) )). % Cyc Constant #52963: fof(ax1_642,axiom,( mtvisible(c_logicaltruthmt) )). % Cyc Constant #25931: fof(ax1_643,axiom,( ! [X] : ( isa(X,c_spatialthing_nonsituational) => spatialthing_nonsituational(X) ) )). fof(ax1_644,axiom,( ! [X] : ( spatialthing_nonsituational(X) => isa(X,c_spatialthing_nonsituational) ) )). % Cyc Constant #29025: fof(ax1_645,axiom,( ! [X] : ( isa(X,c_militaryperson) => militaryperson(X) ) )). fof(ax1_646,axiom,( ! [X] : ( militaryperson(X) => isa(X,c_militaryperson) ) )). % Cyc Constant #202390: fof(ax1_647,axiom,( ! [X] : ( isa(X,c_tptpcol_15_72793) => tptpcol_15_72793(X) ) )). fof(ax1_648,axiom,( ! [X] : ( tptpcol_15_72793(X) => isa(X,c_tptpcol_15_72793) ) )). % Cyc Constant #156482: fof(ax1_649,axiom,( ! [X] : ( isa(X,c_tptpcol_9_26885) => tptpcol_9_26885(X) ) )). fof(ax1_650,axiom,( ! [X] : ( tptpcol_9_26885(X) => isa(X,c_tptpcol_9_26885) ) )). % Cyc Constant #156483: fof(ax1_651,axiom,( ! [X] : ( isa(X,c_tptpcol_10_26886) => tptpcol_10_26886(X) ) )). fof(ax1_652,axiom,( ! [X] : ( tptpcol_10_26886(X) => isa(X,c_tptpcol_10_26886) ) )). % Cyc Constant #261492: fof(ax1_653,axiom,( ! [ARG1,INS] : ( tptptypes_8_823(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_654,axiom,( ! [INS,ARG2] : ( tptptypes_8_823(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #221866: fof(ax1_655,axiom,( ! [X] : ( isa(X,c_tptpcol_16_92269) => tptpcol_16_92269(X) ) )). fof(ax1_656,axiom,( ! [X] : ( tptpcol_16_92269(X) => isa(X,c_tptpcol_16_92269) ) )). % Cyc Constant #238782: fof(ax1_657,axiom,( ! [X] : ( isa(X,c_tptpcol_15_109185) => tptpcol_15_109185(X) ) )). fof(ax1_658,axiom,( ! [X] : ( tptpcol_15_109185(X) => isa(X,c_tptpcol_15_109185) ) )). % Cyc Constant #156224: fof(ax1_659,axiom,( ! [X] : ( isa(X,c_tptpcol_6_26627) => tptpcol_6_26627(X) ) )). fof(ax1_660,axiom,( ! [X] : ( tptpcol_6_26627(X) => isa(X,c_tptpcol_6_26627) ) )). % Cyc Constant #247713: fof(ax1_661,axiom,( ! [X] : ( isa(X,c_tptpcol_12_118116) => tptpcol_12_118116(X) ) )). fof(ax1_662,axiom,( ! [X] : ( tptpcol_12_118116(X) => isa(X,c_tptpcol_12_118116) ) )). % Cyc Constant #148035: fof(ax1_663,axiom,( ! [X] : ( isa(X,c_tptpcol_8_18438) => tptpcol_8_18438(X) ) )). fof(ax1_664,axiom,( ! [X] : ( tptpcol_8_18438(X) => isa(X,c_tptpcol_8_18438) ) )). % Cyc Constant #160567: fof(ax1_665,axiom,( ! [X] : ( isa(X,c_tptpcol_15_30970) => tptpcol_15_30970(X) ) )). fof(ax1_666,axiom,( ! [X] : ( tptpcol_15_30970(X) => isa(X,c_tptpcol_15_30970) ) )). % Cyc Constant #160569: fof(ax1_667,axiom,( ! [X] : ( isa(X,c_tptpcol_16_30972) => tptpcol_16_30972(X) ) )). fof(ax1_668,axiom,( ! [X] : ( tptpcol_16_30972(X) => isa(X,c_tptpcol_16_30972) ) )). % Cyc Constant #238778: fof(ax1_669,axiom,( ! [X] : ( isa(X,c_tptpcol_14_109181) => tptpcol_14_109181(X) ) )). fof(ax1_670,axiom,( ! [X] : ( tptpcol_14_109181(X) => isa(X,c_tptpcol_14_109181) ) )). % Cyc Constant #57903: fof(ax1_671,axiom,( ! [X] : ( isa(X,c_physicalorderingpredicate) => physicalorderingpredicate(X) ) )). fof(ax1_672,axiom,( ! [X] : ( physicalorderingpredicate(X) => isa(X,c_physicalorderingpredicate) ) )). % Cyc Constant #137335: fof(ax1_673,axiom,( ! [X] : ( isa(X,c_tptpcol_16_7738) => tptpcol_16_7738(X) ) )). fof(ax1_674,axiom,( ! [X] : ( tptpcol_16_7738(X) => isa(X,c_tptpcol_16_7738) ) )). % Cyc Constant #262345: fof(ax1_675,axiom,( ! [ARG1,INS] : ( tptp_8_968(ARG1,INS) => subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(INS) ) )). fof(ax1_676,axiom,( ! [INS,ARG2] : ( tptp_8_968(INS,ARG2) => tptpcol_7_7172(INS) ) )). % Cyc Constant #77435: fof(ax1_677,axiom,( ! [ARG1,ARG2,INS] : ( relationexistsall(ARG1,ARG2,INS) => collection(INS) ) )). fof(ax1_678,axiom,( ! [ARG1,INS,ARG3] : ( relationexistsall(ARG1,INS,ARG3) => collection(INS) ) )). fof(ax1_679,axiom,( ! [INS,ARG2,ARG3] : ( relationexistsall(INS,ARG2,ARG3) => binarypredicate(INS) ) )). % Cyc Constant #156225: fof(ax1_680,axiom,( ! [X] : ( isa(X,c_tptpcol_7_26628) => tptpcol_7_26628(X) ) )). fof(ax1_681,axiom,( ! [X] : ( tptpcol_7_26628(X) => isa(X,c_tptpcol_7_26628) ) )). % Cyc Constant #156226: fof(ax1_682,axiom,( ! [X] : ( isa(X,c_tptpcol_8_26629) => tptpcol_8_26629(X) ) )). fof(ax1_683,axiom,( ! [X] : ( tptpcol_8_26629(X) => isa(X,c_tptpcol_8_26629) ) )). % Cyc Constant #244285: fof(ax1_684,axiom,( ! [X] : ( isa(X,c_tptpcol_3_114688) => tptpcol_3_114688(X) ) )). fof(ax1_685,axiom,( ! [X] : ( tptpcol_3_114688(X) => isa(X,c_tptpcol_3_114688) ) )). % Cyc Constant #113102: fof(ax1_686,axiom,( ! [ARG1] : natfunction(f_contextofpcwfn(ARG1),c_contextofpcwfn) )). fof(ax1_687,axiom,( ! [ARG1] : natargument(f_contextofpcwfn(ARG1),n_1,ARG1) )). fof(ax1_688,axiom,( ! [ARG1] : microtheory(f_contextofpcwfn(ARG1)) )). % Cyc Constant #54485: fof(ax1_689,axiom,( ! [ARG1,INS] : ( arg1isa(ARG1,INS) => collection(INS) ) )). fof(ax1_690,axiom,( ! [INS,ARG2] : ( arg1isa(INS,ARG2) => relation(INS) ) )). fof(ax1_691,axiom,( ! [ARG1,OLD,NEW] : ( ( arg1isa(ARG1,OLD) & genls(OLD,NEW) ) => arg1isa(ARG1,NEW) ) )). fof(ax1_692,axiom,( ! [ARG1,OLD,NEW] : ( ( arg1isa(ARG1,OLD) & genls(OLD,NEW) ) => arg1isa(ARG1,NEW) ) )). % Cyc Constant #66840: fof(ax1_693,axiom,( ! [ARG1,INS] : ( objectfoundinlocation(ARG1,INS) => spatialthing_nonsituational(INS) ) )). fof(ax1_694,axiom,( ! [ARG1,INS] : ( objectfoundinlocation(ARG1,INS) => spatialthing_localized(INS) ) )). fof(ax1_695,axiom,( ! [INS,ARG2] : ( objectfoundinlocation(INS,ARG2) => spatialthing_nonsituational(INS) ) )). fof(ax1_696,axiom,( ! [INS,ARG2] : ( objectfoundinlocation(INS,ARG2) => spatialthing_localized(INS) ) )). fof(ax1_697,axiom,( ! [X,Y,Z] : ( ( objectfoundinlocation(X,Y) & objectfoundinlocation(Y,Z) ) => objectfoundinlocation(X,Z) ) )). fof(ax1_698,axiom,( ! [X] : ~ objectfoundinlocation(X,X) )). fof(ax1_699,axiom,( ! [ARG1,OLD,NEW] : ( ( objectfoundinlocation(ARG1,OLD) & geopoliticalsubdivision(NEW,OLD) ) => objectfoundinlocation(ARG1,NEW) ) )). fof(ax1_700,axiom,( ! [ARG1,OLD,NEW] : ( ( objectfoundinlocation(ARG1,OLD) & geographicallysubsumes(NEW,OLD) ) => objectfoundinlocation(ARG1,NEW) ) )). fof(ax1_701,axiom,( ! [ARG1,OLD,NEW] : ( ( objectfoundinlocation(ARG1,OLD) & subregions(NEW,OLD) ) => objectfoundinlocation(ARG1,NEW) ) )). % Cyc Constant #54624: fof(ax1_702,axiom,( ! [X] : ( isa(X,c_ship) => ship(X) ) )). fof(ax1_703,axiom,( ! [X] : ( ship(X) => isa(X,c_ship) ) )). % Cyc Constant #93912: fof(ax1_704,axiom,( ! [ARG1,ARG2,ARG3] : natfunction(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),c_subcollectionofwithrelationtofn) )). fof(ax1_705,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),n_1,ARG1) )). fof(ax1_706,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),n_2,ARG2) )). fof(ax1_707,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),n_3,ARG3) )). fof(ax1_708,axiom,( ! [ARG1,ARG2,ARG3] : collection(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3)) )). % Cyc NART #11809: fof(ax1_709,axiom,( ! [X] : ( isa(X,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) => subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X) ) )). fof(ax1_710,axiom,( ! [X] : ( subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X) => isa(X,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ) )). % Cyc Constant #195136: fof(ax1_711,axiom,( ! [X] : ( isa(X,c_tptpcol_4_65539) => tptpcol_4_65539(X) ) )). fof(ax1_712,axiom,( ! [X] : ( tptpcol_4_65539(X) => isa(X,c_tptpcol_4_65539) ) )). % Cyc Constant #199232: fof(ax1_713,axiom,( ! [X] : ( isa(X,c_tptpcol_5_69635) => tptpcol_5_69635(X) ) )). fof(ax1_714,axiom,( ! [X] : ( tptpcol_5_69635(X) => isa(X,c_tptpcol_5_69635) ) )). % Cyc Constant #145983: fof(ax1_715,axiom,( ! [X] : ( isa(X,c_tptpcol_3_16386) => tptpcol_3_16386(X) ) )). fof(ax1_716,axiom,( ! [X] : ( tptpcol_3_16386(X) => isa(X,c_tptpcol_3_16386) ) )). % Cyc Constant #117270: fof(ax1_717,axiom,( ! [ARG1,INS] : ( no(ARG1,INS) => setorcollection(INS) ) )). fof(ax1_718,axiom,( ! [INS,ARG2] : ( no(INS,ARG2) => setorcollection(INS) ) )). fof(ax1_719,axiom,( ! [X,Y] : ( no(X,Y) => no(Y,X) ) )). fof(ax1_720,axiom,( ! [ARG1,OLD,NEW] : ( ( no(ARG1,OLD) & subsetof(NEW,OLD) ) => no(ARG1,NEW) ) )). fof(ax1_721,axiom,( ! [OLD,ARG2,NEW] : ( ( no(OLD,ARG2) & subsetof(NEW,OLD) ) => no(NEW,ARG2) ) )). fof(ax1_722,axiom,( ! [OLD,ARG2,NEW] : ( ( no(OLD,ARG2) & genls(NEW,OLD) ) => no(NEW,ARG2) ) )). fof(ax1_723,axiom,( ! [ARG1,OLD,NEW] : ( ( no(ARG1,OLD) & genls(NEW,OLD) ) => no(ARG1,NEW) ) )). fof(ax1_724,axiom,( ! [OLD,ARG2,NEW] : ( ( no(OLD,ARG2) & subsetof(NEW,OLD) ) => no(NEW,ARG2) ) )). fof(ax1_725,axiom,( ! [ARG1,OLD,NEW] : ( ( no(ARG1,OLD) & subsetof(NEW,OLD) ) => no(ARG1,NEW) ) )). % Cyc Constant #30683: fof(ax1_726,axiom,( ! [X] : ( isa(X,c_geographicalregion) => geographicalregion(X) ) )). fof(ax1_727,axiom,( ! [X] : ( geographicalregion(X) => isa(X,c_geographicalregion) ) )). % Cyc Constant #347777: fof(ax1_728,axiom,( ! [ARG1] : natfunction(f_tptpquantityfn_21(ARG1),c_tptpquantityfn_21) )). fof(ax1_729,axiom,( ! [ARG1] : natargument(f_tptpquantityfn_21(ARG1),n_1,ARG1) )). fof(ax1_730,axiom,( ! [ARG1] : tptpquantity(f_tptpquantityfn_21(ARG1)) )). % Cyc Constant #57264: fof(ax1_731,axiom,( ! [ARG1,INS] : ( airporthasiatacode(ARG1,INS) => stringoflengthfn3(INS) ) )). fof(ax1_732,axiom,( ! [INS,ARG2] : ( airporthasiatacode(INS,ARG2) => airport_physical(INS) ) )). % Cyc Constant #87761: fof(ax1_733,axiom,( ! [X] : ( isa(X,c_airport_physical) => airport_physical(X) ) )). fof(ax1_734,axiom,( ! [X] : ( airport_physical(X) => isa(X,c_airport_physical) ) )). % Cyc Constant #53540: fof(ax1_735,axiom,( ! [ARG1,ARG2,ARG3] : natfunction(f_instancewithrelationtofn(ARG1,ARG2,ARG3),c_instancewithrelationtofn) )). fof(ax1_736,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_instancewithrelationtofn(ARG1,ARG2,ARG3),n_1,ARG1) )). fof(ax1_737,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_instancewithrelationtofn(ARG1,ARG2,ARG3),n_2,ARG2) )). fof(ax1_738,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_instancewithrelationtofn(ARG1,ARG2,ARG3),n_3,ARG3) )). fof(ax1_739,axiom,( ! [ARG1,ARG2,ARG3] : thing(f_instancewithrelationtofn(ARG1,ARG2,ARG3)) )). % Cyc Constant #242238: fof(ax1_740,axiom,( ! [X] : ( isa(X,c_tptpcol_6_112641) => tptpcol_6_112641(X) ) )). fof(ax1_741,axiom,( ! [X] : ( tptpcol_6_112641(X) => isa(X,c_tptpcol_6_112641) ) )). % Cyc Constant #243262: fof(ax1_742,axiom,( ! [X] : ( isa(X,c_tptpcol_7_113665) => tptpcol_7_113665(X) ) )). fof(ax1_743,axiom,( ! [X] : ( tptpcol_7_113665(X) => isa(X,c_tptpcol_7_113665) ) )). % Cyc Constant #104935: fof(ax1_744,axiom,( ! [X] : ( isa(X,c_artifact) => artifact(X) ) )). fof(ax1_745,axiom,( ! [X] : ( artifact(X) => isa(X,c_artifact) ) )). % Cyc Constant #148261: fof(ax1_746,axiom,( ! [X] : ( isa(X,c_tptpcol_13_18664) => tptpcol_13_18664(X) ) )). fof(ax1_747,axiom,( ! [X] : ( tptpcol_13_18664(X) => isa(X,c_tptpcol_13_18664) ) )). % Cyc Constant #108957: fof(ax1_748,axiom,( ! [X] : ( isa(X,c_firstordercollection) => firstordercollection(X) ) )). fof(ax1_749,axiom,( ! [X] : ( firstordercollection(X) => isa(X,c_firstordercollection) ) )). % Cyc Constant #347770: fof(ax1_750,axiom,( ! [ARG1] : natfunction(f_tptpquantityfn_14(ARG1),c_tptpquantityfn_14) )). fof(ax1_751,axiom,( ! [ARG1] : natargument(f_tptpquantityfn_14(ARG1),n_1,ARG1) )). fof(ax1_752,axiom,( ! [ARG1] : tptpquantity(f_tptpquantityfn_14(ARG1)) )). % Cyc Constant #3361: fof(ax1_753,axiom,( ! [X] : ( isa(X,c_supplies) => supplies(X) ) )). fof(ax1_754,axiom,( ! [X] : ( supplies(X) => isa(X,c_supplies) ) )). % Cyc Constant #117378: fof(ax1_755,axiom,( ! [X] : ( isa(X,c_inanimateobject_nonnatural) => inanimateobject_nonnatural(X) ) )). fof(ax1_756,axiom,( ! [X] : ( inanimateobject_nonnatural(X) => isa(X,c_inanimateobject_nonnatural) ) )). % Cyc Constant #151668: fof(ax1_757,axiom,( ! [X] : ( isa(X,c_tptpcol_13_22071) => tptpcol_13_22071(X) ) )). fof(ax1_758,axiom,( ! [X] : ( tptpcol_13_22071(X) => isa(X,c_tptpcol_13_22071) ) )). % Cyc Constant #151669: fof(ax1_759,axiom,( ! [X] : ( isa(X,c_tptpcol_14_22072) => tptpcol_14_22072(X) ) )). fof(ax1_760,axiom,( ! [X] : ( tptpcol_14_22072(X) => isa(X,c_tptpcol_14_22072) ) )). % Cyc Constant #238144: fof(ax1_761,axiom,( ! [X] : ( isa(X,c_tptpcol_7_108547) => tptpcol_7_108547(X) ) )). fof(ax1_762,axiom,( ! [X] : ( tptpcol_7_108547(X) => isa(X,c_tptpcol_7_108547) ) )). % Cyc Constant #238656: fof(ax1_763,axiom,( ! [X] : ( isa(X,c_tptpcol_8_109059) => tptpcol_8_109059(X) ) )). fof(ax1_764,axiom,( ! [X] : ( tptpcol_8_109059(X) => isa(X,c_tptpcol_8_109059) ) )). % Cyc Constant #223371: fof(ax1_765,axiom,( ! [X] : ( isa(X,c_tptpcol_14_93774) => tptpcol_14_93774(X) ) )). fof(ax1_766,axiom,( ! [X] : ( tptpcol_14_93774(X) => isa(X,c_tptpcol_14_93774) ) )). % Cyc Constant #223372: fof(ax1_767,axiom,( ! [X] : ( isa(X,c_tptpcol_15_93775) => tptpcol_15_93775(X) ) )). fof(ax1_768,axiom,( ! [X] : ( tptpcol_15_93775(X) => isa(X,c_tptpcol_15_93775) ) )). % Cyc Constant #138483: fof(ax1_769,axiom,( ! [X] : ( isa(X,c_tptpcol_16_8886) => tptpcol_16_8886(X) ) )). fof(ax1_770,axiom,( ! [X] : ( tptpcol_16_8886(X) => isa(X,c_tptpcol_16_8886) ) )). % Cyc Constant #119679: fof(ax1_771,axiom,( ! [ARG1,INS] : ( orientation(ARG1,INS) => orientationvector(INS) ) )). fof(ax1_772,axiom,( ! [INS,ARG2] : ( orientation(INS,ARG2) => spatialthing_localized(INS) ) )). % Cyc Constant #24557: fof(ax1_773,axiom,( ! [X] : ( isa(X,c_orientationvector) => orientationvector(X) ) )). fof(ax1_774,axiom,( ! [X] : ( orientationvector(X) => isa(X,c_orientationvector) ) )). % Cyc NART #18865: fof(ax1_775,axiom,( ! [X] : ( isa(X,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible)) => subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(X) ) )). fof(ax1_776,axiom,( ! [X] : ( subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(X) => isa(X,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible)) ) )). % Cyc Constant #261493: fof(ax1_777,axiom,( ! [ARG1,INS] : ( tptptypes_9_824(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_778,axiom,( ! [INS,ARG2] : ( tptptypes_9_824(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261065: fof(ax1_779,axiom,( ! [ARG1,INS] : ( tptptypes_7_396(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_780,axiom,( ! [INS,ARG2] : ( tptptypes_7_396(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #151652: fof(ax1_781,axiom,( ! [X] : ( isa(X,c_tptpcol_12_22055) => tptpcol_12_22055(X) ) )). fof(ax1_782,axiom,( ! [X] : ( tptpcol_12_22055(X) => isa(X,c_tptpcol_12_22055) ) )). % Cyc Constant #159087: fof(ax1_783,axiom,( ! [X] : ( isa(X,c_tptpcol_16_29490) => tptpcol_16_29490(X) ) )). fof(ax1_784,axiom,( ! [X] : ( tptpcol_16_29490(X) => isa(X,c_tptpcol_16_29490) ) )). % Cyc Constant #262228: fof(ax1_785,axiom,( ! [ARG1,INS] : ( tptp_9_720(ARG1,INS) => tptpcol_5_28674(INS) ) )). fof(ax1_786,axiom,( ! [INS,ARG2] : ( tptp_9_720(INS,ARG2) => executionbyfiringsquad(INS) ) )). % Cyc Constant #110446: fof(ax1_787,axiom,( ! [X] : ( isa(X,c_runningshorts) => runningshorts(X) ) )). fof(ax1_788,axiom,( ! [X] : ( runningshorts(X) => isa(X,c_runningshorts) ) )). % Cyc Constant #247616: fof(ax1_789,axiom,( ! [X] : ( isa(X,c_tptpcol_9_118019) => tptpcol_9_118019(X) ) )). fof(ax1_790,axiom,( ! [X] : ( tptpcol_9_118019(X) => isa(X,c_tptpcol_9_118019) ) )). % Cyc Constant #161465: fof(ax1_791,axiom,( ! [X] : ( isa(X,c_tptpcol_16_31868) => tptpcol_16_31868(X) ) )). fof(ax1_792,axiom,( ! [X] : ( tptpcol_16_31868(X) => isa(X,c_tptpcol_16_31868) ) )). % Cyc Constant #63493: fof(ax1_793,axiom,( ! [X] : ( isa(X,c_movement_translationevent) => movement_translationevent(X) ) )). fof(ax1_794,axiom,( ! [X] : ( movement_translationevent(X) => isa(X,c_movement_translationevent) ) )). % Cyc Constant #99582: fof(ax1_795,axiom,( ! [ARG1,INS] : ( directionoftranslation_throughout(ARG1,INS) => unitvectorinterval(INS) ) )). fof(ax1_796,axiom,( ! [INS,ARG2] : ( directionoftranslation_throughout(INS,ARG2) => movement_translationevent(INS) ) )). fof(ax1_797,axiom,( ! [OLD,ARG2,NEW] : ( ( directionoftranslation_throughout(OLD,ARG2) & subevents(OLD,NEW) ) => directionoftranslation_throughout(NEW,ARG2) ) )). % Cyc Constant #19603: fof(ax1_798,axiom,( ! [X] : ( isa(X,c_unitvectorinterval) => unitvectorinterval(X) ) )). fof(ax1_799,axiom,( ! [X] : ( unitvectorinterval(X) => isa(X,c_unitvectorinterval) ) )). % Cyc NART #89985: fof(ax1_800,axiom,( ! [X] : ( isa(X,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) => subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(X) ) )). fof(ax1_801,axiom,( ! [X] : ( subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(X) => isa(X,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) ) )). % Cyc Constant #261842: fof(ax1_802,axiom,( ! [ARG1,INS] : ( tptp_8_875(ARG1,INS) => tptpcol_4_24578(INS) ) )). fof(ax1_803,axiom,( ! [INS,ARG2] : ( tptp_8_875(INS,ARG2) => subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(INS) ) )). % Cyc Constant #67447: fof(ax1_804,axiom,( ! [ARG1,ARG2,INS] : ( relationallexists(ARG1,ARG2,INS) => collection(INS) ) )). fof(ax1_805,axiom,( ! [ARG1,INS,ARG3] : ( relationallexists(ARG1,INS,ARG3) => collection(INS) ) )). fof(ax1_806,axiom,( ! [INS,ARG2,ARG3] : ( relationallexists(INS,ARG2,ARG3) => binarypredicate(INS) ) )). % Cyc Constant #139855: fof(ax1_807,axiom,( ! [X] : ( isa(X,c_tptpcol_16_10258) => tptpcol_16_10258(X) ) )). fof(ax1_808,axiom,( ! [X] : ( tptpcol_16_10258(X) => isa(X,c_tptpcol_16_10258) ) )). % Cyc Constant #79680: fof(ax1_809,axiom,( ! [X] : ( isa(X,c_pushingababycarriage) => pushingababycarriage(X) ) )). fof(ax1_810,axiom,( ! [X] : ( pushingababycarriage(X) => isa(X,c_pushingababycarriage) ) )). % Cyc Constant #86735: fof(ax1_811,axiom,( ! [X] : ( isa(X,c_aspatialinformationstore) => aspatialinformationstore(X) ) )). fof(ax1_812,axiom,( ! [X] : ( aspatialinformationstore(X) => isa(X,c_aspatialinformationstore) ) )). % Cyc Constant #19726: fof(ax1_813,axiom,( ! [X] : ( isa(X,c_collection) => collection(X) ) )). fof(ax1_814,axiom,( ! [X] : ( collection(X) => isa(X,c_collection) ) )). % Cyc Constant #108004: fof(ax1_815,axiom,( ! [X] : ( isa(X,c_fixedordercollection) => fixedordercollection(X) ) )). fof(ax1_816,axiom,( ! [X] : ( fixedordercollection(X) => isa(X,c_fixedordercollection) ) )). % Cyc Constant #221761: fof(ax1_817,axiom,( ! [X] : ( isa(X,c_tptpcol_8_92164) => tptpcol_8_92164(X) ) )). fof(ax1_818,axiom,( ! [X] : ( tptpcol_8_92164(X) => isa(X,c_tptpcol_8_92164) ) )). % Cyc Constant #221762: fof(ax1_819,axiom,( ! [X] : ( isa(X,c_tptpcol_9_92165) => tptpcol_9_92165(X) ) )). fof(ax1_820,axiom,( ! [X] : ( tptpcol_9_92165(X) => isa(X,c_tptpcol_9_92165) ) )). % Cyc Constant #129598: fof(ax1_821,axiom,( ! [X] : ( isa(X,c_tptpcol_1_1) => tptpcol_1_1(X) ) )). fof(ax1_822,axiom,( ! [X] : ( tptpcol_1_1(X) => isa(X,c_tptpcol_1_1) ) )). % Cyc Constant #129599: fof(ax1_823,axiom,( ! [X] : ( isa(X,c_tptpcol_2_2) => tptpcol_2_2(X) ) )). fof(ax1_824,axiom,( ! [X] : ( tptpcol_2_2(X) => isa(X,c_tptpcol_2_2) ) )). % Cyc Constant #261360: fof(ax1_825,axiom,( ! [ARG1,INS] : ( tptptypes_7_691(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_826,axiom,( ! [INS,ARG2] : ( tptptypes_7_691(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #156484: fof(ax1_827,axiom,( ! [X] : ( isa(X,c_tptpcol_11_26887) => tptpcol_11_26887(X) ) )). fof(ax1_828,axiom,( ! [X] : ( tptpcol_11_26887(X) => isa(X,c_tptpcol_11_26887) ) )). % Cyc Constant #156516: fof(ax1_829,axiom,( ! [X] : ( isa(X,c_tptpcol_12_26919) => tptpcol_12_26919(X) ) )). fof(ax1_830,axiom,( ! [X] : ( tptpcol_12_26919(X) => isa(X,c_tptpcol_12_26919) ) )). % Cyc Constant #261487: fof(ax1_831,axiom,( ! [ARG1,INS] : ( tptptypes_6_818(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_832,axiom,( ! [INS,ARG2] : ( tptptypes_6_818(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261488: fof(ax1_833,axiom,( ! [ARG1,INS] : ( tptptypes_7_819(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_834,axiom,( ! [INS,ARG2] : ( tptptypes_7_819(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #24246: fof(ax1_835,axiom,( ! [X] : ( isa(X,c_correctivelensprescription) => correctivelensprescription(X) ) )). fof(ax1_836,axiom,( ! [X] : ( correctivelensprescription(X) => isa(X,c_correctivelensprescription) ) )). % Cyc Constant #117987: fof(ax1_837,axiom,( ! [ARG1,INS] : ( products(ARG1,INS) => artifact(INS) ) )). fof(ax1_838,axiom,( ! [INS,ARG2] : ( products(INS,ARG2) => creationordestructionevent(INS) ) )). % Cyc Constant #98187: fof(ax1_839,axiom,( ! [X] : ( isa(X,c_issuingaprescription) => issuingaprescription(X) ) )). fof(ax1_840,axiom,( ! [X] : ( issuingaprescription(X) => isa(X,c_issuingaprescription) ) )). % Cyc Constant #37503: fof(ax1_841,axiom,( ! [ARG1,ARG2,ARG3] : natfunction(f_subcollectionofwithrelationtotypefn(ARG1,ARG2,ARG3),c_subcollectionofwithrelationtotypefn) )). fof(ax1_842,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtotypefn(ARG1,ARG2,ARG3),n_1,ARG1) )). fof(ax1_843,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtotypefn(ARG1,ARG2,ARG3),n_2,ARG2) )). fof(ax1_844,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtotypefn(ARG1,ARG2,ARG3),n_3,ARG3) )). fof(ax1_845,axiom,( ! [ARG1,ARG2,ARG3] : collection(f_subcollectionofwithrelationtotypefn(ARG1,ARG2,ARG3)) )). % Cyc NART #53069: fof(ax1_846,axiom,( ! [X] : ( isa(X,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)) => subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(X) ) )). fof(ax1_847,axiom,( ! [X] : ( subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(X) => isa(X,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)) ) )). % Cyc Constant #101351: fof(ax1_848,axiom,( ! [X] : ( isa(X,c_mathematicalorcomputationalthing) => mathematicalorcomputationalthing(X) ) )). fof(ax1_849,axiom,( ! [X] : ( mathematicalorcomputationalthing(X) => isa(X,c_mathematicalorcomputationalthing) ) )). % Cyc Constant #247617: fof(ax1_850,axiom,( ! [X] : ( isa(X,c_tptpcol_10_118020) => tptpcol_10_118020(X) ) )). fof(ax1_851,axiom,( ! [X] : ( tptpcol_10_118020(X) => isa(X,c_tptpcol_10_118020) ) )). % Cyc Constant #247681: fof(ax1_852,axiom,( ! [X] : ( isa(X,c_tptpcol_11_118084) => tptpcol_11_118084(X) ) )). fof(ax1_853,axiom,( ! [X] : ( tptpcol_11_118084(X) => isa(X,c_tptpcol_11_118084) ) )). % Cyc Constant #124241: fof(ax1_854,axiom,( ! [X] : ( isa(X,c_terroristgroup) => terroristgroup(X) ) )). fof(ax1_855,axiom,( ! [X] : ( terroristgroup(X) => isa(X,c_terroristgroup) ) )). % Cyc Constant #87244: fof(ax1_856,axiom,( ! [ARG1,INS] : ( hasmembers(ARG1,INS) => agent_generic(INS) ) )). fof(ax1_857,axiom,( ! [INS,ARG2] : ( hasmembers(INS,ARG2) => organization(INS) ) )). % Cyc Constant #65146: fof(ax1_858,axiom,( ! [X] : ( isa(X,c_terrorist) => terrorist(X) ) )). fof(ax1_859,axiom,( ! [X] : ( terrorist(X) => isa(X,c_terrorist) ) )). % Cyc Constant #42488: fof(ax1_860,axiom,( ! [ARG1,ARG2,ARG3] : natfunction(f_subcollectionofwithrelationfromtypefn(ARG1,ARG2,ARG3),c_subcollectionofwithrelationfromtypefn) )). fof(ax1_861,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationfromtypefn(ARG1,ARG2,ARG3),n_1,ARG1) )). fof(ax1_862,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationfromtypefn(ARG1,ARG2,ARG3),n_2,ARG2) )). fof(ax1_863,axiom,( ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationfromtypefn(ARG1,ARG2,ARG3),n_3,ARG3) )). fof(ax1_864,axiom,( ! [ARG1,ARG2,ARG3] : collection(f_subcollectionofwithrelationfromtypefn(ARG1,ARG2,ARG3)) )). % Cyc NART #80403: fof(ax1_865,axiom,( ! [X] : ( isa(X,f_subcollectionofwithrelationfromtypefn(c_terrorist,c_hasmembers,c_terroristgroup)) => subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(X) ) )). fof(ax1_866,axiom,( ! [X] : ( subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(X) => isa(X,f_subcollectionofwithrelationfromtypefn(c_terrorist,c_hasmembers,c_terroristgroup)) ) )). % Cyc Constant #54126: fof(ax1_867,axiom,( ! [ARG1,INS] : ( prettystring(ARG1,INS) => controlcharacterfreestring(INS) ) )). fof(ax1_868,axiom,( ! [INS,ARG2] : ( prettystring(INS,ARG2) => thing(INS) ) )). % Cyc Constant #129596: fof(ax1_869,axiom,( ! [X] : ( isa(X,c_tptpcol_0_0) => tptpcol_0_0(X) ) )). fof(ax1_870,axiom,( ! [X] : ( tptpcol_0_0(X) => isa(X,c_tptpcol_0_0) ) )). % Cyc Constant #380145: fof(ax1_871,axiom,( ! [X] : ( isa(X,c_geolevel_3) => geolevel_3(X) ) )). fof(ax1_872,axiom,( ! [X] : ( geolevel_3(X) => isa(X,c_geolevel_3) ) )). % Cyc Constant #154175: fof(ax1_873,axiom,( ! [X] : ( isa(X,c_tptpcol_4_24578) => tptpcol_4_24578(X) ) )). fof(ax1_874,axiom,( ! [X] : ( tptpcol_4_24578(X) => isa(X,c_tptpcol_4_24578) ) )). % Cyc Constant #154176: fof(ax1_875,axiom,( ! [X] : ( isa(X,c_tptpcol_5_24579) => tptpcol_5_24579(X) ) )). fof(ax1_876,axiom,( ! [X] : ( tptpcol_5_24579(X) => isa(X,c_tptpcol_5_24579) ) )). % Cyc Constant #236095: fof(ax1_877,axiom,( ! [X] : ( isa(X,c_tptpcol_5_106498) => tptpcol_5_106498(X) ) )). fof(ax1_878,axiom,( ! [X] : ( tptpcol_5_106498(X) => isa(X,c_tptpcol_5_106498) ) )). % Cyc Constant #238754: fof(ax1_879,axiom,( ! [X] : ( isa(X,c_tptpcol_12_109157) => tptpcol_12_109157(X) ) )). fof(ax1_880,axiom,( ! [X] : ( tptpcol_12_109157(X) => isa(X,c_tptpcol_12_109157) ) )). % Cyc Constant #238770: fof(ax1_881,axiom,( ! [X] : ( isa(X,c_tptpcol_13_109173) => tptpcol_13_109173(X) ) )). fof(ax1_882,axiom,( ! [X] : ( tptpcol_13_109173(X) => isa(X,c_tptpcol_13_109173) ) )). % Cyc Constant #89394: fof(ax1_883,axiom,( ! [X] : ( isa(X,c_mathematicalthing) => mathematicalthing(X) ) )). fof(ax1_884,axiom,( ! [X] : ( mathematicalthing(X) => isa(X,c_mathematicalthing) ) )). % Cyc Constant #29216: fof(ax1_885,axiom,( ! [X] : ( isa(X,c_setorcollection) => setorcollection(X) ) )). fof(ax1_886,axiom,( ! [X] : ( setorcollection(X) => isa(X,c_setorcollection) ) )). % Cyc Constant #148228: fof(ax1_887,axiom,( ! [X] : ( isa(X,c_tptpcol_11_18631) => tptpcol_11_18631(X) ) )). fof(ax1_888,axiom,( ! [X] : ( tptpcol_11_18631(X) => isa(X,c_tptpcol_11_18631) ) )). % Cyc Constant #148260: fof(ax1_889,axiom,( ! [X] : ( isa(X,c_tptpcol_12_18663) => tptpcol_12_18663(X) ) )). fof(ax1_890,axiom,( ! [X] : ( tptpcol_12_18663(X) => isa(X,c_tptpcol_12_18663) ) )). % Cyc Constant #261069: fof(ax1_891,axiom,( ! [ARG1,INS] : ( tptptypes_8_400(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_892,axiom,( ! [INS,ARG2] : ( tptptypes_8_400(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261070: fof(ax1_893,axiom,( ! [ARG1,INS] : ( tptptypes_9_401(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_894,axiom,( ! [INS,ARG2] : ( tptptypes_9_401(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #347769: fof(ax1_895,axiom,( ! [ARG1] : natfunction(f_tptpquantityfn_13(ARG1),c_tptpquantityfn_13) )). fof(ax1_896,axiom,( ! [ARG1] : natargument(f_tptpquantityfn_13(ARG1),n_1,ARG1) )). fof(ax1_897,axiom,( ! [ARG1] : tptpquantity(f_tptpquantityfn_13(ARG1)) )). % Cyc Constant #24863: fof(ax1_898,axiom,( ! [ARG1,INS] : ( borderson(ARG1,INS) => geographicalregion(INS) ) )). fof(ax1_899,axiom,( ! [INS,ARG2] : ( borderson(INS,ARG2) => geographicalregion(INS) ) )). fof(ax1_900,axiom,( ! [X,Y] : ( borderson(X,Y) => borderson(Y,X) ) )). fof(ax1_901,axiom,( ! [X] : ~ borderson(X,X) )). % Cyc Constant #221861: fof(ax1_902,axiom,( ! [X] : ( isa(X,c_tptpcol_14_92264) => tptpcol_14_92264(X) ) )). fof(ax1_903,axiom,( ! [X] : ( tptpcol_14_92264(X) => isa(X,c_tptpcol_14_92264) ) )). % Cyc Constant #221865: fof(ax1_904,axiom,( ! [X] : ( isa(X,c_tptpcol_15_92268) => tptpcol_15_92268(X) ) )). fof(ax1_905,axiom,( ! [X] : ( tptpcol_15_92268(X) => isa(X,c_tptpcol_15_92268) ) )). % Cyc Constant #246335: fof(ax1_906,axiom,( ! [X] : ( isa(X,c_tptpcol_6_116738) => tptpcol_6_116738(X) ) )). fof(ax1_907,axiom,( ! [X] : ( tptpcol_6_116738(X) => isa(X,c_tptpcol_6_116738) ) )). % Cyc Constant #261056: fof(ax1_908,axiom,( ! [ARG1,INS] : ( tptptypes_5_387(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_909,axiom,( ! [INS,ARG2] : ( tptptypes_5_387(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261057: fof(ax1_910,axiom,( ! [ARG1,INS] : ( tptptypes_6_388(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_911,axiom,( ! [INS,ARG2] : ( tptptypes_6_388(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #104695: fof(ax1_912,axiom,( ! [X] : ( isa(X,c_shavingrazor_manual) => shavingrazor_manual(X) ) )). fof(ax1_913,axiom,( ! [X] : ( shavingrazor_manual(X) => isa(X,c_shavingrazor_manual) ) )). % Cyc Constant #238657: fof(ax1_914,axiom,( ! [X] : ( isa(X,c_tptpcol_9_109060) => tptpcol_9_109060(X) ) )). fof(ax1_915,axiom,( ! [X] : ( tptpcol_9_109060(X) => isa(X,c_tptpcol_9_109060) ) )). % Cyc Constant #238658: fof(ax1_916,axiom,( ! [X] : ( isa(X,c_tptpcol_10_109061) => tptpcol_10_109061(X) ) )). fof(ax1_917,axiom,( ! [X] : ( tptpcol_10_109061(X) => isa(X,c_tptpcol_10_109061) ) )). % Cyc Constant #33466: fof(ax1_918,axiom,( ! [X] : ( isa(X,c_executionbyfiringsquad) => executionbyfiringsquad(X) ) )). fof(ax1_919,axiom,( ! [X] : ( executionbyfiringsquad(X) => isa(X,c_executionbyfiringsquad) ) )). % Cyc Constant #80185: fof(ax1_920,axiom,( mtvisible(c_corecyclmt) )). % Cyc Constant #96482: fof(ax1_921,axiom,( ! [X] : ( isa(X,c_navypersonnel) => navypersonnel(X) ) )). fof(ax1_922,axiom,( ! [X] : ( navypersonnel(X) => isa(X,c_navypersonnel) ) )). % Cyc Constant #221859: fof(ax1_923,axiom,( ! [X] : ( isa(X,c_tptpcol_12_92262) => tptpcol_12_92262(X) ) )). fof(ax1_924,axiom,( ! [X] : ( tptpcol_12_92262(X) => isa(X,c_tptpcol_12_92262) ) )). % Cyc Constant #48859: fof(ax1_925,axiom,( ! [X] : ( isa(X,c_thing) => thing(X) ) )). fof(ax1_926,axiom,( ! [X] : ( thing(X) => isa(X,c_thing) ) )). % Cyc Constant #2465: fof(ax1_927,axiom,( ! [X] : ( isa(X,c_computerdataartifact) => computerdataartifact(X) ) )). fof(ax1_928,axiom,( ! [X] : ( computerdataartifact(X) => isa(X,c_computerdataartifact) ) )). % Cyc Constant #50366: fof(ax1_929,axiom,( ! [X] : ( isa(X,c_applicationcontext) => applicationcontext(X) ) )). fof(ax1_930,axiom,( ! [X] : ( applicationcontext(X) => isa(X,c_applicationcontext) ) )). % Cyc Constant #98385: fof(ax1_931,axiom,( ! [ARG1,INS] : ( inregion(ARG1,INS) => spatialthing_nonsituational(INS) ) )). fof(ax1_932,axiom,( ! [INS,ARG2] : ( inregion(INS,ARG2) => spatialthing_nonsituational(INS) ) )). fof(ax1_933,axiom,( ! [X,Y,Z] : ( ( inregion(X,Y) & inregion(Y,Z) ) => inregion(X,Z) ) )). fof(ax1_934,axiom,( ! [X] : ( spatialthing_nonsituational(X) => inregion(X,X) ) )). % Cyc Constant #347757: fof(ax1_935,axiom,( ! [ARG1] : natfunction(f_tptpquantityfn_1(ARG1),c_tptpquantityfn_1) )). fof(ax1_936,axiom,( ! [ARG1] : natargument(f_tptpquantityfn_1(ARG1),n_1,ARG1) )). fof(ax1_937,axiom,( ! [ARG1] : tptpquantity(f_tptpquantityfn_1(ARG1)) )). % Cyc Constant #9718: fof(ax1_938,axiom,( ! [X] : ( isa(X,c_furpelt) => furpelt(X) ) )). fof(ax1_939,axiom,( ! [X] : ( furpelt(X) => isa(X,c_furpelt) ) )). % Cyc Constant #347754: fof(ax1_940,axiom,( ! [ARG1,INS] : ( tptpofobject(ARG1,INS) => tptpquantity(INS) ) )). fof(ax1_941,axiom,( ! [INS,ARG2] : ( tptpofobject(INS,ARG2) => partiallytangible(INS) ) )). % Cyc Constant #3338: fof(ax1_942,axiom,( ! [ARG1,ARG2,INS] : ( relationallinstance(ARG1,ARG2,INS) => thing(INS) ) )). fof(ax1_943,axiom,( ! [ARG1,INS,ARG3] : ( relationallinstance(ARG1,INS,ARG3) => collection(INS) ) )). fof(ax1_944,axiom,( ! [INS,ARG2,ARG3] : ( relationallinstance(INS,ARG2,ARG3) => binarypredicate(INS) ) )). % Cyc Constant #223363: fof(ax1_945,axiom,( ! [X] : ( isa(X,c_tptpcol_13_93766) => tptpcol_13_93766(X) ) )). fof(ax1_946,axiom,( ! [X] : ( tptpcol_13_93766(X) => isa(X,c_tptpcol_13_93766) ) )). % Cyc Constant #169793: fof(ax1_947,axiom,( ! [X] : ( isa(X,c_tptpcol_9_40196) => tptpcol_9_40196(X) ) )). fof(ax1_948,axiom,( ! [X] : ( tptpcol_9_40196(X) => isa(X,c_tptpcol_9_40196) ) )). % Cyc Constant #169921: fof(ax1_949,axiom,( ! [X] : ( isa(X,c_tptpcol_10_40324) => tptpcol_10_40324(X) ) )). fof(ax1_950,axiom,( ! [X] : ( tptpcol_10_40324(X) => isa(X,c_tptpcol_10_40324) ) )). % Cyc Constant #202304: fof(ax1_951,axiom,( ! [X] : ( isa(X,c_tptpcol_7_72707) => tptpcol_7_72707(X) ) )). fof(ax1_952,axiom,( ! [X] : ( tptpcol_7_72707(X) => isa(X,c_tptpcol_7_72707) ) )). % Cyc Constant #202305: fof(ax1_953,axiom,( ! [X] : ( isa(X,c_tptpcol_8_72708) => tptpcol_8_72708(X) ) )). fof(ax1_954,axiom,( ! [X] : ( tptpcol_8_72708(X) => isa(X,c_tptpcol_8_72708) ) )). % Cyc Constant #223361: fof(ax1_955,axiom,( ! [X] : ( isa(X,c_tptpcol_11_93764) => tptpcol_11_93764(X) ) )). fof(ax1_956,axiom,( ! [X] : ( tptpcol_11_93764(X) => isa(X,c_tptpcol_11_93764) ) )). % Cyc Constant #223362: fof(ax1_957,axiom,( ! [X] : ( isa(X,c_tptpcol_12_93765) => tptpcol_12_93765(X) ) )). fof(ax1_958,axiom,( ! [X] : ( tptpcol_12_93765(X) => isa(X,c_tptpcol_12_93765) ) )). % Cyc Constant #244286: fof(ax1_959,axiom,( ! [X] : ( isa(X,c_tptpcol_4_114689) => tptpcol_4_114689(X) ) )). fof(ax1_960,axiom,( ! [X] : ( tptpcol_4_114689(X) => isa(X,c_tptpcol_4_114689) ) )). % Cyc Constant #244287: fof(ax1_961,axiom,( ! [X] : ( isa(X,c_tptpcol_5_114690) => tptpcol_5_114690(X) ) )). fof(ax1_962,axiom,( ! [X] : ( tptpcol_5_114690(X) => isa(X,c_tptpcol_5_114690) ) )). % Cyc Constant #227902: fof(ax1_963,axiom,( ! [X] : ( isa(X,c_tptpcol_3_98305) => tptpcol_3_98305(X) ) )). fof(ax1_964,axiom,( ! [X] : ( tptpcol_3_98305(X) => isa(X,c_tptpcol_3_98305) ) )). % Cyc Constant #236094: fof(ax1_965,axiom,( ! [X] : ( isa(X,c_tptpcol_4_106497) => tptpcol_4_106497(X) ) )). fof(ax1_966,axiom,( ! [X] : ( tptpcol_4_106497(X) => isa(X,c_tptpcol_4_106497) ) )). % Cyc Constant #109289: fof(ax1_967,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natfunction(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),c_relationexistsallfn) )). fof(ax1_968,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_1,ARG1) )). fof(ax1_969,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_2,ARG2) )). fof(ax1_970,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_3,ARG3) )). fof(ax1_971,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_4,ARG4) )). fof(ax1_972,axiom,( ! [ARG1,ARG2,ARG3,ARG4] : thing(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4)) )). % Cyc Constant #97397: fof(ax1_973,axiom,( ! [ARG1,INS] : ( resultisaarg(ARG1,INS) => positiveinteger(INS) ) )). fof(ax1_974,axiom,( ! [INS,ARG2] : ( resultisaarg(INS,ARG2) => function_denotational(INS) ) )). % Cyc Constant #261058: fof(ax1_975,axiom,( ! [ARG1,INS] : ( tptptypes_7_389(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_976,axiom,( ! [INS,ARG2] : ( tptptypes_7_389(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261059: fof(ax1_977,axiom,( ! [ARG1,INS] : ( tptptypes_8_390(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_978,axiom,( ! [INS,ARG2] : ( tptptypes_8_390(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261361: fof(ax1_979,axiom,( ! [ARG1,INS] : ( tptptypes_8_692(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_980,axiom,( ! [INS,ARG2] : ( tptptypes_8_692(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #261362: fof(ax1_981,axiom,( ! [ARG1,INS] : ( tptptypes_9_693(ARG1,INS) => firstordercollection(INS) ) )). fof(ax1_982,axiom,( ! [INS,ARG2] : ( tptptypes_9_693(INS,ARG2) => firstordercollection(INS) ) )). % Cyc Constant #169985: fof(ax1_983,axiom,( ! [X] : ( isa(X,c_tptpcol_11_40388) => tptpcol_11_40388(X) ) )). fof(ax1_984,axiom,( ! [X] : ( tptpcol_11_40388(X) => isa(X,c_tptpcol_11_40388) ) )). % Cyc Constant #24719: fof(ax1_985,axiom,( ! [X] : ( isa(X,c_marriagelicensedocument) => marriagelicensedocument(X) ) )). fof(ax1_986,axiom,( ! [X] : ( marriagelicensedocument(X) => isa(X,c_marriagelicensedocument) ) )). % Cyc Constant #195133: fof(ax1_987,axiom,( ! [X] : ( isa(X,c_tptpcol_1_65536) => tptpcol_1_65536(X) ) )). fof(ax1_988,axiom,( ! [X] : ( tptpcol_1_65536(X) => isa(X,c_tptpcol_1_65536) ) )). % Cyc Constant #227901: fof(ax1_989,axiom,( ! [X] : ( isa(X,c_tptpcol_2_98304) => tptpcol_2_98304(X) ) )). fof(ax1_990,axiom,( ! [X] : ( tptpcol_2_98304(X) => isa(X,c_tptpcol_2_98304) ) )). % Cyc Constant #221763: fof(ax1_991,axiom,( ! [X] : ( isa(X,c_tptpcol_10_92166) => tptpcol_10_92166(X) ) )). fof(ax1_992,axiom,( ! [X] : ( tptpcol_10_92166(X) => isa(X,c_tptpcol_10_92166) ) )). % Cyc Constant #221827: fof(ax1_993,axiom,( ! [X] : ( isa(X,c_tptpcol_11_92230) => tptpcol_11_92230(X) ) )). fof(ax1_994,axiom,( ! [X] : ( tptpcol_11_92230(X) => isa(X,c_tptpcol_11_92230) ) )). % Cyc Constant #52987: fof(ax1_995,axiom,( ! [X] : ( isa(X,c_orderingpredicate) => orderingpredicate(X) ) )). fof(ax1_996,axiom,( ! [X] : ( orderingpredicate(X) => isa(X,c_orderingpredicate) ) )). % Cyc Constant #148036: fof(ax1_997,axiom,( ! [X] : ( isa(X,c_tptpcol_9_18439) => tptpcol_9_18439(X) ) )). fof(ax1_998,axiom,( ! [X] : ( tptpcol_9_18439(X) => isa(X,c_tptpcol_9_18439) ) )). % Cyc Constant #148164: fof(ax1_999,axiom,( ! [X] : ( isa(X,c_tptpcol_10_18567) => tptpcol_10_18567(X) ) )). fof(ax1_1000,axiom,( ! [X] : ( tptpcol_10_18567(X) => isa(X,c_tptpcol_10_18567) ) )). % Cyc Constant #195134: fof(ax1_1001,axiom,( ! [X] : ( isa(X,c_tptpcol_2_65537) => tptpcol_2_65537(X) ) )). fof(ax1_1002,axiom,( ! [X] : ( tptpcol_2_65537(X) => isa(X,c_tptpcol_2_65537) ) )). % Cyc Constant #211518: fof(ax1_1003,axiom,( ! [X] : ( isa(X,c_tptpcol_3_81921) => tptpcol_3_81921(X) ) )). fof(ax1_1004,axiom,( ! [X] : ( tptpcol_3_81921(X) => isa(X,c_tptpcol_3_81921) ) )). % Cyc Constant #102162: fof(ax1_1005,axiom,( ! [X] : ( isa(X,c_artsupplies) => artsupplies(X) ) )). fof(ax1_1006,axiom,( ! [X] : ( artsupplies(X) => isa(X,c_artsupplies) ) )). % Cyc Constant #62476: fof(ax1_1007,axiom,( ! [X] : ( isa(X,c_enduringthing_localized) => enduringthing_localized(X) ) )). fof(ax1_1008,axiom,( ! [X] : ( enduringthing_localized(X) => isa(X,c_enduringthing_localized) ) )). % Cyc Constant #14857: fof(ax1_1009,axiom,( ! [X] : ( isa(X,c_location_underspecified) => location_underspecified(X) ) )). fof(ax1_1010,axiom,( ! [X] : ( location_underspecified(X) => isa(X,c_location_underspecified) ) )). % Cyc Constant #24658: fof(ax1_1011,axiom,( ! [X] : ( isa(X,c_trajector_underspecified) => trajector_underspecified(X) ) )). fof(ax1_1012,axiom,( ! [X] : ( trajector_underspecified(X) => isa(X,c_trajector_underspecified) ) )). % Cyc Constant #113597: fof(ax1_1013,axiom,( ! [X] : ( isa(X,c_individual) => individual(X) ) )). fof(ax1_1014,axiom,( ! [X] : ( individual(X) => isa(X,c_individual) ) )). % Cyc Constant #111039: fof(ax1_1015,axiom,( ! [X] : ( isa(X,c_partiallyintangibleindividual) => partiallyintangibleindividual(X) ) )). fof(ax1_1016,axiom,( ! [X] : ( partiallyintangibleindividual(X) => isa(X,c_partiallyintangibleindividual) ) )). % Cyc Constant #151619: fof(ax1_1017,axiom,( ! [X] : ( isa(X,c_tptpcol_10_22022) => tptpcol_10_22022(X) ) )). fof(ax1_1018,axiom,( ! [X] : ( tptpcol_10_22022(X) => isa(X,c_tptpcol_10_22022) ) )). % Cyc Constant #151620: fof(ax1_1019,axiom,( ! [X] : ( isa(X,c_tptpcol_11_22023) => tptpcol_11_22023(X) ) )). fof(ax1_1020,axiom,( ! [X] : ( tptpcol_11_22023(X) => isa(X,c_tptpcol_11_22023) ) )). % Cyc Constant #150080: fof(ax1_1021,axiom,( ! [X] : ( isa(X,c_tptpcol_5_20483) => tptpcol_5_20483(X) ) )). fof(ax1_1022,axiom,( ! [X] : ( tptpcol_5_20483(X) => isa(X,c_tptpcol_5_20483) ) )). % Cyc Constant #202388: fof(ax1_1023,axiom,( ! [X] : ( isa(X,c_tptpcol_13_72791) => tptpcol_13_72791(X) ) )). fof(ax1_1024,axiom,( ! [X] : ( tptpcol_13_72791(X) => isa(X,c_tptpcol_13_72791) ) )). % Cyc Constant #202389: fof(ax1_1025,axiom,( ! [X] : ( isa(X,c_tptpcol_14_72792) => tptpcol_14_72792(X) ) )). fof(ax1_1026,axiom,( ! [X] : ( tptpcol_14_72792(X) => isa(X,c_tptpcol_14_72792) ) )). % Cyc Constant #66844: fof(ax1_1027,axiom,( ! [X] : ( isa(X,c_ridgeline_topographical) => ridgeline_topographical(X) ) )). fof(ax1_1028,axiom,( ! [X] : ( ridgeline_topographical(X) => isa(X,c_ridgeline_topographical) ) )). % Cyc Constant #145984: fof(ax1_1029,axiom,( ! [X] : ( isa(X,c_tptpcol_4_16387) => tptpcol_4_16387(X) ) )). fof(ax1_1030,axiom,( ! [X] : ( tptpcol_4_16387(X) => isa(X,c_tptpcol_4_16387) ) )). % Cyc Constant #145985: fof(ax1_1031,axiom,( ! [X] : ( isa(X,c_tptpcol_5_16388) => tptpcol_5_16388(X) ) )). fof(ax1_1032,axiom,( ! [X] : ( tptpcol_5_16388(X) => isa(X,c_tptpcol_5_16388) ) )). % Cyc Constant #151617: fof(ax1_1033,axiom,( ! [X] : ( isa(X,c_tptpcol_8_22020) => tptpcol_8_22020(X) ) )). fof(ax1_1034,axiom,( ! [X] : ( tptpcol_8_22020(X) => isa(X,c_tptpcol_8_22020) ) )). % Cyc Constant #151618: fof(ax1_1035,axiom,( ! [X] : ( isa(X,c_tptpcol_9_22021) => tptpcol_9_22021(X) ) )). fof(ax1_1036,axiom,( ! [X] : ( tptpcol_9_22021(X) => isa(X,c_tptpcol_9_22021) ) )). % Cyc Constant #127156: fof(ax1_1037,axiom,( ! [X] : ( isa(X,c_transitivebinarypredicate) => transitivebinarypredicate(X) ) )). fof(ax1_1038,axiom,( ! [X] : ( transitivebinarypredicate(X) => isa(X,c_transitivebinarypredicate) ) )). % Cyc Constant #119918: fof(ax1_1039,axiom,( ! [ARG1,INS] : ( geographicalsubregions(ARG1,INS) => geographicalregion(INS) ) )). fof(ax1_1040,axiom,( ! [INS,ARG2] : ( geographicalsubregions(INS,ARG2) => geographicalregion(INS) ) )). fof(ax1_1041,axiom,( ! [X,Y,Z] : ( ( geographicalsubregions(X,Y) & geographicalsubregions(Y,Z) ) => geographicalsubregions(X,Z) ) )). fof(ax1_1042,axiom,( ! [X] : ( geographicalregion(X) => geographicalsubregions(X,X) ) )). % Cyc Constant #170017: fof(ax1_1043,axiom,( ! [X] : ( isa(X,c_tptpcol_12_40420) => tptpcol_12_40420(X) ) )). fof(ax1_1044,axiom,( ! [X] : ( tptpcol_12_40420(X) => isa(X,c_tptpcol_12_40420) ) )). % Cyc Constant #170018: fof(ax1_1045,axiom,( ! [X] : ( isa(X,c_tptpcol_13_40421) => tptpcol_13_40421(X) ) )). fof(ax1_1046,axiom,( ! [X] : ( tptpcol_13_40421(X) => isa(X,c_tptpcol_13_40421) ) )). % Cyc Constant #221759: fof(ax1_1047,axiom,( ! [X] : ( isa(X,c_tptpcol_6_92162) => tptpcol_6_92162(X) ) )). fof(ax1_1048,axiom,( ! [X] : ( tptpcol_6_92162(X) => isa(X,c_tptpcol_6_92162) ) )). % Cyc Constant #222783: fof(ax1_1049,axiom,( ! [X] : ( isa(X,c_tptpcol_7_93186) => tptpcol_7_93186(X) ) )). fof(ax1_1050,axiom,( ! [X] : ( tptpcol_7_93186(X) => isa(X,c_tptpcol_7_93186) ) )). % Cyc Constant #10889: fof(ax1_1051,axiom,( ! [ARG1,INS] : ( most(ARG1,INS) => setorcollection(INS) ) )). fof(ax1_1052,axiom,( ! [ARG1,INS] : ( most(ARG1,INS) => setorcollection(INS) ) )). fof(ax1_1053,axiom,( ! [INS,ARG2] : ( most(INS,ARG2) => setorcollection(INS) ) )). fof(ax1_1054,axiom,( ! [INS,ARG2] : ( most(INS,ARG2) => setorcollection(INS) ) )). fof(ax1_1055,axiom,( ! [X] : ( setorcollection(X) => most(X,X) ) )). fof(ax1_1056,axiom,( ! [X] : ( setorcollection(X) => most(X,X) ) )). fof(ax1_1057,axiom,( ! [ARG1,OLD,NEW] : ( ( most(ARG1,OLD) & subsetof(OLD,NEW) ) => most(ARG1,NEW) ) )). fof(ax1_1058,axiom,( ! [ARG1,OLD,NEW] : ( ( most(ARG1,OLD) & subsetof(OLD,NEW) ) => most(ARG1,NEW) ) )). % Cyc Constant #115179: fof(ax1_1059,axiom,( ! [ARG1,INS] : ( subsetof(ARG1,INS) => setorcollection(INS) ) )). fof(ax1_1060,axiom,( ! [INS,ARG2] : ( subsetof(INS,ARG2) => setorcollection(INS) ) )). fof(ax1_1061,axiom,( ! [X,Y,Z] : ( ( subsetof(X,Y) & subsetof(Y,Z) ) => subsetof(X,Z) ) )). fof(ax1_1062,axiom,( ! [X] : ( setorcollection(X) => subsetof(X,X) ) )). fof(ax1_1063,axiom,( ! [OLD,ARG2,NEW] : ( ( subsetof(OLD,ARG2) & subsetof(NEW,OLD) ) => subsetof(NEW,ARG2) ) )). fof(ax1_1064,axiom,( ! [ARG1,OLD,NEW] : ( ( subsetof(ARG1,OLD) & subsetof(OLD,NEW) ) => subsetof(ARG1,NEW) ) )). fof(ax1_1065,axiom,( ! [ARG1,OLD,NEW] : ( ( subsetof(ARG1,OLD) & subsetof(OLD,NEW) ) => subsetof(ARG1,NEW) ) )). % Cyc Constant #40273: fof(ax1_1066,axiom,( ! [ARG1,INS] : ( genlpreds(ARG1,INS) => predicate(INS) ) )). fof(ax1_1067,axiom,( ! [ARG1,INS] : ( genlpreds(ARG1,INS) => predicate(INS) ) )). fof(ax1_1068,axiom,( ! [INS,ARG2] : ( genlpreds(INS,ARG2) => predicate(INS) ) )). fof(ax1_1069,axiom,( ! [INS,ARG2] : ( genlpreds(INS,ARG2) => predicate(INS) ) )). fof(ax1_1070,axiom,( ! [X,Y,Z] : ( ( genlpreds(X,Y) & genlpreds(Y,Z) ) => genlpreds(X,Z) ) )). fof(ax1_1071,axiom,( ! [X] : ( predicate(X) => genlpreds(X,X) ) )). fof(ax1_1072,axiom,( ! [X] : ( predicate(X) => genlpreds(X,X) ) )). % Cyc Constant #45259: fof(ax1_1073,axiom,( ! [ARG1,INS] : ( genlinverse(ARG1,INS) => binarypredicate(INS) ) )). fof(ax1_1074,axiom,( ! [INS,ARG2] : ( genlinverse(INS,ARG2) => binarypredicate(INS) ) )). fof(ax1_1075,axiom,( ! [OLD,ARG2,NEW] : ( ( genlinverse(OLD,ARG2) & genlpreds(NEW,OLD) ) => genlinverse(NEW,ARG2) ) )). fof(ax1_1076,axiom,( ! [ARG1,OLD,NEW] : ( ( genlinverse(ARG1,OLD) & genlpreds(OLD,NEW) ) => genlinverse(ARG1,NEW) ) )). % Cyc Constant #27757: fof(ax1_1077,axiom,( mtvisible(c_basekb) )). % Cyc Constant #29331: fof(ax1_1078,axiom,( ! [X] : ( isa(X,c_microtheory) => microtheory(X) ) )). fof(ax1_1079,axiom,( ! [X] : ( microtheory(X) => isa(X,c_microtheory) ) )). % Cyc Constant #129091: fof(ax1_1080,axiom,( ! [ARG1] : natfunction(f_urlfn(ARG1),c_urlfn) )). fof(ax1_1081,axiom,( ! [ARG1] : natargument(f_urlfn(ARG1),n_1,ARG1) )). fof(ax1_1082,axiom,( ! [ARG1] : uniformresourcelocator(f_urlfn(ARG1)) )). % Cyc Constant #78971: fof(ax1_1083,axiom,( ! [ARG1] : natfunction(f_urlreferentfn(ARG1),c_urlreferentfn) )). fof(ax1_1084,axiom,( ! [ARG1] : natargument(f_urlreferentfn(ARG1),n_1,ARG1) )). fof(ax1_1085,axiom,( ! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) )). % Cyc Constant #71728: fof(ax1_1086,axiom,( ! [ARG1,ARG2] : natfunction(f_contentmtofcdafromeventfn(ARG1,ARG2),c_contentmtofcdafromeventfn) )). fof(ax1_1087,axiom,( ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_1,ARG1) )). fof(ax1_1088,axiom,( ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_2,ARG2) )). fof(ax1_1089,axiom,( ! [ARG1,ARG2] : microtheory(f_contentmtofcdafromeventfn(ARG1,ARG2)) )). % Cyc Constant #72115: fof(ax1_1090,axiom,( ! [ARG1,INS] : ( isa(ARG1,INS) => collection(INS) ) )). fof(ax1_1091,axiom,( ! [ARG1,INS] : ( isa(ARG1,INS) => collection(INS) ) )). fof(ax1_1092,axiom,( ! [INS,ARG2] : ( isa(INS,ARG2) => thing(INS) ) )). fof(ax1_1093,axiom,( ! [INS,ARG2] : ( isa(INS,ARG2) => thing(INS) ) )). fof(ax1_1094,axiom,( ! [ARG1,OLD,NEW] : ( ( isa(ARG1,OLD) & genls(OLD,NEW) ) => isa(ARG1,NEW) ) )). % Cyc Constant #101883: fof(ax1_1095,axiom,( ! [X] : ( isa(X,c_inanimateobject) => inanimateobject(X) ) )). fof(ax1_1096,axiom,( ! [X] : ( inanimateobject(X) => isa(X,c_inanimateobject) ) )). % Cyc Constant #202306: fof(ax1_1097,axiom,( ! [X] : ( isa(X,c_tptpcol_9_72709) => tptpcol_9_72709(X) ) )). fof(ax1_1098,axiom,( ! [X] : ( tptpcol_9_72709(X) => isa(X,c_tptpcol_9_72709) ) )). % Cyc Constant #202307: fof(ax1_1099,axiom,( ! [X] : ( isa(X,c_tptpcol_10_72710) => tptpcol_10_72710(X) ) )). fof(ax1_1100,axiom,( ! [X] : ( tptpcol_10_72710(X) => isa(X,c_tptpcol_10_72710) ) )). % Cyc Constant #170026: fof(ax1_1101,axiom,( ! [X] : ( isa(X,c_tptpcol_14_40429) => tptpcol_14_40429(X) ) )). fof(ax1_1102,axiom,( ! [X] : ( tptpcol_14_40429(X) => isa(X,c_tptpcol_14_40429) ) )). % Cyc Constant #170027: fof(ax1_1103,axiom,( ! [X] : ( isa(X,c_tptpcol_15_40430) => tptpcol_15_40430(X) ) )). fof(ax1_1104,axiom,( ! [X] : ( tptpcol_15_40430(X) => isa(X,c_tptpcol_15_40430) ) )). % Cyc Constant #0: fof(ax1_1105,axiom,( ! [ARG1,INS] : ( genls(ARG1,INS) => collection(INS) ) )). fof(ax1_1106,axiom,( ! [ARG1,INS] : ( genls(ARG1,INS) => collection(INS) ) )). fof(ax1_1107,axiom,( ! [INS,ARG2] : ( genls(INS,ARG2) => collection(INS) ) )). fof(ax1_1108,axiom,( ! [INS,ARG2] : ( genls(INS,ARG2) => collection(INS) ) )). fof(ax1_1109,axiom,( ! [X,Y,Z] : ( ( genls(X,Y) & genls(Y,Z) ) => genls(X,Z) ) )). fof(ax1_1110,axiom,( ! [X] : ( collection(X) => genls(X,X) ) )). fof(ax1_1111,axiom,( ! [X] : ( collection(X) => genls(X,X) ) )). fof(ax1_1112,axiom,( ! [OLD,ARG2,NEW] : ( ( genls(OLD,ARG2) & genls(NEW,OLD) ) => genls(NEW,ARG2) ) )). fof(ax1_1113,axiom,( ! [ARG1,OLD,NEW] : ( ( genls(ARG1,OLD) & genls(OLD,NEW) ) => genls(ARG1,NEW) ) )). % Cyc Constant #36435: fof(ax1_1114,axiom,( ! [X] : ( isa(X,c_partiallytangible) => partiallytangible(X) ) )). fof(ax1_1115,axiom,( ! [X] : ( partiallytangible(X) => isa(X,c_partiallytangible) ) )). % Cyc Constant #108599: fof(ax1_1116,axiom,( ! [X] : ( isa(X,c_intangible) => intangible(X) ) )). fof(ax1_1117,axiom,( ! [X] : ( intangible(X) => isa(X,c_intangible) ) )). % Cyc Constant #78648: fof(ax1_1118,axiom,( ! [ARG1,INS] : ( disjointwith(ARG1,INS) => collection(INS) ) )). fof(ax1_1119,axiom,( ! [INS,ARG2] : ( disjointwith(INS,ARG2) => collection(INS) ) )). fof(ax1_1120,axiom,( ! [X,Y] : ( disjointwith(X,Y) => disjointwith(Y,X) ) )). fof(ax1_1121,axiom,( ! [ARG1,OLD,NEW] : ( ( disjointwith(ARG1,OLD) & genls(NEW,OLD) ) => disjointwith(ARG1,NEW) ) )). fof(ax1_1122,axiom,( ! [OLD,ARG2,NEW] : ( ( disjointwith(OLD,ARG2) & genls(NEW,OLD) ) => disjointwith(NEW,ARG2) ) )). % Cyc Constant #19550: fof(ax1_1123,axiom,( ! [SPECMT,GENLMT] : ( ( mtvisible(SPECMT) & genlmt(SPECMT,GENLMT) ) => mtvisible(GENLMT) ) )). fof(ax1_1124,axiom,( ! [ARG1,INS] : ( genlmt(ARG1,INS) => microtheory(INS) ) )). fof(ax1_1125,axiom,( ! [ARG1,INS] : ( genlmt(ARG1,INS) => microtheory(INS) ) )). fof(ax1_1126,axiom,( ! [INS,ARG2] : ( genlmt(INS,ARG2) => microtheory(INS) ) )). fof(ax1_1127,axiom,( ! [INS,ARG2] : ( genlmt(INS,ARG2) => microtheory(INS) ) )). fof(ax1_1128,axiom,( ! [X,Y,Z] : ( ( genlmt(X,Y) & genlmt(Y,Z) ) => genlmt(X,Z) ) )). fof(ax1_1129,axiom,( ! [X] : ( microtheory(X) => genlmt(X,X) ) )). fof(ax1_1130,axiom,( ! [X] : ( microtheory(X) => genlmt(X,X) ) )). % Cyc Constant #95028: fof(ax1_1131,axiom,( mtvisible(c_universalvocabularymt) )). %------------------------------------------------------------------------------