| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14432-14432 |
Plante non florissante est disjointement decompos� en algue, foug�re, + mousse |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 3385-3385 |
Seaweed est une sous-classe de algue |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 968-968 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1143-1143 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 645-645 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 176-176 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 179-179 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2329-2329 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 597-597 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 213-213 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 666-666 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 180-180 |
|
