spouse |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25014-25014 | spouse and domestic partner are disjoint |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3713-3713 | spouse and domestic partner are disjoint |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16739-16740 | spouse and domestic partner are disjoint |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16737-16737 | The number 1 argument of spouse is an instance of human |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16738-16738 | The number 2 argument of spouse is an instance of human |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16734-16734 | spouse is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16736-16736 | spouse is an instance of partial valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16735-16735 | spouse is an instance of symmetric relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16733-16733 | spouse is a subrelation of legal relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16731-16731 | spouse is a subrelation of mutual acquaintance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16497-16497 | spouse is a subrelation of relative |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4598-4598 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4597-4597 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4596-4596 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54802-54802 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54801-54801 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54800-54800 |
antecedent |
![]() |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24793-24800 | A man is the stepfather of a human if and only if there exists another human such that the other human is a mother of the human and the man is the spouse of the other human and the man is not a father of the human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24810-24817 | A woman is the stepfather of a human if and only if there exists another human such that the other human is a father of the human and the woman is the spouse of the other human and the woman is not a mother of the human |
No TPTP formula. May not be expressible in strict first order. | Government.kif 1388-1393 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1377-1382 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23948-23962 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1018-1027 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9132-9137 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15541-15547 |
|
![]() |
![]() |