domain |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1380-1385 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 205-213 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 38-44 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 40-48 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 202-202 | The number 1 argument of domain is an instance of relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 203-203 | The number 2 argument of domain is an instance of positive integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 204-204 | The number 3 argument of domain is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 201-201 | domain is an instance of ternary predicate |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 291-291 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 296-296 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 168-168 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 82-82 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1988-1988 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 120-120 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 177-177 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 378-378 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 122-122 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 188-188 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 175-175 | |
No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 116-116 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20127-20127 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 292-292 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20126-20126 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20125-20125 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 118-118 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 180-180 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 33091-33098 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2996-3001 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 215-221 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 412-417 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18312-18316 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 180-184 |
|
consequent |
![]() |
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3225-3225 | The number 1 argument of average buying price is an instance of collection |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3270-3270 | The number 1 argument of average buying price is an instance of collection |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2411-2411 | The number 1 argument of aborted is an instance of agent |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2412-2412 | The number 2 argument of aborted is an instance of process |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2510-2510 | The number 1 argument of aborted launch is an instance of agent |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2511-2511 | The number 2 argument of aborted launch is an instance of taking off |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2431-2431 | The number 1 argument of aborted mission is an instance of agent |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2432-2432 | The number 2 argument of aborted mission is an instance of military operation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4775-4775 | The number 1 argument of absolute value is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1274-1274 | The number 1 argument of Acceleration fn is an instance of function quantity |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1275-1275 | The number 2 argument of Acceleration fn is an instance of time duration |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1276-1276 | The number 3 argument of Acceleration fn is an instance of object |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1277-1277 | The number 4 argument of Acceleration fn is an instance of directional attribute |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2333-2333 | The number 1 argument of account is an instance of financial asset |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4725-4725 | The number 1 argument of addition is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | The number 2 argument of addition is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 224-224 | The number 1 argument of address is an instance of computer file |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8932-8932 | The number 1 argument of afternoon of is an instance of day |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3044-3044 | The number 1 argument of agreement organization is an instance of agreement |
No TPTP formula. May not be expressible in strict first order. | Music.kif 932-932 | The number 1 argument of album copies function is an instance of album |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7613-7613 | The number 2 argument of Amounts fn is an instance of corpuscular object |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7614-7614 | The number 3 argument of Amounts fn is an instance of unit of mass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5272-5272 | The number 1 argument of arccosine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5282-5282 | The number 1 argument of arcsine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5262-5262 | The number 1 argument of arctangent is an instance of real number |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |