No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 6436-6436 |
痿 是 减少 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 1247-1247 |
Braking 是 减少 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 10990-10990 |
冷却 是 减少 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17194-17194 |
减速 是 减少 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17232-17232 |
缩短 是 减少 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1111-1111 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1439-1439 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 789-789 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 321-321 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 324-324 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2473-2473 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 741-741 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 326-326 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 360-360 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 810-810 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 325-325 |
|