No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19470-19471 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10849-10849 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 9981-9981 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10856-10856 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10857-10857 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10852-10852 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10854-10854 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10855-10855 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10848-10848 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10850-10850 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10853-10853 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10851-10851 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19469-19469 |
Digit character is a subclass of character |