No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4536-4536 |
The number 1 argument of addition is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4537-4537 |
The number 2 argument of addition is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4566-4566 |
The number 1 argument of division is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4567-4567 |
The number 2 argument of division is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4788-4788 |
The number 1 argument of max is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4789-4789 |
The number 2 argument of max is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4814-4814 |
The number 1 argument of min is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4815-4815 |
The number 2 argument of min is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4523-4523 |
The number 1 argument of multiplication is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4524-4524 |
The number 2 argument of multiplication is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4855-4855 |
The number 1 argument of rational number is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4862-4862 |
The number 1 argument of real number is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4550-4550 |
The number 1 argument of subtraction is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4551-4551 |
The number 2 argument of subtraction is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 1445-1445 |
The number 1 argument of variance average function is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 576-576 |
The number 3 argument of current interest rate is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 582-582 |
The number 2 argument of fixed interest rate is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 545-545 |
The number 2 argument of interest rate per period is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 3265-3265 |
The number 2 argument of passenger capacity max number is an instance of number |
No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 561-561 |
The number 2 argument of prime interest rate is an instance of number |