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 133-135
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 27-29
No TPTP formula. May not be expressible in strict first order.	spanish_format.kif 28-30
No TPTP formula. May not be expressible in strict first order.	Merge.kif 131-131	子类别的 1 数量是类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 132-132	子类别的 2 数量是类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 129-129	子类别是二元谓语的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18551-18551	子类别是 ClosedWorldPredicate 的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 130-130	子类别是偏序关系的 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 324-324
No TPTP formula. May not be expressible in strict first order.	french_format.kif 182-182
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 271-271
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2002-2002
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 134-134
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 175-175
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 419-419
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 308-308
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 202-202
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 192-192
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 463-463
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 21366-21366	子领域是子类别的 subrelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5392-5392	子集是子类别的 subrelation
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55706-55706
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 55705-55705
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55704-55704

antecedent

No TPTP formula. May not be expressible in strict first order.	Medicine.kif 3984-4004	如果 ADHD 是施事体的 attribute 和 ADHD 不是另一个施事体的 attribute 和那个施事体不 equal 那个另外施事体和过程是类的 instance 和另一个过程是那个类的 instance 和那个类是有意图的心理过程的 subclass 和那个施事体是那个过程的 agent 和那个另外施事体是那个另外过程的 agent 和那个过程出现的 time 的 duration 是持续时间和那个另外过程出现的 time 的 duration 是另一个持续时间，然后那个另外持续时间是 greaterThan 那个持续时间的声明 has 容易的语气
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1186-1201	如果 Oversized 是客体的 attribute 和那个客体是类的 immediateInstance 和那个类是 HotelUnit 的 subclass，然后有存在物理，实数,，，另一个实数， and 和测量单位这样那个物理是那个类的 immediateInstance 和那个测量单位是 UnitOfArea 的 instance 和那个物理的 measure 是那个实数那个测量单位和那个客体的 measure 是那个另外实数那个测量单位和那个实数是面积测量的 instance 和那个另外实数是面积测量的 instance 和那个另外实数是 greaterThan 那个实数
No TPTP formula. May not be expressible in strict first order.	Biography.kif 730-740	如果作家是施事体的 attribute 和实体是有点有内用物体的 instance 和有点有内用物体是文本的 subclass 或那个有点有内用物体是 Document 的 subclass 和过程是写作的 instance 和那个施事体是那个过程的 agent 和那个实体是那个过程的 result，然后那个施事体是那个有点有内用物体的 authors
No TPTP formula. May not be expressible in strict first order.	WMD.kif 789-793	如果有点过程是有点生化剂的 biochemical 病毒传递和另一个有点过程是有点过程的 subclass，然后另一个有点过程是有点生化剂的 biochemical 病毒传递
No TPTP formula. May not be expressible in strict first order.	WMD.kif 976-980	如果有点生物是有点生物制剂的病毒传递者和另一个有点生物是有点生物的 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.	Government.kif 583-589	如果正整数 day 是有点假日的 commemorates 日期和实体是有点假日的 instance 和那个有点假日是固定假期的 subclass 和整数是 lessThanOrEqualTo 另一个实体-YEAR，然后那个实体是那个正整数 day 的 instance
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 504-520	如果施事体是有认知的主事的 customer 和那个施事体有有点物理和有点物理是客体的 subclass 和实体是那个有点物理的 instance，然后那个施事体允许那个有认知的主事执行有存在另一个实体这样那个另外实体是过程的 instance 和那个实体是那个另外实体的 resource 或那个实体是导致那个另外实体的 instrument 或那个实体是那个另外实体的 patient 和那个有认知的主事是那个另外实体的 agent 或那个有认知的主事经历了那个另外实体的任务
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 522-538	如果施事体是有认知的主事的 customer 和那个施事体有有点物理和有点物理是过程的 subclass，然后有存在实体，另一个实体， and 和第三实体这样那个另外实体是那个施事体的财产的 element 和那个施事体是那个实体的 agent 和那个有认知的主事是那个实体的 patient 和那个实体是那个有点物理的 instance 或那个第三实体是那个有点物理的 instance 和那个实体%n是那个第三实体的subProcess 和那个实体是 located 在那个另外实体的声明 has 可能性的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13574-13585	如果有点客体的 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 13543-13554	如果有点客体的 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 957-961	如果疾病或综合症是对于有点过程的 disease 治愈有点生物活性物质和另一个有点过程是有点过程的 subclass，然后那个疾病或综合症是对于另一个有点过程的 disease 治愈有点生物活性物质
No TPTP formula. May not be expressible in strict first order.	WMD.kif 963-967	如果疾病或综合症是对于有点过程的 disease 治愈有点生物活性物质和另一个有点生物活性物质是有点生物活性物质的 subclass，然后那个疾病或综合症是对于有点过程的 disease 治愈另一个有点生物活性物质
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2112-2121	如果地缘政治区域是对于有点时距在其间物理量的 electricity 消耗和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域的 annual 电力消耗在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2156-2165	如果地缘政治区域是对于有点时距在周期物理量的 electricity 输出和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域的 annual 电力输出在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2202-2211	如果地缘政治区域是对于有点时距在周期物理量的 electricity 输出和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域 annual 的电力输入在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1980-1989	如果地缘政治区域是对于有点时距在周期物理量的 electricity 生产和有点时距是年的 subclass 或那个有点时距是那个地缘政治区域的 fiscal 年的 subclass，然后有存在时间位置这样那个时间位置是那个有点时距的 instance 和那个物理量是那个地缘政治区域的 annual 电力生产在那个时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Food.kif 2876-2882	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是 AnimalFat 的 subclass 和另一个有点客体是脂肪组织的 subclass，然后 %每个那个另外有点客体是动物的 initially part
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4629-4634	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是咖啡豆的 subclass 和另一个有点客体是种子的 subclass，然后 %每个那个另外有点客体是 CoffeePlant 的 initially part
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4693-4699	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是可可豆的 subclass 和另一个有点客体是种子的 subclass，然后 %每个那个另外有点客体是可可樹的 initially part
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 18428-18433	如果机构 equal DepartmentOfPreventingFn 另一个机构 and 有点物理和有点物理是过程的 subclass 和那个机构是那个另外机构 Organization 的一部分，然后那个机构 inhibits 那个有点物理
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4945-4950	如果有点客体 equal OrganicObjectFn 有点有机物体和有点客体是 meat 的 subclass，然后有点有机物体是动物的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4166-4172	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是 Malt 的 subclass 和另一个有点客体是谷物的 subclass，然后 %每个那个另外有点客体是谷物草的 initially part
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4532-4543	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是 OilFromPlant 的 subclass 和另一个有点客体是种子的 subclass 或那个另外有点客体是水果的 subclass，然后有存在第三有点客体这样第三有点客体是开花植物的 subclass 和 %每个那个另外有点客体是那个第三有点客体的 initially part

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.	Mid-level-ontology.kif 31419-31426	如果 applicableRelation 客体 and 关系和那个客体是那个客体C 的 instance 和那个关系的 1 数量是另一个类的 instance，然后那个客体C equal 那个另外类或那个客体C 是那个另外类的 subclass
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1478-1491	如果 DutyFree 是客体的 attribute 和那个客体是商店的 instance，然后有存在地缘政治区域，实体,，，另一个有点客体， and 和过程这样那个地缘政治区域是地缘政治区域的 instance 和那个客体是 located 在那个地缘政治区域和另一个有点客体是客体的 subclass 和那个另外有点客体是那个地缘政治区域的 import 商品种类和那个实体是那个另外有点客体的 instance 和那个过程是出售的 instance 和那个实体是那个过程的 patient 和那个过程是 located 在那个客体
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 24293-24303	如果日是人类的 birthdate 和那个日是正整数 day 的 instance，然后有存在另一个有点日和整数这样那个人类的 birthday 是另一个有点日和那个另外有点日是日的 subclass 和那个整数是整数的 instance 和那个另外有点日 equal 那个正整数 day 和那个整数是 greaterThan 另一个整数
No TPTP formula. May not be expressible in strict first order.	Merge.kif 221-227	如果关系的正整数数量是类的 instance 和那个关系的那个正整数数量是另一个类的 instance，然后那个类是那个另外类的 subclass 或那个另外类是那个类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3006-3011	如果关系的正整数数量是类的 subclass 和那个关系是谓语的 instance 和那个关系 @ROW，然后 (@ROW) 的第那个正整数几个元素是那个类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 244-250	如果关系的正整数数量是类的 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.	Economy.kif 4945-4950	如果有点客体 equal OrganicObjectFn 有点有机物体和有点客体是 meat 的 subclass，然后有点有机物体是动物的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4532-4543	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是 OilFromPlant 的 subclass 和另一个有点客体是种子的 subclass 或那个另外有点客体是水果的 subclass，然后有存在第三有点客体这样第三有点客体是开花植物的 subclass 和 %每个那个另外有点客体是那个第三有点客体的 initially part
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5258-5265	如果有点客体 equal OrganicObjectFn 有点有机物体和有点客体是客体的 subclass，然后有点有机物体是生物的 subclass 或那个有点有机物体是解剖结构的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5032-5036	如果有点客体 equal OrganicObjectFn 有点有机物体和有点客体是毛皮的 subclass，然后有点有机物体是皮肤的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5235-5244	如果有点客体 equal OrganicObjectFn 另一个有点客体和有点客体是 WoodProduct 的 subclass 和另一个有点客体是 PlantStem 的 subclass，然后有存在第三有点客体这样第三有点客体是植物树的 subclass 和 %每个那个另外有点客体是那个第三有点客体的 initially part
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1780-1788	如果有点客体 equal 另一个有点客体跟属性的 attr 和第三客体是有点客体的 instance，然后那个第三客体是另一个有点客体的 instance 和那个有点客体是那个另外有点客体的 subclass 和那个属性是那个第三客体的 attribute
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3840-3845	如果客体是 AegilopsGrass 的 instance 和另一个客体是那个客体的 part 和那个另外客体是那个另外客体LASS 的 instance，然后那个另外客体LASS 是 DiploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3963-3968	如果客体是 CommonWheatGrass 的 instance 和那个客体ELL 是那个客体的 part 和那个客体ELL 是那个客体LASS 的 instance，然后那个客体LASS 是 HexaploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3993-3998	如果客体是 SpeltWheatGrass 的 instance 和那个客体ELL 是那个客体的 part 和那个客体ELL 是那个客体LASS 的 instance，然后那个客体LASS 是 HexaploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12060-12072	如果过程是决定的 instance 和有认知的主事是那个过程的 agent 和集合是集合的 instance 和那个集合是那个过程的 patient 和实体是那个集合的 element，然后那个有认知的主事 believes 有存在另一个实体这样那个实体是那个另外实体的 instance 和那个另外实体是有意图过程的 subclass 和那个有认知的主事能够担当主事的角色做那个另外实体
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3904-3909	如果客体是 DurumWheatGrass 的 instance 和另一个客体是那个客体的 part 和那个另外客体是那个另外客体LASS 的 instance，然后那个另外客体LASS 是 TetraploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3934-3939	如果客体是 EinkornWheatGrass 的 instance 和另一个客体是那个客体的 part 和那个客体是那个另外客体LASS 的 instance，然后那个另外客体LASS 是 DiploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3872-3877	如果客体是 EmmerWheatGrass 的 instance 和另一个客体是那个客体的 part 和那个另外客体是那个另外客体LASS 的 instance，然后那个另外客体LASS 是 TetraploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3948-3953	如果客体是 TriticumUrartu 的 instance 和另一个客体是那个客体的 part 和那个客体是那个另外客体LASS 的 instance，然后那个另外客体LASS 是 DiploidCell 的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5485-5493	如果过程是砍伐的 instance 和实体是那个过程的 result，然后有存在那个实体TEM 这样那个实体是一个 dead 那个实体TEM 的 instance 和那个实体TEM 是 PlantStem 的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18111-18119	如果过程是收获的 instance 和实体是那个过程的 result，然后有存在那个实体RG 这样那个实体是一个 dead 那个实体RG 的 instance 和那个实体RG 是有机物体的 subclass
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3432-3461	如果可穿戴物品是听力保护的 instance 和动物是人类的 instance 和那个动物 wears 那个可穿戴物品，然后那个可穿戴物品的目的是有存在实体，另一个实体， and 和第三实体这样那个实体是过程的 instance 和那个另外实体是那个第三实体所描述的类别的 subclass 和那个实体 prevents 那个另外实体的发生和那个可穿戴物品是导致那个实体的 instrument
No TPTP formula. May not be expressible in strict first order.	Dining.kif 219-223	如果 Catalog 是 AlcoholMenu 的 instance 和有点实体是在那个 Catalog ，然后有点实体是酒精饮料的 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.	Military.kif 886-897	地缘政治区域的 fit 对于军服务男性 equal 符号串所描述的类别 instance 的数量
No TPTP formula. May not be expressible in strict first order.	Cars.kif 5094-5097	有存在有点客体这样有点客体是 HandToolBox 的 subclass 和 manufacturer 那个有点客体 and SortimoCorp

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1170-1170	AAM 是空袭导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1169-1169	AAM 是空中发射导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1171-1171	AAM 是导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1647-1647	AAV 是两栖车辆的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1646-1646	AAV 是军车的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1648-1648	AAV 是乘用车的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1649-1649	AAV 是动力车辆的 subclass
No TPTP formula. May not be expressible in strict first order.	Muscles.kif 778-778	ABranchOfDorsalPrimaryDivisionOfSuboccipitalNerve 是 Nerve 的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 26388-26388	ACPowerSource 是能量源的 subclass
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 3293-3293	ADHD 是心理功能障碍的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1123-1123	AG m 是空中发射导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1124-1124	AG m 是地面攻击导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1203-1203	AG m114 是 AG m 的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1205-1205	AG m114 是反装甲武器的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1204-1204	AG m114 是束骑导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1136-1136	AG m65 是 AG m 的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1138-1138	AG m65 是反装甲武器的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1137-1137	AG m65 是红外导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1889-1889	A h1 是直升机的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1890-1890	A h1 是军车的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1177-1177	AI m9 是 AAM 的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 1178-1178	AI m9 是红外导弹的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 2130-2130	AMEV 是救护车的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 2129-2129	AMEV 是陆地车辆的 subclass
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 2128-2128	AMEV 是军车的 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: