appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2781-2781 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8742-8742 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1511-1511 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8740-8740 | Year is internally related to year duration |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8739-8739 | Year is internally related to year |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8738-8738 | Year is a subclass of time interval |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8556-8556 | The values returned by year are subclasses of year |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8995-8995 | Leap year is a subclass of year |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1274-1274 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 63756-63756 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1765-1765 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 952-952 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 487-487 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 491-491 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2636-2636 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 904-904 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 527-527 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 973-973 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 492-492 |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | People.kif 96-96 | The number 2 argument of births per thousand is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 468-468 | The number 2 argument of children born per woman is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 129-129 | The number 2 argument of deaths per thousand is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 255-255 | The number 2 argument of deaths per thousand live births is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 421-421 | The number 2 argument of female life expectancy at birth is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 324-324 | The number 2 argument of life expectancy at birth is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 373-373 | The number 2 argument of male life expectancy at birth is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 165-165 | The number 2 argument of migrants per thousand is an instance of year |
No TPTP formula. May not be expressible in strict first order. | People.kif 63-63 | The number 2 argument of population growth is an instance of year |
No TPTP formula. May not be expressible in strict first order. | Military.kif 925-925 | The number 2 argument of reaching military age annually male is an instance of year |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3740-3740 | The number 2 argument of fiscal year starting is a subclass of year |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8572-8572 | The number 2 argument of month is a subclass of year |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8969-8969 | The number 2 argument of quarter fn is a subclass of year |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8951-8951 | The number 2 argument of week fn is a subclass of year |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 744-744 | The number 2 argument of last renovation is a subclass of year |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 723-723 | The number 2 argument of year built is a subclass of year |
antecedent |
![]() |
consequent |
![]() |
![]() |
![]() |