TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2745-2746
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8567-8569
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1471-1472
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8564-8564	紧接未来函数的 1 数量是时间位置的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8561-8561	紧接未来函数是时间关系的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8563-8563	紧接未来函数是总值关系的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8562-8562	紧接未来函数是一元函数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8565-8565	紧接未来函数的 range 是时距的实例

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 463-463
No TPTP formula. May not be expressible in strict first order.	english_format.kif 469-469
No TPTP formula. May not be expressible in strict first order.	french_format.kif 268-268
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 137-137
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2058-2058
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 220-220
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 274-274
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 605-605
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 176-176
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 289-289
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 295-295
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 278-278
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 29349-29349
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 464-464
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 29348-29348
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 29347-29347
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 279-279

antecedent

No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3231-3245	如果啟動中是工程组件的 attribute 在物理 holdsDuring 和准备好主持是那个工程组件的 attribute 在那个物理2 holdsDuring 和那个物理2 equal 紧接那个物理出现的 time after 和另一个工程组件是 ComputerDisplay 的 instance 和那个另外工程组件是和那个工程组件 connected，然后有存在实体这样那个实体是主頁面的 instance 和那个实体是在那个另外工程组件 displayed 的声明 has 容易的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 9866-9888	如果客体是 Antacid 的 instance 和运动是消化的 instance 和施事体是那个运动的 agent 和移动那个运动 and 那个客体和另一个客体是胃的 instance 和那个另外客体是那个施事体的 part 和那个另外客体 contains 第三客体和那个第三客体是流体的 instance 在紧接那个运动出现的 time before holdsDuring 和那个另外客体 contains 第四客体和那个第四客体是流体的 instance 在紧接那个运动出现的 time after holdsDuring 和 phMeasure 那个第三客体 and 实数和 phMeasure 那个第四客体 and 另一个实数，然后那个另外实数是 greaterThan 那个实数
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 9927-9949	如果客体是 ProtonPumpInhibitor 的 instance 和运动是消化的 instance 和施事体是那个运动的 agent 和移动那个运动 and 那个客体和另一个客体是胃的 instance 和那个另外客体是那个施事体的 part 和那个另外客体 contains 第三客体和那个第三客体是流体的 instance 在紧接那个运动出现的 time before holdsDuring 和那个另外客体 contains 第四客体和那个第四客体是流体的 instance 在紧接那个运动出现的 time after holdsDuring 和 phMeasure 那个第三客体 and 实数和 phMeasure 那个第四客体 and 另一个实数，然后那个另外实数是 greaterThan 那个实数
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1926-1940	如果电脑程序是数据压缩的 instance 和数字数据是由那个电脑程序 processed 和那个数字数据 requires 实数实体在紧接那个电脑程序出现的 time before holdsDuring 和那个数字数据 requires 另一个实数那个实体在紧接那个电脑程序出现的 time after holdsDuring，然后那个另外实数是 lessThan 那个实数
No TPTP formula. May not be expressible in strict first order.	Geography.kif 7016-7030	如果过程是凝华的 instance 和实体是那个过程的 patient 和那个实体的 measure 是实数焦耳在紧接那个过程出现的 time before holdsDuring 和那个实体的 measure 是另一个实数焦耳在紧接那个过程出现的 time after holdsDuring，然后那个另外实数是 lessThan 那个实数
No TPTP formula. May not be expressible in strict first order.	Cars.kif 777-792	如果过程是运动的 instance 和另一个过程是震的 instance 和客体是 Damper 的 instance 和另一个客体是那个另外过程的 patient 和那个客体是那个另外客体的 part 和那个过程 causes 那个另外过程和实体是 UnitOfLength 的 instance 和 physicalAmplitude 那个另外过程 and 实数那个实体在那个过程出现的 time holdsDuring 和 physicalAmplitude 那个另外过程 and 另一个实数那个实体在紧接那个过程 after holdsDuring，然后那个实数是 greaterThan 那个另外实数
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 1328-1340	如果过程是碰撞的 instance 和实体是那个过程的 patient 和 ImpairedBodyPartFn 脑是那个实体的 attribute 在紧接那个过程 after holdsDuring，然后 Concussion 是那个实体的 attribute 在紧接那个过程 after holdsDuring 的声明 has 容易的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 1325-1348	如果客体是 Lever 的 instance 和过程是 Pushing 的 instance 和物理是运动的 instance 和测量单位是 UnitOfLength 的 instance 和那个过程在另一个客体结束和 physicalEnd 那个另外客体 and 那个客体和 physicalEnd 第三客体 and 那个客体和那个另外客体不 equal 那个第三客体和那个另外客体是 located 在那个过程1 在紧接那个物理出现的 time before holdsDuring 和那个另外客体是 located 在那个过程2 在紧接那个物理出现的 time after holdsDuring 和那个第三客体是 located 在那个过程3 在紧接那个物理出现的 time before holdsDuring 和那个第三客体是 located 在那个过程4 在紧接那个物理出现的 time after holdsDuring 和那个过程1 和那个过程2 的 distance 是实数那个测量单位和那个过程3 和那个过程4 的 distance 是另一个实数那个测量单位，然后那个另外实数是 greaterThan 那个实数
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3972-3986	如果过程是 LoggingIn 的 instance 和施事体有 account 用户帐号和那个用户帐号是在 WebSite 的 account 和时距 equal 紧接那个过程出现的 time after 和那个施事体是那个过程的 agent，然后有存在实体这样那个实体是电脑程序的 instance 和那个施事体是那个实体的 agent 和那个 WebSite 是那个实体的 patient 在那个时距 holdsDuring 的声明 has 可能性的语气
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3988-4002	如果过程是 LoggingIn 的 instance 和施事体有 account 用户帐号和 deviceAccount 那个用户帐号 and 电脑和时距 equal 紧接那个过程出现的 time after 和那个施事体是那个过程的 agent，然后有存在实体这样那个实体是电脑程序的 instance 和那个施事体是那个实体的 agent 和那个电脑是导致那个实体的 instrument 在那个时距 holdsDuring 的声明 has 可能性的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 10582-10597	如果过程是 MuscleRelaxing 的 instance 和实体是那个过程的 patient 和那个实体是肌肉的 instance 和那个实体的 length 是实数另一个实体在紧接那个过程出现的 time before holdsDuring 和那个实体的 length 是另一个实数那个另外实体在紧接那个过程出现的 time after holdsDuring，然后那个另外实数是 greaterThan 那个实数
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 10560-10575	如果过程是 MuscularContraction 的 instance 和实体是那个过程的 patient 和那个实体是肌肉的 instance 和那个实体的 length 是实数另一个实体在紧接那个过程出现的 time before holdsDuring 和那个实体的 length 是另一个实数那个另外实体在紧接那个过程出现的 time after holdsDuring，然后那个实数是 greaterThan 那个另外实数
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1970-1982	如果实体是自身连接物体的 instance 和过程是 Compressing 的 instance 和那个实体是那个过程的 patient 和那个实体的 measure 是实数另一个实体在紧接那个过程出现的 time before holdsDuring 和那个另外实体是 UnitOfVolume 的 instance 和那个实体的 measure 是另一个实数那个另外实体在紧接那个过程出现的 time after holdsDuring，然后那个实数是 greaterThan 那个另外实数
No TPTP formula. May not be expressible in strict first order.	Geography.kif 7068-7082	如果过程是升华的 instance 和实体是那个过程的 patient 和那个实体的 measure 是实数焦耳在紧接那个过程出现的 time before holdsDuring 和那个实体的 measure 是另一个实数焦耳在紧接那个过程出现的 time after holdsDuring，然后那个另外实数是 greaterThan 那个实数

