![]() |
![]() ![]()
|
![]() |
|
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2619-2619 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7288-7288 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4420-4420 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4419-4419 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4418-4418 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7287-7287 | United states dollar is an instance of UnitOfCurrency |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2951-2951 | United states dollar is a currency value of united states dollar bill |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60347-60347 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60346-60346 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60345-60345 |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2302-2302 | "USD" in ISO-4217-A denotes united states dollar |
consequent |
![]() |
statement |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7295-7297 | A real number united states cent(s) is equal to the real number and 0.01 united states dollar(s) |
![]() |
![]() |