| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16984-16984 |
假 是 真值 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16981-16981 |
真正 是 真值 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1235-1235 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1691-1691 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 913-913 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 446-446 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 449-449 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2597-2597 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 865-865 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 451-451 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 485-485 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 934-934 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 450-450 |
|
