No TPTP formula. May not be expressible in strict first order. | Merge.kif 2310-2310 | 子類 TrichotomizingRelation and BinaryRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2375-2375 | 子類 TotalOrderingRelation and TrichotomizingRelation |