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 6639-6643 |
|
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 6636-6636 |
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 6635-6635 |
Unit fn is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6634-6634 |
Unit fn is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6637-6637 |
The range of unit fn is an instance of unit of measure |