No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4014-4014 |
剥夺了规范 和 赋予规范 是 disjoint 关系 |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2105-2106 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4019-4021 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 756-757 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4015-4015 |
剥夺了规范 的 1 数量 是 实体 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4016-4016 |
剥夺了规范 的 2 数量 是 公式 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4017-4017 |
剥夺了规范 的 3 数量 是 客观标准 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4013-4013 |
剥夺了规范 是 三元谓语 的 instance |