No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 2455-2455 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 2454-2454 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 2453-2453 |
|
No TPTP formula. May not be expressible in strict first order. |
Music.kif 838-838 |
Musical interpretation is an instance of ternary function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3161-3161 |
Sub-list function is an instance of ternary function |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 24470-24470 |
Substring fn is an instance of ternary function |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 923-923 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1053-1053 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 599-599 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 129-129 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 132-132 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2284-2284 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 551-551 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 166-166 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 620-620 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 133-133 |
|