| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 6441-6441 |
子類 痿 and Decreasing |
| No TPTP formula. May not be expressible in strict first order. |
Cars.kif 1247-1247 |
子類 Braking and Decreasing |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 10978-10978 |
子類 Cooling and Decreasing |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17166-17166 |
子類 減速 and Decreasing |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17204-17204 |
子類 縮短 and Decreasing |
| 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 |
|
