| No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 1925-1925 |
例 問價格 and TernaryRelation |
| No TPTP formula. May not be expressible in strict first order. |
Music.kif 1493-1493 |
例 releaseForSale and TernaryRelation |
| No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 4549-4549 |
例 securityQA and TernaryRelation |
| No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 3304-3304 |
例 稅收遞延收入 and TernaryRelation |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3399-3399 |
子類 BinaryFunction and TernaryRelation |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3490-3490 |
子類 TernaryPredicate and TernaryRelation |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 910-910 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1027-1027 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 586-586 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 116-116 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 119-119 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2271-2271 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 538-538 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 153-153 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 607-607 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 120-120 |
|
TernaryRelation