| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 193-193 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 194-194 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 116-116 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 302-302 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1945-1945 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 68-68 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-cz.txt 110-110 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 247-247 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 338-338 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 135-135 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 121-121 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 494-494 |
|
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 194-194 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 58600-58600 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 58599-58599 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 58598-58598 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-de.txt 78-78 |
|
totalOrderingOn