subclass |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1371-1373 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 133-135 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 27-29 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 28-30 | |
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 129-129 | subclass is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18660-18660 | subclass is an instance of closed world predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | subclass is an instance of partial ordering relation |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 319-319 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 324-324 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 182-182 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 271-271 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2002-2002 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 134-134 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 175-175 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 419-419 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 308-308 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 202-202 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 192-192 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 463-463 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22956-22956 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55708-55708 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55707-55707 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55706-55706 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 133-133 | sub field is a subrelation of subclass |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
No TPTP formula. May not be expressible in strict first order. | Military.kif 963-974 | equal the fit for military service male of a geopolitical area and the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 5170-5173 | There exists a kind of object such that a kind of object is a subclass of tool box and the maker of the kind of object is Sortimo Corporation |
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 778-778 | A branch of dorsal primary division of suboccipital nerve is a subclass of nerve |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28254-28254 | Ac power source is a subclass of power source |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3294-3294 | Attention deficit hyperactivity disorder is a subclass of psychological dysfunction |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27208-27208 | Am / fm alarm clock is a subclass of alarm clock |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27209-27209 | Am / fm alarm clock is a subclass of radio receiver |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 293-293 | AM radio station is a subclass of radio station |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 236-236 | AM radio system is a subclass of radio system |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 4075-4075 | AOC number is a subclass of symbolic string |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3601-3601 | ATM machine is a subclass of stationary artifact |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3677-3677 | ATM slot is a subclass of hole |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 4876-4876 | Atv tire is a subclass of tire |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2169-2169 | Audio/Video Control Transport Protocol is a subclass of computer program |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6430-6430 | AVPU status is a subclass of relational attribute |
No TPTP formula. May not be expressible in strict first order. | Food.kif 1994-1994 | Abalone is a subclass of mollusk |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4952-4952 | Abatacept is a subclass of Immunosupressant |
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 527-527 | Abayah is a subclass of cloak |
No TPTP formula. May not be expressible in strict first order. | People.kif 1213-1213 | Abbey is a subclass of religious organization |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14148-14148 | Abdomen is a subclass of animal anatomical structure |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1272-1272 | Abdominal aorta is a subclass of artery |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 135-135 | Abducens nerve [CNVI] is a subclass of nerve |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 2046-2046 | Abducting is a subclass of body motion |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 2047-2047 | Abducting is a subclass of moving away from |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 1608-1608 | Abductor digiti minimi muscle is a subclass of muscle |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 2127-2127 | Abductor hallucis muscle is a subclass of muscle |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 1581-1581 | Abductor pollicis brevis muscle is a subclass of muscle |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |