No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2793-2793 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 8768-8768 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1512-1512 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 8766-8766 |
Decade is internally related to decade duration |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 8765-8765 |
Decade is a subclass of time interval |