No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 35-43	如果 军车 是 对于 正整数 的 weapon 携带容量 有点 武器 和 客体 是 有点 武器 的 instance 和 那个 客体 能够担当 格角色 的角色做 有点 过程 和 有点 过程 是 射击 的 subclass 或 那个 有点 过程 是 损坏 的 subclass， 然后 那个 军车 能够担当 那个 格角色 的角色做 那个 有点 过程
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18366-18370	如果 睡着 是 客体 的 attribute 或 觉醒 是 那个 客体 的 attribute， 然后 活的 是 那个 客体 的 attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8173-8177	如果 时点%n在另一个 时点before发生 或 那个 时点 equal 那个 另外 时点， 然后 那个 时点%n{doesn't}在那个 另外 时点 之前或同时发生
No TPTP formula. May not be expressible in strict first order.	Geography.kif 433-440	如果 方向属性 equal 北 或 那个 方向属性 equal 南， 然后 0.0 圆周角度 的 region 那个 方向属性 的 length 是 1.0 海里

Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners