| Counting(counting)
| | CBC, blood_count, blood_profile, census, chalk_up, circulation, complete_blood_count, count, count_down, count_off, countdown, counting, differential_blood_count, enumerate, enumeration, foliate, itemise, itemize, list, miscount, nose_count, nosecount, number, numerate, numeration, page, paginate, poll, pollen_count, recite, reckoning, recount, sperm_count, tally |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3135-3136 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12132-12134 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 5937-5937 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12131-12131 | Counting is a subclass of calculating |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1151-1151 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1519-1519 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 829-829 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 361-361 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 364-364 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2513-2513 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 781-781 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 366-366 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 400-400 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 850-850 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 365-365 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12136-12142 |
|
|
|
|