| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13182-13182 |
命令 是 指令g 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13208-13208 |
询问 是 指令g 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13194-13194 |
要求 是 指令g 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1199-1199 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1615-1615 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 877-877 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 410-410 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 413-413 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2561-2561 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 829-829 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 415-415 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 449-449 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 898-898 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 414-414 |
|
