No TPTP formula. May not be expressible in strict first order. | Merge.kif 15790-15790 | 子類 永久居留權 and 住宅 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15820-15820 | 子類 單身家庭住所 and 永久居留權 |
No TPTP formula. May not be expressible in strict first order. | Government.kif 1538-1538 | 子類 行政住所 and 永久居留權 |