appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3747-3748 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16813-16815 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16812-16812 | Educational organization is a subclass of organization |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8681-8681 | Library is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8711-8711 | Museum is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16903-16903 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1071-1071 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1353-1353 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 749-749 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 281-281 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 284-284 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2433-2433 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 701-701 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 320-320 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 770-770 | School is a subclass of educational organization |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 285-285 | School is a subclass of educational organization |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17044-17044 | The number 2 argument of student is an instance of educational organization |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17116-17116 | The number 2 argument of teacher is an instance of educational organization |
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1003-1007 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 10750-10754 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 10761-10765 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16881-16888 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22896-22901 |
|