| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1273-1273 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 951-951 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 486-486 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 490-490 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2635-2635 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 903-903 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 526-526 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 972-972 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 491-491 |
|
MutuallyDisjointClass