TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1371-1373
No TPTP formula. May not be expressible in strict first order.	Merge.kif 132-134
No TPTP formula. May not be expressible in strict first order.	Merge.kif 130-130	子类别的 1 数量是集或类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 131-131	子类别的 2 数量是集或类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 128-128	子类别是二元谓语的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 129-129	子类别是偏序关系的 instance

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 319-319
No TPTP formula. May not be expressible in strict first order.	english_format.kif 327-327
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5114-5114	子集是子类别的 subrelation
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55628-55628
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 320-320
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55627-55627
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55626-55626

antecedent

No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1140-1152	如果 Oversized 是客体的 attribute 和那个客体是集或类的 immediateInstance 和那个集或类是 HotelUnit 的 subclass，然后有存在另一个客体，物理量， and 和另一个物理量这样那个另外客体是那个集或类的 immediateInstance 和那个另外客体的 measure 是那个物理量和那个客体的 measure 是那个另外物理量和那个物理量是面积测量的 instance 和那个另外物理量是面积测量的 instance 和那个另外物理量是 greaterThan 那个物理量
No TPTP formula. May not be expressible in strict first order.	Media.kif 1853-1857	如果施事体是有点音乐作品的 authors 和有点音乐作品是音乐作品的 subclass，然后那个施事体 composed 那个有点音乐作品
No TPTP formula. May not be expressible in strict first order.	WMD.kif 784-788	如果有点过程是有点生化剂的 biochemical 病毒传递和另一个有点过程是有点过程的 subclass，然后另一个有点过程是有点生化剂的 biochemical 病毒传递
No TPTP formula. May not be expressible in strict first order.	WMD.kif 931-935	如果有点生物是有点生物制剂的病毒传递者和另一个有点生物是有点生物的 subclass，然后另一个有点生物是有点生物制剂的病毒传递者
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 48-56	如果客体能够担当格角色的角色做有点过程和有点过程是射击的 subclass，然后有存在另一个客体这样那个另外客体是武器的 instance 和那个另外客体是那个客体的 part 和那个另外客体能够担当那个格角色的角色做那个有点过程
No TPTP formula. May not be expressible in strict first order.	Media.kif 2859-2865	如果符号串在 ISO-4217-A denotes UnitOfCurrency 和另一个符号串在 ISO-3166-1-alpha-2 denotes 地缘政治区域和那个地缘政治区域是地缘政治区域的 subclass 和那个另外符号串 equal 那个符号串的 sub-string 从 0 对于 2 ，然后那个 UnitOfCurrency 是那个地缘政治区域的 currency 类别
No TPTP formula. May not be expressible in strict first order.	Government.kif 606-612	如果正整数 day 是假日的 commemorates 日期和实体是那个假日的 instance 和那个假日是固定假期的 subclass 和整数是 lessThanOrEqualTo 另一个实体-YEAR，然后那个实体是那个正整数 day 的 instance
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 480-496	如果有认知的主事是另一个有认知的主事的 customer 和那个有认知的主事有有点物理和有点物理是客体的 subclass 和实体是那个有点物理的 instance，然后那个有认知的主事允许那个另外有认知的主事执行有存在另一个实体这样那个另外实体是过程的 instance 和那个实体是那个另外实体的 resource 或那个实体是导致那个另外实体的 instrument 或那个实体是那个另外实体的 patient 和那个另外有认知的主事是那个另外实体的 agent 或那个另外有认知的主事经历了那个另外实体的任务
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 498-514	如果有认知的主事是另一个有认知的主事的 customer 和那个有认知的主事有有点物理和有点物理是过程的 subclass，然后有存在实体和另一个实体这样那个另外实体是那个有认知的主事的财产的 element 和那个有认知的主事是那个实体的 agent 和那个另外有认知的主事是那个实体的 patient 和那个实体是那个有点物理的 instance 或第三实体是第四实体的 instance 和那个实体%n是那个第三实体的subProcess 和那个实体是 located 在那个另外实体的声明 has 可能性的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11174-11185	如果有点客体的 maximum 预期价值是实数测量单位和集或类是 NonCompositeUnitOfMeasure 的 subclass 和那个测量单位是那个集或类的 instance，然后有存在实体，那个实数UANTITY， and 和第三实体这样那个实体是有点客体的 instance 和那个实体的 measure 是那个实数UANTITY 那个第三实体和那个第三实体是那个集或类的 instance 和那个实数UANTITY 那个第三实体是 greaterThan 那个实数那个测量单位的声明 has 较不可能的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11145-11156	如果有点客体的 minimum 预期价值是实数测量单位和集或类是 NonCompositeUnitOfMeasure 的 subclass 和那个测量单位是那个集或类的 instance，然后有存在实体，那个实数UANTITY， and 和第三实体这样那个实体是有点客体的 instance 和那个实体的 measure 是那个实数UANTITY 那个第三实体和那个第三实体是那个集或类的 instance 和那个实数UANTITY 那个第三实体是 lessThan 那个实数那个测量单位的声明 has 较不可能的语气
No TPTP formula. May not be expressible in strict first order.	WMD.kif 912-916	如果疾病或综合症是对于有点过程的 disease 治愈有点生物活性物质和另一个有点过程是有点过程的 subclass，然后那个疾病或综合症是对于另一个有点过程的 disease 治愈有点生物活性物质
No TPTP formula. May not be expressible in strict first order.	WMD.kif 918-922	如果疾病或综合症是对于有点过程的 disease 治愈有点生物活性物质和另一个有点生物活性物质是有点生物活性物质的 subclass，然后那个疾病或综合症是对于有点过程的 disease 治愈另一个有点生物活性物质
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2116-2125	如果地缘政治区域是对于有点时距在其间物理量的 electricity 消耗和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域的 annual 电力消耗在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2160-2169	如果地缘政治区域是对于有点时距在周期物理量的 electricity 输出和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域的 annual 电力输出在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2206-2215	如果地缘政治区域是对于有点时距在周期物理量的 electricity 输出和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域 annual 的电力输入在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1984-1993	如果地缘政治区域是对于有点时距在周期物理量的 electricity 生产和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域的 annual 电力生产在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Media.kif 195-200	如果有点获得 equal receiving 一个有点客体和另一个有点获得 equal receiving 一个另一个有点客体和有点客体是另一个有点客体的 subclass，然后有点获得是另一个有点获得的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16094-16098	如果 equal DepartmentOfPreventingFn 机构 and 有点过程和有点过程是过程的 subclass，然后那个 inhibits 那个有点过程
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16100-16109	如果 equal DepartmentOfPreventingFn 机构 and 过程和那个过程是过程的 subclass，然后那个机构 doesn't desires 有存在实体这样那个实体是那个过程的 instance 和那个机构是事件那个实体的 involved
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2281-2290	如果地缘政治区域对于有点时距在周期货币测量 export 全部和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个货币测量是那个地缘政治区域的 annual 总共输出在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 334-349	如果集或类的使用是对于有点 HotelUnit 免费和那个集或类是客体的 subclass 和暂住是有点 HotelUnit 的 instance 和人类 stays 在那个暂住和那个暂住是施事体的财产的 element 和客体是那个集或类的 instance 和那个客体是 located 在那个暂住和过程是过程的 instance 和那个人类是那个过程的 agent 和那个客体是那个过程的 patient 或那个客体是导致那个过程的 instrument 或那个客体是那个过程的 resource，然后那个过程是对于那个施事体的 price 0 美国美元
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 351-365	如果集或类的使用是对于有点 HotelUnit 免费和那个集或类是过程的 subclass 和暂住是有点 HotelUnit 的 instance 和人类 stays 在那个暂住和那个暂住是施事体的财产的 element 和那个人类是过程的 patient 和那个过程是那个集或类的 instance 或另一个过程是那个集或类的 instance 和那个过程%n是那个另外过程的subProcess 和那个过程是 located 在那个暂住，然后那个过程是对于那个施事体的 price 0 美国美元
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 784-805	如果有点物理的使用对于有点 HotelFunctionRoom 是免费和实体是有点 HotelFunctionRoom 的 instance 和那个实体是施事体的财产的 element 和过程是租的 instance 和那个实体是那个过程的 patient 和那个施事体是那个过程的 agent 和那个过程在另一个实体结束和有点物理是客体的 subclass，然后有存在第三实体和第四实体这样那个第三实体是那个有点物理的 instance 和那个第四实体是过程的 instance 和那个第三实体是那个第四实体的 resource 或那个第三实体是导致那个第四实体的 instrument 或那个第三实体是那个第四实体的 patient 和那个另外实体是那个第四实体的 agent 或那个另外实体经历了那个第四实体的声明 has 可能性的语气
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 289-308	如果人类是在有认知的主事的 guest 和那个人类 stays 在暂住和那个暂住是那个有认知的主事的财产的 element 和那个暂住是那个暂住OOM 的 instance 和有点物理是 amenity 在那个暂住OOM 和有点物理是客体的 subclass，然后有存在另一个物理这样那个另外物理是那个有点物理的 instance 和那个另外物理是 located 在那个暂住和那个有认知的主事允许那个人类执行有存在实体这样那个人类是那个实体的 agent 和那个另外物理是导致那个实体的 instrument 或那个另外物理是那个实体的 patient 或那个另外物理是那个实体的 resource 的任务

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 794-796	集或类是类的 instance 若且唯若那个集或类是实体的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 220-226	如果关系的正整数数量是集或类的 instance 和那个关系的那个正整数数量是另一个集或类的 instance，然后那个集或类是那个另外集或类的 subclass 或那个另外集或类是那个集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2899-2904	如果关系的正整数数量是集或类的 subclass 和那个关系是谓语的 instance 和那个关系 @ROW，然后 (@ROW) 的第那个正整数几个元素是那个集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 243-249	如果关系的正整数数量是集或类的 subclass 和那个关系的那个正整数数量是另一个集或类的 subclass，然后那个集或类是那个另外集或类的 subclass 或那个另外集或类是那个集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Media.kif 195-200	如果有点获得 equal receiving 一个有点客体和另一个有点获得 equal receiving 一个另一个有点客体和有点客体是另一个有点客体的 subclass，然后有点获得是另一个有点获得的 subclass
No TPTP formula. May not be expressible in strict first order.	Dining.kif 215-219	如果 Catalog 是 AlcoholMenu 的 instance 和有点实体是在那个 Catalog ，然后有点实体是酒精饮料的 subclass
No TPTP formula. May not be expressible in strict first order.	Dining.kif 204-208	如果 Catalog 是 BeverageMenu 的 instance 和有点实体是在那个 Catalog ，然后有点实体是饮料的 subclass
No TPTP formula. May not be expressible in strict first order.	Dining.kif 178-182	如果 Catalog 是 Menu 的 instance 和有点实体是在那个 Catalog ，然后有点实体是 food for 人类的 subclass
No TPTP formula. May not be expressible in strict first order.	Dining.kif 225-229	如果 Catalog 是 WineMenu 的 instance 和有点实体是在那个 Catalog ，然后有点实体是 WineMenu 的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11929-11933	如果过程是出版的 instance 和集或类是那个过程的 patient，然后那个集或类是文本的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14488-14492	如果关系是经济关系的 instance 和那个关系的 1 数量是集或类的 instance，然后那个集或类是地缘政治区域的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3274-3278	如果函数是序列函数的 instance 和那个函数的 range 是集或类的实例，然后那个集或类是整数的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 28228-28257	如果过程是 BreakingRecord 的 instance 和施事体是那个过程的 agent，然后有存在集或类，另一个集或类,，，另一个过程,，，时点,，，格角色,，，第三集或类， and 和实体这样那个集或类是集合的 instance 和那个施事体是那个集或类的 instance 和那个另外集或类是过程的 subclass 和那个第三集或类是地区的 subclass 和那个时点是时点的 instance 和那个实体是数量的 instance 和那个过程提到那个实体和那个实体提到那个另外集或类和那个施事体对于那个另外过程在事件那个格角色 plays 角色和那个另外过程是 located 在 2 和不存在另一个实体和第三实体这样那个另外实体是那个集或类的 instance 和那个另外实体不 equal 那个施事体和那个第三实体是那个另外集或类的 instance 和那个另外实体对于那个第三实体在事件那个格角色 plays 角色和那个第三实体是 located 在 2 在那个时点和那个过程出现的 time 的结束间的时段 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 323-329	如果函数的 range 是集或类的实例和那个函数的 range 是另一个集或类的实例，然后那个集或类是那个另外集或类的 subclass 或那个另外集或类是那个集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 338-342	如果函数的所得值是有点集或类的 subclass 和那个函数(@ROW) equal 另一个集或类，然后那个另外集或类是有点集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 350-356	如果函数的所得值是有点集或类的 subclass 和那个函数的所得值是另一个有点集或类的 subclass，然后有点集或类是另一个有点集或类的 subclass 或那个另外有点集或类是那个有点集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18748-18755	如果医生是客体的 attribute，然后有存在有点过程和另一个有点过程这样有点过程是诊断过程的 subclass 和另一个有点过程是治疗过程的 subclass 和那个客体能够担当主事的角色做那个有点过程和那个客体能够担当主事的角色做那个另外有点过程
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 74-78	如果集或类和另一个集或类的 intersection 是第三集或类，然后那个第三集或类是那个集或类的 subclass 和那个第三集或类是那个另外集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Languages.kif 14683-14687	如果符号串在 ISO-639-1 denotes 集或类，然后那个集或类是人类语言的 instance 或那个集或类是人类语言的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1206-1208	如果疾病或综合症是对于有点过程的 disease 治愈口服抗生素，然后有点过程是消化的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1233-1235	如果疾病或综合症是对于有点过程的 disease 治愈外用抗生素，然后有点过程是遮盖的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2844-2849	如果类分拆成不相交的 @ROW，然后对所有集或类如果那个集或类是 (@ROW) 的 member，然后那个集或类是那个类的 subclass
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6352-6354	如果有点地理区域 equal 另一个有点地理区域所有的 instances 在第三地理区域，然后有点地理区域是另一个有点地理区域的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1689-1698	如果类 equal 集或类跟属性的 attr，然后对所有实体如果那个实体是那个类的 instance，然后那个实体是那个集或类的 instance 和那个类是那个集或类的 subclass 和那个实体有那个属性的 attribute
No TPTP formula. May not be expressible in strict first order.	Media.kif 3173-3175	如果符号串是在语言的 title 对于集或类的例子，然后那个集或类是群体的 subclass

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

