Class(class)![]() ![]() ![]() ![]() | ![]() | brand, categorial, categoric, categorical, categorisation, categorization, category, class, classification, color, colour, connotation, denomination, description, family, form, genus, histocompatibility_complex, intension, kind, kingdom, like, make, manner, nature, paradigm, pigeonhole, rubric, sort, species, stamp, stripe, style, substitution_class, the_like, the_likes_of, trichotomy, variety, way |
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 2125-2133 | |
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 10632-10632 | |
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 10634-10634 | |
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 10630-10630 | |
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 9943-9943 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10636-10636 | |
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. | Merge.kif 2123-2123 | Class is a subclass of set or class |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1749-1749 | The range of extension is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5570-5570 | The range of kappa is an instance of class |
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 93-93 | |
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 1696-1696 | The number 1 argument of TTFx is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3562-3562 | The number 2 argument of closed on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 395-395 | The number 1 argument of disjoint is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 396-396 | The number 2 argument of disjoint is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 566-566 | The number 1 argument of disjoint decomposition is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 567-567 | The number 2 argument of disjoint decomposition is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 210-210 | The number 3 argument of domain is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-232 | The number 3 argument of domain subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3693-3693 | The number 2 argument of equivalence relation on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 548-548 | The number 1 argument of exhaustive decomposition is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 549-549 | The number 2 argument of exhaustive decomposition is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 91-91 | The number 2 argument of immediate instance is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 153-153 | The number 1 argument of immediate subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 154-154 | The number 2 argument of immediate subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 82-82 | The number 2 argument of instance is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3630-3630 | The number 2 argument of partial ordering on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 582-582 | The number 1 argument of partition is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 583-583 | The number 2 argument of partition is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 307-307 | The number 2 argument of range is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3591-3591 | The number 2 argument of reflexive on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | The number 1 argument of subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | The number 2 argument of subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8997-8997 | The number 1 argument of successor class is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8998-8998 | The number 2 argument of successor class is an instance of class |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4736-4736 | The number 1 argument of total is an instance of class |
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 31123-31128 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31130-31135 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31291-31296 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31320-31325 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31224-31229 |
|
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 31430-31437 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31158-31163 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31460-31465 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31342-31347 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31385-31390 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31203-31208 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31177-31182 |
|
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 182-197 |
|
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 2240-2247 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2249-2258 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 137-141 |
|
![]() |
![]() |