|
|
   Class
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1806-1810 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2138-2146 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 421-427 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10629-10629 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10628-10628 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10631-10631 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10630-10630 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10627-10627 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10626-10626 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 9942-9942 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10633-10633 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10625-10625 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2136-2136 | Classe est une sous-classe de ensemble ou classe |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1762-1762 | Le domaine de ExtensionFn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5585-5585 | Le domaine de KappaFn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1516-1516 | Le domaine de WeekBeforeMenstruationFn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 886-886 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 974-974 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 562-562 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 92-92 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 95-95 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2247-2247 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 514-514 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 97-97 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 129-129 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 583-583 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 96-96 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1490-1490 | Le nombre 1 argument de TTFxFn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3576-3576 | Le nombre 2 argument de closedOn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 395-395 | Le nombre 1 argument de disjoint est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 396-396 | Le nombre 2 argument de disjoint est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 566-566 | Le nombre 1 argument de disjointDecomposition est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 567-567 | Le nombre 2 argument de disjointDecomposition est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 210-210 | Le nombre 3 argument de domain est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-232 | Le nombre 3 argument de domainSubclass est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3707-3707 | Le nombre 2 argument de equivalenceRelationOn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 548-548 | Le nombre 1 argument de exhaustiveDecomposition est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 549-549 | Le nombre 2 argument de exhaustiveDecomposition est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 91-91 | Le nombre 2 argument de immediateInstance est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 153-153 | Le nombre 1 argument de immediateSubclass est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 154-154 | Le nombre 2 argument de immediateSubclass est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 82-82 | Le nombre 2 argument de instance est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31031-31031 | Le nombre 1 argument de memberMeasure est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22702-22702 | Le nombre 2 argument de memberType est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22716-22716 | Le nombre 2 argument de memberTypeCount est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3644-3644 | Le nombre 2 argument de partialOrderingOn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 582-582 | Le nombre 1 argument de partition est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 583-583 | Le nombre 2 argument de partition est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 307-307 | Le nombre 2 argument de range est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3605-3605 | Le nombre 2 argument de reflexiveOn est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | Le nombre 1 argument de subclass est une instance de classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | Le nombre 2 argument de subclass est une instance de classe |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31042-31047 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31049-31054 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31218-31223 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31247-31252 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31143-31148 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31196-31201 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31357-31364 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31077-31082 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31387-31392 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31269-31274 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31312-31317 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31122-31127 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31096-31101 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 828-830 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 145-160 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 574-578 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 558-562 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2034-2041 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2043-2052 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 137-141 |
|
|
|
