No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 10362-10373	如果 过程 是 Breath 的 instance， 然后 有存在 另一个 过程 和 第三 过程 这样 那个 另外 过程%n是那个 过程的subProcess 和 那个 第三 过程%n是那个 过程的subProcess 和 那个 另外 过程 出现 的 time 比那个 第三 过程 出现 的 time发生的earlier 和 那个 另外 过程 出现 的 time 接着 那个 第三 过程 出现 的 time
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8892-8899	如果 时距 是 一天的时间 的 instance， 然后 有存在 另一个 时距 和 第三 时距 这样 那个 另外 时距 是 晚上的时间 的 instance 和 那个 第三 时距 是 晚上的时间 的 instance 和 那个 时距 接着 那个 另外 时距 和 那个 第三 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1626-1638	如果 过程 是 山洪暴发 的 instance， 然后 有存在 另一个 过程 和 实数 这样 那个 另外 过程 是 水运动 的 instance 和 那个 另外 过程 causes 那个 过程 和 那个 另外 过程 出现 的 time 接着 那个 过程 出现 的 time 和 那个 另外 过程 出现 的 time 的 duration 是 那个 实数 小时 和 那个 实数 是 lessThan 6.0
No TPTP formula. May not be expressible in strict first order.	Cars.kif 114-132	如果 物理 是 FourStrokeEngine 的 instance， 然后 那个 物理 的 目的 是 有存在 实体， 另一个 实体,， ， 第三 实体,， ， 第四 实体， and 和 那个 实体2 这样 那个 实体 是 FourStrokeIntake 的 instance 和 那个 另外 实体 是 FourStrokeCompression 的 instance 和 那个 第三 实体 是 FourStrokeCombustion 的 instance 和 那个 第四 实体 是 FourStrokeExhaust 的 instance 和 那个 实体2 是 FourStrokeIntake 的 instance 和 那个 实体 是 located 在 那个 物理 和 那个 另外 实体 是 located 在 那个 物理 和 那个 第三 实体 是 located 在 那个 物理 和 那个 第四 实体 是 located 在 那个 物理 和 那个 实体2 是 located 在 那个 物理 和 那个 实体 接着 那个 另外 实体 和 那个 另外 实体 接着 那个 第三 实体 和 那个 第三 实体 接着 那个 第四 实体 和 那个 第四 实体 接着 那个 实体2
No TPTP formula. May not be expressible in strict first order.	Cars.kif 147-164	如果 过程 是 FourStrokeEngineCycle 的 instance， 然后 有存在 时距， 另一个 时距,， ， 第三 时距,， ， 第四 时距， and 和 那个 时距2 这样 那个 时距 是 FourStrokeIntake 的 instance 和 那个 另外 时距 是 FourStrokeCompression 的 instance 和 那个 第三 时距 是 FourStrokeCombustion 的 instance 和 那个 第四 时距 是 FourStrokeExhaust 的 instance 和 那个 时距2 是 FourStrokeIntake 的 instance 和 那个 时距%n是那个 过程的subProcess 和 那个 另外 时距%n是那个 过程的subProcess 和 那个 第三 时距%n是那个 过程的subProcess 和 那个 第四 时距%n是那个 过程的subProcess 和 那个 时距2%n是那个 过程的subProcess 和 那个 时距 接着 那个 另外 时距 和 那个 另外 时距 接着 那个 第三 时距 和 那个 第三 时距 接着 那个 第四 时距 和 那个 第四 时距 接着 那个 时距2
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8508-8510	如果 时距 是 时距 的 instance， 然后 那个 时距 before 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8539-8541	如果 时距 是 时距 的 instance， 然后 那个 时距 接着 那个 时距 之后
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 266-286	如果 时距 是 ListOnSite 的 instance， 然后 有存在 客体， 实体,， ， 另一个 时距,， ， 第三 时距， and 和 施事体 这样 那个 客体 是 WebSite 的 instance 和 那个 实体 是 WebListing 的 instance 和 那个 另外 时距 是 时距 的 instance 和 那个 第三 时距 是 时距 的 instance 和 那个 实体 是 那个 时距 的 patient 和 那个 另外 时距 的结束 equal 那个 时距 的结束 和 那个 时距 比那个 第三 时距发生的earlier 和 那个 时距 接着 那个 第三 时距 和 不 那个 实体 是在 那个 客体 hosted 在 那个 另外 时距 holdsDuring 和 那个 实体 是在 那个 客体 hosted 在 那个 第三 时距 holdsDuring 和 那个 施事体 是 那个 时距 的 agent 和 那个 施事体 possesses 那个 客体
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8914-8921	如果 时距 是 晚上的时间 的 instance， 然后 有存在 另一个 时距 和 第三 时距 这样 那个 另外 时距 是 一天的时间 的 instance 和 那个 第三 时距 是 一天的时间 的 instance 和 那个 时距 接着 那个 另外 时距 和 那个 第三 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19165-19170	如果 时距 是 春暖花开的季节 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 夏季 的 instance 和 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19172-19177	如果 时距 是 春暖花开的季节 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 冬季 的 instance 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19190-19195	如果 时距 是 夏季 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 秋季 的 instance 和 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19183-19188	如果 时距 是 夏季 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 春暖花开的季节 的 instance 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Cars.kif 264-278	如果 过程 是 TwoStrokeEngineCycle 的 instance， 然后 有存在 时距， 另一个 时距,， ， 那个 过程T， and 和 那个 时距2 这样 那个 时距 是 TwoStrokeIntake 的 instance 和 那个 另外 时距 是 TwoStrokeCompression 的 instance 和 那个 过程T 是 TwoStrokeTransfer 的 instance 和 那个 时距2 是 TwoStrokeIntake 的 instance 和 那个 时距%n是那个 过程的subProcess 和 那个 另外 时距%n是那个 过程的subProcess 和 那个 过程T%n是那个 过程的subProcess 和 那个 时距2%n是那个 过程的subProcess 和 那个 时距 接着 那个 另外 时距 和 那个 另外 时距 接着 那个 过程T 和 那个 过程T 接着 那个 时距2
No TPTP formula. May not be expressible in strict first order.	Media.kif 369-374	如果 时距 是 Advent 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 ChristmasDay 的 instance 和 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Media.kif 362-367	如果 时距 是 ChristmasDay 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 Advent 的 instance 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Media.kif 430-435	如果 时距 是 EasterSunday 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 Lent 的 instance 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Media.kif 423-428	如果 时距 是 Lent 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 EasterSunday 的 instance 和 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Cars.kif 2029-2049	如果 过程 是 VaporCompressionCycle 的 instance， 然后 有存在 另一个 过程， 第三 过程,， ， 第四 过程， and 和 那个 另外 过程2 这样 那个 另外 过程 是 Compressing 的 instance 和 那个 第三 过程 是 凝结 的 instance 和 那个 第四 过程 是 蒸发 的 instance 和 那个 另外 过程2 是 Compressing 的 instance 和 那个 另外 过程%n是那个 过程的subProcess 和 那个 第三 过程%n是那个 过程的subProcess 和 那个 第四 过程%n是那个 过程的subProcess 和 那个 另外 过程2%n是那个 过程的subProcess 和 那个 另外 过程 出现 的 time 接着 那个 第三 过程 出现 的 time 和 那个 第三 过程 出现 的 time 接着 那个 第四 过程 出现 的 time 和 那个 第四 过程 出现 的 time 接着 那个 另外 过程2 出现 的 time
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19120-19128	如果 时距 是 周末 的 instance， 然后 有存在 另一个 时距 和 第三 时距 这样 那个 另外 时距 是 星期六 的 instance 和 那个 第三 时距 是 星期日 的 instance 和 那个 另外 时距 starts了才到 那个 时距 和 那个 第三 时距 finishes了才到 那个 时距 和 那个 另外 时距 接着 那个 第三 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19152-19157	如果 时距 是 冬季 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 秋季 的 instance 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19145-19150	如果 时距 是 冬季 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 春暖花开的季节 的 instance 和 那个 时距 接着 那个 另外 时距

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