| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9330-9330 | Domingo e' uma sub-classe de Dia |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 311-311 | AdventSunday e' uma sub-classe de Domingo |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 460-460 | PalmSunday e' uma sub-classe de Domingo |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 485-485 | EasterSunday e' uma sub-classe de Domingo |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 551-551 | Pentecost e' uma sub-classe de Domingo |
|
|