| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 10969-10969 |
Diminuir e' uma sub-classe de Modificacao de Quantidade |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 3336-3336 |
Focusing e' uma sub-classe de Modificacao de Quantidade |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 10927-10927 |
Aumentar e' uma sub-classe de Modificacao de Quantidade |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1108-1108 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1433-1433 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 786-786 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 318-318 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 321-321 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2470-2470 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 738-738 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 323-323 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 357-357 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 807-807 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 322-322 |
|
