No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 429-429 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 435-435 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 249-249 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 295-295 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2043-2043 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 201-201 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-cz.txt 254-254 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 559-559 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 331-331 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 270-270 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 272-272 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 487-487 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 8196-8196 |
子關係 一時之間 and 暫時之間或等於 |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 430-430 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 57448-57448 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 57447-57447 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 57446-57446 |
|