July
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2801-2801 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9144-9144 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1542-1542 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4917-4917 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9142-9142 | July is a subclass of month |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9030-9030 | August is the successor class of July. |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9029-9029 | July is the successor class of June. |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1283-1283 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1783-1783 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 961-961 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 496-496 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 500-500 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2645-2645 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 913-913 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 502-502 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 536-536 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 982-982 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 501-501 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9150-9154 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9136-9140 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9146-9148 |
|
statement |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4285-4285 | The day 1 is a date dissolved of warsaw pact |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2928-2928 | The day 4 is a date established of caribbean community and common market |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3239-3239 | The day 1 is a date established of european organization for nuclear research |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3414-3414 | The day 22 is a date established of international bank for reconstruction and development |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3567-3567 | The day 22 is a date established of international monetary fund |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3817-3817 | The day 29 is a date established of permanent court of arbitration |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4081-4081 | The day 31 is a date established of united nations mission in ethiopia and eritrea |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4136-4136 | The month July is a date established of united nations population fund |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4290-4290 | The day 12 is a date established of wassenaar arrangement |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4350-4350 | The day 22 is a date established of world health organization |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4356-4356 | The day 14 is a date established of world intellectual property organization |