No TPTP formula. May not be expressible in strict first order. |
Merge.kif 784-784 |
Assignment is an instance of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4844-4844 |
Greatest common divisor is an instance of function |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 405-405 |
Latitude is an instance of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4929-4929 |
Least common multiple is an instance of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2931-2931 |
List is an instance of function |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 442-442 |
Longitude is an instance of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3398-3398 |
Binary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3472-3472 |
Continuous function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3461-3461 |
Quaternary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3450-3450 |
Ternary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3358-3358 |
Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 916-916 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1039-1039 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 592-592 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 122-122 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 125-125 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2277-2277 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 544-544 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 127-127 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 159-159 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 613-613 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 126-126 |
|