No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 523-523 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 528-528 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 309-309 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 209-209 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2077-2077 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 261-261 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-cz.txt 315-315 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 680-680 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 247-247 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 330-330 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 337-337 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 400-400 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16437-16437 |
子關係 女兒 and 親 |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16448-16448 |
子關係 兒子 and 親 |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 44430-44430 |
|
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 524-524 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 44429-44429 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 44428-44428 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 401-401 |
|