spouse |
appearance as argument number 1 |
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 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4594-4594 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4593-4593 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4592-4592 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54798-54798 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54797-54797 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54796-54796 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23152-23159 | 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 23169-23176 | 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 1426-1431 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1415-1420 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22307-22321 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1025-1034 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7965-7970 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14170-14176 |
|