No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4013-4013 |
deprivesNorm et confersNorm sont 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 4018-4020 |
|
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 4014-4014 |
Le nombre 1 argument de deprivesNorm est une instance de entit� |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4015-4015 |
Le nombre 2 argument de deprivesNorm est une instance de formule |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4016-4016 |
Le nombre 3 argument de deprivesNorm est une instance de norme objective |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4012-4012 |
deprivesNorm est une instance de pr�dicat ternaire |