|
|
   NonnegativeRealNumber
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1745-1745 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1923-1924 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 353-353 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11508-11508 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10149-10149 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1921-1921 | Nombre r�el non n�gatif est une sous-classe de nombre r�el |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4763-4763 | Le domaine de AbsoluteValueFn est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1976-1976 | Nombre entier non n�gatif est une sous-classe de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1932-1932 | Nombre r�el positif est une sous-classe de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 863-863 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 928-928 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 539-539 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 69-69 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 72-72 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2224-2224 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 491-491 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 106-106 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 560-560 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 73-73 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 871-871 | Le nombre 2 argument de cloudCoverFraction est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1306-1306 | Le nombre 2 argument de incomeDistributionByGiniIndex est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1291-1291 | Le nombre 2 argument de incomeDistributionByGiniIndexInPeriod est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1366-1366 | Le nombre 2 argument de laborForceTotal est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1356-1356 | Le nombre 2 argument de laborForceTotalInPeriod est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 954-954 | Le nombre 3 argument de overcastDaysInPeriod est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1024-1024 | Le nombre 2 argument de relativeHumidity est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1675-1675 | Le nombre 2 argument de slopeGradient est une instance de nombre r�el non n�gatif |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | Nombre r�el est compl�tement d�compos� en nombre r�el n�gatif + nombre r�el non n�gatif |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1926-1930 | Nombre r�el est une instance de nombre r�el non n�gatif nombre r�el est plus grand ou �gal � 0 nombre r�el est une instance de nombre r�el |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5195-5199 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | La valeur absolue de nombre r�el est nombre r�el non n�gatif nombre r�el est une instance de nombre r�el nombre r�el non n�gatif est une instance de nombre r�el nombre r�el est une instance de nombre r�el non n�gatif nombre r�el est nombre r�el non n�gatif nombre r�el est une instance de nombre r�el n�gatif nombre r�el non n�gatif est nombre r�el) |
|
|
|
