No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17273-17273 |
CentralTimeZone e' uma instancia de Zona Temporal |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17239-17239 |
CoordinatedUniversalTimeZone e' uma instancia de Zona Temporal |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17285-17285 |
EasternTimeZone e' uma instancia de Zona Temporal |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17261-17261 |
MountainTimeZone e' uma instancia de Zona Temporal |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17246-17246 |
PacificTimeZone e' uma instancia de Zona Temporal |
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 |
|