consequent

No TPTP formula. May not be expressible in strict first order.	Government.kif 702-717	如果命题 agreement 对于另一个命题的修改日期有点时间位置，然后有存在另一个时间位置这样那个另外时间位置是有点时间位置的 instance 和那个另外命题不是那个命题的 subProposition 在紧接那个另外时间位置 before holdsDuring 和那个另外命题是那个命题的 subProposition 在紧接那个另外时间位置 after holdsDuring 或那个另外命题是那个命题的 subProposition 在紧接那个另外时间位置 before holdsDuring 和那个另外命题不是那个命题的 subProposition 在紧接那个另外时间位置 after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Government.kif 678-683	如果时点是协议的 agreement 生效日期和那个协议要求有认知的主事执行公式的任务和时间位置是那个时点的 instance，然后那个有认知的主事有义务执行那个公式的任务在紧接那个时间位置 after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Government.kif 685-690	如果时点是协议的 agreement 生效日期和那个协议允许有认知的主事执行公式的任务和时间位置是那个时点的 instance，然后那个有认知的主事有权利去做那个公式在紧接那个时间位置 after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 1035-1048	如果过程是任命的 instance 和实体是那个过程的 patient，然后有存在另一个实体和第三实体这样那个实体 doesn't 在那个第三实体任职那个另外实体在那个过程出现的 time 的开始 holdsDuring 和那个实体在那个第三实体任职那个另外实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4482-4491	如果过程是 ActivatingADeactivatedAccount 的 instance 和实体是用户帐号的 instance 和那个实体是那个过程的 patient，然后 AccountDeactivated 是那个实体的 attribute 在紧接那个过程出现的 time before holdsDuring 和 AccountActive 是那个实体的 attribute 在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1252-1267	如果过程是 Braking 的 instance 和实体是那个过程的 patient，然后实数英里每小時 equal AccelerationFn 另一个实体, 第三实体, 那个实体 and 第四实体在紧接那个过程出现的 time before holdsDuring 和另一个实数英里每小時 equal AccelerationFn 那个另外实体, 那个第三实体, 那个实体 and 那个第四实体在紧接那个过程出现的 time after holdsDuring 和那个实数是 greaterThan 那个另外实数
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2397-2406	如果金融账户是担保债券的 instance 和抵押是那个金融账户的 secured 和施事体 possesses 那个金融账户和过程是财务违约的 instance 和那个金融账户是那个过程的 patient，然后那个施事体 possesses 那个抵押在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15963-15970	如果过程是遮盖的 instance 和实体是那个过程的 patient 和客体是导致那个过程的 instrument，然后 covers 那个客体 and 那个实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 767-785	如果过程是 Cricothyroidotomy 的 instance 和实体是那个过程的 patient，然后那个过程的目的是有存在另一个实体这样那个另外实体是 ImpairmentFn 呼吸的 instance 和那个实体是那个另外实体的 patient 在紧接那个过程出现的 time before holdsDuring 和有存在那个另外实体这样那个另外实体是 ImpairmentFn 呼吸的 instance 和那个实体是那个另外实体的 patient doesn't 在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 2784-2796	如果实体是 COVIDAntibody 的 instance 和 Covid19 不是另一个实体的 attribute 和那个实体是那个另外实体的 part 在时间位置 holdsDuring，然后 Covid19 是那个另外实体的 attribute 的声明 has 较不可能的语气在紧接那个时间位置 after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4123-4135	如果过程是 ChangingAccountInfo 的 instance 和施事体是那个过程的 agent 和那个施事体有 account 用户帐号和 accountInformation 那个用户帐号 and 命题，然后有存在实体这样那个实体不 equal 那个命题和 accountInformation 那个用户帐号 and 那个实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4079-4092	如果过程是 ChangingPassword 的 instance 和施事体是那个过程的 agent 和那个施事体有 account 用户帐号和那个用户帐号有 password 电脑密码，然后有存在实体这样那个实体是电脑密码的 instance 和那个实体不 equal 那个电脑密码和那个用户帐号有 password 那个实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4101-4114	如果过程是 ChangingUserName 的 instance 和施事体是那个过程的 agent 和那个施事体有 account 用户帐号和那个用户帐号的 user name 是用户名，然后有存在实体这样那个实体是用户名的 instance 和那个实体不 equal 那个用户名和那个用户帐号的 user name 是那个实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4143-4153	如果过程是 CreatingAnAccount 的 instance 和施事体是那个过程的 agent，然后有存在实体，另一个实体， and 和第三实体这样那个施事体有 account 那个实体和那个实体有 password 那个另外实体和那个实体的 user name 是那个第三实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 391-401	如果过程是关闭帐户的 instance 和实体是那个过程的 patient，然后那个实体是金融账户的 instance 在紧接那个过程出现的 time before holdsDuring 和那个实体不是金融账户的 instance 在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4566-4576	如果过程是 DeletingAnAccount 的 instance 和实体是 Account 的 instance 和施事体有 account 那个实体在紧接那个过程出现的 time before holdsDuring 和那个实体是那个过程的 patient 和那个施事体是那个过程的 agent，然后不那个施事体有 account 那个实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30103-30111	如果过程是损坏的 instance 和实体是设备的 instance 和那个实体是那个过程的 patient，然后 DeviceDamaged 是那个实体的 attribute 在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4498-4507	如果过程是 DeactivatingAnAccount 的 instance 和实体是用户帐号的 instance 和那个实体是那个过程的 patient，然后 AccountDeactivated 是那个实体的 attribute 在紧接那个过程出现的 time after holdsDuring 和 AccountActive 是那个实体的 attribute 在紧接那个过程出现的 time before holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10258-10273	如果过程是死亡的 instance 和施事体是生物的 instance 和那个施事体经历了那个过程，然后有存在实体和另一个实体这样那个实体是那个过程的 result 和那个实体是有机物体的 instance 和死是那个实体的 attribute 在那个过程出现的 time 之后 holdsDuring 和如果那个另外实体是那个实体的 part 在紧接那个过程出现的 time after holdsDuring，然后那个另外实体是那个施事体的 part 在紧接那个过程出现的 time before holdsDuring
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 436-453	如果金融交易是存款的 instance 和金融账户是金融账户的 instance 和那个金融交易在那个金融账户的 currency 结束和实数测量单位是那个金融交易的 transaction 总额和那个金融账户对于 %3 的 current 帐户存款和另一个实数 equal (第三实数和那个实数)，然后那个金融账户对于 %3 的 current 帐户存款
No TPTP formula. May not be expressible in strict first order.	MilitaryPersons.kif 133-140	如果过程是疏散的 instance 和施事体是那个过程的 agent 和那个施事体是军事组织的 instance 和另一个施事体经历了那个过程，然后撤离者是那个另外施事体的 attribute 在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	engineering.kif 939-952	如果客体是 Faucet 的 instance 和过程是液体运动的 instance 和实体是那个过程的 patient 和那个过程是 located 在那个客体，然后不存在另一个实体这样那个另外实体是管的 instance 和那个另外实体 contains 那个实体在紧接那个过程出现的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4451-4461	如果过程是 Forgetting 的 instance 和施事体经历了那个过程，然后有存在实体这样那个施事体 doesn't knows 那个实体在紧接那个过程出现的 time after holdsDuring 和那个施事体 knows 那个实体在紧接那个过程出现的 time before holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 25150-25171	如果 TelecomNumber 是 Hotline 的 instance 和那个 TelecomNumber 是施事体的 telephone number 和那个施事体是机构的 instance，然后那个 TelecomNumber 的目的是有存在实体这样那个实体是致电的 instance 和那个实体在那个施事体结束和有存在另一个实体这样那个另外实体是沟通的 instance 和那个 TelecomNumber 是导致那个另外实体的 instrument 和那个另外实体出现的 time 的开始 equal 紧接那个实体出现的 time after 的开始的声明 has 容易的语气
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 1328-1340	如果过程是碰撞的 instance 和实体是那个过程的 patient 和 ImpairedBodyPartFn 脑是那个实体的 attribute 在紧接那个过程 after holdsDuring，然后 Concussion 是那个实体的 attribute 在紧接那个过程 after holdsDuring 的声明 has 容易的语气

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

No TPTP formula. May not be expressible in strict first order.	Government.kif 2755-2758	时间位置是 1 day 的 instance 和安第斯国际社会是 "Andean Community of Nations" 的 conventional 全名在紧接那个时间位置 after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Government.kif 2729-2733	时间位置是 1996 year 的 instance 和法语社区的代理机构是 "Agency for the French-Speaking Community" 的 conventional 全名在紧接那个时间位置 after holdsDuring

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: