| LeapYear(leap year)
| | 366_days, bissextile_year, intercalary_year, leap_year |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2791-2792 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8997-8999 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1530-1532 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 7181-7181 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8995-8995 | Leap year is a subclass of year |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1275-1275 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1767-1767 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 953-953 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 488-488 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 492-492 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2637-2637 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 905-905 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 528-528 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 974-974 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 493-493 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9001-9009 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9073-9078 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9066-9071 |
|
|
|
|