No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2143-2147 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4341-4346 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 799-803 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4337-4337 |
Le nombre 1 argument de preventsSubclass est une sous-classe de processus |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4338-4338 |
Le nombre 2 argument de preventsSubclass est une sous-classe de processus |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4334-4334 |
preventsSubclass est une instance de pr�dicat binaire |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4335-4335 |
preventsSubclass est une instance de relation irr�flexive |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4336-4336 |
preventsSubclass est une instance de relation partielle |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4339-4339 |
preventsSubclass est reli� � l'int�rieur de SUMO � hindersSubclass |