appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3401-3401 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14508-14508 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 204-204 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14507-14507 | Worm is a subclass of invertebrate |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14504-14504 | Invertebrate is disjointly decomposed into worm, mollusk, and arthropod |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14510-14510 | Leech is a subclass of worm |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 978-978 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1163-1163 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 655-655 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 186-186 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 189-189 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2339-2339 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 607-607 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 191-191 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 223-223 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 676-676 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 190-190 |