No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 16249-16249 |
Legal summons is a subclass of ordering |
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 1657-1657 |
Operation order is a subclass of ordering |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1200-1200 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1617-1617 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 878-878 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 411-411 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 414-414 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2562-2562 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 830-830 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 416-416 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 450-450 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 899-899 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 415-415 |
|