TreeView Knowledge Base Browser

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

No TPTP formula. May not be expressible in strict first order.	Medicine.kif 3984-4004	ADHD e' um atributo de AutonomousAgent ADHD e' um atributo de AutonomousAgent AutonomousAgent e' igual a AutonomousAgent Processo e' uma instancia de Classe Processo e' uma instancia de Classe Classe e' uma sub-classe de Processo Psicologico Intencional Processo e' um agente de AutonomousAgent Processo e' um agente de AutonomousAgent a duracao de tempo de existencia de Processo e' Duracao Temporal a duracao de tempo de existencia de Processo e' Duracao Temporal o argumento Duracao Temporal e' maior que Duracao Temporal tem a forca modal de Likely
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1186-1201	Oversized e' um atributo de Objeto Objeto e' uma instancia imediata de Classe Classe e' uma sub-classe de HotelUnit Fisico Numero Real, Numero Real and Unidade de Medida Fisico e' uma instancia imediata de Classe Unidade de Medida e' uma instancia de UnitOfArea a medida de Fisico e' Numero Real Unidade de Medida(s) a medida de Objeto e' Numero Real Unidade de Medida(s) Numero Real e' uma instancia de Medida de Area Numero Real e' uma instancia de Medida de Area Numero Real e' maior que Numero Real
No TPTP formula. May not be expressible in strict first order.	Biography.kif 730-740	Writer e' um atributo de AutonomousAgent Entidade e' uma instancia de Objeto Representendo Conteudo Abstrato Objeto Representendo Conteudo Abstrato e' uma sub-classe de Texto Objeto Representendo Conteudo Abstrato e' uma sub-classe de Document Processo e' uma instancia de Escrever Processo e' um agente de AutonomousAgent Entidade e' o resultado de Processo AutonomousAgent e' o autor de Objeto Representendo Conteudo Abstrato
No TPTP formula. May not be expressible in strict first order.	WMD.kif 789-793	biochemicalAgentDelivery BiochemicalAgent and Processo Processo e' uma sub-classe de Processo biochemicalAgentDelivery BiochemicalAgent and Processo
No TPTP formula. May not be expressible in strict first order.	WMD.kif 976-980	biologicalAgentCarrier BiologicalAgent and Organismo Organismo e' uma sub-classe de Organismo biologicalAgentCarrier BiologicalAgent and Organismo
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 48-56	Objeto e' capaz de fazer Processo no role Role em Caso Processo e' uma sub-classe de Atirar Objeto Objeto e' uma instancia de Arma Objeto e' uma &parte de Objeto Objeto e' capaz de fazer Processo no role Role em Caso
No TPTP formula. May not be expressible in strict first order.	Government.kif 619-625	commemoratesDate Holiday and o dia Inteiro positivo Entidade e' uma instancia de Holiday Holiday e' uma sub-classe de FixedHoliday Numero Inteiro e' menor ou igual a Entidade-YEAR Entidade e' uma instancia de o dia Inteiro positivo
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 504-520	customer Agente Cognitivo and AutonomousAgent propertyAmenity AutonomousAgent and Fisico Fisico e' uma sub-classe de Objeto Entidade e' uma instancia de Fisico AutonomousAgent autoriza Agente Cognitivo a executar tarefas de tipo Entidade Entidade e' uma instancia de Processo Entidade e' um recurso para Entidade Entidade e' um instrumento para Entidade Entidade e' um patient de Entidade Entidade e' um agente de Agente Cognitivo Agente Cognitivo experimenta Entidade
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 522-538	customer Agente Cognitivo and AutonomousAgent propertyAmenity AutonomousAgent and Fisico Fisico e' uma sub-classe de Processo o argumento Entidade Entidade and Entidade Entidade e' um elemento de propriedade de AutonomousAgent Entidade e' um agente de AutonomousAgent Agente Cognitivo e' um patient de Entidade Entidade e' uma instancia de Fisico Entidade e' uma instancia de Fisico Entidade e' um sub-processo de Entidade Entidade e' situado em Entidade tem a forca modal de Possibility
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13547-13558	defaultMaximumMeasure Objeto and Numero Real Unidade de Medida(s) Classe e' uma sub-classe de NonCompositeUnitOfMeasure Unidade de Medida e' uma instancia de Classe o argumento Entidade Numero RealUANTITY and Entidade Entidade e' uma instancia de Objeto a medida de Entidade e' Numero RealUANTITY Entidade(s) Entidade e' uma instancia de Classe Numero RealUANTITY Entidade(s) e' maior que Numero Real Unidade de Medida(s) tem a forca modal de Unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13516-13527	defaultMinimumMeasure Objeto and Numero Real Unidade de Medida(s) Classe e' uma sub-classe de NonCompositeUnitOfMeasure Unidade de Medida e' uma instancia de Classe o argumento Entidade Numero RealUANTITY and Entidade Entidade e' uma instancia de Objeto a medida de Entidade e' Numero RealUANTITY Entidade(s) Entidade e' uma instancia de Classe Numero RealUANTITY e' menos que Numero Real tem a forca modal de Unlikely
No TPTP formula. May not be expressible in strict first order.	WMD.kif 957-961	diseaseMedicine Doenca ou Sindrome, Substancia Biologica Ativa and Processo Processo e' uma sub-classe de Processo diseaseMedicine Doenca ou Sindrome, Substancia Biologica Ativa and Processo
No TPTP formula. May not be expressible in strict first order.	WMD.kif 963-967	diseaseMedicine Doenca ou Sindrome, Substancia Biologica Ativa and Processo Substancia Biologica Ativa e' uma sub-classe de Substancia Biologica Ativa diseaseMedicine Doenca ou Sindrome, Substancia Biologica Ativa and Processo
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2112-2121	electricityConsumptionInPeriod Area Geopolitica, Quantidade Fisica and Intervalo Temporal Intervalo Temporal e' uma sub-classe de Ano Intervalo Temporal e' uma sub-classe de FiscalYearFn Area Geopolitica Posicao Temporal Posicao Temporal e' uma instancia de Intervalo Temporal annualElectricityConsumption Area Geopolitica and Quantidade Fisica vale durante Posicao Temporal
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2156-2165	electricityExportInPeriod Area Geopolitica, Quantidade Fisica and Intervalo Temporal Intervalo Temporal e' uma sub-classe de Ano Intervalo Temporal e' uma sub-classe de FiscalYearFn Area Geopolitica Posicao Temporal Posicao Temporal e' uma instancia de Intervalo Temporal annualElectricityExport Area Geopolitica and Quantidade Fisica vale durante Posicao Temporal
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2202-2211	electricityImportInPeriod Area Geopolitica, Quantidade Fisica and Intervalo Temporal Intervalo Temporal e' uma sub-classe de Ano Intervalo Temporal e' uma sub-classe de FiscalYearFn Area Geopolitica Posicao Temporal Posicao Temporal e' uma instancia de Intervalo Temporal annualElectricityImport Area Geopolitica and Quantidade Fisica vale durante Posicao Temporal
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1980-1989	electricityProductionInPeriod Area Geopolitica, Quantidade Fisica and Intervalo Temporal Intervalo Temporal e' uma sub-classe de Ano Intervalo Temporal e' uma sub-classe de FiscalYearFn Area Geopolitica Posicao Temporal Posicao Temporal e' uma instancia de Intervalo Temporal annualElectricityProduction Area Geopolitica and Quantidade Fisica vale durante Posicao Temporal
No TPTP formula. May not be expressible in strict first order.	Food.kif 2876-2882	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de AnimalFat Objeto e' uma sub-classe de Tecido Gorduroso initialPart Objeto and Animal
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4629-4634	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de CoffeeBean Objeto e' uma sub-classe de Seed initialPart Objeto and CoffeePlant
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4693-4699	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de CocoaBean Objeto e' uma sub-classe de Seed initialPart Objeto and CocoaTree
No TPTP formula. May not be expressible in strict first order.	Media.kif 195-200	Obter e' igual a ReceivingAnObjectFn Objeto Obter e' igual a ReceivingAnObjectFn Objeto Objeto e' uma sub-classe de Objeto Obter e' uma sub-classe de Obter
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18401-18406	Organizacao e' igual a DepartmentOfPreventingFn Organizacao and Fisico Fisico e' uma sub-classe de Processo Organizacao e' uma parte da organizacao Organizacao Organizacao inhibe Fisico
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4945-4950	Objeto e' igual a OrganicObjectFn Objeto Organico Objeto e' uma sub-classe de Carne Objeto Organico e' uma sub-classe de Animal
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4166-4172	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de Malt Objeto e' uma sub-classe de CerealGrain initialPart Objeto and CerealGrass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4532-4543	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de OilFromPlant Objeto e' uma sub-classe de Seed Objeto e' uma sub-classe de Fruit Objeto Objeto e' uma sub-classe de Planta Florindo initialPart Objeto and Objeto

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 31387-31394	applicableRelation Objeto and Relacao Objeto e' uma instancia de ObjetoC o argumento numero 1 de Relacao e' uma instancia de Classe ObjetoC e' igual a Classe ObjetoC e' uma sub-classe de Classe
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1478-1491	DutyFree e' um atributo de Objeto Objeto e' uma instancia de Store Area Geopolitica Entidade, Objeto and Processo Area Geopolitica e' uma instancia de Area Geopolitica Objeto e' situado em Area Geopolitica Objeto e' uma sub-classe de Objeto importCommodityType Area Geopolitica and Objeto Entidade e' uma instancia de Objeto Processo e' uma instancia de Vender Entidade e' um patient de Processo Processo e' situado em Objeto
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 24236-24246	birthdate Humano and Dia Dia e' uma instancia de o dia Inteiro positivo Dia Numero Inteiro birthday Humano and Dia Dia e' uma sub-classe de Dia Numero Inteiro e' uma instancia de Numero Inteiro Dia e' igual a o dia Inteiro positivo Numero Inteiro e' maior que Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Merge.kif 221-227	O argumento numero Inteiro positivo de Relacao e' uma instancia de Classe o argumento numero Inteiro positivo de Relacao e' uma instancia de Classe Classe e' uma sub-classe de Classe Classe e' uma sub-classe de Classe
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3005-3010	O argumento numero Inteiro positivo de Relacao e' uma sub-classe de Classe Relacao e' uma instancia de Predicado Relacao @ROW Inteiro positivoth elemento de (@ROW) e' uma sub-classe de Classe
No TPTP formula. May not be expressible in strict first order.	Merge.kif 244-250	O argumento numero Inteiro positivo de Relacao e' uma sub-classe de Classe o argumento numero Inteiro positivo de Relacao e' uma sub-classe de Classe Classe e' uma sub-classe de Classe Classe e' uma sub-classe de Classe
No TPTP formula. May not be expressible in strict first order.	Media.kif 195-200	Obter e' igual a ReceivingAnObjectFn Objeto Obter e' igual a ReceivingAnObjectFn Objeto Objeto e' uma sub-classe de Objeto Obter e' uma sub-classe de Obter
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4945-4950	Objeto e' igual a OrganicObjectFn Objeto Organico Objeto e' uma sub-classe de Carne Objeto Organico e' uma sub-classe de Animal
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4532-4543	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de OilFromPlant Objeto e' uma sub-classe de Seed Objeto e' uma sub-classe de Fruit Objeto Objeto e' uma sub-classe de Planta Florindo initialPart Objeto and Objeto
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5258-5265	Objeto e' igual a OrganicObjectFn Objeto Organico Objeto e' uma sub-classe de Objeto Objeto Organico e' uma sub-classe de Organismo Objeto Organico e' uma sub-classe de Estructura Anatomica
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5032-5036	Objeto e' igual a OrganicObjectFn Objeto Organico Objeto e' uma sub-classe de Pelt Objeto Organico e' uma sub-classe de Skin
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5235-5244	Objeto e' igual a OrganicObjectFn Objeto Objeto e' uma sub-classe de WoodProduct Objeto e' uma sub-classe de PlantStem Objeto Objeto e' uma sub-classe de BotanicalTree initialPart Objeto and Objeto
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1780-1788	Objeto e' igual a AttrFn Objeto and Atributo Objeto e' uma instancia de Objeto Objeto e' uma instancia de Objeto Objeto e' uma sub-classe de Objeto Atributo e' um atributo de Objeto
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3840-3845	Objeto e' uma instancia de AegilopsGrass Objeto e' uma &parte de Objeto Objeto e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de DiploidCell
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3963-3968	Objeto e' uma instancia de CommonWheatGrass ObjetoELL e' uma &parte de Objeto ObjetoELL e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de HexaploidCell
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3993-3998	Objeto e' uma instancia de SpeltWheatGrass ObjetoELL e' uma &parte de Objeto ObjetoELL e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de HexaploidCell
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12014-12026	Processo e' uma instancia de Deciding Processo e' um agente de Agente Cognitivo Conjunto e' uma instancia de Conjunto Conjunto e' um patient de Processo Entidade e' um elemento de Conjunto Agente Cognitivo acredita que Entidade Entidade e' uma instancia de Entidade Entidade e' uma sub-classe de Processo Intencional Agente Cognitivo e' capaz de fazer Entidade no role agent
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3904-3909	Objeto e' uma instancia de DurumWheatGrass Objeto e' uma &parte de Objeto Objeto e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de TetraploidCell
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3934-3939	Objeto e' uma instancia de EinkornWheatGrass Objeto e' uma &parte de Objeto Objeto e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de DiploidCell
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3872-3877	Objeto e' uma instancia de EmmerWheatGrass Objeto e' uma &parte de Objeto Objeto e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de TetraploidCell
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3948-3953	Objeto e' uma instancia de TriticumUrartu Objeto e' uma &parte de Objeto Objeto e' uma instancia de ObjetoLASS ObjetoLASS e' uma sub-classe de DiploidCell
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5485-5493	Processo e' uma instancia de Felling Entidade e' o resultado de Processo EntidadeTEM Entidade e' uma instancia de DeadFn EntidadeTEM EntidadeTEM e' uma sub-classe de PlantStem
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18084-18092	Processo e' uma instancia de Harvesting Entidade e' o resultado de Processo EntidadeRG Entidade e' uma instancia de DeadFn EntidadeRG EntidadeRG e' uma sub-classe de Objeto Organico
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3447-3476	WearableItem e' uma instancia de HearingProtection Animal e' uma instancia de Humano Animal usa WearableItem WearableItem tem por fim Entidade Entidade and Entidade Entidade e' uma instancia de Processo Entidade e' uma sub-classe de a classe descrita por Entidade Entidade proibe a ocurrencia de Entidade WearableItem e' um instrumento para Entidade
No TPTP formula. May not be expressible in strict first order.	Dining.kif 219-223	Catalog e' uma instancia de AlcoholMenu catalogItem Entidade and Catalog Entidade e' uma sub-classe de AlcoholicBeverage

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

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: