No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12710-12710 |
Decodificar e' disjunto de Codificar |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3207-3208 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12711-12713 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10811-10811 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10805-10805 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10807-10807 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10813-10813 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10814-10814 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10808-10808 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10816-10816 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10809-10809 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10810-10810 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10806-10806 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12709-12709 |
Decodificar e' uma sub-classe de Escrever |