| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12028-12028 |
决定 是 选择 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 318-318 |
指定 是 选择 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12109-12109 |
判断 是 选择 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12096-12096 |
表决 是 选择 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1147-1147 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1511-1511 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 825-825 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 357-357 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 360-360 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2509-2509 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 777-777 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 362-362 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 396-396 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 846-846 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 361-361 |
|
Selecting