| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17224-17224 |
中央时区 是 时区 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17190-17190 |
协调的通用世界时区 是 时区 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17236-17236 |
东部时区 是 时区 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17212-17212 |
山区时区 是 时区 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17197-17197 |
太平洋时区 是 时区 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1238-1238 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1697-1697 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 916-916 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 449-449 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 452-452 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2600-2600 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 868-868 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 454-454 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 488-488 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 937-937 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 453-453 |
|
