RemainderFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2267-2268 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5100-5102 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 932-933 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5096-5096 | 余函数 的 1 数量 是 整数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5097-5097 | 余函数 的 2 数量 是 整数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5093-5093 | 余函数 是 二元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5095-5095 | 余函数 是 部分值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5098-5098 | 余函数 的 range 是 整数 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 722-722 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 724-724 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 434-434 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 252-252 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2151-2151 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 386-386 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 446-446 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 935-935 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 289-289 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 456-456 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 496-496 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 723-723 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49442-49442 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49441-49441 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49440-49440 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5130-5142 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5104-5115 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4861-4872 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4874-4888 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4946-4956 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4958-4972 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9001-9009 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5117-5128 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5144-5147 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5149-5152 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5154-5165 |