| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13204-13204 |
子類 Ordering and Directing |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13230-13230 |
子類 Questioning and Directing |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13216-13216 |
子類 Requesting and Directing |
| 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 |
|
