No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23373-23373 |
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 16564-16565 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16562-16562 |
The number 1 argument of spouse is an instance of human |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16563-16563 |
The number 2 argument of spouse is an instance of human |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16559-16559 |
spouse is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16561-16561 |
spouse is an instance of partial valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16560-16560 |
spouse is an instance of symmetric relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16558-16558 |
spouse is a subrelation of legal relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16556-16556 |
spouse is a subrelation of mutual acquaintance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16322-16322 |
spouse is a subrelation of relative |