| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9065-9065 | Month is a subclass of time interval |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9070-9070 | January is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9084-9084 | February is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9108-9108 | March is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9122-9122 | April is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9136-9136 | May is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9150-9150 | June is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9164-9164 | July is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9178-9178 | August is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9192-9192 | September is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9207-9207 | October is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9221-9221 | November is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9235-9235 | December is a subclass of month |
|
|