No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4014-4014 |
deprives norm and confers norm are disjoint |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2105-2106 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4019-4021 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 756-757 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4015-4015 |
The number 1 argument of deprives norm is an instance of entity |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4016-4016 |
The number 2 argument of deprives norm is an instance of formula |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4017-4017 |
The number 3 argument of deprives norm is an instance of objective norm |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4013-4013 |
deprives norm is an instance of ternary predicate |