| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9043-9043 | 月 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9048-9048 | 一月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9062-9062 | 二月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9086-9086 | 三月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9100-9100 | A四月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9114-9114 | 五月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9128-9128 | 六月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9142-9142 | 七月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9156-9156 | 八月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9170-9170 | 九月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9185-9185 | 十月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9199-9199 | 十一月 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9213-9213 | 十二月 是 月 的 subclass |
|
|