|
|
   RealNumber
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1737-1738 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1895-1897 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 345-346 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11735-11735 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10223-10223 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11734-11734 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | O conceito Numero Real e' completamente decomposto em Numero Real negativo + Numero Real nao-negativo |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1893-1893 | O conceito Numero Real e' completamente decomposto em Numero Racional + Numero Irracional |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | Numero Real e' uma sub-classe de Numero |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2009-2009 | Numero Complexo e' disjunto de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1825-1825 | O conceito Numero e' completamente decomposto em Numero Real, Numero Imaginario, + Numero Complexo |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4714-4714 | O contra-dominio de AdditionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5260-5260 | O contra-dominio de ArcCosineFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5270-5270 | O contra-dominio de ArcSineFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5250-5250 | O contra-dominio de ArcTangentFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3272-3272 | O contra-dominio de AverageFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 71-71 | O contra-dominio de BirthsPerThousandFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 443-443 | O contra-dominio de ChildrenBornPerWomanFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3331-3331 | O contra-dominio de ClickThroughRateFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4802-4802 | O contra-dominio de CosineFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 104-104 | O contra-dominio de DeathsPerThousandFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 230-230 | O contra-dominio de DeathsPerThousandLiveBirthsFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4744-4744 | O contra-dominio de DivisionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4821-4821 | O contra-dominio de ExponentiationFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 396-396 | O contra-dominio de FemaleLifeExpectancyAtBirthFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 299-299 | O contra-dominio de LifeExpectancyAtBirthFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4555-4555 | O contra-dominio de LiftFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3241-3241 | O contra-dominio de ListSumFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4977-4977 | O contra-dominio de LogFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 348-348 | O contra-dominio de MaleLifeExpectancyAtBirthFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 193-193 | O contra-dominio de MaleToFemaleRatioFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | People.kif 140-140 | O contra-dominio de MigrantsPerThousandFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4701-4701 | O contra-dominio de MultiplicationFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3088-3088 | O contra-dominio de PPIFn e' uma instancia de Numero Real |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4762-4762 | O argumento numero 1 de AbsoluteValueFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4712-4712 | O argumento numero 1 de AdditionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4713-4713 | O argumento numero 2 de AdditionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5259-5259 | O argumento numero 1 de ArcCosineFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5269-5269 | O argumento numero 1 de ArcSineFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5249-5249 | O argumento numero 1 de ArcTangentFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4783-4783 | O argumento numero 1 de CeilingFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4810-4810 | O argumento numero 1 de DenominatorFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4742-4742 | O argumento numero 1 de DivisionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4743-4743 | O argumento numero 2 de DivisionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4819-4819 | O argumento numero 1 de ExponentiationFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4828-4828 | O argumento numero 1 de FloorFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4923-4923 | O argumento numero 1 de IntegerSquareRootFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4975-4975 | O argumento numero 1 de LogFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6348-6348 | O argumento numero 1 de MeasureFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4699-4699 | O argumento numero 1 de MultiplicationFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4700-4700 | O argumento numero 2 de MultiplicationFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5036-5036 | O argumento numero 1 de NumeratorFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | O argumento numero 1 de ReciprocalFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5170-5170 | O argumento numero 1 de RoundFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5189-5189 | O argumento numero 1 de SignumFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5211-5211 | O argumento numero 1 de SineFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5219-5219 | O argumento numero 1 de SquareRootFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | O argumento numero 1 de SubtractionFn e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | O argumento numero 2 de SubtractionFn e' uma instancia de Numero Real |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | Numero Real e' uma instancia de Numero Real negativo Numero Real e' menos que 0 Numero Real e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1926-1930 | Numero Real e' uma instancia de Numero Real nao-negativo Numero Real e' maior ou igual a 0 Numero Real e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1937-1941 | Numero Real e' uma instancia de Numero Real positivo Numero Real e' maior que 0 Numero Real e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 |
|
| No TPTP formula. May not be expressible in strict first order. | Food.kif 770-781 |
|
|
|
|
