No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23372-23372 |
spouse and domestic partner are disjoint |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3713-3713 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16586-16587 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16584-16584 |
The number 1 argument of spouse is an instance of human |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16585-16585 |
The number 2 argument of spouse is an instance of human |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16581-16581 |
spouse is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16583-16583 |
spouse is an instance of partial valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16582-16582 |
spouse is an instance of symmetric relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16580-16580 |
spouse is a subrelation of legal relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16578-16578 |
spouse is a subrelation of mutual acquaintance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16344-16344 |
spouse is a subrelation of relative |