No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2073-2073 |
Time duration is a subclass of time measure |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2078-2078 |
Time position is a subclass of time measure |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 877-877 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 956-956 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 553-553 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 83-83 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 86-86 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2238-2238 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 505-505 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 88-88 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 120-120 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 574-574 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 87-87 |
|