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 | O argumento numero 1 de subclass e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | O argumento numero 2 de subclass e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | subclass e' uma instancia de Predicado Binario |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18472-18472 | subclass e' uma instancia de ClosedWorldPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | subclass e' uma instancia de Relacao parcialmente Ordenada |
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 21339-21339 | subField e' uma sub-relacao de subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5391-5391 | Subconjunto e' uma sub-relacao de subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55704-55704 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55703-55703 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55702-55702 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31387-31394 | |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1478-1491 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 221-227 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3005-3010 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 244-250 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 195-200 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4945-4950 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4532-4543 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5258-5265 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5032-5036 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5235-5244 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1780-1788 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3840-3845 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3963-3968 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3993-3998 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12014-12026 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3904-3909 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3934-3939 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3872-3877 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3948-3953 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5485-5493 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18084-18092 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3447-3476 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 219-223 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | Military.kif 895-906 | FitForMilitaryServiceMaleFn Area Geopolitica e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 5109-5112 | Objeto Objeto e' uma sub-classe de HandToolBox manufacturer Objeto and SortimoCorp |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1170-1170 | AAM e' uma sub-classe de AirAttackMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1169-1169 | AAM e' uma sub-classe de AirLaunchMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1171-1171 | AAM e' uma sub-classe de GuidedMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1647-1647 | AAV e' uma sub-classe de AmphibiousVehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1646-1646 | AAV e' uma sub-classe de MilitaryVehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1648-1648 | AAV e' uma sub-classe de PassengerVehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1649-1649 | AAV e' uma sub-classe de PoweredVehicle |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 778-778 | ABranchOfDorsalPrimaryDivisionOfSuboccipitalNerve e' uma sub-classe de Nerve |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26355-26355 | ACPowerSource e' uma sub-classe de PowerSource |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3293-3293 | ADHD e' uma sub-classe de Disfuncao Psicologica |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1123-1123 | AGM e' uma sub-classe de AirLaunchMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1124-1124 | AGM e' uma sub-classe de GroundAttackMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1203-1203 | AGM114 e' uma sub-classe de AGM |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1205-1205 | AGM114 e' uma sub-classe de AntiArmorWeapon |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1204-1204 | AGM114 e' uma sub-classe de BeamRidingGMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1136-1136 | AGM65 e' uma sub-classe de AGM |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1138-1138 | AGM65 e' uma sub-classe de AntiArmorWeapon |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1137-1137 | AGM65 e' uma sub-classe de InfraRedGMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1889-1889 | AH1 e' uma sub-classe de Helicopter |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1890-1890 | AH1 e' uma sub-classe de MilitaryVehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1177-1177 | AIM9 e' uma sub-classe de AAM |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1178-1178 | AIM9 e' uma sub-classe de InfraRedGMissile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2130-2130 | AMEV e' uma sub-classe de Ambulance |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2129-2129 | AMEV e' uma sub-classe de LandVehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2128-2128 | AMEV e' uma sub-classe de MilitaryVehicle |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |