AOCnumber |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3170-3172 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3169-3169 | AOCnumber 是 符号串 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3173-3173 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3188-3198 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3175-3177 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3179-3186 |