![]() |
![]() ![]()
|
![]() |
|
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2528-2529 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6841-6843 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1229-1230 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6839-6839 | Hertz is an instance of systeme international unit |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6838-6838 | Hertz is an instance of unit of frequency |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28047-28047 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28046-28046 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28045-28045 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1570-1577 |
|
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1579-1588 |
|
![]() |
![]() |