| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9043-9043 | Month is a subclass of time interval |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9048-9048 | January is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9062-9062 | February is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9086-9086 | March is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9100-9100 | April is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9114-9114 | May is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9128-9128 | June is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9142-9142 | July is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9156-9156 | August is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9170-9170 | September is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9185-9185 | October is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9199-9199 | November is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9213-9213 | December is a subclass of month |
|
|