No TPTP formula. May not be expressible in strict first order.

Cars.kif 5090-5093

有存在施事体这样那个施事体是 HandToolBox 的 subclass 和 manufacturer SortimoCorp and 那个施事体

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	WMD.kif 1300-1300	球孢子菌 posadasii 的 biological agent 是危及生命的特工的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1293-1293	球孢子菌丝虫的 biological agent 是危及生命的特工的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1479-1479	疟疾疟原虫的 biological agent 是生物制剂的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1288-1288	Serratia marcenscens 的 biological agent 是危及生命的特工的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1840-1840	蜱传脑炎病毒的 biological agent 是危及生命的特工的 subclass
No TPTP formula. May not be expressible in strict first order.	WMD.kif 400-400	鼠疫耶尔森氏菌的 biological agent 是危及生命的特工的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3938-3938	一个 dead 苹果是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3964-3964	一个 dead 鳄梨是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3967-3967	一个 dead 香蕉是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3935-3935	一个 dead 浆果是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3970-3970	一个 dead 面包果是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3843-3843	一个 dead 卷心菜是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3876-3876	一个 dead 胡萝卜是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3896-3896	一个 dead 木薯是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3846-3846	一个 dead 菜花是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3944-3944	一个 dead 柑橘类水果是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3973-3973	一个 dead 椰子是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3840-3840	一个 dead 黄瓜是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3976-3976	一个 dead 日期水果是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4019-4019	一个 dead 食用坚果是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3849-3849	一个 dead 茄子是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3927-3927	一个 dead 葡萄是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4033-4033	一个 dead 花生是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3837-3837	一个 dead 绿叶蔬菜是杂货生产的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3979-3979	一个 dead 芒果是杂货生产的 subclass

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: