No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3575-3576 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15682-15684 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2894-2894 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2899-2899 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2898-2898 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2900-2900 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2895-2895 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2720-2720 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2901-2901 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2897-2897 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2893-2893 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2896-2896 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15681-15681 |
Patent is a subclass of certificate |