|
|
   BinaryNumber
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1755-1756 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2005-2006 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 364-365 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4962-4962 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4864-4864 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4963-4963 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2003-2003 | 二进制数 是 实数 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 873-873 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 948-948 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 549-549 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 79-79 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 82-82 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2234-2234 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 501-501 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 116-116 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 570-570 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 83-83 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 801-812 |
|
|
|
