| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9065-9065 | 子類 Month and TimeInterval |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9070-9070 | 子類 January and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9084-9084 | 子類 February and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9108-9108 | 子類 March and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9122-9122 | 子類 April and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9136-9136 | 子類 May and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9150-9150 | 子類 June and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9164-9164 | 子類 July and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9178-9178 | 子類 August and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9192-9192 | 子類 September and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9207-9207 | 子類 October and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9221-9221 | 子類 November and Month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9235-9235 | 子類 December and Month |
|
|