No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2472-2475 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6614-6618 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1165-1168 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6611-6611 |
The number 1 argument of unit fn is an instance of physical quantity |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6610-6610 |
Unit fn is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6609-6609 |
Unit fn is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6612-6612 |
The range of unit fn is an instance of unit of measure |