TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1500-1501
No TPTP formula. May not be expressible in strict first order.	Merge.kif 397-399
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 63-64
No TPTP formula. May not be expressible in strict first order.	spanish_format.kif 72-74
No TPTP formula. May not be expressible in strict first order.	Merge.kif 395-395	不相交的 1 数量是类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 396-396	不相交的 2 数量是类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 393-393	不相交是二元谓语的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 394-394	不相交是对称关系的 instance

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 285-285
No TPTP formula. May not be expressible in strict first order.	english_format.kif 290-290
No TPTP formula. May not be expressible in strict first order.	french_format.kif 165-165
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 75-75
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1985-1985
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 117-117
No TPTP formula. May not be expressible in strict first order.	relations-cb.txt 109-109
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 182-182
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 370-370
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 59-59
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 185-185
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 172-172
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 166-166
No TPTP formula. May not be expressible in strict first order.	Merge.kif 569-569	不相交的分拆和不相交是内部相关
No TPTP formula. May not be expressible in strict first order.	Merge.kif 414-414	不相交关系和不相交是内部相关
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 286-286
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19848-19848
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19847-19847
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19846-19846
No TPTP formula. May not be expressible in strict first order.	terms-de.txt 115-115
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 167-167

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 419-424	如果关系的正整数数量是类的 instance 和另一个关系的那个正整数数量是另一个类的 instance 和那个类和 % 2 是 disjoint，然后那个关系和那个另外关系是 disjoint 关系
No TPTP formula. May not be expressible in strict first order.	Merge.kif 426-431	如果关系的正整数数量是类的 subclass 和另一个关系的那个正整数数量是另一个类的 subclass 和那个类和 % 2 是 disjoint，然后那个关系和那个另外关系是 disjoint 关系
No TPTP formula. May not be expressible in strict first order.	Merge.kif 433-438	如果函数的 range 是类的实例和另一个函数的 range 是另一个类的实例和那个类和 % 2 是 disjoint，然后那个函数和那个另外函数是 disjoint 关系
No TPTP formula. May not be expressible in strict first order.	Merge.kif 440-445	如果函数的所得值是有点类的 subclass 和另一个函数的所得值是另一个有点类的 subclass 和有点类和 % 2 是 disjoint，然后那个函数和那个另外函数是 disjoint 关系
No TPTP formula. May not be expressible in strict first order.	Merge.kif 401-407	如果类和 % 2 是 disjoint，然后不存在实体这样那个实体是那个类的 instance 和那个实体是另一个类的 instance

consequent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 2968-2973	如果类分拆成不相交的另一个类, 第三类, 和第四类，然后那个另外类和 % 2 是 disjoint 和那个第三类和 % 2 是 disjoint 和那个第四类和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2957-2966	如果类分拆成不相交的 @ROW，然后对所有第三类和第四类如果那个第三类是 (@ROW) 的 member 和那个第四类是 (@ROW) 的 member 和那个第三类不 equal 那个第四类，然后那个第三类和 % 2 是 disjoint

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 974-974	在线以上和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8792-8792	下午和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 360-360	AltKey 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 362-362	AltKey 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 361-361	AltKey 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1313-1313	AltKeyHoldDown 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1312-1312	AltKeyHoldDown 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 8233-8233	无氧运动装置和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19107-19107	上午和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6937-6937	公寓楼和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 295-295	ArrowKey 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14678-14678	文章和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 172-172	火炮和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5954-5954	沥青和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 14023-14023	天文体和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12348-12348	连接和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1656-1656	AudioInput 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1657-1657	AudioInput 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1655-1655	AudioInput 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10164-10164	自主过程和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 15737-15737	谷仓和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Sports.kif 740-740	棒球偷和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Sports.kif 739-739	棒球偷和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Sports.kif 748-748	棒球罢工和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Sports.kif 696-696	棒球步行和 % 2 是 disjoint

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: