equal |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1391-1392 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 48-49 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 53-54 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 297-297 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 302-302 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 171-171 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 96-96 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1991-1991 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 123-123 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 179-179 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 387-387 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 136-136 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 191-191 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 178-178 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 205-205 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 298-298 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22317-22317 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22316-22316 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 206-206 |
antecedent |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | People.kif 456-469 | Ano e' uma instancia de o ano Numero Inteiro ChildrenBornPerWomanFn Area Geopolitica and Ano 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. | Military.kif 933-946 | ReachingMilitaryAgeAnnuallyMaleFn Area Geopolitica and Ano 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. | Mid-level-ontology.kif 13333-13336 | Numero Real Numero Real OunceMass(s) e' igual a Numero Real + 16.0 PoundMass(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4736-4737 | Numero Inteiro ( Numero Inteiro+2) e' igual a ( Numero Inteiro + 1) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4720-4721 | Numero Inteiro ( Numero Inteiro+1) e' igual a ( Numero Inteiro + 1) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3037-3040 | @ROW Entidade comprimento de (@ROW + Entidade) e' igual a (comprimento de (@ROW)+1) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3042-3046 | @ROW Entidade comprimento de (@ROW + Entidade)th elemento de (@ROW + Entidade) e' igual a Entidade |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2915-2915 | BigSix e' igual a GroupOf6 |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5265-5265 | ArcCosineFn o coseno de Numero Real e' igual a Numero Real |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5275-5275 | ArcSineFn o seno de Numero Real e' igual a Numero Real |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5255-5255 | ArcTangentFn a tangente de Numero Real e' igual a Numero Real |
No TPTP formula. May not be expressible in strict first order. | Military.kif 872-881 | AvailableForMilitaryServiceMaleFn 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. | Merge.kif 14182-14182 | O numero de instancias dentro de Continente e' igual a 7 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2003-2003 | O numero de instancias dentro de NativityMagi e' igual a 3 |
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. | Economy.kif 2008-2008 | 1 KilowattHour(s) e' igual a 3.6 1 milhao Joules(s) |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2009-2009 | 1 KilowattHour(s) e' igual a 3600000.0 Joule(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7112-7114 | 1 WeekDuration(s) e' igual a 7 DayDuration(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7139-7141 | 1 YearDuration(s) e' igual a 365 DayDuration(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 382-382 | 1.0 AngularDegree(s) e' igual a 60.0 ArcMinute(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 401-401 | 1.0 ArcMinute(s) e' igual a 60.0 ArcSecond(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3842-3842 | 1.0 Fathom(s) e' igual a 6.0 FootLength(s) |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13601-13603 | 1.0 MetricTon(s) e' igual a 2205.0 PoundMass(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3865-3867 | 1.0 NauticalMile(s) e' igual a 1852.0 Meter(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3861-3863 | 1.0 NauticalMile(s) e' igual a 6076.1 FootLength(s) |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13696-13700 | 1.0 SquareMile(s) e' igual a PerFn 1.0 Mile(s) and 1.0 Mile(s) |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13706-13710 | 1.0 SquareYard(s) e' igual a PerFn 1.0 YardLength(s) and 1.0 YardLength(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 402-402 | Numero Real ArcMinute(s) e' igual a 60.0 + Numero Real ArcSecond(s) |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 383-383 | Numero Real AngularDegree(s) e' igual a 60.0 + Numero Real ArcMinute(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7151-7153 | Numero Real Amu(s) e' igual a Numero Real + 1.6605402E-24 Gram(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7173-7175 | Numero Real Angstrom(s) e' igual a Numero Real + 1.0E-10 Meter(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7367-7369 | Numero Real AngularDegree(s) e' igual a Numero Real + Pi + 180.0 Radian(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7353-7355 | Numero Real BritishThermalUnit(s) e' igual a Numero Real + 1055.05585262 Joule(s) |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |