No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3519-3519 |
Nation est disjoint de continent |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3521-3521 |
Africa est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3537-3537 |
Antarctica est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3548-3548 |
Asia est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
CountriesAndRegions.kif 43-43 |
Europe est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3527-3527 |
NorthAmerica est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3554-3554 |
Oceania est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3531-3531 |
SouthAmerica est une instance de continent |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 956-956 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1119-1119 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 632-632 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 163-163 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 166-166 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2317-2317 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 584-584 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 168-168 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 200-200 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 653-653 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 167-167 |
|