No TPTP formula. May not be expressible in strict first order. | Economy.kif 1980-1989 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3738-3742 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2288-2295 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2583-2592 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2594-2601 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2156-2165 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2112-2121 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2167-2174 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1991-1998 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2202-2211 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2277-2286 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2123-2130 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2213-2220 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8738-8738 | 年 是 时距 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8995-8995 | 闰年 是 年 的 subclass |