No TPTP formula. May not be expressible in strict first order. | Merge.kif 15790-15790 | 永久居留权 是 住宅 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15820-15820 | 单身家庭住所 是 永久居留权 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Government.kif 1538-1538 | 行政住所 是 永久居留权 的 subclass |