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 |
O argumento numero 1 de preventsSubclass e' uma sub-classe de Processo |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4338-4338 |
O argumento numero 2 de preventsSubclass e' uma sub-classe de Processo |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4334-4334 |
preventsSubclass e' uma instancia de Predicado Binario |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4335-4335 |
preventsSubclass e' uma instancia de Relacao Irreflexiva |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4336-4336 |
preventsSubclass e' uma instancia de Relacao Parcial |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4339-4339 |
preventsSubclass e' relacionado internamente por SUMO a hindersSubclass |