No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3714-3715 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16735-16736 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16732-16732 |
The number 1 argument of husband is an instance of man |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16733-16733 |
The number 2 argument of husband is an instance of woman |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16728-16728 |
husband is an instance of asymmetric relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16729-16729 |
husband is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16730-16730 |
husband is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16731-16731 |
husband is an instance of partial valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16734-16734 |
husband is an inverse of wife |