No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3084-3085 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 11781-11783 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1854-1856 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 11089-11089 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 11092-11092 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10036-10036 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 11088-11088 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 11091-11091 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 11090-11090 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 11779-11779 |
回馈 是 给予 的 subclass |