| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1272-1272 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 950-950 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 485-485 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 489-489 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2634-2634 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 902-902 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 525-525 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 971-971 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 490-490 |
|
PairwiseDisjointClass