From f5461eb3d4eb2605b546a4ed202c12bcdaa1f4e4 Mon Sep 17 00:00:00 2001 From: "john.j.camilleri" Date: Mon, 16 Sep 2013 07:17:27 +0000 Subject: Remove contribs and examples Everything has now been moved to a separate repository at https://github.com/GrammaticalFramework/gf-contrib The contents of the examples folder are build during SetupWeb --- examples/SUMO/TPTP/Mid_level_ontologyLemAx.p | 5378 -------------------------- 1 file changed, 5378 deletions(-) delete mode 100644 examples/SUMO/TPTP/Mid_level_ontologyLemAx.p (limited to 'examples/SUMO/TPTP/Mid_level_ontologyLemAx.p') diff --git a/examples/SUMO/TPTP/Mid_level_ontologyLemAx.p b/examples/SUMO/TPTP/Mid_level_ontologyLemAx.p deleted file mode 100644 index 9d1cf5795..000000000 --- a/examples/SUMO/TPTP/Mid_level_ontologyLemAx.p +++ /dev/null @@ -1,5378 +0,0 @@ -fof(axMidLem0, axiom, - ( ! [Var_CORPSE] : - (hasType(type_HumanCorpse, Var_CORPSE) => -(( ? [Var_HUMAN] : - (hasType(type_Human, Var_HUMAN) & -(((f_before(f_WhenFn(Var_HUMAN),f_WhenFn(Var_CORPSE))) & (( ~ ( ? [Var_OTHERPART] : - (hasType(type_Object, Var_OTHERPART) & -(((f_holdsDuring(f_WhenFn(Var_CORPSE),part(Var_OTHERPART,Var_CORPSE))) & (( ~ (f_holdsDuring(f_WhenFn(Var_HUMAN),part(Var_OTHERPART,Var_HUMAN))))))))))))))))))). - -fof(axMidLem1, axiom, - ( ! [Var_CORPSE] : - (hasType(type_HumanCorpse, Var_CORPSE) => -(f_attribute(Var_CORPSE,inst_Dead))))). - -fof(axMidLem2, axiom, - ( ! [Var_SLAVE] : - ((hasType(type_Object, Var_SLAVE) & hasType(type_Entity, Var_SLAVE)) => -(((f_attribute(Var_SLAVE,inst_HumanSlave)) => (( ? [Var_PERSON] : - (hasType(type_Human, Var_PERSON) & -(((Var_PERSON != Var_SLAVE) & (f_possesses(Var_PERSON,Var_SLAVE)))))))))))). - -fof(axMidLem3, axiom, - ( ! [Var_ADULT] : - (hasType(type_HumanAdult, Var_ADULT) => -(( ! [Var_NUMBER] : - ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((f_age(Var_ADULT,f_MeasureFn(Var_NUMBER,inst_YearDuration))) => (f_greaterThanOrEqualTo(Var_NUMBER,18)))))))))). - -fof(axMidLem4, axiom, - ( ! [Var_YOUTH] : - (hasType(type_HumanYouth, Var_YOUTH) => -(( ! [Var_NUMBER] : - ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((f_age(Var_YOUTH,f_MeasureFn(Var_NUMBER,inst_YearDuration))) => (f_lessThan(Var_NUMBER,18)))))))))). - -fof(axMidLem5, axiom, - ( ! [Var_CHILD] : - (hasType(type_HumanChild, Var_CHILD) => -(f_attribute(Var_CHILD,inst_NonFullyFormed))))). - -fof(axMidLem6, axiom, - ( ! [Var_CHILD] : - (hasType(type_HumanChild, Var_CHILD) => -(( ! [Var_NUMBER] : - ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((f_age(Var_CHILD,f_MeasureFn(Var_NUMBER,inst_YearDuration))) => (f_lessThanOrEqualTo(Var_NUMBER,14)))))))))). - -fof(axMidLem7, axiom, - ( ! [Var_TEEN] : - (hasType(type_Teenager, Var_TEEN) => -(( ! [Var_NUMBER] : - ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((f_age(Var_TEEN,f_MeasureFn(Var_NUMBER,inst_YearDuration))) => (((f_greaterThan(Var_NUMBER,12)) & (f_lessThan(Var_NUMBER,20)))))))))))). - -fof(axMidLem8, axiom, - ( ! [Var_BABY] : - (hasType(type_HumanBaby, Var_BABY) => -(( ! [Var_NUMBER] : - ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((f_age(Var_BABY,f_MeasureFn(Var_NUMBER,inst_YearDuration))) => (f_lessThanOrEqualTo(Var_NUMBER,1)))))))))). - -fof(axMidLem9, axiom, - ( ! [Var_O2] : - (hasType(type_Object, Var_O2) => -(( ! [Var_O1] : - (hasType(type_Object, Var_O1) => -(((f_older(Var_O1,Var_O2)) => (( ? [Var_U] : - (hasType(type_UnitOfMeasure, Var_U) & -(( ? [Var_N2] : - ((hasType(type_RealNumber, Var_N2) & hasType(type_Quantity, Var_N2)) & -(( ? [Var_N1] : - ((hasType(type_RealNumber, Var_N1) & hasType(type_Quantity, Var_N1)) & -(((f_age(Var_O1,f_MeasureFn(Var_N1,Var_U))) & (((f_age(Var_O2,f_MeasureFn(Var_N2,Var_U))) & (f_greaterThan(Var_N1,Var_N2))))))))))))))))))))))). - -fof(axMidLem10, axiom, - ( ! [Var_P] : - (hasType(type_Wading, Var_P) => -(( ? [Var_W] : - (hasType(type_BodyOfWater, Var_W) & -(f_located(Var_P,Var_W)))))))). - -fof(axMidLem11, axiom, - ( ! [Var_S] : - (hasType(type_Somersaulting, Var_S) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Object, Var_A)) => -(((f_agent(Var_S,Var_A)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_S)),attribute(Var_A,inst_Sitting))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_S)),attribute(Var_A,inst_Sitting))))))))))))). - -fof(axMidLem12, axiom, - ( ! [Var_L] : - (hasType(type_Sunlight, Var_L) => -(f_origin(Var_L,inst_Sol))))). - -fof(axMidLem13, axiom, - ( ! [Var_W] : - (hasType(type_WrittenCommunication, Var_W) => -(( ? [Var_T] : - (hasType(type_Text, Var_T) & -(( ? [Var_C] : - (hasType(type_Character, Var_C) & -(( ? [Var_S] : - (hasType(type_Script, Var_S) & -(((f_result(Var_W,Var_T)) & (((f_part(Var_C,Var_T)) & (f_member(Var_C,Var_S)))))))))))))))))). - -fof(axMidLem14, axiom, - ( ! [Var_T] : - (hasType(type_Paragraph, Var_T) => -(( ? [Var_S] : - (hasType(type_Sentence, Var_S) & -(f_part(Var_S,Var_T)))))))). - -fof(axMidLem15, axiom, - ( ! [Var_MUSIC] : - (hasType(type_InstrumentalMusic, Var_MUSIC) => -(( ? [Var_INSTRUMENT] : - (hasType(type_MusicalInstrument, Var_INSTRUMENT) & -(f_instrument(Var_MUSIC,Var_INSTRUMENT)))))))). - -fof(axMidLem16, axiom, - ( ! [Var_M] : - (hasType(type_VocalMusic, Var_M) => -(( ? [Var_S] : - (hasType(type_Singing, Var_S) & -(f_subProcess(Var_S,Var_M)))))))). - -fof(axMidLem17, axiom, - ( ! [Var_WI] : - (hasType(type_WindInstrument, Var_WI) => -(( ! [Var_M] : - (hasType(type_Music, Var_M) => -(( ! [Var_A] : - (hasType(type_Agent, Var_A) => -(((((f_agent(Var_M,Var_A)) & (f_instrument(Var_M,Var_WI)))) => (( ? [Var_B] : - (hasType(type_Exhaling, Var_B) & -(((f_agent(Var_B,Var_A)) & (f_subProcess(Var_B,Var_M)))))))))))))))))). - -fof(axMidLem18, axiom, - ( ! [Var_R] : - (hasType(type_Ringing, Var_R) => -(( ? [Var_B] : - (hasType(type_Bell, Var_B) & -(f_instrument(Var_R,Var_B)))))))). - -fof(axMidLem19, axiom, - ( ! [Var_B] : - (hasType(type_Bell, Var_B) => -(( ! [Var_I] : - (hasType(type_Impacting, Var_I) => -(((f_destination(Var_I,Var_B)) => (( ? [Var_MT] : - (hasType(type_MusicalTone, Var_MT) & -(f_causes(Var_I,Var_MT))))))))))))). - -fof(axMidLem20, axiom, - ( ! [Var_D] : - (hasType(type_Drumming, Var_D) => -(( ? [Var_DRUM] : - (hasType(type_Drum, Var_DRUM) & -(( ? [Var_I] : - (hasType(type_Impacting, Var_I) & -(( ? [Var_A] : - (hasType(type_Agent, Var_A) & -(((f_agent(Var_D,Var_A)) & (((f_instrument(Var_D,Var_DRUM)) & (((f_subProcess(Var_I,Var_D)) & (((f_agent(Var_I,Var_A)) & (f_patient(Var_I,Var_DRUM)))))))))))))))))))))). - -fof(axMidLem21, axiom, - ( ! [Var_COMMUNICATE] : - (hasType(type_WrittenCommunication, Var_COMMUNICATE) => -(( ? [Var_WRITE] : - (hasType(type_Writing, Var_WRITE) & -(( ? [Var_READ] : - (hasType(type_Reading, Var_READ) & -(( ? [Var_TEXT] : - (hasType(type_Text, Var_TEXT) & -(((f_instrument(Var_COMMUNICATE,Var_TEXT)) & (((f_result(Var_WRITE,Var_TEXT)) & (((f_patient(Var_READ,Var_TEXT)) & (((f_subProcess(Var_WRITE,Var_COMMUNICATE)) & (f_subProcess(Var_READ,Var_COMMUNICATE)))))))))))))))))))))). - -fof(axMidLem22, axiom, - ( ! [Var_C] : - (hasType(type_Corresponding, Var_C) => -(( ? [Var_M] : - (hasType(type_Mailing, Var_M) & -(( ? [Var_T] : - (hasType(type_Text, Var_T) & -(((f_subProcess(Var_M,Var_C)) & (((f_patient(Var_M,Var_T)) & (f_patient(Var_C,Var_T))))))))))))))). - -fof(axMidLem23, axiom, - ( ! [Var_REMIND] : - (hasType(type_Reminding, Var_REMIND) => -(( ? [Var_REMEMBER] : - (hasType(type_Remembering, Var_REMEMBER) & -(f_causes(Var_REMIND,Var_REMEMBER)))))))). - -fof(axMidLem24, axiom, - ( ! [Var_ACTION] : - (hasType(type_LegalAction, Var_ACTION) => -(( ? [Var_REGISTER] : - (hasType(type_Registering, Var_REGISTER) & -(f_subProcess(Var_REGISTER,Var_ACTION)))))))). - -fof(axMidLem25, axiom, - ( ! [Var_ANSWER] : - (hasType(type_Answering, Var_ANSWER) => -(( ? [Var_QUESTION] : - (hasType(type_Questioning, Var_QUESTION) & -(((f_refers(Var_ANSWER,Var_QUESTION)) & (f_earlier(f_WhenFn(Var_QUESTION),f_WhenFn(Var_ANSWER))))))))))). - -fof(axMidLem26, axiom, - ( ! [Var_ARGUE] : - (hasType(type_Arguing, Var_ARGUE) => -(( ? [Var_STATEMENT] : - (hasType(type_Statement, Var_STATEMENT) & -(( ? [Var_ARGUMENT] : - (hasType(type_Argument, Var_ARGUMENT) & -(((f_patient(Var_ARGUE,Var_STATEMENT)) & (f_containsInformation(Var_STATEMENT,Var_ARGUMENT))))))))))))). - -fof(axMidLem27, axiom, - ( ! [Var_STATE] : - (hasType(type_TellingALie, Var_STATE) => -(( ! [Var_STATEMENT] : - ((hasType(type_Entity, Var_STATEMENT) & hasType(type_Sentence, Var_STATEMENT)) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) => -(((((f_agent(Var_STATE,Var_AGENT)) & (f_patient(Var_STATE,Var_STATEMENT)))) => (f_holdsDuring(f_WhenFn(Var_STATE),believes(Var_AGENT,truth(Var_STATEMENT,inst_False))))))))))))))). - -fof(axMidLem28, axiom, - ( ! [Var_FOUND] : - (hasType(type_Founding, Var_FOUND) => -(( ? [Var_ORG] : - (hasType(type_Organization, Var_ORG) & -(f_result(Var_FOUND,Var_ORG)))))))). - -fof(axMidLem29, axiom, - ( ! [Var_P] : - (hasType(type_TurningOffDevice, Var_P) => -(( ! [Var_D] : - ((hasType(type_Entity, Var_D) & hasType(type_Object, Var_D)) => -(((f_patient(Var_P,Var_D)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_P)),attribute(Var_D,inst_DeviceOn))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_P)),attribute(Var_D,inst_DeviceOff))))))))))))). - -fof(axMidLem30, axiom, - ( ! [Var_P] : - (hasType(type_TurningOnDevice, Var_P) => -(( ! [Var_D] : - ((hasType(type_Entity, Var_D) & hasType(type_Object, Var_D)) => -(((f_patient(Var_P,Var_D)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_P)),attribute(Var_D,inst_DeviceOff))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_P)),attribute(Var_D,inst_DeviceOn))))))))))))). - -fof(axMidLem31, axiom, - ( ! [Var_PROJECTILE] : - (hasType(type_Projectile, Var_PROJECTILE) => -(( ? [Var_SHELL] : - (hasType(type_ProjectileShell, Var_SHELL) & -(f_part(Var_SHELL,Var_PROJECTILE)))))))). - -fof(axMidLem32, axiom, - ( ! [Var_SHOOT] : - (hasType(type_Shooting, Var_SHOOT) => -(( ? [Var_PROJECTILE] : - (hasType(type_Projectile, Var_PROJECTILE) & -(( ? [Var_GUN] : - (hasType(type_Gun, Var_GUN) & -(((f_patient(Var_SHOOT,Var_PROJECTILE)) & (f_instrument(Var_SHOOT,Var_GUN))))))))))))). - -fof(axMidLem33, axiom, - ( ! [Var_B] : - (hasType(type_GunBarrel, Var_B) => -(( ? [Var_G] : - (hasType(type_Gun, Var_G) & -(f_part(Var_B,Var_G)))))))). - -fof(axMidLem34, axiom, - ( ! [Var_G] : - (hasType(type_Gun, Var_G) => -(( ! [Var_B] : - (hasType(type_GunBarrel, Var_B) => -(( ! [Var_S] : - (hasType(type_Shooting, Var_S) => -(( ! [Var_P] : - (hasType(type_Projectile, Var_P) => -(( ! [Var_GUN] : - (hasType(type_Object, Var_GUN) => -(((((f_part(Var_B,Var_G)) & (((f_instrument(Var_S,Var_GUN)) & (f_patient(Var_S,Var_P)))))) => (( ? [Var_SUB] : - ((hasType(type_Process, Var_SUB) & hasType(type_Motion, Var_SUB)) & -(((f_subProcess(Var_SUB,Var_S)) & (f_path(Var_SUB,Var_B)))))))))))))))))))))))). - -fof(axMidLem35, axiom, - ( ! [Var_STOCK] : - (hasType(type_GunStock, Var_STOCK) => -(( ? [Var_GUN] : - (hasType(type_Gun, Var_GUN) & -(f_part(Var_STOCK,Var_GUN)))))))). - -fof(axMidLem36, axiom, - ( ! [Var_S] : - (hasType(type_Shield, Var_S) => -(( ? [Var_H] : - (hasType(type_Handle, Var_H) & -(f_part(Var_H,Var_S)))))))). - -fof(axMidLem37, axiom, - ( ! [Var_W] : - (hasType(type_WingDevice, Var_W) => -(( ? [Var_A] : - (hasType(type_Aircraft, Var_A) & -(f_part(Var_W,Var_A)))))))). - -fof(axMidLem38, axiom, - ( ! [Var_S] : - (hasType(type_Shelf, Var_S) => -(( ? [Var_F] : - (hasType(type_Furniture, Var_F) & -(f_part(Var_S,Var_F)))))))). - -fof(axMidLem39, axiom, - ( ! [Var_C] : - ((hasType(type_Object, Var_C) & hasType(type_SelfConnectedObject, Var_C) & hasType(type_Hole, Var_C)) => -(((f_attribute(Var_C,inst_ContainerFull)) => (( ? [Var_H] : - (hasType(type_Hole, Var_H) & -(( ? [Var_S] : - (hasType(type_Object, Var_S) & -(((f_hole(Var_H,Var_C)) & (f_fills(Var_S,Var_C))))))))))))))). - -fof(axMidLem40, axiom, - ( ! [Var_PP] : - (hasType(type_PetroleumProduct, Var_PP) => -(( ? [Var_O] : - (hasType(type_OrganicCompound, Var_O) & -(f_part(Var_O,Var_PP)))))))). - -fof(axMidLem41, axiom, - ( ! [Var_DEVICE] : - (hasType(type_SwitchDevice, Var_DEVICE) => -(( ? [Var_ELECTRIC] : - (hasType(type_ElectricDevice, Var_ELECTRIC) & -(( ? [Var_PROC2] : - (hasType(type_Process, Var_PROC2) & -(( ? [Var_PROC1] : - (hasType(type_Process, Var_PROC1) & -(((f_instrument(Var_PROC1,Var_DEVICE)) & (((f_causes(Var_PROC1,Var_PROC2)) & (f_instrument(Var_PROC2,Var_ELECTRIC)))))))))))))))))). - -fof(axMidLem42, axiom, - ( ! [Var_AERATE] : - (hasType(type_Aerating, Var_AERATE) => -(( ? [Var_AIR] : - (hasType(type_Air, Var_AIR) & -(( ? [Var_S] : - ((hasType(type_Entity, Var_S) & hasType(type_Object, Var_S)) & -(((f_patient(Var_AERATE,Var_AIR)) & (((f_patient(Var_AERATE,Var_S)) & (f_attribute(Var_S,inst_Liquid))))))))))))))). - -fof(axMidLem43, axiom, - ( ! [Var_C] : - (hasType(type_CigarOrCigarette, Var_C) => -(( ? [Var_T] : - (hasType(type_Tobacco, Var_T) & -(f_part(Var_T,Var_C)))))))). - -fof(axMidLem44, axiom, - ( ! [Var_C] : - (hasType(type_Compass, Var_C) => -(( ? [Var_D] : - (hasType(type_DirectionalAttribute, Var_D) & -(f_represents(Var_C,Var_D)))))))). - -fof(axMidLem45, axiom, - ( ! [Var_C] : - (hasType(type_Crane, Var_C) => -(( ? [Var_H] : - (hasType(type_HoistingDevice, Var_H) & -(f_component(Var_H,Var_C)))))))). - -fof(axMidLem46, axiom, - ( ! [Var_DEV] : - (hasType(type_ElectricDevice, Var_DEV) => -(( ! [Var_EV] : - (hasType(type_Process, Var_EV) => -(((f_patient(Var_EV,Var_DEV)) => (( ? [Var_R] : - (hasType(type_Electricity, Var_R) & -(f_resourceS(Var_EV,Var_R))))))))))))). - -fof(axMidLem47, axiom, - ( ! [Var_S] : - (hasType(type_ElectricalSignalling, Var_S) => -(( ? [Var_D] : - (hasType(type_ElectricDevice, Var_D) & -(f_instrument(Var_S,Var_D)))))))). - -fof(axMidLem48, axiom, - ( ! [Var_S] : - (hasType(type_ElectronicSignalling, Var_S) => -(( ? [Var_D] : - (hasType(type_Computer, Var_D) & -(f_instrument(Var_S,Var_D)))))))). - -fof(axMidLem49, axiom, - ( ! [Var_S] : - (hasType(type_SafeContainer, Var_S) => -(( ? [Var_L] : - (hasType(type_Lock, Var_L) & -(f_part(Var_L,Var_S)))))))). - -fof(axMidLem50, axiom, - ( ! [Var_DEVICE] : - (hasType(type_SelfPoweredDevice, Var_DEVICE) => -(( ? [Var_SOURCE] : - (hasType(type_Device, Var_SOURCE) & -(f_powerPlant(Var_DEVICE,Var_SOURCE)))))))). - -fof(axMidLem51, axiom, - ( ! [Var_D] : - (hasType(type_AnimalPoweredDevice, Var_D) => -(( ! [Var_P] : - (hasType(type_Process, Var_P) => -(((f_instrument(Var_P,Var_D)) => (( ? [Var_A] : - (hasType(type_Animal, Var_A) & -(f_instrument(Var_P,Var_A))))))))))))). - -fof(axMidLem52, axiom, - ( ! [Var_H] : - ((hasType(type_LengthMeasure, Var_H) & hasType(type_Quantity, Var_H)) => -(( ! [Var_S2] : - ((hasType(type_SelfConnectedObject, Var_S2) & hasType(type_Object, Var_S2) & hasType(type_Entity, Var_S2) & hasType(type_Quantity, Var_S2)) => -(( ! [Var_S1] : - ((hasType(type_SelfConnectedObject, Var_S1) & hasType(type_Object, Var_S1) & hasType(type_Entity, Var_S1) & hasType(type_Quantity, Var_S1)) => -(( ! [Var_F] : - ((hasType(type_Object, Var_F) & hasType(type_SelfConnectedObject, Var_F)) => -(((f_attribute(Var_F,inst_Flat)) => (((f_side(Var_S1,Var_F)) & (((f_side(Var_S2,Var_F)) & (((f_meetsSpatially(Var_S1,Var_S2)) & (((Var_S1 != Var_S2) & (((f_height(Var_F,Var_H)) & (((f_greaterThan(Var_S1,f_MultiplicationFn(2,Var_H))) & (f_greaterThan(Var_S2,f_MultiplicationFn(2,Var_H))))))))))))))))))))))))))))). - -fof(axMidLem53, axiom, - ( ! [Var_H] : - ((hasType(type_PhysicalQuantity, Var_H) & hasType(type_Quantity, Var_H)) => -(( ! [Var_S2] : - ((hasType(type_SelfConnectedObject, Var_S2) & hasType(type_Object, Var_S2) & hasType(type_Entity, Var_S2) & hasType(type_Quantity, Var_S2)) => -(( ! [Var_S1] : - ((hasType(type_SelfConnectedObject, Var_S1) & hasType(type_Object, Var_S1) & hasType(type_Entity, Var_S1) & hasType(type_Quantity, Var_S1)) => -(( ! [Var_F] : - ((hasType(type_Object, Var_F) & hasType(type_SelfConnectedObject, Var_F)) => -(((f_attribute(Var_F,inst_LongAndThin)) => (((f_side(Var_S1,Var_F)) & (((f_side(Var_S2,Var_F)) & (((f_meetsSpatially(Var_S1,Var_S2)) & (((Var_S1 != Var_S2) & (((f_length(Var_F,Var_H)) & (((f_lessThan(Var_S1,f_MultiplicationFn(3,Var_H))) & (f_lessThan(Var_S2,f_MultiplicationFn(3,Var_H))))))))))))))))))))))))))))). - -fof(axMidLem54, axiom, - ( ! [Var_O] : - ((hasType(type_Object, Var_O) & hasType(type_SelfConnectedObject, Var_O)) => -(((f_attribute(Var_O,inst_LevelShape)) => (( ~ ( ? [Var_H2] : - ((hasType(type_LengthMeasure, Var_H2) & hasType(type_Quantity, Var_H2)) & -(( ? [Var_H1] : - ((hasType(type_LengthMeasure, Var_H1) & hasType(type_Quantity, Var_H1)) & -(( ? [Var_T] : - ((hasType(type_SelfConnectedObject, Var_T) & hasType(type_Object, Var_T)) & -(( ? [Var_P2] : - ((hasType(type_Object, Var_P2) & hasType(type_SelfConnectedObject, Var_P2)) & -(( ? [Var_P1] : - ((hasType(type_Object, Var_P1) & hasType(type_SelfConnectedObject, Var_P1)) & -(((f_top(Var_T,Var_O)) & (((f_part(Var_P1,Var_T)) & (((f_part(Var_P2,Var_T)) & (((f_height(Var_P1,Var_H1)) & (((f_height(Var_P2,Var_H2)) & (f_greaterThan(Var_H1,Var_H2))))))))))))))))))))))))))))))))). - -fof(axMidLem55, axiom, - ( ! [Var_T] : - ((hasType(type_Object, Var_T) & hasType(type_Entity, Var_T)) => -(((f_attribute(Var_T,inst_SymmetricShape)) => (( ? [Var_C2] : - (hasType(type_Object, Var_C2) & -(( ? [Var_C1] : - (hasType(type_Object, Var_C1) & -(((f_copy(Var_C1,Var_C2)) & (Var_T = f_MereologicalSumFn(Var_C1,Var_C2))))))))))))))). - -fof(axMidLem56, axiom, - ( ! [Var_B] : - (hasType(type_Baton, Var_B) => -(f_attribute(Var_B,inst_LongAndThin))))). - -fof(axMidLem57, axiom, - ( ! [Var_N] : - (hasType(type_BroadcastNetwork, Var_N) => -(( ? [Var_O] : - (hasType(type_Organization, Var_O) & -(( ! [Var_M] : - ((hasType(type_SelfConnectedObject, Var_M) & hasType(type_Object, Var_M)) => -(((f_member(Var_M,Var_N)) => (f_possesses(Var_O,Var_M))))))))))))). - -fof(axMidLem58, axiom, - ( ! [Var_CANDLE] : - (hasType(type_Candle, Var_CANDLE) => -(f_material(type_Wax,Var_CANDLE))))). - -fof(axMidLem59, axiom, - ( ! [Var_L] : - (hasType(type_Lightning, Var_L) => -(( ? [Var_C] : - (hasType(type_Cloud, Var_C) & -(f_located(Var_L,Var_C)))))))). - -fof(axMidLem60, axiom, - ( ! [Var_T] : - (hasType(type_Thunder, Var_T) => -(( ? [Var_L] : - (hasType(type_Lightning, Var_L) & -(f_causes(Var_L,Var_T)))))))). - -fof(axMidLem61, axiom, - ( ! [Var_L] : - (hasType(type_VehicleLight, Var_L) => -(( ? [Var_V] : - (hasType(type_Vehicle, Var_V) & -(f_part(Var_L,Var_V)))))))). - -fof(axMidLem62, axiom, - ( ! [Var_L] : - (hasType(type_Headlight, Var_L) => -(( ? [Var_V] : - (hasType(type_Vehicle, Var_V) & -(f_part(Var_L,f_FrontFn(Var_V))))))))). - -fof(axMidLem63, axiom, - ( ! [Var_L] : - (hasType(type_Taillight, Var_L) => -(( ? [Var_V] : - (hasType(type_Vehicle, Var_V) & -(f_part(Var_L,f_BackFn(Var_V))))))))). - -fof(axMidLem64, axiom, - ( ! [Var_PP] : - (hasType(type_PaintedPicture, Var_PP) => -(( ? [Var_PAINT] : - (hasType(type_Paint, Var_PAINT) & -(( ? [Var_PAINTING] : - (hasType(type_Painting, Var_PAINTING) & -(((f_resourceS(Var_PAINTING,Var_PAINT)) & (f_result(Var_PAINTING,Var_PP))))))))))))). - -fof(axMidLem65, axiom, - ( ! [Var_W] : - (hasType(type_WatercolorPicture, Var_W) => -(( ? [Var_WP] : - (hasType(type_WatercolorPaint, Var_WP) & -(( ? [Var_P] : - (hasType(type_Painting, Var_P) & -(((f_resourceS(Var_P,Var_WP)) & (f_result(Var_P,Var_W))))))))))))). - -fof(axMidLem66, axiom, - ( ! [Var_P] : - (hasType(type_Portrait, Var_P) => -(( ? [Var_F] : - (hasType(type_Face, Var_F) & -(f_represents(Var_P,Var_F)))))))). - -fof(axMidLem67, axiom, - ( ! [Var_F] : - (hasType(type_Folding, Var_F) => -(( ! [Var_O] : - ((hasType(type_Entity, Var_O) & hasType(type_Object, Var_O)) => -(((f_patient(Var_F,Var_O)) => (( ? [Var_C] : - (hasType(type_Covering, Var_C) & -(( ? [Var_P2] : - ((hasType(type_Object, Var_P2) & hasType(type_Entity, Var_P2)) & -(( ? [Var_P1] : - (hasType(type_Object, Var_P1) & -(((f_subProcess(Var_C,Var_F)) & (((f_part(Var_P1,Var_O)) & (((f_part(Var_P2,Var_O)) & (((f_instrument(Var_C,Var_P1)) & (f_patient(Var_C,Var_P2))))))))))))))))))))))))))). - -fof(axMidLem68, axiom, - ( ! [Var_P] : - (hasType(type_WatercolorPaint, Var_P) => -(( ? [Var_W] : - (hasType(type_Water, Var_W) & -(f_part(Var_W,Var_P)))))))). - -fof(axMidLem69, axiom, - ( ! [Var_P] : - (hasType(type_OilPaint, Var_P) => -(( ? [Var_O] : - (hasType(type_Oil, Var_O) & -(f_part(Var_O,Var_P)))))))). - -fof(axMidLem70, axiom, - ( ! [Var_P] : - (hasType(type_OilPicture, Var_P) => -(( ? [Var_O] : - (hasType(type_OilPaint, Var_O) & -(( ? [Var_PAINTING] : - (hasType(type_Painting, Var_PAINTING) & -(((f_resourceS(Var_PAINTING,Var_O)) & (f_result(Var_PAINTING,Var_P))))))))))))). - -fof(axMidLem71, axiom, - ( ! [Var_PAINT] : - (hasType(type_ArtPainting, Var_PAINT) => -(( ? [Var_PICTURE] : - (hasType(type_PaintedPicture, Var_PICTURE) & -(f_result(Var_PAINT,Var_PICTURE)))))))). - -fof(axMidLem72, axiom, - ( ! [Var_N] : - ((hasType(type_RealNumber, Var_N) & hasType(type_Quantity, Var_N)) => -(( ! [Var_S] : - (hasType(type_Solution, Var_S) => -(((f_potentialOfHydrogen(Var_S,Var_N)) => (((f_greaterThanOrEqualTo(Var_N,0)) & (f_lessThanOrEqualTo(Var_N,14)))))))))))). - -fof(axMidLem73, axiom, - ( ! [Var_T] : - (hasType(type_Tracing, Var_T) => -(( ? [Var_P] : - (hasType(type_Blueprint, Var_P) & -(f_result(Var_T,Var_P)))))))). - -fof(axMidLem74, axiom, - ( ! [Var_C] : - (hasType(type_ComposingMusic, Var_C) => -(( ? [Var_M] : - (hasType(type_MusicalComposition, Var_M) & -(f_result(Var_C,Var_M)))))))). - -fof(axMidLem75, axiom, - ( ! [Var_DRAW] : - (hasType(type_Drawing, Var_DRAW) => -(( ? [Var_SKETCH] : - (hasType(type_Sketch, Var_SKETCH) & -(f_result(Var_DRAW,Var_SKETCH)))))))). - -fof(axMidLem76, axiom, - ( ! [Var_F] : - (hasType(type_Focusing, Var_F) => -(( ? [Var_L] : - (hasType(type_Lens, Var_L) & -(f_patient(Var_F,Var_L)))))))). - -fof(axMidLem77, axiom, - ( ! [Var_VEHICLE] : - (hasType(type_LandVehicle, Var_VEHICLE) => -(( ? [Var_WHEEL] : - (hasType(type_Wheel, Var_WHEEL) & -(f_part(Var_WHEEL,Var_VEHICLE)))))))). - -fof(axMidLem78, axiom, - ( ! [Var_C] : - (hasType(type_VehicleController, Var_C) => -(( ? [Var_V] : - (hasType(type_Vehicle, Var_V) & -(f_part(Var_C,Var_V)))))))). - -fof(axMidLem79, axiom, - ( ! [Var_W] : - (hasType(type_VehicleWindow, Var_W) => -(( ? [Var_V] : - (hasType(type_Vehicle, Var_V) & -(f_part(Var_W,Var_V)))))))). - -fof(axMidLem80, axiom, - ( ! [Var_W] : - (hasType(type_Windshield, Var_W) => -(( ? [Var_A] : - (hasType(type_Automobile, Var_A) & -(f_part(Var_W,f_FrontFn(Var_A))))))))). - -fof(axMidLem81, axiom, - ( ! [Var_W] : - (hasType(type_VehicleWheel, Var_W) => -(( ! [Var_V] : - (hasType(type_RoadVehicle, Var_V) => -(((f_part(Var_W,Var_V)) => (( ? [Var_A] : - (hasType(type_Axle, Var_A) & -(((f_component(Var_A,Var_V)) & (f_connected(Var_W,Var_A))))))))))))))). - -fof(axMidLem82, axiom, - ( ! [Var_BILL] : - (hasType(type_CurrencyBill, Var_BILL) => -(( ? [Var_PAPER] : - (hasType(type_Paper, Var_PAPER) & -(f_part(Var_PAPER,Var_BILL)))))))). - -fof(axMidLem83, axiom, - ( ! [Var_WIRE] : - (hasType(type_Wire, Var_WIRE) => -(f_material(type_Metal,Var_WIRE))))). - -fof(axMidLem84, axiom, - ( ! [Var_TL] : - (hasType(type_TelephoneLine, Var_TL) => -(( ? [Var_T1] : - ((hasType(type_Telephone, Var_T1) | hasType(type_Telegraph, Var_T1)) & -(( ? [Var_T2] : - ((hasType(type_Telephone, Var_T2) | hasType(type_Telegraph, Var_T2)) & -(((Var_T1 != Var_T2) & (f_connects(Var_TL,Var_T1,Var_T2))))))))))))). - -fof(axMidLem85, axiom, - ( ! [Var_S] : - (hasType(type_String, Var_S) => -(f_material(type_Fabric,Var_S))))). - -fof(axMidLem86, axiom, - ( ! [Var_PLUG] : - (hasType(type_Plug, Var_PLUG) => -(( ? [Var_HOLE] : - (hasType(type_Hole, Var_HOLE) & -(f_completelyFills(Var_PLUG,Var_HOLE)))))))). - -fof(axMidLem87, axiom, - ( ! [Var_POTTERY] : - (hasType(type_Pottery, Var_POTTERY) => -(( ? [Var_CLAY] : - (hasType(type_Clay, Var_CLAY) & -(f_part(Var_CLAY,Var_POTTERY)))))))). - -fof(axMidLem88, axiom, - ( ! [Var_C] : - (hasType(type_Compartment, Var_C) => -(( ? [Var_O] : - (hasType(type_Container, Var_O) & -(((Var_C != Var_O) & (f_part(Var_C,Var_O)))))))))). - -fof(axMidLem89, axiom, - ( ! [Var_TAPE] : - (hasType(type_Tape, Var_TAPE) => -(( ? [Var_PART] : - ((hasType(type_Paper, Var_PART) | hasType(type_Fabric, Var_PART)) & -(f_part(Var_PART,Var_TAPE)))))))). - -fof(axMidLem90, axiom, - ( ! [Var_R] : - (hasType(type_HorseRiding, Var_R) => -(( ? [Var_H] : - (hasType(type_Horse, Var_H) & -(f_instrument(Var_R,Var_H)))))))). - -fof(axMidLem91, axiom, - ( ! [Var_BAG] : - (hasType(type_Bag, Var_BAG) => -(( ? [Var_PART] : - (hasType(type_Fabric, Var_PART) & -(f_part(Var_PART,Var_BAG)))))))). - -fof(axMidLem92, axiom, - ( ! [Var_TANK] : - (hasType(type_FluidContainer, Var_TANK) => -(( ! [Var_STUFF] : - (hasType(type_Object, Var_STUFF) => -(((f_contains(Var_TANK,Var_STUFF)) => (f_attribute(Var_STUFF,inst_Fluid)))))))))). - -fof(axMidLem93, axiom, - ( ! [Var_BOTTLE] : - (hasType(type_Bottle, Var_BOTTLE) => -(( ! [Var_STUFF] : - (hasType(type_Object, Var_STUFF) => -(((f_contains(Var_BOTTLE,Var_STUFF)) => (f_attribute(Var_STUFF,inst_Liquid)))))))))). - -fof(axMidLem94, axiom, - ( ! [Var_BOTTLE] : - (hasType(type_Bottle, Var_BOTTLE) => -(( ! [Var_WIDTH2] : - ((hasType(type_PhysicalQuantity, Var_WIDTH2) & hasType(type_Quantity, Var_WIDTH2)) => -(( ! [Var_WIDTH1] : - ((hasType(type_PhysicalQuantity, Var_WIDTH1) & hasType(type_Quantity, Var_WIDTH1)) => -(( ! [Var_TOP] : - ((hasType(type_SelfConnectedObject, Var_TOP) & hasType(type_Object, Var_TOP)) => -(( ! [Var_BOTTOM] : - ((hasType(type_SelfConnectedObject, Var_BOTTOM) & hasType(type_Object, Var_BOTTOM)) => -(((((f_bottom(Var_BOTTOM,Var_BOTTLE)) & (((f_top(Var_TOP,Var_BOTTLE)) & (((f_width(Var_BOTTOM,Var_WIDTH1)) & (f_width(Var_TOP,Var_WIDTH2)))))))) => (f_lessThan(Var_WIDTH2,Var_WIDTH1))))))))))))))))))). - -fof(axMidLem95, axiom, - ( ! [Var_B] : - (hasType(type_Brick, Var_B) => -(f_material(type_Clay,Var_B))))). - -fof(axMidLem96, axiom, - ( ! [Var_TO] : - (hasType(type_TwoDimensionalObject, Var_TO) => -(( ! [Var_O] : - ((hasType(type_Object, Var_O) & hasType(type_GeometricFigure, Var_O)) => -(((f_attribute(Var_O,inst_RoundShape)) => (( ! [Var_P] : - ((hasType(type_GeometricFigure, Var_P) & hasType(type_Object, Var_P)) => -(((f_pointOfFigure(Var_P,Var_O)) & (((f_meetsSpatially(Var_P,Var_O)) & (((f_meetsSpatially(Var_P,Var_TO)) & (( ? [Var_T] : - (hasType(type_OneDimensionalFigure, Var_T) & -(f_tangent(Var_T,Var_TO)))))))))))))))))))))). - -fof(axMidLem97, axiom, - ( ! [Var_B] : - (hasType(type_Bubble, Var_B) => -(( ? [Var_S] : - ((hasType(type_SelfConnectedObject, Var_S) & hasType(type_Object, Var_S)) & -(((f_surface(Var_S,Var_B)) & (f_attribute(Var_S,inst_Liquid)))))))))). - -fof(axMidLem98, axiom, - ( ! [Var_B] : - (hasType(type_Bubble, Var_B) => -(( ! [Var_P] : - (hasType(type_Object, Var_P) => -(((f_interiorPart(Var_P,Var_B)) => (f_attribute(Var_P,inst_Gas)))))))))). - -fof(axMidLem99, axiom, - ( ! [Var_B] : - (hasType(type_Bubble, Var_B) => -(((( ~ ( ? [Var_S] : - (hasType(type_Attribute, Var_S) & -(( ? [Var_X] : - ((hasType(type_Object, Var_X) & hasType(type_Entity, Var_X)) & -(((f_attribute(Var_X,Var_S)) & (((Var_X != inst_Gas) & (f_meetsSpatially(Var_X,Var_B))))))))))))) => (f_attribute(Var_B,inst_RoundShape))))))). - -fof(axMidLem100, axiom, - ( ! [Var_B] : - (hasType(type_Belt, Var_B) => -(( ! [Var_P] : - (hasType(type_Animal, Var_P) => -(((f_wears(Var_P,Var_B)) => (( ? [Var_C] : - (hasType(type_Clothing, Var_C) & -(((f_wears(Var_P,Var_C)) & (f_meetsSpatially(Var_B,Var_C))))))))))))))). - -fof(axMidLem101, axiom, - ( ! [Var_T] : - (hasType(type_TieClothing, Var_T) => -(( ! [Var_P] : - ((hasType(type_Animal, Var_P) & hasType(type_Object, Var_P)) => -(((f_wears(Var_P,Var_T)) => (( ? [Var_N] : - (hasType(type_Neck, Var_N) & -(((f_part(Var_N,Var_P)) & (f_contains(Var_T,Var_N))))))))))))))). - -fof(axMidLem102, axiom, - ( ! [Var_C] : - (hasType(type_Collar, Var_C) => -(( ? [Var_OC] : - ((hasType(type_Coat, Var_OC) | hasType(type_Shirt, Var_OC)) & -(f_part(Var_C,Var_OC)))))))). - -fof(axMidLem103, axiom, - ( ! [Var_C] : - (hasType(type_Collar, Var_C) => -(( ! [Var_P] : - ((hasType(type_Animal, Var_P) & hasType(type_Object, Var_P)) => -(((f_wears(Var_P,Var_C)) => (( ? [Var_N] : - (hasType(type_Neck, Var_N) & -(((f_part(Var_N,Var_P)) & (f_meetsSpatially(Var_C,Var_N))))))))))))))). - -fof(axMidLem104, axiom, - ( ! [Var_G] : - (hasType(type_Glove, Var_G) => -(( ! [Var_P] : - ((hasType(type_Animal, Var_P) & hasType(type_Object, Var_P)) => -(((f_wears(Var_P,Var_G)) => (( ? [Var_H] : - (hasType(type_Hand, Var_H) & -(((f_part(Var_H,Var_P)) & (f_meetsSpatially(Var_G,Var_H))))))))))))))). - -fof(axMidLem105, axiom, - ( ! [Var_HAT] : - (hasType(type_Hat, Var_HAT) => -(( ! [Var_PERSON] : - ((hasType(type_Animal, Var_PERSON) & hasType(type_Object, Var_PERSON)) => -(((f_wears(Var_PERSON,Var_HAT)) => (( ? [Var_HEAD] : - (hasType(type_Head, Var_HEAD) & -(((f_part(Var_HEAD,Var_PERSON)) & (f_meetsSpatially(Var_HAT,Var_HEAD))))))))))))))). - -fof(axMidLem106, axiom, - ( ! [Var_T] : - (hasType(type_Trousers, Var_T) => -(( ! [Var_H] : - ((hasType(type_Animal, Var_H) & hasType(type_Object, Var_H)) => -(((f_wears(Var_H,Var_T)) => (( ? [Var_L] : - (hasType(type_Leg, Var_L) & -(((f_part(Var_L,Var_H)) & (f_contains(Var_T,Var_L))))))))))))))). - -fof(axMidLem107, axiom, - ( ! [Var_SHOE] : - (hasType(type_Shoe, Var_SHOE) => -(( ! [Var_PERSON] : - ((hasType(type_Animal, Var_PERSON) & hasType(type_Object, Var_PERSON)) => -(((f_wears(Var_PERSON,Var_SHOE)) => (( ? [Var_FOOT] : - (hasType(type_Foot, Var_FOOT) & -(((f_part(Var_FOOT,Var_PERSON)) & (f_meetsSpatially(Var_SHOE,Var_FOOT))))))))))))))). - -fof(axMidLem108, axiom, - ( ! [Var_SS] : - (hasType(type_ShoeSole, Var_SS) => -(( ? [Var_S] : - (hasType(type_Shoe, Var_S) & -(f_bottom(Var_SS,Var_S)))))))). - -fof(axMidLem109, axiom, - ( ! [Var_S] : - (hasType(type_Sandal, Var_S) => -(( ? [Var_SOLE] : - (hasType(type_ShoeSole, Var_SOLE) & -(((f_part(Var_SOLE,Var_S)) & (f_attribute(Var_SOLE,inst_Flat)))))))))). - -fof(axMidLem110, axiom, - ( ! [Var_S] : - (hasType(type_Sock, Var_S) => -(( ! [Var_P] : - ((hasType(type_Animal, Var_P) & hasType(type_Object, Var_P)) => -(((f_wears(Var_P,Var_S)) => (( ? [Var_F] : - (hasType(type_Foot, Var_F) & -(((f_part(Var_F,Var_P)) & (f_contains(Var_S,Var_F))))))))))))))). - -fof(axMidLem111, axiom, - ( ! [Var_S] : - (hasType(type_Sleeve, Var_S) => -(( ! [Var_P] : - ((hasType(type_Animal, Var_P) & hasType(type_Object, Var_P)) => -(((f_wears(Var_P,Var_S)) => (( ? [Var_A] : - (hasType(type_Arm, Var_A) & -(((f_part(Var_A,Var_P)) & (f_contains(Var_S,Var_A))))))))))))))). - -fof(axMidLem112, axiom, - ( ! [Var_S] : - (hasType(type_Sleeve, Var_S) => -(( ? [Var_C] : - ((hasType(type_Shirt, Var_C) | hasType(type_Coat, Var_C)) & -(f_part(Var_S,Var_C)))))))). - -fof(axMidLem113, axiom, - ( ! [Var_SUIT] : - (hasType(type_ClothingSuit, Var_SUIT) => -(( ! [Var_PERSON] : - (hasType(type_Animal, Var_PERSON) => -(( ! [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) => -(( ! [Var_ITEM1] : - ((hasType(type_SelfConnectedObject, Var_ITEM1) & hasType(type_Clothing, Var_ITEM1)) => -(((((f_member(Var_ITEM1,Var_SUIT)) & (f_holdsDuring(Var_TIME,wears(Var_PERSON,Var_ITEM1))))) => (( ! [Var_ITEM2] : - ((hasType(type_SelfConnectedObject, Var_ITEM2) & hasType(type_Clothing, Var_ITEM2)) => -(((f_member(Var_ITEM2,Var_SUIT)) => (f_holdsDuring(Var_TIME,wears(Var_PERSON,Var_ITEM2)))))))))))))))))))))). - -fof(axMidLem114, axiom, - ( ! [Var_LEATHER] : - (hasType(type_Leather, Var_LEATHER) => -(( ? [Var_MAKE] : - (hasType(type_Making, Var_MAKE) & -(( ? [Var_SKIN] : - (hasType(type_Skin, Var_SKIN) & -(((f_resourceS(Var_MAKE,Var_SKIN)) & (f_result(Var_MAKE,Var_LEATHER))))))))))))). - -fof(axMidLem115, axiom, - ( ! [Var_W] : - (hasType(type_Wool, Var_W) => -(( ? [Var_M] : - (hasType(type_Making, Var_M) & -(( ? [Var_H] : - (hasType(type_Hair, Var_H) & -(( ? [Var_S] : - (hasType(type_Sheep, Var_S) & -(((f_result(Var_M,Var_W)) & (((f_resourceS(Var_M,Var_H)) & (f_part(Var_H,Var_S)))))))))))))))))). - -fof(axMidLem116, axiom, - ( ! [Var_POCKET] : - (hasType(type_Pocket, Var_POCKET) => -(( ? [Var_CLOTHING] : - (hasType(type_Clothing, Var_CLOTHING) & -(f_part(Var_POCKET,Var_CLOTHING)))))))). - -fof(axMidLem117, axiom, - ( ! [Var_F] : - (hasType(type_CottonFabric, Var_F) => -(( ? [Var_M] : - (hasType(type_Making, Var_M) & -(( ? [Var_C] : - (hasType(type_Cotton, Var_C) & -(((f_resourceS(Var_M,Var_C)) & (f_result(Var_M,Var_F))))))))))))). - -fof(axMidLem118, axiom, - ( ! [Var_F] : - (hasType(type_CottonFabric, Var_F) => -(f_material(type_Cotton,Var_F))))). - -fof(axMidLem119, axiom, - ( ! [Var_CC] : - (hasType(type_ChangingClothing, Var_CC) => -(( ? [Var_R] : - (hasType(type_RemovingClothing, Var_R) & -(( ? [Var_D] : - (hasType(type_Dressing, Var_D) & -(((f_subProcess(Var_R,Var_CC)) & (f_subProcess(Var_D,Var_CC))))))))))))). - -fof(axMidLem120, axiom, - ( ! [Var_P] : - (hasType(type_Washing, Var_P) => -(( ? [Var_D] : - (hasType(type_Detergent, Var_D) & -(( ? [Var_W] : - (hasType(type_Water, Var_W) & -(((f_instrument(Var_P,Var_D)) & (f_instrument(Var_P,Var_W))))))))))))). - -fof(axMidLem121, axiom, - ( ! [Var_S] : - (hasType(type_Sewing, Var_S) => -(( ? [Var_F] : - (hasType(type_Fabric, Var_F) & -(f_patient(Var_S,Var_F)))))))). - -fof(axMidLem122, axiom, - ( ! [Var_S] : - (hasType(type_Soldering, Var_S) => -(( ! [Var_OBJ2] : - ((hasType(type_Entity, Var_OBJ2) & hasType(type_SelfConnectedObject, Var_OBJ2)) => -(( ! [Var_OBJ1] : - ((hasType(type_Entity, Var_OBJ1) & hasType(type_SelfConnectedObject, Var_OBJ1)) => -(((((f_patient(Var_S,Var_OBJ1)) & (((f_patient(Var_S,Var_OBJ2)) & (Var_OBJ1 != Var_OBJ2))))) => (( ? [Var_A] : - (hasType(type_MetallicAlloy, Var_A) & -(f_connects(Var_A,Var_OBJ1,Var_OBJ2)))))))))))))))). - -fof(axMidLem123, axiom, - ( ! [Var_DOCTOR] : - ((hasType(type_CognitiveAgent, Var_DOCTOR) & hasType(type_Agent, Var_DOCTOR)) => -(( ! [Var_PATIENT] : - ((hasType(type_Human, Var_PATIENT) & hasType(type_Entity, Var_PATIENT)) => -(((f_patientMedical(Var_PATIENT,Var_DOCTOR)) => (( ? [Var_PROCESS] : - ((hasType(type_DiagnosticProcess, Var_PROCESS) | hasType(type_TherapeuticProcess, Var_PROCESS)) & -(((f_patient(Var_PROCESS,Var_PATIENT)) & (f_agent(Var_PROCESS,Var_DOCTOR))))))))))))))). - -fof(axMidLem124, axiom, - ( ! [Var_I] : - (hasType(type_InfectiousDisease, Var_I) => -(( ! [Var_O] : - (hasType(type_Microorganism, Var_O) => -(( ! [Var_A] : - ((hasType(type_Object, Var_A) & hasType(type_Entity, Var_A)) => -(((f_attribute(Var_A,Var_I)) => (( ? [Var_P] : - (hasType(type_PathologicProcess, Var_P) & -(((f_agent(Var_P,Var_O)) & (f_experiencer(Var_P,Var_A)))))))))))))))))). - -fof(axMidLem125, axiom, - ( ! [Var_H] : - (hasType(type_Object, Var_H) => -(((f_attribute(Var_H,inst_Emphysema)) => (( ? [Var_L] : - (hasType(type_Lung, Var_L) & -(( ? [Var_P] : - (hasType(type_PathologicProcess, Var_P) & -(((f_part(Var_L,Var_H)) & (f_located(Var_P,Var_L))))))))))))))). - -fof(axMidLem126, axiom, - ( ! [Var_H] : - (hasType(type_Human, Var_H) => -(((f_attribute(Var_H,inst_Fever)) => (( ? [Var_N] : - ((hasType(type_RealNumber, Var_N) & hasType(type_Quantity, Var_N)) & -(((f_measure(Var_H,f_MeasureFn(Var_N,inst_FahrenheitDegree))) & (f_greaterThan(Var_N,98.6)))))))))))). - -fof(axMidLem127, axiom, - ( ! [Var_H] : - (hasType(type_Object, Var_H) => -(((f_attribute(Var_H,inst_Goiter)) => (( ? [Var_G] : - (hasType(type_ThyroidGland, Var_G) & -(( ? [Var_P] : - (hasType(type_PathologicProcess, Var_P) & -(((f_part(Var_G,Var_H)) & (f_located(Var_P,Var_G))))))))))))))). - -fof(axMidLem128, axiom, - ( ! [Var_O2] : - ((hasType(type_Organism, Var_O2) & hasType(type_Object, Var_O2)) => -(( ! [Var_O1] : - (hasType(type_Organism, Var_O1) => -(((f_parasite(Var_O1,Var_O2)) => (f_inhabits(Var_O1,Var_O2)))))))))). - -fof(axMidLem129, axiom, - ( ! [Var_O2] : - ((hasType(type_Organism, Var_O2) & hasType(type_Entity, Var_O2)) => -(( ! [Var_O1] : - ((hasType(type_Organism, Var_O1) & hasType(type_Agent, Var_O1)) => -(((f_parasite(Var_O1,Var_O2)) => (( ? [Var_I] : - (hasType(type_Injuring, Var_I) & -(((f_agent(Var_I,Var_O1)) & (f_patient(Var_I,Var_O2))))))))))))))). - -fof(axMidLem130, axiom, - ( ! [Var_PERSON] : - (hasType(type_Object, Var_PERSON) => -(((f_attribute(Var_PERSON,inst_Cancer)) => (( ? [Var_TUMOR] : - (hasType(type_Tumor, Var_TUMOR) & -(f_part(Var_TUMOR,Var_PERSON)))))))))). - -fof(axMidLem131, axiom, - ( ! [Var_CS] : - (hasType(type_ConjugatedSubstance, Var_CS) => -(( ? [Var_C1] : - (hasType(type_CompoundSubstance, Var_C1) & -(( ? [Var_C2] : - (hasType(type_CompoundSubstance, Var_C2) & -(( ? [Var_P] : - (hasType(type_ChemicalSynthesis, Var_P) & -(((Var_C1 != Var_C2) & (((f_resourceS(Var_P,Var_C1)) & (((f_resourceS(Var_P,Var_C2)) & (f_result(Var_P,Var_CS)))))))))))))))))))). - -fof(axMidLem132, axiom, - ( ! [Var_COMPOUND2] : - ((hasType(type_CompoundSubstance, Var_COMPOUND2) & hasType(type_PureSubstance, Var_COMPOUND2)) => -(( ! [Var_COMPOUND1] : - ((hasType(type_CompoundSubstance, Var_COMPOUND1) & hasType(type_PureSubstance, Var_COMPOUND1)) => -(((f_conjugate(Var_COMPOUND1,Var_COMPOUND2)) => (( ? [Var_NUMBER2] : - ((hasType(type_PositiveInteger, Var_NUMBER2) & hasType(type_Quantity, Var_NUMBER2) & hasType(type_Entity, Var_NUMBER2)) & -(( ? [Var_NUMBER1] : - ((hasType(type_PositiveInteger, Var_NUMBER1) & hasType(type_Entity, Var_NUMBER1) & hasType(type_Quantity, Var_NUMBER1)) & -(((f_protonNumber(Var_COMPOUND1,Var_NUMBER1)) & (((f_protonNumber(Var_COMPOUND2,Var_NUMBER2)) & (((Var_NUMBER1 = f_AdditionFn(Var_NUMBER2,1)) | (Var_NUMBER2 = f_AdditionFn(Var_NUMBER1,1)))))))))))))))))))))). - -fof(axMidLem133, axiom, - ( ! [Var_BITE] : - (hasType(type_Biting, Var_BITE) => -(( ! [Var_ANIMAL] : - ((hasType(type_Agent, Var_ANIMAL) & hasType(type_Object, Var_ANIMAL)) => -(((f_agent(Var_BITE,Var_ANIMAL)) => (( ? [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) & -(((f_part(Var_MOUTH,Var_ANIMAL)) & (f_instrument(Var_BITE,Var_MOUTH))))))))))))))). - -fof(axMidLem134, axiom, - ( ! [Var_S] : - (hasType(type_Strangling, Var_S) => -(( ? [Var_T] : - (hasType(type_Throat, Var_T) & -(f_patient(Var_S,Var_T)))))))). - -fof(axMidLem135, axiom, - ( ! [Var_SPIT] : - (hasType(type_Spitting, Var_SPIT) => -(( ! [Var_ANIMAL] : - ((hasType(type_Agent, Var_ANIMAL) & hasType(type_Object, Var_ANIMAL)) => -(((f_agent(Var_SPIT,Var_ANIMAL)) => (( ? [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) & -(((f_part(Var_MOUTH,Var_ANIMAL)) & (f_origin(Var_SPIT,Var_MOUTH))))))))))))))). - -fof(axMidLem136, axiom, - ( ! [Var_P] : - (hasType(type_Punching, Var_P) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Object, Var_A)) => -(((f_agent(Var_P,Var_A)) => (( ? [Var_H] : - (hasType(type_Hand, Var_H) & -(((f_attribute(Var_H,inst_Fist)) & (((f_part(Var_H,Var_A)) & (f_instrument(Var_P,Var_H))))))))))))))))). - -fof(axMidLem137, axiom, - ( ! [Var_KICK] : - (hasType(type_Kicking, Var_KICK) => -(( ! [Var_ANIMAL] : - ((hasType(type_Agent, Var_ANIMAL) & hasType(type_Object, Var_ANIMAL)) => -(((f_agent(Var_KICK,Var_ANIMAL)) => (( ? [Var_FOOT] : - (hasType(type_Foot, Var_FOOT) & -(((f_part(Var_FOOT,Var_ANIMAL)) & (f_instrument(Var_KICK,Var_FOOT))))))))))))))). - -fof(axMidLem138, axiom, - ( ! [Var_MESSAGING] : - (hasType(type_Messaging, Var_MESSAGING) => -(( ? [Var_M] : - (hasType(type_Message, Var_M) & -(f_patient(Var_MESSAGING,Var_M)))))))). - -fof(axMidLem139, axiom, - ( ! [Var_PERSON2] : - (hasType(type_Human, Var_PERSON2) => -(( ! [Var_PERSON1] : - (hasType(type_Human, Var_PERSON1) => -(((f_neighbor(Var_PERSON1,Var_PERSON2)) => (( ? [Var_HOME2] : - ((hasType(type_PermanentResidence, Var_HOME2) & hasType(type_Entity, Var_HOME2) & hasType(type_Object, Var_HOME2)) & -(( ? [Var_HOME1] : - ((hasType(type_PermanentResidence, Var_HOME1) & hasType(type_Entity, Var_HOME1) & hasType(type_Object, Var_HOME1)) & -(((f_home(Var_PERSON1,Var_HOME1)) & (((f_home(Var_PERSON2,Var_HOME2)) & (((Var_HOME1 != Var_HOME2) & (f_orientation(Var_HOME1,Var_HOME2,inst_Near)))))))))))))))))))))). - -fof(axMidLem140, axiom, - ( ! [Var_OBJ2] : - (hasType(type_SelfConnectedObject, Var_OBJ2) => -(( ! [Var_MEAS] : - ((hasType(type_PhysicalQuantity, Var_MEAS) & hasType(type_ConstantQuantity, Var_MEAS)) => -(( ! [Var_OBJ1] : - (hasType(type_Object, Var_OBJ1) => -(((((f_measure(Var_OBJ1,Var_MEAS)) & (f_contains(Var_OBJ2,Var_OBJ1)))) => (f_capacity(Var_OBJ2,Var_MEAS))))))))))))). - -fof(axMidLem141, axiom, - ( ! [Var_ITEM] : - (hasType(type_Entity, Var_ITEM) => -(( ! [Var_LIST] : - (hasType(type_List, Var_LIST) => -(((f_LastFn(Var_LIST) = Var_ITEM) <=> (( ? [Var_NUMBER] : - ((hasType(type_Entity, Var_NUMBER) & hasType(type_PositiveInteger, Var_NUMBER)) & -(((f_ListLengthFn(Var_LIST) = Var_NUMBER) & (f_ListOrderFn(Var_LIST,Var_NUMBER) = Var_ITEM)))))))))))))). - -fof(axMidLem142, axiom, - ( ! [Var_LIST] : - (hasType(type_List, Var_LIST) => -(((Var_LIST != inst_NullList) => (f_FirstFn(Var_LIST) = f_ListOrderFn(Var_LIST,1))))))). - -fof(axMidLem143, axiom, - ( ! [Var_AGENT] : - ((hasType(type_Entity, Var_AGENT) & hasType(type_Agent, Var_AGENT)) => -(( ! [Var_COUNTRY] : - (hasType(type_Nation, Var_COUNTRY) => -(( ! [Var_CITY] : - (hasType(type_City, Var_CITY) => -(( ! [Var_ROAD] : - (hasType(type_Roadway, Var_ROAD) => -(( ! [Var_PLACE] : - ((hasType(type_StationaryArtifact, Var_PLACE) & hasType(type_Address, Var_PLACE)) => -(((f_StreetAddressFn(Var_PLACE,Var_ROAD,Var_CITY,Var_COUNTRY) = Var_AGENT) => (f_address(Var_AGENT,Var_PLACE))))))))))))))))))). - -fof(axMidLem144, axiom, - ( ! [Var_AGENT] : - (hasType(type_Entity, Var_AGENT) => -(( ! [Var_COUNTRY] : - (hasType(type_Nation, Var_COUNTRY) => -(( ! [Var_CITY] : - (hasType(type_City, Var_CITY) => -(( ! [Var_ROAD] : - (hasType(type_Roadway, Var_ROAD) => -(( ! [Var_PLACE] : - ((hasType(type_StationaryArtifact, Var_PLACE) & hasType(type_Object, Var_PLACE)) => -(((f_StreetAddressFn(Var_PLACE,Var_ROAD,Var_CITY,Var_COUNTRY) = Var_AGENT) => (( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(f_part(Var_PLACE,Var_BUILDING)))))))))))))))))))))). - -fof(axMidLem145, axiom, - ( ! [Var_P] : - (hasType(type_VotingPoll, Var_P) => -(( ? [Var_V] : - (hasType(type_Voting, Var_V) & -(f_located(Var_V,Var_P)))))))). - -fof(axMidLem146, axiom, - ( ! [Var_CAMP] : - (hasType(type_Camp, Var_CAMP) => -(( ? [Var_TENT] : - (hasType(type_Tent, Var_TENT) & -(f_part(Var_TENT,Var_CAMP)))))))). - -fof(axMidLem147, axiom, - ( ! [Var_TENT] : - (hasType(type_Tent, Var_TENT) => -(( ? [Var_FABRIC] : - (hasType(type_Fabric, Var_FABRIC) & -(f_part(Var_FABRIC,Var_TENT)))))))). - -fof(axMidLem148, axiom, - ( ! [Var_RESIDENCE] : - (hasType(type_ExecutiveResidence, Var_RESIDENCE) => -(( ? [Var_PERSON] : - (hasType(type_Human, Var_PERSON) & -(( ? [Var_POSITION] : - (hasType(type_Position, Var_POSITION) & -(( ? [Var_AREA] : - ((hasType(type_Object, Var_AREA) & hasType(type_GeopoliticalArea, Var_AREA)) & -(((f_located(Var_RESIDENCE,Var_AREA)) & (((f_home(Var_PERSON,Var_RESIDENCE)) & (f_chiefOfState(Var_AREA,Var_POSITION,Var_PERSON)))))))))))))))))). - -fof(axMidLem149, axiom, - ( ! [Var_UNIT] : - (hasType(type_ApartmentUnit, Var_UNIT) => -(( ! [Var_PERSON] : - ((hasType(type_Human, Var_PERSON) & hasType(type_Agent, Var_PERSON)) => -(((f_home(Var_PERSON,Var_UNIT)) => (( ~ (f_possesses(Var_PERSON,Var_UNIT)))))))))))). - -fof(axMidLem150, axiom, - ( ! [Var_UNIT] : - (hasType(type_ApartmentUnit, Var_UNIT) => -(( ? [Var_BUILDING] : - (hasType(type_ApartmentBuilding, Var_BUILDING) & -(f_part(Var_UNIT,Var_BUILDING)))))))). - -fof(axMidLem151, axiom, - ( ! [Var_U] : - ((hasType(type_PermanentResidence, Var_U) & hasType(type_Object, Var_U) & hasType(type_Residence, Var_U) & hasType(type_Entity, Var_U)) => -(( ! [Var_L] : - (hasType(type_Agent, Var_L) => -(((f_landlord(Var_L,Var_U)) => (( ? [Var_R] : - (hasType(type_Renting, Var_R) & -(( ? [Var_P] : - (hasType(type_Agent, Var_P) & -(((f_possesses(Var_L,Var_U)) & (((f_tenant(Var_P,Var_U)) & (((f_agent(Var_R,Var_P)) & (f_patient(Var_R,Var_U)))))))))))))))))))))). - -fof(axMidLem152, axiom, - ( ! [Var_U] : - ((hasType(type_Residence, Var_U) & hasType(type_PermanentResidence, Var_U) & hasType(type_Object, Var_U) & hasType(type_Entity, Var_U)) => -(( ! [Var_P] : - (hasType(type_Agent, Var_P) => -(((f_tenant(Var_P,Var_U)) => (( ? [Var_R] : - (hasType(type_Renting, Var_R) & -(( ? [Var_L] : - (hasType(type_Agent, Var_L) & -(((f_landlord(Var_L,Var_U)) & (((f_agent(Var_R,Var_P)) & (((f_possesses(Var_L,Var_U)) & (f_patient(Var_R,Var_U)))))))))))))))))))))). - -fof(axMidLem153, axiom, - ( ! [Var_UNIT] : - (hasType(type_CondominiumUnit, Var_UNIT) => -(( ? [Var_BUILDING] : - (hasType(type_CondominiumBuilding, Var_BUILDING) & -(f_part(Var_UNIT,Var_BUILDING)))))))). - -fof(axMidLem154, axiom, - ( ! [Var_BUILDING] : - (hasType(type_ApartmentBuilding, Var_BUILDING) => -(( ? [Var_UNIT1] : - (hasType(type_ApartmentUnit, Var_UNIT1) & -(( ? [Var_UNIT2] : - (hasType(type_ApartmentUnit, Var_UNIT2) & -(((f_part(Var_UNIT1,Var_BUILDING)) & (((f_part(Var_UNIT2,Var_BUILDING)) & (Var_UNIT1 != Var_UNIT2)))))))))))))). - -fof(axMidLem155, axiom, - ( ! [Var_BUILDING] : - (hasType(type_CondominiumBuilding, Var_BUILDING) => -(( ? [Var_UNIT1] : - (hasType(type_CondominiumUnit, Var_UNIT1) & -(( ? [Var_UNIT2] : - (hasType(type_CondominiumUnit, Var_UNIT2) & -(((f_part(Var_UNIT1,Var_BUILDING)) & (((f_part(Var_UNIT2,Var_BUILDING)) & (Var_UNIT1 != Var_UNIT2)))))))))))))). - -fof(axMidLem156, axiom, - ( ! [Var_D] : - (hasType(type_Dormitory, Var_D) => -(( ? [Var_S] : - (hasType(type_School, Var_S) & -(f_possesses(Var_S,Var_D)))))))). - -fof(axMidLem157, axiom, - ( ! [Var_B] : - (hasType(type_FarmBuilding, Var_B) => -(( ? [Var_F] : - (hasType(type_Farm, Var_F) & -(f_located(Var_B,Var_F)))))))). - -fof(axMidLem158, axiom, - ( ! [Var_C] : - (hasType(type_EntertainmentCompany, Var_C) => -(( ? [Var_P] : - ((hasType(type_CommercialService, Var_P) & hasType(type_Performance, Var_P)) & -(f_agent(Var_P,Var_C)))))))). - -fof(axMidLem159, axiom, - ( ! [Var_I] : - (hasType(type_InsuranceCompany, Var_I) => -(( ? [Var_C] : - (hasType(type_Contract, Var_C) & -(f_insured(Var_C,Var_I)))))))). - -fof(axMidLem160, axiom, - ( ! [Var_S] : - (hasType(type_FinancialService, Var_S) => -(( ? [Var_O] : - (hasType(type_FinancialCompany, Var_O) & -(f_agent(Var_S,Var_O)))))))). - -fof(axMidLem161, axiom, - ( ! [Var_C] : - (hasType(type_Partnership, Var_C) => -(( ? [Var_H1] : - (hasType(type_Human, Var_H1) & -(( ? [Var_H2] : - (hasType(type_Human, Var_H2) & -(((Var_H1 != Var_H2) & (((f_possesses(Var_H1,Var_C)) & (f_possesses(Var_H2,Var_C))))))))))))))). - -fof(axMidLem162, axiom, - ( ! [Var_W] : - (hasType(type_Welfare, Var_W) => -(( ? [Var_O] : - (hasType(type_ServiceOrganization, Var_O) & -(f_agent(Var_W,Var_O)))))))). - -fof(axMidLem163, axiom, - ( ! [Var_C] : - (hasType(type_Publisher, Var_C) => -(( ? [Var_S] : - ((hasType(type_CommercialService, Var_S) & hasType(type_Publication, Var_S)) & -(f_agent(Var_S,Var_C)))))))). - -fof(axMidLem164, axiom, - ( ! [Var_C] : - (hasType(type_FamilyBusiness, Var_C) => -(( ! [Var_P2] : - ((hasType(type_Agent, Var_P2) & hasType(type_Organism, Var_P2)) => -(( ! [Var_P1] : - ((hasType(type_Agent, Var_P1) & hasType(type_Organism, Var_P1)) => -(((((f_possesses(Var_P1,Var_C)) & (f_possesses(Var_P2,Var_C)))) => (f_familyRelation(Var_P1,Var_P2))))))))))))). - -fof(axMidLem165, axiom, - ( ! [Var_C] : - (hasType(type_Restaurant, Var_C) => -(( ? [Var_S] : - ((hasType(type_CommercialService, Var_S) & hasType(type_Selling, Var_S)) & -(( ? [Var_F] : - (hasType(type_Food, Var_F) & -(( ? [Var_B] : - (hasType(type_RestaurantBuilding, Var_B) & -(((f_agent(Var_S,Var_C)) & (((f_located(Var_S,Var_B)) & (f_patient(Var_S,Var_F)))))))))))))))))). - -fof(axMidLem166, axiom, - ( ! [Var_C] : - (hasType(type_Proprietorship, Var_C) => -(( ? [Var_H] : - (hasType(type_Human, Var_H) & -(((f_possesses(Var_H,Var_C)) & (( ~ ( ? [Var_H2] : - ((hasType(type_Entity, Var_H2) & hasType(type_Agent, Var_H2)) & -(((Var_H != Var_H2) & (f_possesses(Var_H2,Var_C)))))))))))))))). - -fof(axMidLem167, axiom, - ( ! [Var_AUDITORIUM] : - (hasType(type_Auditorium, Var_AUDITORIUM) => -(( ? [Var_STAGE] : - (hasType(type_PerformanceStage, Var_STAGE) & -(f_part(Var_STAGE,Var_AUDITORIUM)))))))). - -fof(axMidLem168, axiom, - ( ! [Var_SEAT] : - (hasType(type_AuditoriumSeat, Var_SEAT) => -(( ? [Var_AUDITORIUM] : - (hasType(type_Auditorium, Var_AUDITORIUM) & -(f_part(Var_SEAT,Var_AUDITORIUM)))))))). - -fof(axMidLem169, axiom, - ( ! [Var_PERSON] : - (hasType(type_Human, Var_PERSON) => -(( ! [Var_DESCENDANTS] : - ((hasType(type_Entity, Var_DESCENDANTS) & hasType(type_Collection, Var_DESCENDANTS)) => -(((f_DescendantsFn(Var_PERSON) = Var_DESCENDANTS) => (( ! [Var_MEMBER] : - ((hasType(type_SelfConnectedObject, Var_MEMBER) & hasType(type_Organism, Var_MEMBER)) => -(((f_member(Var_MEMBER,Var_DESCENDANTS)) <=> (f_ancestor(Var_MEMBER,Var_PERSON))))))))))))))). - -fof(axMidLem170, axiom, - ( ! [Var_BROOD] : - (hasType(type_Brood, Var_BROOD) => -(( ! [Var_MEMBER2] : - ((hasType(type_SelfConnectedObject, Var_MEMBER2) & hasType(type_Organism, Var_MEMBER2)) => -(( ! [Var_MEMBER1] : - ((hasType(type_SelfConnectedObject, Var_MEMBER1) & hasType(type_Organism, Var_MEMBER1)) => -(((((f_member(Var_MEMBER1,Var_BROOD)) & (f_member(Var_MEMBER2,Var_BROOD)))) => (f_sibling(Var_MEMBER1,Var_MEMBER2))))))))))))). - -fof(axMidLem171, axiom, - ( ! [Var_BROOD] : - (hasType(type_Brood, Var_BROOD) => -(( ? [Var_TIME] : - (hasType(type_Entity, Var_TIME) & -(( ! [Var_MEMBER] : - ((hasType(type_SelfConnectedObject, Var_MEMBER) & hasType(type_Entity, Var_MEMBER)) => -(((f_member(Var_MEMBER,Var_BROOD)) => (( ? [Var_BIRTH] : - (hasType(type_Birth, Var_BIRTH) & -(((f_experiencer(Var_BIRTH,Var_MEMBER)) & (Var_TIME = f_WhenFn(Var_BIRTH)))))))))))))))))). - -fof(axMidLem172, axiom, - ( ! [Var_AT] : - (hasType(type_AnimalTeam, Var_AT) => -(( ? [Var_P] : - (hasType(type_Pulling, Var_P) & -(f_agent(Var_P,Var_AT)))))))). - -fof(axMidLem173, axiom, - ( ! [Var_S] : - (hasType(type_TeamSport, Var_S) => -(( ? [Var_T1] : - (hasType(type_SportsTeam, Var_T1) & -(( ? [Var_T2] : - (hasType(type_SportsTeam, Var_T2) & -(((f_contestParticipant(Var_S,Var_T1)) & (((f_contestParticipant(Var_S,Var_T2)) & (Var_T1 != Var_T2)))))))))))))). - -fof(axMidLem174, axiom, - ( ! [Var_CO] : - (hasType(type_CommunicationOrganization, Var_CO) => -(( ? [Var_CS] : - (hasType(type_CommunicationSystem, Var_CS) & -(( ? [Var_C] : - (hasType(type_Communication, Var_C) & -(((f_instrument(Var_C,Var_CS)) & (f_agent(Var_C,Var_CO))))))))))))). - -fof(axMidLem175, axiom, - ( ! [Var_COMPANY] : - (hasType(type_Tavern, Var_COMPANY) => -(( ? [Var_SERVICE] : - ((hasType(type_CommercialService, Var_SERVICE) & hasType(type_Selling, Var_SERVICE)) & -(( ? [Var_BEVERAGE] : - (hasType(type_AlcoholicBeverage, Var_BEVERAGE) & -(((f_agent(Var_SERVICE,Var_COMPANY)) & (f_patient(Var_SERVICE,Var_BEVERAGE))))))))))))). - -fof(axMidLem176, axiom, - ( ! [Var_D] : - (hasType(type_DrugStore, Var_D) => -(( ! [Var_M] : - (hasType(type_Medicine, Var_M) => -(( ? [Var_S] : - (hasType(type_Selling, Var_S) & -(((f_agent(Var_S,Var_D)) & (f_patient(Var_S,Var_M))))))))))))). - -fof(axMidLem177, axiom, - ( ! [Var_STORE] : - (hasType(type_GroceryStore, Var_STORE) => -(( ? [Var_SELL] : - (hasType(type_Selling, Var_SELL) & -(( ? [Var_FOOD] : - (hasType(type_Food, Var_FOOD) & -(((f_agent(Var_SELL,Var_STORE)) & (f_patient(Var_SELL,Var_FOOD))))))))))))). - -fof(axMidLem178, axiom, - ( ! [Var_SALE] : - (hasType(type_BargainSale, Var_SALE) => -(( ! [Var_OBJ] : - (hasType(type_Object, Var_OBJ) => -(((f_patient(Var_SALE,Var_OBJ)) => (( ? [Var_AGENT2] : - (hasType(type_Agent, Var_AGENT2) & -(( ? [Var_AGENT1] : - (hasType(type_Agent, Var_AGENT1) & -(( ? [Var_PRICE2] : - ((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) & -(( ? [Var_PRICE1] : - ((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) & -(((f_holdsDuring(f_ImmediatePastFn(f_WhenFn(Var_SALE)),price(Var_OBJ,Var_PRICE1,Var_AGENT1))) & (((f_holdsDuring(f_WhenFn(Var_SALE),price(Var_OBJ,Var_PRICE2,Var_AGENT2))) & (f_lessThan(Var_PRICE2,Var_PRICE1)))))))))))))))))))))))))). - -fof(axMidLem179, axiom, - ( ~ (f_overlapsTemporally(inst_CommonEra,inst_BeforeCommonEra)))). - -fof(axMidLem180, axiom, - ( ! [Var_STEEPLE] : - (hasType(type_Steeple, Var_STEEPLE) => -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(f_part(Var_STEEPLE,Var_BUILDING)))))))). - -fof(axMidLem181, axiom, - ( ! [Var_P] : - (hasType(type_CommunistParty, Var_P) => -(( ! [Var_A] : - (hasType(type_GeopoliticalArea, Var_A) => -(( ! [Var_M] : - ((hasType(type_SelfConnectedObject, Var_M) & hasType(type_CognitiveAgent, Var_M)) => -(((f_member(Var_M,Var_P)) => (f_desires(Var_M,governmentType(Var_A,inst_CommunistState)))))))))))))). - -fof(axMidLem182, axiom, - ( ! [Var_AREA] : - ((hasType(type_GeopoliticalArea, Var_AREA) & hasType(type_PermanentResidence, Var_AREA)) => -(( ! [Var_PERSON] : - ((hasType(type_SelfConnectedObject, Var_PERSON) & hasType(type_Human, Var_PERSON)) => -(((f_member(Var_PERSON,f_ResidentFn(Var_AREA))) => (f_home(Var_PERSON,Var_AREA)))))))))). - -fof(axMidLem183, axiom, - ( ! [Var_AREA] : - (hasType(type_GeopoliticalArea, Var_AREA) => -(( ! [Var_POPULATION] : - ((hasType(type_Entity, Var_POPULATION) & (hasType(type_SetOrClass, Var_POPULATION) | hasType(type_Collection, Var_POPULATION))) => -(( ! [Var_CITIZENRY] : - ((hasType(type_Entity, Var_CITIZENRY) & (hasType(type_SetOrClass, Var_CITIZENRY) | hasType(type_Collection, Var_CITIZENRY))) => -(((((Var_CITIZENRY = f_CitizenryFn(Var_AREA)) & (Var_POPULATION = f_ResidentFn(Var_AREA)))) => (f_greaterThanOrEqualTo(f_CardinalityFn(Var_POPULATION),f_CardinalityFn(Var_CITIZENRY)))))))))))))). - -fof(axMidLem184, axiom, - ( ! [Var_DISTRICT] : - (hasType(type_CityDistrict, Var_DISTRICT) => -(( ? [Var_CITY] : - (hasType(type_City, Var_CITY) & -(f_geopoliticalSubdivision(Var_DISTRICT,Var_CITY)))))))). - -fof(axMidLem185, axiom, - ( ! [Var_C] : - (hasType(type_Cemetery, Var_C) => -(( ? [Var_T] : - (hasType(type_Tomb, Var_T) & -(f_located(Var_T,Var_C)))))))). - -fof(axMidLem186, axiom, - ( ! [Var_PARK] : - (hasType(type_Park, Var_PARK) => -(( ? [Var_GOV] : - (hasType(type_Government, Var_GOV) & -(f_possesses(Var_GOV,Var_PARK)))))))). - -fof(axMidLem187, axiom, - ( ! [Var_P] : - (hasType(type_PublicPark, Var_P) => -(( ? [Var_G] : - (hasType(type_Government, Var_G) & -(f_possesses(Var_G,Var_P)))))))). - -fof(axMidLem188, axiom, - ( ! [Var_A] : - (hasType(type_CultivatedLandArea, Var_A) => -(( ? [Var_C] : - (hasType(type_Agriculture, Var_C) & -(f_located(Var_C,Var_A)))))))). - -fof(axMidLem189, axiom, - ( ! [Var_B] : - (hasType(type_CityBlock, Var_B) => -(( ? [Var_C] : - (hasType(type_City, Var_C) & -(f_part(Var_B,Var_C)))))))). - -fof(axMidLem190, axiom, - ( ! [Var_PERSON] : - (hasType(type_Human, Var_PERSON) => -(((f_occupiesPosition(Var_PERSON,inst_SecretaryOfTheInterior,inst_UnitedStatesDepartmentOfInterior)) => (f_leader(inst_UnitedStatesDepartmentOfInterior,Var_PERSON))))))). - -fof(axMidLem191, axiom, - ( ! [Var_GOVERNMENT] : - (hasType(type_StateGovernment, Var_GOVERNMENT) => -(( ? [Var_STATE] : - (hasType(type_StateOrProvince, Var_STATE) & -(f_GovernmentFn(Var_STATE) = Var_GOVERNMENT))))))). - -fof(axMidLem192, axiom, - ( ! [Var_B] : - (hasType(type_Battle, Var_B) => -(( ? [Var_U1] : - (hasType(type_MilitaryUnit, Var_U1) & -(( ? [Var_U2] : - (hasType(type_MilitaryUnit, Var_U2) & -(((Var_U1 != Var_U2) & (((f_agent(Var_B,Var_U1)) & (f_agent(Var_B,Var_U2))))))))))))))). - -fof(axMidLem193, axiom, - ( ! [Var_WAR] : - (hasType(type_War, Var_WAR) => -(( ! [Var_U2] : - ((hasType(type_MilitaryUnit, Var_U2) & hasType(type_Organization, Var_U2)) => -(( ! [Var_U1] : - ((hasType(type_MilitaryUnit, Var_U1) & hasType(type_Organization, Var_U1)) => -(((f_hostileForces(Var_U1,Var_U2)) => (( ? [Var_A2] : - ((hasType(type_Agent, Var_A2) & hasType(type_GeopoliticalArea, Var_A2)) & -(( ? [Var_A1] : - ((hasType(type_Agent, Var_A1) & hasType(type_GeopoliticalArea, Var_A1)) & -(( ? [Var_W] : - (hasType(type_Contest, Var_W) & -(((f_contestParticipant(Var_W,Var_A1)) & (((f_contestParticipant(Var_W,Var_A2)) & (((f_subOrganization(Var_U1,f_GovernmentFn(Var_A1))) & (f_subOrganization(Var_U2,f_GovernmentFn(Var_A2))))))))))))))))))))))))))))). - -fof(axMidLem194, axiom, - ( ! [Var_ORG] : - (hasType(type_ServiceOrganization, Var_ORG) => -(( ? [Var_PROC] : - (hasType(type_RegulatoryProcess, Var_PROC) & -(( ? [Var_GOV] : - (hasType(type_Government, Var_GOV) & -(((f_patient(Var_PROC,Var_ORG)) & (f_agent(Var_PROC,Var_GOV))))))))))))). - -fof(axMidLem195, axiom, - ( ! [Var_L] : - (hasType(type_Library, Var_L) => -(( ? [Var_B] : - (hasType(type_Building, Var_B) & -(( ? [Var_T] : - (hasType(type_Text, Var_T) & -(((f_possesses(Var_L,Var_B)) & (f_located(Var_T,Var_B))))))))))))). - -fof(axMidLem196, axiom, - ( ! [Var_BOARD] : - (hasType(type_OrganizationalBoard, Var_BOARD) => -(( ? [Var_MANAGE] : - (hasType(type_Managing, Var_MANAGE) & -(( ? [Var_ORG] : - ((hasType(type_Organization, Var_ORG) & hasType(type_Entity, Var_ORG)) & -(((f_subOrganization(Var_BOARD,Var_ORG)) & (((f_agent(Var_MANAGE,Var_BOARD)) & (f_patient(Var_MANAGE,Var_ORG))))))))))))))). - -fof(axMidLem197, axiom, - ( ! [Var_ORG] : - (hasType(type_UnionOrganization, Var_ORG) => -(( ! [Var_MEMBER] : - ((hasType(type_SelfConnectedObject, Var_MEMBER) & hasType(type_CognitiveAgent, Var_MEMBER)) => -(( ? [Var_COLL] : - ((hasType(type_Corporation, Var_COLL) & hasType(type_Industry, Var_COLL)) & -(((f_member(Var_MEMBER,Var_ORG)) => (((f_employs(Var_COLL,Var_MEMBER)) | (( ? [Var_CORP] : - ((hasType(type_SelfConnectedObject, Var_CORP) & hasType(type_Organization, Var_CORP)) & -(((f_member(Var_CORP,Var_COLL)) & (f_employs(Var_CORP,Var_MEMBER)))))))))))))))))))). - -fof(axMidLem198, axiom, - ( ! [Var_S] : - (hasType(type_Hydrocarbon, Var_S) => -(( ? [Var_P1] : - (hasType(type_Carbon, Var_P1) & -(( ? [Var_P2] : - (hasType(type_Hydrogen, Var_P2) & -(Var_S = f_MereologicalSumFn(Var_P1,Var_P2))))))))))). - -fof(axMidLem199, axiom, - ( ! [Var_A] : - (hasType(type_Alkaloid, Var_A) => -(( ? [Var_N] : - (hasType(type_Nitrogen, Var_N) & -(f_part(Var_N,Var_A)))))))). - -fof(axMidLem200, axiom, - ( ! [Var_P] : - (hasType(type_Protein, Var_P) => -(( ? [Var_A] : - (hasType(type_AminoAcid, Var_A) & -(f_part(Var_A,Var_P)))))))). - -fof(axMidLem201, axiom, - ( ! [Var_S] : - (hasType(type_Cholesterol, Var_S) => -(( ? [Var_P] : - (hasType(type_BiologicalProcess, Var_P) & -(( ? [Var_L] : - (hasType(type_Liver, Var_L) & -(((f_located(Var_P,Var_L)) & (f_result(Var_P,Var_S))))))))))))). - -fof(axMidLem202, axiom, - ( ! [Var_CA] : - (hasType(type_ChemicalAcid, Var_CA) => -(( ! [Var_CB] : - (hasType(type_ChemicalBase, Var_CB) => -(( ! [Var_C] : - (hasType(type_ChemicalProcess, Var_C) => -(((((f_patient(Var_C,Var_CA)) & (f_patient(Var_C,Var_CB)))) => (( ? [Var_CS] : - (hasType(type_ChemicalSalt, Var_CS) & -(f_result(Var_C,Var_CS)))))))))))))))). - -fof(axMidLem203, axiom, - ( ! [Var_SALT] : - (hasType(type_SodiumChloride, Var_SALT) => -(( ? [Var_SYNTHESIS] : - (hasType(type_ChemicalSynthesis, Var_SYNTHESIS) & -(( ? [Var_SODIUM] : - (hasType(type_Sodium, Var_SODIUM) & -(( ? [Var_CHLORINE] : - (hasType(type_Chlorine, Var_CHLORINE) & -(((f_resourceS(Var_SYNTHESIS,Var_SODIUM)) & (((f_resourceS(Var_SYNTHESIS,Var_CHLORINE)) & (f_result(Var_SYNTHESIS,Var_SALT)))))))))))))))))). - -fof(axMidLem204, axiom, - ( ! [Var_WATER] : - (hasType(type_Water, Var_WATER) => -(( ? [Var_SYNTHESIS] : - (hasType(type_ChemicalSynthesis, Var_SYNTHESIS) & -(( ? [Var_HYDROGEN] : - (hasType(type_Hydrogen, Var_HYDROGEN) & -(( ? [Var_OXYGEN] : - (hasType(type_Oxygen, Var_OXYGEN) & -(((f_resourceS(Var_SYNTHESIS,Var_HYDROGEN)) & (((f_resourceS(Var_SYNTHESIS,Var_OXYGEN)) & (f_result(Var_SYNTHESIS,Var_WATER)))))))))))))))))). - -fof(axMidLem205, axiom, - ( ! [Var_ALLOY] : - (hasType(type_MetallicAlloy, Var_ALLOY) => -(( ? [Var_METAL1] : - (hasType(type_Metal, Var_METAL1) & -(( ? [Var_METAL2] : - (hasType(type_Metal, Var_METAL2) & -(((Var_METAL1 != Var_METAL2) & (((f_part(Var_METAL1,Var_ALLOY)) & (f_part(Var_METAL2,Var_ALLOY))))))))))))))). - -fof(axMidLem206, axiom, - ( ! [Var_STEEL] : - (hasType(type_Steel, Var_STEEL) => -(( ? [Var_IRON] : - (hasType(type_Iron, Var_IRON) & -(f_part(Var_IRON,Var_STEEL)))))))). - -fof(axMidLem207, axiom, - ( ! [Var_BRASS] : - (hasType(type_Brass, Var_BRASS) => -(( ? [Var_COPPER] : - (hasType(type_Copper, Var_COPPER) & -(( ? [Var_ZINC] : - (hasType(type_Zinc, Var_ZINC) & -(((f_part(Var_COPPER,Var_BRASS)) & (f_part(Var_ZINC,Var_BRASS))))))))))))). - -fof(axMidLem208, axiom, - ( ! [Var_POWDER] : - (hasType(type_Powder, Var_POWDER) => -(f_attribute(Var_POWDER,inst_Solid))))). - -fof(axMidLem209, axiom, - ( ! [Var_FOG] : - (hasType(type_Fog, Var_FOG) => -(( ? [Var_LAND] : - (hasType(type_LandArea, Var_LAND) & -(f_meetsSpatially(Var_FOG,Var_LAND)))))))). - -fof(axMidLem210, axiom, - ( ! [Var_ICE] : - (hasType(type_Ice, Var_ICE) => -(( ! [Var_NUMBER] : - ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((f_measure(Var_ICE,f_MeasureFn(Var_NUMBER,inst_CelsiusDegree))) => (f_lessThanOrEqualTo(Var_NUMBER,0)))))))))). - -fof(axMidLem211, axiom, - ( ! [Var_L] : - (hasType(type_Lawn, Var_L) => -(( ? [Var_G] : - (hasType(type_Grass, Var_G) & -(f_located(Var_G,Var_L)))))))). - -fof(axMidLem212, axiom, - ( ! [Var_M] : - (hasType(type_Meteorite, Var_M) => -(( ? [Var_T] : - (hasType(type_TimePosition, Var_T) & -(f_holdsDuring(Var_T,meetsSpatially(Var_M,inst_PlanetEarth))))))))). - -fof(axMidLem213, axiom, - ( ! [Var_M] : - (hasType(type_Meteorite, Var_M) => -(( ? [Var_T] : - (hasType(type_TimePosition, Var_T) & -(f_holdsDuring(Var_T,meetsSpatially(Var_M,inst_EarthsAtmosphere))))))))). - -fof(axMidLem214, axiom, - ( ! [Var_AR] : - (hasType(type_AtmosphericRegion, Var_AR) => -(f_geographicSubregion(Var_AR,inst_EarthsAtmosphere))))). - -fof(axMidLem215, axiom, - ( ! [Var_C] : - (hasType(type_Creek, Var_C) => -(( ! [Var_R] : - (hasType(type_River, Var_R) => -(f_smaller(Var_C,Var_R)))))))). - -fof(axMidLem216, axiom, - ( ! [Var_FRONT] : - (hasType(type_StormFront, Var_FRONT) => -(( ? [Var_AIR1] : - (hasType(type_Air, Var_AIR1) & -(( ? [Var_AIR2] : - (hasType(type_Air, Var_AIR2) & -(f_between(Var_AIR1,Var_FRONT,Var_AIR2))))))))))). - -fof(axMidLem217, axiom, - ( ! [Var_REGION] : - (hasType(type_Object, Var_REGION) => -(( ! [Var_OBJ] : - ((hasType(type_Object, Var_OBJ) & hasType(type_Physical, Var_OBJ)) => -(((f_orientation(Var_OBJ,Var_REGION,inst_Outside)) <=> (( ~ (f_partlyLocated(Var_OBJ,Var_REGION)))))))))))). - -fof(axMidLem218, axiom, - ( ! [Var_REGION] : - (hasType(type_Object, Var_REGION) => -(( ! [Var_OBJ] : - (hasType(type_Object, Var_OBJ) => -(((f_part(Var_OBJ,Var_REGION)) <=> (( ~ (f_orientation(Var_OBJ,Var_REGION,inst_Outside)))))))))))). - -fof(axMidLem219, axiom, - ( ! [Var_W] : - (hasType(type_WoodArtifact, Var_W) => -(f_material(type_Wood,Var_W))))). - -fof(axMidLem220, axiom, - ( ! [Var_R] : - (hasType(type_Rubber, Var_R) => -(( ? [Var_T] : - (hasType(type_BotanicalTree, Var_T) & -(f_part(Var_R,Var_T)))))))). - -fof(axMidLem221, axiom, - ( ! [Var_M] : - (hasType(type_Medicine, Var_M) => -(( ? [Var_P] : - (hasType(type_TherapeuticProcess, Var_P) & -(f_instrument(Var_P,Var_M)))))))). - -fof(axMidLem222, axiom, - ( ! [Var_O] : - (hasType(type_Opium, Var_O) => -(( ? [Var_A] : - (hasType(type_Alkaloid, Var_A) & -(f_part(Var_A,Var_O)))))))). - -fof(axMidLem223, axiom, - ( ! [Var_L] : - (hasType(type_Lesion, Var_L) => -(( ? [Var_I] : - (hasType(type_Injuring, Var_I) & -(f_result(Var_I,Var_L)))))))). - -fof(axMidLem224, axiom, - ( ! [Var_L] : - (hasType(type_Lesion, Var_L) => -(( ? [Var_O] : - (hasType(type_Organ, Var_O) & -(( ? [Var_S] : - ((hasType(type_SelfConnectedObject, Var_S) & hasType(type_Object, Var_S)) & -(((f_surface(Var_S,Var_O)) & (f_located(Var_L,Var_S))))))))))))). - -fof(axMidLem225, axiom, - ( ! [Var_T] : - (hasType(type_Tendon, Var_T) => -(( ? [Var_M] : - (hasType(type_Muscle, Var_M) & -(( ? [Var_B] : - (hasType(type_Bone, Var_B) & -(f_connects(Var_T,Var_M,Var_B))))))))))). - -fof(axMidLem226, axiom, - ( ! [Var_SWEAT] : - (hasType(type_Sweat, Var_SWEAT) => -(( ? [Var_PART] : - (hasType(type_SodiumChloride, Var_PART) & -(f_part(Var_PART,Var_SWEAT)))))))). - -fof(axMidLem227, axiom, - ( ! [Var_B] : - (hasType(type_TreeBranch, Var_B) => -(( ? [Var_T] : - (hasType(type_BotanicalTree, Var_T) & -(f_part(Var_B,Var_T)))))))). - -fof(axMidLem228, axiom, - ( ! [Var_FLOWER] : - (hasType(type_Flower, Var_FLOWER) => -(( ? [Var_PLANT] : - (hasType(type_FloweringPlant, Var_PLANT) & -(( ? [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) & -(f_holdsDuring(Var_TIME,part(Var_FLOWER,Var_PLANT)))))))))))). - -fof(axMidLem229, axiom, - ( ! [Var_C] : - (hasType(type_BloodCell, Var_C) => -(( ? [Var_B] : - (hasType(type_Blood, Var_B) & -(f_part(Var_C,Var_B)))))))). - -fof(axMidLem230, axiom, - ( ! [Var_C] : - (hasType(type_WhiteBloodCell, Var_C) => -(( ? [Var_N] : - (hasType(type_CellNucleus, Var_N) & -(f_part(Var_N,Var_C)))))))). - -fof(axMidLem231, axiom, - ( ! [Var_B] : - (hasType(type_BloodTypeA, Var_B) => -(( ? [Var_A] : - (hasType(type_AntigenA, Var_A) & -(f_part(Var_A,Var_B)))))))). - -fof(axMidLem232, axiom, - ( ! [Var_B] : - (hasType(type_BloodTypeAB, Var_B) => -(( ? [Var_A] : - (hasType(type_AntigenA, Var_A) & -(f_part(Var_A,Var_B)))))))). - -fof(axMidLem233, axiom, - ( ! [Var_B] : - (hasType(type_BloodTypeAB, Var_B) => -(( ? [Var_A] : - (hasType(type_AntigenB, Var_A) & -(f_part(Var_A,Var_B)))))))). - -fof(axMidLem234, axiom, - ( ! [Var_B] : - (hasType(type_BloodTypeB, Var_B) => -(( ? [Var_A] : - (hasType(type_AntigenB, Var_A) & -(f_part(Var_A,Var_B)))))))). - -fof(axMidLem235, axiom, - ( ! [Var_N] : - (hasType(type_NerveCell, Var_N) => -(( ? [Var_S] : - (hasType(type_NervousSystem, Var_S) & -(f_part(Var_N,Var_S)))))))). - -fof(axMidLem236, axiom, - ( ! [Var_SUBSTANCE] : - (hasType(type_LiquidBodySubstance, Var_SUBSTANCE) => -(f_attribute(Var_SUBSTANCE,inst_Liquid))))). - -fof(axMidLem237, axiom, - ( ! [Var_T] : - (hasType(type_TearSubstance, Var_T) => -(( ? [Var_E] : - (hasType(type_Eye, Var_E) & -(( ? [Var_P] : - (hasType(type_Process, Var_P) & -(((f_instrument(Var_P,Var_E)) & (f_result(Var_P,Var_T))))))))))))). - -fof(axMidLem238, axiom, - ( ! [Var_MILK] : - (hasType(type_Milk, Var_MILK) => -(( ? [Var_MAMMAL] : - (hasType(type_Mammal, Var_MAMMAL) & -(( ? [Var_PROCESS] : - (hasType(type_Process, Var_PROCESS) & -(((f_attribute(Var_MAMMAL,inst_Female)) & (((f_instrument(Var_PROCESS,Var_MAMMAL)) & (f_result(Var_PROCESS,Var_MILK))))))))))))))). - -fof(axMidLem239, axiom, - ( ! [Var_NUCLEUS] : - (hasType(type_CellNucleus, Var_NUCLEUS) => -(( ? [Var_CELL] : - (hasType(type_Cell, Var_CELL) & -(f_part(Var_NUCLEUS,Var_CELL)))))))). - -fof(axMidLem240, axiom, - ( ! [Var_BEVERAGE] : - (hasType(type_AlcoholicBeverage, Var_BEVERAGE) => -(( ? [Var_ALCOHOL] : - (hasType(type_Alcohol, Var_ALCOHOL) & -(f_part(Var_ALCOHOL,Var_BEVERAGE)))))))). - -fof(axMidLem241, axiom, - ( ! [Var_BEVERAGE] : - (hasType(type_DistilledAlcoholicBeverage, Var_BEVERAGE) => -(( ? [Var_REMOVE] : - (hasType(type_Removing, Var_REMOVE) & -(( ? [Var_WATER] : - (hasType(type_Water, Var_WATER) & -(((f_patient(Var_REMOVE,Var_WATER)) & (f_origin(Var_REMOVE,Var_BEVERAGE))))))))))))). - -fof(axMidLem242, axiom, - ( ! [Var_B] : - (hasType(type_Brandy, Var_B) => -(( ? [Var_D] : - (hasType(type_Distilling, Var_D) & -(( ? [Var_W] : - (hasType(type_Wine, Var_W) & -(((f_resourceS(Var_D,Var_W)) & (f_result(Var_D,Var_B))))))))))))). - -fof(axMidLem243, axiom, - ( ! [Var_C] : - (hasType(type_SpinalCord, Var_C) => -(( ? [Var_S] : - (hasType(type_NervousSystem, Var_S) & -(f_part(Var_C,Var_S)))))))). - -fof(axMidLem244, axiom, - ( ! [Var_C] : - (hasType(type_SpinalCord, Var_C) => -(( ? [Var_S] : - (hasType(type_SpinalColumn, Var_S) & -(f_contains(Var_S,Var_C)))))))). - -fof(axMidLem245, axiom, - ( ! [Var_SKIN] : - (hasType(type_Skin, Var_SKIN) => -(( ? [Var_ANIMAL] : - (hasType(type_Animal, Var_ANIMAL) & -(( ? [Var_SURFACE] : - ((hasType(type_SelfConnectedObject, Var_SURFACE) & hasType(type_Object, Var_SURFACE)) & -(((f_surface(Var_SURFACE,Var_ANIMAL)) & (((f_part(Var_SKIN,Var_ANIMAL)) & (f_overlapsSpatially(Var_SKIN,Var_SURFACE))))))))))))))). - -fof(axMidLem246, axiom, - ( ! [Var_R] : - (hasType(type_Retina, Var_R) => -(( ? [Var_E] : - (hasType(type_Eye, Var_E) & -(f_part(Var_R,Var_E)))))))). - -fof(axMidLem247, axiom, - ( ! [Var_DUCT] : - (hasType(type_BronchialDuct, Var_DUCT) => -(( ? [Var_LUNG] : - (hasType(type_Lung, Var_LUNG) & -(f_located(Var_DUCT,Var_LUNG)))))))). - -fof(axMidLem248, axiom, - ( ! [Var_VESSEL] : - (hasType(type_BloodVessel, Var_VESSEL) => -(( ? [Var_BLOOD] : - (hasType(type_Blood, Var_BLOOD) & -(( ? [Var_TRANSFER] : - (hasType(type_Transfer, Var_TRANSFER) & -(((f_patient(Var_TRANSFER,Var_BLOOD)) & (f_instrument(Var_TRANSFER,Var_VESSEL))))))))))))). - -fof(axMidLem249, axiom, - ( ! [Var_A] : - (hasType(type_Alveolus, Var_A) => -(( ? [Var_L] : - (hasType(type_Lung, Var_L) & -(f_located(Var_A,Var_L)))))))). - -fof(axMidLem250, axiom, - ( ! [Var_ARTERY] : - (hasType(type_Artery, Var_ARTERY) => -(( ! [Var_TRANSFER] : - (hasType(type_Transfer, Var_TRANSFER) => -(( ! [Var_BLOOD] : - (hasType(type_Blood, Var_BLOOD) => -(((((f_patient(Var_TRANSFER,Var_BLOOD)) & (f_instrument(Var_TRANSFER,Var_ARTERY)))) => (( ? [Var_HEART] : - (hasType(type_Heart, Var_HEART) & -(f_origin(Var_TRANSFER,Var_HEART)))))))))))))))). - -fof(axMidLem251, axiom, - ( ! [Var_V] : - (hasType(type_Vein, Var_V) => -(( ! [Var_T] : - (hasType(type_Transfer, Var_T) => -(( ! [Var_B] : - (hasType(type_Blood, Var_B) => -(((((f_patient(Var_T,Var_B)) & (f_instrument(Var_T,Var_V)))) => (( ? [Var_H] : - (hasType(type_Heart, Var_H) & -(f_destination(Var_T,Var_H)))))))))))))))). - -fof(axMidLem252, axiom, - ( ! [Var_ARTERY] : - (hasType(type_PulmonaryArtery, Var_ARTERY) => -(( ! [Var_TRANSFER] : - (hasType(type_Transfer, Var_TRANSFER) => -(( ! [Var_BLOOD] : - (hasType(type_Blood, Var_BLOOD) => -(((((f_patient(Var_TRANSFER,Var_BLOOD)) & (f_instrument(Var_TRANSFER,Var_ARTERY)))) => (( ? [Var_LUNG] : - (hasType(type_Lung, Var_LUNG) & -(f_destination(Var_TRANSFER,Var_LUNG)))))))))))))))). - -fof(axMidLem253, axiom, - ( ! [Var_V] : - (hasType(type_PulmonaryVein, Var_V) => -(( ! [Var_T] : - (hasType(type_Transfer, Var_T) => -(( ! [Var_B] : - (hasType(type_Blood, Var_B) => -(((((f_patient(Var_T,Var_B)) & (f_instrument(Var_T,Var_V)))) => (( ? [Var_L] : - (hasType(type_Lung, Var_L) & -(( ? [Var_H] : - (hasType(type_Heart, Var_H) & -(( ? [Var_P] : - (hasType(type_Object, Var_P) & -(((f_origin(Var_T,Var_L)) & (((f_part(Var_V,Var_P)) & (((f_part(Var_L,Var_P)) & (((f_part(Var_H,Var_P)) & (f_destination(Var_T,Var_H)))))))))))))))))))))))))))))). - -fof(axMidLem254, axiom, - ( ! [Var_C] : - (hasType(type_Capillary, Var_C) => -(( ? [Var_A] : - (hasType(type_Artery, Var_A) & -(( ? [Var_V] : - (hasType(type_Vein, Var_V) & -(f_connects(Var_C,Var_A,Var_V))))))))))). - -fof(axMidLem255, axiom, - ( ! [Var_I] : - (hasType(type_Inhaling, Var_I) => -(( ? [Var_L] : - (hasType(type_Lung, Var_L) & -(f_destination(Var_I,Var_L)))))))). - -fof(axMidLem256, axiom, - ( ! [Var_E] : - (hasType(type_Exhaling, Var_E) => -(( ? [Var_L] : - (hasType(type_Lung, Var_L) & -(f_origin(Var_E,Var_L)))))))). - -fof(axMidLem257, axiom, - ( ! [Var_NOSE] : - (hasType(type_Nose, Var_NOSE) => -(( ? [Var_N1] : - (hasType(type_Nostril, Var_N1) & -(( ? [Var_N2] : - (hasType(type_Nostril, Var_N2) & -(((Var_N1 != Var_N2) & (((f_connected(Var_N1,Var_NOSE)) & (f_connected(Var_N2,Var_NOSE))))))))))))))). - -fof(axMidLem258, axiom, - ( ! [Var_NOS] : - (hasType(type_Nostril, Var_NOS) => -(( ? [Var_N] : - (hasType(type_Nose, Var_N) & -(( ? [Var_T] : - (hasType(type_Throat, Var_T) & -(f_connects(Var_NOS,Var_N,Var_T))))))))))). - -fof(axMidLem259, axiom, - ( ! [Var_HEART] : - (hasType(type_Heart, Var_HEART) => -(( ? [Var_TRANSFER] : - (hasType(type_Transfer, Var_TRANSFER) & -(( ? [Var_BLOOD] : - (hasType(type_Blood, Var_BLOOD) & -(((f_instrument(Var_TRANSFER,Var_HEART)) & (f_patient(Var_TRANSFER,Var_BLOOD))))))))))))). - -fof(axMidLem260, axiom, - ( ! [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) => -(( ? [Var_FACE] : - (hasType(type_Face, Var_FACE) & -(f_part(Var_MOUTH,Var_FACE)))))))). - -fof(axMidLem261, axiom, - ( ! [Var_TONGUE] : - (hasType(type_Tongue, Var_TONGUE) => -(( ? [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) & -(f_part(Var_TONGUE,Var_MOUTH)))))))). - -fof(axMidLem262, axiom, - ( ! [Var_H] : - (hasType(type_Hoof, Var_H) => -(( ? [Var_F] : - (hasType(type_Foot, Var_F) & -(( ? [Var_A] : - (hasType(type_HoofedMammal, Var_A) & -(((f_part(Var_H,Var_F)) & (f_part(Var_F,Var_A))))))))))))). - -fof(axMidLem263, axiom, - ( ! [Var_TOOTH] : - (hasType(type_Tooth, Var_TOOTH) => -(( ? [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) & -(f_part(Var_TOOTH,Var_MOUTH)))))))). - -fof(axMidLem264, axiom, - ( ! [Var_S] : - (hasType(type_Skull, Var_S) => -(( ? [Var_V] : - (hasType(type_Vertebrate, Var_V) & -(( ? [Var_H] : - (hasType(type_Head, Var_H) & -(((f_part(Var_H,Var_V)) & (f_part(Var_S,Var_H))))))))))))). - -fof(axMidLem265, axiom, - ( ! [Var_H] : - (hasType(type_Horn, Var_H) => -(( ? [Var_M] : - (hasType(type_HoofedMammal, Var_M) & -(f_part(Var_H,Var_M)))))))). - -fof(axMidLem266, axiom, - ( ! [Var_O] : - (hasType(type_Ossification, Var_O) => -(( ? [Var_B] : - (hasType(type_Bone, Var_B) & -(f_result(Var_O,Var_B)))))))). - -fof(axMidLem267, axiom, - ( ! [Var_CHEW] : - (hasType(type_Chewing, Var_CHEW) => -(( ? [Var_EAT] : - (hasType(type_Eating, Var_EAT) & -(f_subProcess(Var_CHEW,Var_EAT)))))))). - -fof(axMidLem268, axiom, - ( ! [Var_LIP] : - (hasType(type_Lip, Var_LIP) => -(( ? [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) & -(f_part(Var_LIP,Var_MOUTH)))))))). - -fof(axMidLem269, axiom, - ( ! [Var_L] : - (hasType(type_Licking, Var_L) => -(( ? [Var_T] : - (hasType(type_Tongue, Var_T) & -(f_instrument(Var_L,Var_T)))))))). - -fof(axMidLem270, axiom, - ( ! [Var_E] : - (hasType(type_Embracing, Var_E) => -(( ? [Var_P1] : - (hasType(type_Human, Var_P1) & -(( ? [Var_P2] : - (hasType(type_Human, Var_P2) & -(((Var_P1 != Var_P2) & (((f_agent(Var_E,Var_P1)) & (f_agent(Var_E,Var_P2))))))))))))))). - -fof(axMidLem271, axiom, - ( ! [Var_S] : - (hasType(type_Skeleton, Var_S) => -(( ? [Var_A] : - (hasType(type_Animal, Var_A) & -(f_interiorPart(Var_S,Var_A)))))))). - -fof(axMidLem272, axiom, - ( ! [Var_BONE] : - (hasType(type_Bone, Var_BONE) => -(( ? [Var_SKELETON] : - ((hasType(type_Skeleton, Var_SKELETON) | hasType(type_Exoskeleton, Var_SKELETON)) & -(f_part(Var_BONE,Var_SKELETON)))))))). - -fof(axMidLem273, axiom, - ( ! [Var_X] : - (hasType(type_Exoskeleton, Var_X) => -(( ? [Var_A] : - (hasType(type_Animal, Var_A) & -(((f_part(Var_X,Var_A)) & (( ~ ( ? [Var_PART] : - (hasType(type_Object, Var_PART) & -(((f_properPart(Var_PART,Var_A)) & (f_orientation(Var_PART,Var_X,inst_Outside)))))))))))))))). - -fof(axMidLem274, axiom, - ( ! [Var_J] : - (hasType(type_BodyJoint, Var_J) => -(( ? [Var_S] : - (hasType(type_Skeleton, Var_S) & -(( ? [Var_P2] : - ((hasType(type_CorpuscularObject, Var_P2) & hasType(type_SelfConnectedObject, Var_P2)) & -(( ? [Var_P1] : - ((hasType(type_CorpuscularObject, Var_P1) & hasType(type_SelfConnectedObject, Var_P1)) & -(((f_component(Var_P1,Var_S)) & (((f_component(Var_P2,Var_S)) & (((f_component(Var_J,Var_S)) & (f_connects(Var_J,Var_P1,Var_P2)))))))))))))))))))). - -fof(axMidLem275, axiom, - ( ! [Var_THROAT] : - (hasType(type_Throat, Var_THROAT) => -(( ? [Var_MOUTH] : - (hasType(type_Mouth, Var_MOUTH) & -(f_connected(Var_THROAT,Var_MOUTH)))))))). - -fof(axMidLem276, axiom, - ( ! [Var_HAIR] : - (hasType(type_Hair, Var_HAIR) => -(( ? [Var_MAMMAL] : - (hasType(type_Mammal, Var_MAMMAL) & -(( ? [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) & -(f_holdsDuring(Var_TIME,part(Var_HAIR,Var_MAMMAL)))))))))))). - -fof(axMidLem277, axiom, - ( ! [Var_H] : - (hasType(type_FacialHair, Var_H) => -(( ? [Var_F] : - (hasType(type_Face, Var_F) & -(f_part(Var_H,Var_F)))))))). - -fof(axMidLem278, axiom, - ( ! [Var_P] : - (hasType(type_Peeling, Var_P) => -(( ! [Var_O] : - ((hasType(type_Entity, Var_O) & hasType(type_Object, Var_O)) => -(((f_patient(Var_P,Var_O)) => (( ? [Var_S] : - (hasType(type_Skin, Var_S) & -(f_part(Var_O,Var_S))))))))))))). - -fof(axMidLem279, axiom, - ( ! [Var_I] : - (hasType(type_Intestine, Var_I) => -(( ? [Var_S] : - (hasType(type_Stomach, Var_S) & -(f_connected(Var_I,Var_S)))))))). - -fof(axMidLem280, axiom, - ( ! [Var_HYPO] : - (hasType(type_Hypothalamus, Var_HYPO) => -(( ? [Var_BRAIN] : - (hasType(type_Brain, Var_BRAIN) & -(f_part(Var_HYPO,Var_BRAIN)))))))). - -fof(axMidLem281, axiom, - ( ! [Var_EYE] : - (hasType(type_Eye, Var_EYE) => -(( ? [Var_HEAD] : - (hasType(type_Head, Var_HEAD) & -(f_part(Var_EYE,Var_HEAD)))))))). - -fof(axMidLem282, axiom, - ( ! [Var_EAR] : - (hasType(type_Ear, Var_EAR) => -(( ? [Var_HEAD] : - (hasType(type_Head, Var_HEAD) & -(f_part(Var_EAR,Var_HEAD)))))))). - -fof(axMidLem283, axiom, - ( ! [Var_NOSE] : - (hasType(type_Nose, Var_NOSE) => -(( ? [Var_FACE] : - (hasType(type_Face, Var_FACE) & -(f_part(Var_NOSE,Var_FACE)))))))). - -fof(axMidLem284, axiom, - ( ! [Var_HORMONE] : - (hasType(type_HormoneTSH, Var_HORMONE) => -(( ? [Var_GLAND] : - (hasType(type_ThyroidGland, Var_GLAND) & -(( ? [Var_PROC] : - (hasType(type_Process, Var_PROC) & -(((f_instrument(Var_PROC,Var_GLAND)) & (f_result(Var_PROC,Var_HORMONE))))))))))))). - -fof(axMidLem285, axiom, - ( ! [Var_ARM] : - (hasType(type_Arm, Var_ARM) => -(( ? [Var_PRIMATE] : - (hasType(type_Primate, Var_PRIMATE) & -(f_part(Var_ARM,Var_PRIMATE)))))))). - -fof(axMidLem286, axiom, - ( ! [Var_HAND] : - (hasType(type_Hand, Var_HAND) => -(( ? [Var_ARM] : - (hasType(type_Arm, Var_ARM) & -(f_part(Var_HAND,Var_ARM)))))))). - -fof(axMidLem287, axiom, - ( ! [Var_DIGIT] : - (hasType(type_DigitAppendage, Var_DIGIT) => -(( ? [Var_LIMB] : - (hasType(type_Limb, Var_LIMB) & -(f_part(Var_DIGIT,Var_LIMB)))))))). - -fof(axMidLem288, axiom, - ( ! [Var_FINGER] : - (hasType(type_Finger, Var_FINGER) => -(( ? [Var_HAND] : - (hasType(type_Hand, Var_HAND) & -(f_part(Var_FINGER,Var_HAND)))))))). - -fof(axMidLem289, axiom, - ( ! [Var_N] : - (hasType(type_NailDigit, Var_N) => -(( ? [Var_D] : - (hasType(type_DigitAppendage, Var_D) & -(f_part(Var_N,Var_D)))))))). - -fof(axMidLem290, axiom, - ( ! [Var_LIMB] : - (hasType(type_Limb, Var_LIMB) => -(( ? [Var_VERTEBRATE] : - (hasType(type_Vertebrate, Var_VERTEBRATE) & -(f_part(Var_LIMB,Var_VERTEBRATE)))))))). - -fof(axMidLem291, axiom, - ( ! [Var_LEG] : - (hasType(type_Leg, Var_LEG) => -(( ? [Var_PRIMATE] : - (hasType(type_Primate, Var_PRIMATE) & -(f_part(Var_LEG,Var_PRIMATE)))))))). - -fof(axMidLem292, axiom, - ( ! [Var_FOOT] : - (hasType(type_Foot, Var_FOOT) => -(( ? [Var_LIMB] : - (hasType(type_Leg, Var_LIMB) & -(f_part(Var_FOOT,Var_LIMB)))))))). - -fof(axMidLem293, axiom, - ( ! [Var_A] : - (hasType(type_Ankle, Var_A) => -(( ? [Var_L] : - (hasType(type_Leg, Var_L) & -(f_part(Var_A,Var_L)))))))). - -fof(axMidLem294, axiom, - ( ! [Var_E] : - (hasType(type_Elbow, Var_E) => -(( ? [Var_A] : - (hasType(type_Arm, Var_A) & -(f_part(Var_E,Var_A)))))))). - -fof(axMidLem295, axiom, - ( ! [Var_W] : - (hasType(type_Wrist, Var_W) => -(( ? [Var_A] : - (hasType(type_Arm, Var_A) & -(f_part(Var_W,Var_A)))))))). - -fof(axMidLem296, axiom, - ( ! [Var_TOE] : - (hasType(type_Toe, Var_TOE) => -(( ? [Var_FOOT] : - (hasType(type_Foot, Var_FOOT) & -(f_part(Var_TOE,Var_FOOT)))))))). - -fof(axMidLem297, axiom, - ( ! [Var_KNEE] : - (hasType(type_Knee, Var_KNEE) => -(( ? [Var_LEG] : - (hasType(type_Leg, Var_LEG) & -(f_part(Var_KNEE,Var_LEG)))))))). - -fof(axMidLem298, axiom, - ( ! [Var_SHOULDER] : - (hasType(type_Shoulder, Var_SHOULDER) => -(( ? [Var_PRIMATE] : - (hasType(type_Primate, Var_PRIMATE) & -(f_part(Var_SHOULDER,Var_PRIMATE)))))))). - -fof(axMidLem299, axiom, - ( ! [Var_KNUCKLE] : - (hasType(type_Knuckle, Var_KNUCKLE) => -(( ? [Var_FINGER] : - (hasType(type_Finger, Var_FINGER) & -(f_part(Var_KNUCKLE,Var_FINGER)))))))). - -fof(axMidLem300, axiom, - ( ! [Var_TORSO] : - (hasType(type_Torso, Var_TORSO) => -(( ! [Var_LIMB] : - (hasType(type_Limb, Var_LIMB) => -(( ~ (f_overlapsSpatially(Var_TORSO,Var_LIMB)))))))))). - -fof(axMidLem301, axiom, - ( ! [Var_B] : - (hasType(type_Breast, Var_B) => -(( ? [Var_T] : - (hasType(type_Torso, Var_T) & -(f_part(Var_B,f_FrontFn(Var_T))))))))). - -fof(axMidLem302, axiom, - ( ! [Var_B] : - (hasType(type_Breast, Var_B) => -(( ? [Var_P] : - (hasType(type_Primate, Var_P) & -(f_part(Var_B,Var_P)))))))). - -fof(axMidLem303, axiom, - ( ! [Var_NECK] : - (hasType(type_Neck, Var_NECK) => -(( ? [Var_HEAD] : - (hasType(type_Head, Var_HEAD) & -(f_connected(Var_NECK,Var_HEAD)))))))). - -fof(axMidLem304, axiom, - ( ! [Var_FACE] : - (hasType(type_Face, Var_FACE) => -(( ? [Var_HEAD] : - (hasType(type_Head, Var_HEAD) & -(f_part(Var_FACE,Var_HEAD)))))))). - -fof(axMidLem305, axiom, - ( ! [Var_FACE] : - (hasType(type_Face, Var_FACE) => -(( ? [Var_VERTEBRATE] : - (hasType(type_Vertebrate, Var_VERTEBRATE) & -(f_part(Var_FACE,Var_VERTEBRATE)))))))). - -fof(axMidLem306, axiom, - ( ! [Var_CHIN] : - (hasType(type_Chin, Var_CHIN) => -(( ? [Var_FACE] : - (hasType(type_Face, Var_FACE) & -(f_part(Var_CHIN,Var_FACE)))))))). - -fof(axMidLem307, axiom, - ( ! [Var_CHIN] : - (hasType(type_Chin, Var_CHIN) => -(( ! [Var_FACE] : - (hasType(type_Object, Var_FACE) => -(( ! [Var_PART] : - (hasType(type_Object, Var_PART) => -(((((f_part(Var_PART,Var_FACE)) & (( ~ (f_part(Var_PART,Var_CHIN)))))) => (f_orientation(Var_PART,Var_CHIN,inst_Below))))))))))))). - -fof(axMidLem308, axiom, - ( ! [Var_R] : - (hasType(type_Regretting, Var_R) => -(( ! [Var_T] : - (hasType(type_Sentence, Var_T) => -(((f_patient(Var_R,Var_T)) => (f_truth(Var_T,inst_True)))))))))). - -fof(axMidLem309, axiom, - ( ! [Var_C] : - (hasType(type_Congratulating, Var_C) => -(( ? [Var_D] : - ((hasType(type_Entity, Var_D) & hasType(type_Agent, Var_D)) & -(( ? [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_CognitiveAgent, Var_A)) & -(( ? [Var_P] : - ((hasType(type_Process, Var_P) & hasType(type_Physical, Var_P) & hasType(type_Entity, Var_P)) & -(((f_destination(Var_C,Var_D)) & (((f_agent(Var_P,Var_D)) & (((f_agent(Var_C,Var_A)) & (((f_wants(Var_A,Var_P)) & (f_refers(Var_C,Var_P)))))))))))))))))))))). - -fof(axMidLem310, axiom, - ( ! [Var_EXPRESS] : - (hasType(type_FacialExpression, Var_EXPRESS) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_EXPRESS,Var_AGENT)) => (( ? [Var_FACE] : - (hasType(type_Face, Var_FACE) & -(((f_part(Var_FACE,Var_AGENT)) & (f_instrument(Var_EXPRESS,Var_FACE))))))))))))))). - -fof(axMidLem311, axiom, - ( ! [Var_SMILE] : - (hasType(type_Smiling, Var_SMILE) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_SMILE,Var_AGENT)) => (f_holdsDuring(f_WhenFn(Var_SMILE),attribute(Var_AGENT,inst_Happiness))))))))))). - -fof(axMidLem312, axiom, - ( ! [Var_FROWN] : - (hasType(type_Frowning, Var_FROWN) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_FROWN,Var_AGENT)) => (f_holdsDuring(f_WhenFn(Var_FROWN),attribute(Var_AGENT,inst_Unhappiness))))))))))). - -fof(axMidLem313, axiom, - ( ! [Var_LAUGH] : - (hasType(type_Laughing, Var_LAUGH) => -(( ? [Var_SMILE] : - (hasType(type_Smiling, Var_SMILE) & -(f_subProcess(Var_SMILE,Var_LAUGH)))))))). - -fof(axMidLem314, axiom, - ( ! [Var_WEEP] : - (hasType(type_Weeping, Var_WEEP) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_WEEP,Var_AGENT)) => (f_holdsDuring(f_WhenFn(Var_WEEP),attribute(Var_AGENT,inst_Unhappiness))))))))))). - -fof(axMidLem315, axiom, - ( ! [Var_HG] : - (hasType(type_HandGesture, Var_HG) => -(( ? [Var_H] : - (hasType(type_Hand, Var_H) & -(f_patient(Var_HG,Var_H)))))))). - -fof(axMidLem316, axiom, - ( ! [Var_S] : - (hasType(type_Sinking, Var_S) => -(( ? [Var_W] : - (hasType(type_BodyOfWater, Var_W) & -(f_located(Var_S,Var_W)))))))). - -fof(axMidLem317, axiom, - ( ! [Var_WHOLE] : - ((hasType(type_Object, Var_WHOLE) & hasType(type_Entity, Var_WHOLE)) => -(( ! [Var_HALF] : - ((hasType(type_Object, Var_HALF) & hasType(type_Entity, Var_HALF)) => -(((f_half(Var_HALF,Var_WHOLE)) => (( ? [Var_OTHER] : - ((hasType(type_Object, Var_OTHER) & hasType(type_Entity, Var_OTHER)) & -(((f_half(Var_OTHER,Var_WHOLE)) & (((Var_OTHER != Var_HALF) & (Var_WHOLE = f_MereologicalSumFn(Var_HALF,Var_OTHER))))))))))))))))). - -fof(axMidLem318, axiom, - ( ! [Var_W] : - ((hasType(type_Object, Var_W) & hasType(type_Entity, Var_W)) => -(( ! [Var_T] : - ((hasType(type_Object, Var_T) & hasType(type_Entity, Var_T)) => -(((f_third(Var_T,Var_W)) => (( ? [Var_O2] : - ((hasType(type_Object, Var_O2) & hasType(type_Entity, Var_O2)) & -(( ? [Var_O1] : - ((hasType(type_Object, Var_O1) & hasType(type_Entity, Var_O1)) & -(((f_third(Var_O1,Var_W)) & (((f_third(Var_O2,Var_W)) & (((Var_O1 != Var_T) & (((Var_O2 != Var_T) & (((Var_O1 != Var_O2) & (Var_W = f_MereologicalSumFn(Var_T,f_MereologicalSumFn(Var_O1,Var_O2))))))))))))))))))))))))))). - -fof(axMidLem319, axiom, - ( ! [Var_W] : - (hasType(type_Object, Var_W) => -(( ! [Var_Q] : - (hasType(type_Object, Var_Q) => -(((f_quarter(Var_Q,Var_W)) <=> (( ? [Var_H] : - (hasType(type_Object, Var_H) & -(((f_half(Var_H,Var_W)) & (f_half(Var_Q,Var_H))))))))))))))). - -fof(axMidLem320, axiom, - ( ! [Var_WHOLE] : - (hasType(type_Object, Var_WHOLE) => -(( ! [Var_MOST] : - (hasType(type_Object, Var_MOST) => -(((f_most(Var_MOST,Var_WHOLE)) => (( ? [Var_UNIT] : - (hasType(type_UnitOfMeasure, Var_UNIT) & -(( ? [Var_NUMBER2] : - ((hasType(type_RealNumber, Var_NUMBER2) & hasType(type_Quantity, Var_NUMBER2)) & -(( ? [Var_NUMBER1] : - ((hasType(type_RealNumber, Var_NUMBER1) & hasType(type_Quantity, Var_NUMBER1)) & -(( ? [Var_HALF] : - (hasType(type_Object, Var_HALF) & -(((f_half(Var_HALF,Var_WHOLE)) & (((f_measure(Var_HALF,f_MeasureFn(Var_NUMBER1,Var_UNIT))) & (((f_measure(Var_MOST,f_MeasureFn(Var_NUMBER2,Var_UNIT))) & (f_greaterThan(Var_NUMBER2,Var_NUMBER1)))))))))))))))))))))))))))). - -fof(axMidLem321, axiom, - ( ! [Var_CHART] : - (hasType(type_Chart, Var_CHART) => -(( ? [Var_QUANTITY] : - (hasType(type_PhysicalQuantity, Var_QUANTITY) & -(f_refers(Var_CHART,Var_QUANTITY)))))))). - -fof(axMidLem322, axiom, - ( ! [Var_FLAG] : - (hasType(type_Flag, Var_FLAG) => -(( ? [Var_FABRIC] : - (hasType(type_Fabric, Var_FABRIC) & -(f_part(Var_FABRIC,Var_FLAG)))))))). - -fof(axMidLem323, axiom, - ( ! [Var_FLAG] : - (hasType(type_Flag, Var_FLAG) => -(( ? [Var_AREA] : - (hasType(type_GeopoliticalArea, Var_AREA) & -(f_refers(Var_FLAG,Var_AREA)))))))). - -fof(axMidLem324, axiom, - ( ! [Var_F] : - (hasType(type_Flag, Var_F) => -(( ? [Var_N] : - (hasType(type_Nation, Var_N) & -(f_refers(Var_F,Var_N)))))))). - -fof(axMidLem325, axiom, - ( ! [Var_G] : - (hasType(type_GraphDiagram, Var_G) => -(( ? [Var_Q] : - (hasType(type_PhysicalQuantity, Var_Q) & -(f_refers(Var_G,Var_Q)))))))). - -fof(axMidLem326, axiom, - ( ! [Var_M] : - (hasType(type_Map, Var_M) => -(( ? [Var_A] : - (hasType(type_GeographicArea, Var_A) & -(f_represents(Var_M,Var_A)))))))). - -fof(axMidLem327, axiom, - ( ! [Var_SHOOT] : - (hasType(type_Photographing, Var_SHOOT) => -(( ? [Var_PHOTO] : - (hasType(type_Photograph, Var_PHOTO) & -(( ? [Var_CAMERA] : - (hasType(type_Camera, Var_CAMERA) & -(((f_result(Var_SHOOT,Var_PHOTO)) & (f_instrument(Var_SHOOT,Var_CAMERA))))))))))))). - -fof(axMidLem328, axiom, - ( ! [Var_COMPOSE] : - (hasType(type_Composing, Var_COMPOSE) => -(( ? [Var_MUSIC] : - (hasType(type_MusicalComposition, Var_MUSIC) & -(f_result(Var_COMPOSE,Var_MUSIC)))))))). - -fof(axMidLem329, axiom, - ( ! [Var_NUMBER] : - ((hasType(type_Entity, Var_NUMBER) & hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((Var_NUMBER = f_MultiplicationFn(1,Var_NUMBER)) => (f_MeasureFn(Var_NUMBER,inst_TonMass) = f_MeasureFn(f_MultiplicationFn(Var_NUMBER,2000),inst_PoundMass))))))). - -fof(axMidLem330, axiom, - ( ! [Var_A] : - ((hasType(type_RealNumber, Var_A) & hasType(type_Quantity, Var_A)) => -(( ! [Var_O] : - (hasType(type_Object, Var_O) => -(((f_measure(Var_O,f_MeasureFn(Var_A,inst_MetricTon))) <=> (f_measure(Var_O,f_MeasureFn(f_MultiplicationFn(Var_A,2205),inst_PoundMass))))))))))). - -fof(axMidLem331, axiom, - ( ! [Var_N] : - ((hasType(type_Entity, Var_N) & hasType(type_RealNumber, Var_N) & hasType(type_Quantity, Var_N)) => -(((Var_N = f_MultiplicationFn(1,Var_N)) => (f_MeasureFn(Var_N,inst_MillenniumDuration) = f_MeasureFn(f_MultiplicationFn(Var_N,1000),inst_YearDuration))))))). - -fof(axMidLem332, axiom, - ( ! [Var_S] : - (hasType(type_Song, Var_S) => -(( ? [Var_L] : - (hasType(type_Lyrics, Var_L) & -(f_part(Var_L,Var_S)))))))). - -fof(axMidLem333, axiom, - ( ! [Var_PASS] : - (hasType(type_PassingABill, Var_PASS) => -(( ! [Var_TEXT] : - ((hasType(type_Entity, Var_TEXT) & hasType(type_Object, Var_TEXT)) => -(((f_patient(Var_PASS,Var_TEXT)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_PASS)),attribute(Var_TEXT,inst_LegislativeBill))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_PASS)),attribute(Var_TEXT,inst_Law))))))))))))). - -fof(axMidLem334, axiom, - ( ! [Var_L] : - (hasType(type_LawEnforcement, Var_L) => -(( ! [Var_P] : - (hasType(type_PoliceOrganization, Var_P) => -(( ! [Var_AGENT] : - (hasType(type_Agent, Var_AGENT) => -(((f_agent(Var_L,Var_AGENT)) => (( ? [Var_O] : - (hasType(type_PoliceOrganization, Var_O) & -(f_member(Var_P,Var_O)))))))))))))))). - -fof(axMidLem335, axiom, - ( ! [Var_I] : - (hasType(type_Imprisoning, Var_I) => -(( ? [Var_P] : - (hasType(type_Prison, Var_P) & -(f_located(Var_I,Var_P)))))))). - -fof(axMidLem336, axiom, - ( ! [Var_S] : - (hasType(type_Espionage, Var_S) => -(( ? [Var_GOV1] : - (hasType(type_Government, Var_GOV1) & -(( ? [Var_GOV2] : - (hasType(type_Government, Var_GOV2) & -(((f_agent(Var_S,Var_GOV1)) & (((f_patient(Var_S,Var_GOV2)) & (Var_GOV1 != Var_GOV2)))))))))))))). - -fof(axMidLem337, axiom, - ( ! [Var_T] : - ((hasType(type_Object, Var_T) & hasType(type_Contract, Var_T)) => -(((f_attribute(Var_T,inst_Treaty)) => (( ? [Var_N1] : - (hasType(type_Nation, Var_N1) & -(( ? [Var_N2] : - (hasType(type_Nation, Var_N2) & -(((f_agreementMember(Var_T,Var_N1)) & (((f_agreementMember(Var_T,Var_N2)) & (Var_N1 != Var_N2)))))))))))))))). - -fof(axMidLem338, axiom, - ( ! [Var_FACT] : - (hasType(type_Fact, Var_FACT) => -(f_truth(Var_FACT,inst_True))))). - -fof(axMidLem339, axiom, - ( ! [Var_RECORD] : - (hasType(type_AudioRecording, Var_RECORD) => -(( ? [Var_SOUND] : - (hasType(type_RadiatingSound, Var_SOUND) & -(( ? [Var_INFO] : - (hasType(type_Proposition, Var_INFO) & -(((f_containsInformation(Var_RECORD,Var_INFO)) & (f_realization(Var_SOUND,Var_INFO))))))))))))). - -fof(axMidLem340, axiom, - ( ! [Var_LABEL] : - (hasType(type_Label, Var_LABEL) => -(( ? [Var_OBJ] : - (hasType(type_SelfConnectedObject, Var_OBJ) & -(((f_connected(Var_LABEL,Var_OBJ)) & (f_refers(Var_LABEL,Var_OBJ)))))))))). - -fof(axMidLem341, axiom, - ( ! [Var_X] : - (hasType(type_DutyTax, Var_X) => -(( ! [Var_OBJ] : - (hasType(type_Entity, Var_OBJ) => -(((((f_refers(Var_X,Var_OBJ)) & (f_patient(Var_X,Var_OBJ)))) => (( ? [Var_T] : - (hasType(type_Transfer, Var_T) & -(( ? [Var_N1] : - (hasType(type_Nation, Var_N1) & -(( ? [Var_N2] : - (hasType(type_Nation, Var_N2) & -(((f_patient(Var_T,Var_OBJ)) & (((f_origin(Var_T,Var_N1)) & (((f_destination(Var_T,Var_N2)) & (((Var_N1 != Var_N2) & (((f_earlier(f_WhenFn(Var_T),f_WhenFn(Var_X))) & (f_causes(Var_T,Var_X))))))))))))))))))))))))))))). - -fof(axMidLem342, axiom, - ( ! [Var_A] : - (hasType(type_Announcement, Var_A) => -(( ? [Var_CD] : - (hasType(type_ContentDevelopment, Var_CD) & -(( ? [Var_I] : - (hasType(type_SocialInteraction, Var_I) & -(((f_result(Var_CD,Var_A)) & (((f_refers(Var_A,Var_I)) & (f_earlier(f_WhenFn(Var_CD),f_WhenFn(Var_I)))))))))))))))). - -fof(axMidLem343, axiom, - ( ! [Var_PROG] : - (hasType(type_PerformanceProgram, Var_PROG) => -(( ? [Var_PERF] : - (hasType(type_Performance, Var_PERF) & -(( ? [Var_PROP] : - (hasType(type_Proposition, Var_PROP) & -(((f_containsInformation(Var_PROG,Var_PROP)) & (f_realization(Var_PERF,Var_PROP))))))))))))). - -fof(axMidLem344, axiom, - ( ! [Var_SHOT] : - (hasType(type_MotionPictureShot, Var_SHOT) => -(( ? [Var_MOVIE] : - (hasType(type_MotionPicture, Var_MOVIE) & -(f_subsumesContentInstance(Var_MOVIE,Var_SHOT)))))))). - -fof(axMidLem345, axiom, - ( ! [Var_S] : - (hasType(type_MotionPictureScene, Var_S) => -(( ! [Var_MOVIE] : - (hasType(type_ContentBearingObject, Var_MOVIE) => -(( ? [Var_M] : - (hasType(type_MotionPicture, Var_M) & -(f_subsumesContentInstance(Var_MOVIE,Var_S))))))))))). - -fof(axMidLem346, axiom, - ( ! [Var_PROGRAM] : - (hasType(type_BroadcastProgram, Var_PROGRAM) => -(( ? [Var_BROADCAST] : - (hasType(type_Broadcasting, Var_BROADCAST) & -(f_patient(Var_BROADCAST,Var_PROGRAM)))))))). - -fof(axMidLem347, axiom, - ( ! [Var_CHAPTER] : - (hasType(type_Chapter, Var_CHAPTER) => -(( ? [Var_BOOK] : - (hasType(type_Book, Var_BOOK) & -(f_subsumesContentInstance(Var_BOOK,Var_CHAPTER)))))))). - -fof(axMidLem348, axiom, - ( ! [Var_PAPER] : - (hasType(type_Newspaper, Var_PAPER) => -(( ? [Var_REPORT] : - (hasType(type_Report, Var_REPORT) & -(f_subsumesContentInstance(Var_PAPER,Var_REPORT)))))))). - -fof(axMidLem349, axiom, - ( ! [Var_C] : - (hasType(type_HolidayCard, Var_C) => -(f_material(type_Paper,Var_C))))). - -fof(axMidLem350, axiom, - ( ! [Var_C] : - (hasType(type_HolidayCard, Var_C) => -(( ? [Var_H] : - (hasType(type_Holiday, Var_H) & -(f_refers(Var_C,Var_H)))))))). - -fof(axMidLem351, axiom, - ( ! [Var_ACCOUNT] : - (hasType(type_HistoricalAccount, Var_ACCOUNT) => -(( ? [Var_EVENT] : - ((hasType(type_Entity, Var_EVENT) & hasType(type_Physical, Var_EVENT)) & -(((f_represents(Var_ACCOUNT,Var_EVENT)) & (f_earlier(f_WhenFn(Var_EVENT),f_WhenFn(Var_ACCOUNT))))))))))). - -fof(axMidLem352, axiom, - ( ! [Var_B] : - (hasType(type_Biography, Var_B) => -(( ? [Var_H] : - (hasType(type_Human, Var_H) & -(f_refers(Var_B,Var_H)))))))). - -fof(axMidLem353, axiom, - ( ! [Var_S] : - (hasType(type_MysteryStory, Var_S) => -(( ? [Var_C] : - (hasType(type_CriminalAction, Var_C) & -(f_refers(Var_S,Var_C)))))))). - -fof(axMidLem354, axiom, - ( ! [Var_H] : - ((hasType(type_Object, Var_H) & hasType(type_Agent, Var_H)) => -(((f_attribute(Var_H,inst_LiteracyAttribute)) <=> (((f_hasSkill(type_Reading,Var_H)) & (f_hasSkill(type_Writing,Var_H))))))))). - -fof(axMidLem355, axiom, - ( ! [Var_C] : - (hasType(type_Curb, Var_C) => -(( ? [Var_S] : - (hasType(type_Sidewalk, Var_S) & -(( ? [Var_R] : - (hasType(type_Roadway, Var_R) & -(f_connects(Var_C,Var_S,Var_R))))))))))). - -fof(axMidLem356, axiom, - ( ! [Var_LEVEL1] : - (hasType(type_BuildingLevel, Var_LEVEL1) => -(( ! [Var_LEVEL2] : - (hasType(type_BuildingLevel, Var_LEVEL2) => -(( ! [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) => -(((((f_part(Var_LEVEL1,Var_BUILDING)) & (f_part(Var_LEVEL2,Var_BUILDING)))) => (( ? [Var_STEPS] : - (hasType(type_Steps, Var_STEPS) & -(f_connects(Var_STEPS,Var_LEVEL1,Var_LEVEL2)))))))))))))))). - -fof(axMidLem357, axiom, - ( ! [Var_W] : - (hasType(type_Window, Var_W) => -(f_attribute(Var_W,inst_Transparent))))). - -fof(axMidLem358, axiom, - ( ! [Var_W] : - (hasType(type_Skylight, Var_W) => -(( ? [Var_C] : - (hasType(type_Ceiling, Var_C) & -(f_part(Var_W,Var_C)))))))). - -fof(axMidLem359, axiom, - ( ! [Var_W] : - (hasType(type_RearWindow, Var_W) => -(( ? [Var_A] : - (hasType(type_Automobile, Var_A) & -(f_part(Var_W,f_BackFn(Var_A))))))))). - -fof(axMidLem360, axiom, - ( ! [Var_DOOR] : - (hasType(type_Door, Var_DOOR) => -(( ? [Var_WAY] : - (hasType(type_Doorway, Var_WAY) & -(f_part(Var_DOOR,Var_WAY)))))))). - -fof(axMidLem361, axiom, - ( ! [Var_WALL] : - (hasType(type_Wall, Var_WALL) => -(( ? [Var_ARTIFACT] : - ((hasType(type_Building, Var_ARTIFACT) | hasType(type_Room, Var_ARTIFACT)) & -(f_part(Var_WALL,Var_ARTIFACT)))))))). - -fof(axMidLem362, axiom, - ( ! [Var_FLOOR] : - (hasType(type_Floor, Var_FLOOR) => -(( ? [Var_ARTIFACT] : - (hasType(type_Room, Var_ARTIFACT) & -(f_part(Var_FLOOR,Var_ARTIFACT)))))))). - -fof(axMidLem363, axiom, - ( ! [Var_C] : - (hasType(type_Ceiling, Var_C) => -(( ? [Var_R] : - (hasType(type_Room, Var_R) & -(f_top(Var_C,Var_R)))))))). - -fof(axMidLem364, axiom, - ( ! [Var_ROOF] : - (hasType(type_Roof, Var_ROOF) => -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(f_top(Var_ROOF,Var_BUILDING)))))))). - -fof(axMidLem365, axiom, - ( ! [Var_F] : - (hasType(type_Fireplace, Var_F) => -(( ? [Var_C] : - (hasType(type_Chimney, Var_C) & -(f_connected(Var_F,Var_C)))))))). - -fof(axMidLem366, axiom, - ( ! [Var_F] : - (hasType(type_Fireplace, Var_F) => -(( ? [Var_B] : - (hasType(type_Building, Var_B) & -(f_part(Var_F,Var_B)))))))). - -fof(axMidLem367, axiom, - ( ! [Var_LEVEL] : - (hasType(type_BuildingLevel, Var_LEVEL) => -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(f_part(Var_LEVEL,Var_BUILDING)))))))). - -fof(axMidLem368, axiom, - ( ! [Var_T] : - (hasType(type_Transportation, Var_T) => -(( ! [Var_D] : - (hasType(type_Pump, Var_D) => -(((f_instrument(Var_T,Var_D)) => (( ? [Var_F] : - (hasType(type_Object, Var_F) & -(((f_instrument(Var_T,Var_F)) & (f_attribute(Var_F,inst_Fluid))))))))))))))). - -fof(axMidLem369, axiom, - ( ! [Var_GARAGE] : - (hasType(type_Garage, Var_GARAGE) => -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(f_part(Var_GARAGE,Var_BUILDING)))))))). - -fof(axMidLem370, axiom, - ( ! [Var_B] : - (hasType(type_Bathroom, Var_B) => -(( ? [Var_W] : - (hasType(type_WashBasin, Var_W) & -(f_located(Var_W,Var_B)))))))). - -fof(axMidLem371, axiom, - ( ! [Var_ROOM] : - (hasType(type_Bedroom, Var_ROOM) => -(( ? [Var_BED] : - (hasType(type_Bed, Var_BED) & -(f_located(Var_BED,Var_ROOM)))))))). - -fof(axMidLem372, axiom, - ( ! [Var_R] : - (hasType(type_Classroom, Var_R) => -(( ? [Var_S] : - (hasType(type_School, Var_S) & -(f_part(Var_R,Var_S)))))))). - -fof(axMidLem373, axiom, - ( ! [Var_PORCH] : - (hasType(type_Porch, Var_PORCH) => -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(f_connected(Var_PORCH,Var_BUILDING)))))))). - -fof(axMidLem374, axiom, - ( ! [Var_SIDE] : - (hasType(type_Sidewalk, Var_SIDE) => -(( ? [Var_ROAD] : - (hasType(type_Roadway, Var_ROAD) & -(f_orientation(Var_SIDE,Var_ROAD,inst_Near)))))))). - -fof(axMidLem375, axiom, - ( ! [Var_LAB] : - (hasType(type_Laboratory, Var_LAB) => -(( ? [Var_EXPERIMENT] : - (hasType(type_Experimenting, Var_EXPERIMENT) & -(f_located(Var_EXPERIMENT,Var_LAB)))))))). - -fof(axMidLem376, axiom, - ( ! [Var_BARN] : - (hasType(type_Barn, Var_BARN) => -(( ? [Var_FARM] : - (hasType(type_Farm, Var_FARM) & -(f_located(Var_BARN,Var_FARM)))))))). - -fof(axMidLem377, axiom, - ( ! [Var_STAGE] : - (hasType(type_PerformanceStage, Var_STAGE) => -(( ? [Var_AUDITORIUM] : - (hasType(type_Auditorium, Var_AUDITORIUM) & -(f_part(Var_STAGE,Var_AUDITORIUM)))))))). - -fof(axMidLem378, axiom, - ( ! [Var_W] : - (hasType(type_PerformanceStageWing, Var_W) => -(( ? [Var_S] : - (hasType(type_PerformanceStage, Var_S) & -(f_part(Var_W,Var_S)))))))). - -fof(axMidLem379, axiom, - ( ! [Var_BROADCAST] : - (hasType(type_Broadcasting, Var_BROADCAST) => -(( ? [Var_DEVICE] : - (hasType(type_CommunicationDevice, Var_DEVICE) & -(f_instrument(Var_BROADCAST,Var_DEVICE)))))))). - -fof(axMidLem380, axiom, - ( ! [Var_C] : - (hasType(type_PeriodicalPublisher, Var_C) => -(( ? [Var_PUBLISH] : - (hasType(type_Publication, Var_PUBLISH) & -(( ? [Var_PERIODICAL] : - (hasType(type_Periodical, Var_PERIODICAL) & -(((f_agent(Var_PUBLISH,Var_C)) & (f_patient(Var_PUBLISH,Var_PERIODICAL))))))))))))). - -fof(axMidLem381, axiom, - ( ! [Var_EXPLOSION] : - (hasType(type_Explosion, Var_EXPLOSION) => -(( ? [Var_PROC] : - (hasType(type_ChemicalProcess, Var_PROC) & -(f_causes(Var_PROC,Var_EXPLOSION)))))))). - -fof(axMidLem382, axiom, - ( ! [Var_PERFORMANCE] : - (hasType(type_Performance, Var_PERFORMANCE) => -(( ? [Var_SUB] : - ((hasType(type_DramaticActing, Var_SUB) | hasType(type_Music, Var_SUB)) & -(f_subProcess(Var_SUB,Var_PERFORMANCE)))))))). - -fof(axMidLem383, axiom, - ( ! [Var_PERFORMANCE] : - (hasType(type_Performance, Var_PERFORMANCE) => -(( ? [Var_STAGE] : - (hasType(type_PerformanceStage, Var_STAGE) & -(f_located(Var_PERFORMANCE,Var_STAGE)))))))). - -fof(axMidLem384, axiom, - ( ! [Var_R] : - (hasType(type_Reciting, Var_R) => -(( ? [Var_T] : - (hasType(type_Text, Var_T) & -(( ? [Var_P] : - (hasType(type_Proposition, Var_P) & -(((f_realization(Var_R,Var_P)) & (f_containsInformation(Var_T,Var_P))))))))))))). - -fof(axMidLem385, axiom, - ( ! [Var_SERMON] : - (hasType(type_Sermon, Var_SERMON) => -(( ? [Var_SERVICE] : - (hasType(type_ReligiousService, Var_SERVICE) & -(f_subProcess(Var_SERMON,Var_SERVICE)))))))). - -fof(axMidLem386, axiom, - ( ! [Var_CAST] : - (hasType(type_DramaticCast, Var_CAST) => -(( ? [Var_TEXT] : - (hasType(type_FictionalText, Var_TEXT) & -(( ? [Var_PROC] : - (hasType(type_Process, Var_PROC) & -(( ? [Var_PROP] : - (hasType(type_Proposition, Var_PROP) & -(((f_containsInformation(Var_TEXT,Var_PROP)) & (((f_realization(Var_PROC,Var_PROP)) & (( ! [Var_MEMBER] : - ((hasType(type_SelfConnectedObject, Var_MEMBER) & hasType(type_Agent, Var_MEMBER)) => -(((f_member(Var_MEMBER,Var_CAST)) => (( ? [Var_SUB] : - (hasType(type_DramaticActing, Var_SUB) & -(((f_agent(Var_SUB,Var_MEMBER)) & (f_subProcess(Var_SUB,Var_PROC)))))))))))))))))))))))))))). - -fof(axMidLem387, axiom, - ( ! [Var_MEETING] : - (hasType(type_FormalMeeting, Var_MEETING) => -(( ? [Var_PLANNING] : - (hasType(type_Planning, Var_PLANNING) & -(((f_result(Var_PLANNING,Var_MEETING)) & (f_earlier(f_WhenFn(Var_PLANNING),f_WhenFn(Var_MEETING))))))))))). - -fof(axMidLem388, axiom, - ( ! [Var_F] : - (hasType(type_Funeral, Var_F) => -(( ? [Var_D] : - (hasType(type_Death, Var_D) & -(f_refers(Var_F,Var_D)))))))). - -fof(axMidLem389, axiom, - ( ! [Var_RESOLUTION] : - (hasType(type_Resolution, Var_RESOLUTION) => -(( ? [Var_AGENT] : - (hasType(type_Organization, Var_AGENT) & -(( ? [Var_MEETING] : - (hasType(type_FormalMeeting, Var_MEETING) & -(((f_agent(Var_RESOLUTION,Var_AGENT)) & (f_subProcess(Var_RESOLUTION,Var_MEETING))))))))))))). - -fof(axMidLem390, axiom, - ( ! [Var_SMOKING] : - (hasType(type_Smoking, Var_SMOKING) => -(( ? [Var_BURN] : - (hasType(type_Combustion, Var_BURN) & -(( ? [Var_CIGAR] : - (hasType(type_CigarOrCigarette, Var_CIGAR) & -(( ? [Var_BREATHE] : - (hasType(type_Breathing, Var_BREATHE) & -(( ? [Var_SMOKE] : - (hasType(type_Entity, Var_SMOKE) & -(((f_subProcess(Var_BURN,Var_SMOKING)) & (((f_resourceS(Var_BURN,Var_CIGAR)) & (((f_result(Var_BURN,Var_SMOKE)) & (((f_patient(Var_BREATHE,Var_SMOKE)) & (f_subProcess(Var_BREATHE,Var_SMOKING))))))))))))))))))))))))). - -fof(axMidLem391, axiom, - ( ! [Var_CHARGE] : - (hasType(type_LegalCharge, Var_CHARGE) => -(( ? [Var_GOV] : - (hasType(type_Government, Var_GOV) & -(f_agent(Var_CHARGE,Var_GOV)))))))). - -fof(axMidLem392, axiom, - ( ! [Var_P] : - (hasType(type_Pleading, Var_P) => -(( ? [Var_J] : - (hasType(type_JudicialProcess, Var_J) & -(f_subProcess(Var_P,Var_J)))))))). - -fof(axMidLem393, axiom, - ( ! [Var_P] : - (hasType(type_Pleading, Var_P) => -(( ? [Var_C] : - (hasType(type_CriminalAction, Var_C) & -(f_refers(Var_P,Var_C)))))))). - -fof(axMidLem394, axiom, - ( ! [Var_TESTIFY] : - (hasType(type_Testifying, Var_TESTIFY) => -(( ? [Var_PROC] : - (hasType(type_JudicialProcess, Var_PROC) & -(f_subProcess(Var_TESTIFY,Var_PROC)))))))). - -fof(axMidLem395, axiom, - ( ! [Var_PROCESS] : - (hasType(type_JudicialProcess, Var_PROCESS) => -(( ? [Var_ROOM] : - (hasType(type_CourtRoom, Var_ROOM) & -(f_located(Var_PROCESS,Var_ROOM)))))))). - -fof(axMidLem396, axiom, - ( ! [Var_OPINION] : - (hasType(type_LegalOpinion, Var_OPINION) => -(( ? [Var_DECISION] : - (hasType(type_LegalDecision, Var_DECISION) & -(( ? [Var_PROPOSITION] : - ((hasType(type_Proposition, Var_PROPOSITION) & hasType(type_Argument, Var_PROPOSITION)) & -(( ? [Var_TEXT] : - ((hasType(type_Entity, Var_TEXT) & hasType(type_ContentBearingPhysical, Var_TEXT)) & -(((f_result(Var_DECISION,Var_TEXT)) & (((f_containsInformation(Var_TEXT,Var_PROPOSITION)) & (f_conclusion(Var_PROPOSITION,Var_OPINION)))))))))))))))))). - -fof(axMidLem397, axiom, - ( ! [Var_S] : - (hasType(type_Sentencing, Var_S) => -(( ! [Var_P] : - (hasType(type_Entity, Var_P) => -(((f_patient(Var_S,Var_P)) => (( ? [Var_C] : - (hasType(type_LegalConviction, Var_C) & -(((f_causes(Var_C,Var_S)) & (((f_patient(Var_C,Var_P)) & (f_earlier(f_WhenFn(Var_C),f_WhenFn(Var_S)))))))))))))))))). - -fof(axMidLem398, axiom, - ( ! [Var_CALL] : - (hasType(type_GameCall, Var_CALL) => -(( ? [Var_GAME] : - (hasType(type_Game, Var_GAME) & -(f_refers(Var_CALL,Var_GAME)))))))). - -fof(axMidLem399, axiom, - ( ! [Var_OP] : - (hasType(type_BeginningOperations, Var_OP) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((f_agent(Var_OP,Var_ORG)) => (f_starts(Var_OP,f_WhenFn(Var_ORG))))))))))). - -fof(axMidLem400, axiom, - ( ! [Var_OP] : - (hasType(type_CeasingOperations, Var_OP) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((f_agent(Var_OP,Var_ORG)) => (f_finishes(Var_OP,f_WhenFn(Var_ORG))))))))))). - -fof(axMidLem401, axiom, - ( ! [Var_B] : - (hasType(type_BecomingDrunk, Var_B) => -(( ! [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_Object, Var_A)) => -(((f_experiencer(Var_B,Var_A)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_B)),attribute(Var_A,inst_Sober))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_B)),attribute(Var_A,inst_Drunk))))))))))))). - -fof(axMidLem402, axiom, - ( ! [Var_B] : - (hasType(type_SoberingUp, Var_B) => -(( ! [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_Object, Var_A)) => -(((f_experiencer(Var_B,Var_A)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_B)),attribute(Var_A,inst_Drunk))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_B)),attribute(Var_A,inst_Sober))))))))))))). - -fof(axMidLem403, axiom, - ( ! [Var_FALL] : - (hasType(type_FallingAsleep, Var_FALL) => -(( ! [Var_AGENT] : - ((hasType(type_Entity, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_experiencer(Var_FALL,Var_AGENT)) => (( ? [Var_FINISH] : - ((hasType(type_TimeInterval, Var_FINISH) & hasType(type_TimePosition, Var_FINISH)) & -(( ? [Var_START] : - ((hasType(type_TimeInterval, Var_START) & hasType(type_TimePosition, Var_START)) & -(((f_starts(Var_START,f_WhenFn(Var_FALL))) & (((f_finishes(Var_FINISH,f_WhenFn(Var_FALL))) & (((f_holdsDuring(Var_START,attribute(Var_AGENT,inst_Awake))) & (f_holdsDuring(Var_FINISH,attribute(Var_AGENT,inst_Asleep))))))))))))))))))))))). - -fof(axMidLem404, axiom, - ( ! [Var_WAKE] : - (hasType(type_WakingUp, Var_WAKE) => -(( ! [Var_AGENT] : - ((hasType(type_Entity, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_experiencer(Var_WAKE,Var_AGENT)) => (( ? [Var_FINISH] : - ((hasType(type_TimeInterval, Var_FINISH) & hasType(type_TimePosition, Var_FINISH)) & -(( ? [Var_START] : - ((hasType(type_TimeInterval, Var_START) & hasType(type_TimePosition, Var_START)) & -(((f_starts(Var_START,f_WhenFn(Var_WAKE))) & (((f_finishes(Var_FINISH,f_WhenFn(Var_WAKE))) & (((f_holdsDuring(Var_START,attribute(Var_AGENT,inst_Asleep))) & (f_holdsDuring(Var_FINISH,attribute(Var_AGENT,inst_Awake))))))))))))))))))))))). - -fof(axMidLem405, axiom, - ( ! [Var_G] : - (hasType(type_GainingConsciousness, Var_G) => -(( ! [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_Object, Var_A)) => -(((f_experiencer(Var_G,Var_A)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_G)),attribute(Var_A,inst_Unconscious))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_G)),attribute(Var_A,inst_Awake))))))))))))). - -fof(axMidLem406, axiom, - ( ! [Var_L] : - (hasType(type_LosingConsciousness, Var_L) => -(( ! [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_Object, Var_A)) => -(((f_experiencer(Var_L,Var_A)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_L)),attribute(Var_A,inst_Awake))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_L)),attribute(Var_A,inst_Unconscious))))))))))))). - -fof(axMidLem407, axiom, - ( ! [Var_DEGREE] : - (hasType(type_AcademicDegree, Var_DEGREE) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) => -(((f_possesses(Var_AGENT,Var_DEGREE)) => (( ? [Var_PROGRAM] : - (hasType(type_EducationalProgram, Var_PROGRAM) & -(( ? [Var_STUDY] : - (hasType(type_Process, Var_STUDY) & -(((f_realization(Var_STUDY,Var_PROGRAM)) & (f_experiencer(Var_STUDY,Var_AGENT)))))))))))))))))). - -fof(axMidLem408, axiom, - ( ! [Var_L] : - (hasType(type_License, Var_L) => -(( ? [Var_ORG] : - (hasType(type_GovernmentOrganization, Var_ORG) & -(f_issuedBy(Var_L,Var_ORG)))))))). - -fof(axMidLem409, axiom, - ( ! [Var_P] : - (hasType(type_PassCertificate, Var_P) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Physical, Var_A)) => -(((f_possesses(Var_A,Var_P)) => (( ? [Var_L] : - (hasType(type_Object, Var_L) & -(f_confersNorm(Var_P,located(Var_A,Var_L),inst_Permission))))))))))))). - -fof(axMidLem410, axiom, - ( ! [Var_T] : - (hasType(type_Testament, Var_T) => -(( ? [Var_B] : - (hasType(type_Bequeathing, Var_B) & -(f_refers(Var_T,Var_B)))))))). - -fof(axMidLem411, axiom, - ( ! [Var_PROGRAM] : - (hasType(type_EducationalProgram, Var_PROGRAM) => -(( ? [Var_COURSE1] : - (hasType(type_EducationalCourse, Var_COURSE1) & -(( ? [Var_COURSE2] : - (hasType(type_EducationalCourse, Var_COURSE2) & -(((Var_COURSE1 != Var_COURSE2) & (((f_subPlan(Var_COURSE1,Var_PROGRAM)) & (f_subPlan(Var_COURSE2,Var_PROGRAM))))))))))))))). - -fof(axMidLem412, axiom, - ( ! [Var_COURSE] : - (hasType(type_EducationalCourse, Var_COURSE) => -(( ? [Var_CLASS] : - (hasType(type_EducationalProcess, Var_CLASS) & -(( ? [Var_ORG] : - (hasType(type_EducationalOrganization, Var_ORG) & -(((f_realization(Var_CLASS,Var_COURSE)) & (f_located(Var_CLASS,Var_ORG))))))))))))). - -fof(axMidLem413, axiom, - ( ! [Var_ENTER] : - (hasType(type_Matriculation, Var_ENTER) => -(( ! [Var_COLLEGE] : - (hasType(type_College, Var_COLLEGE) => -(( ! [Var_STUDENT] : - (hasType(type_Entity, Var_STUDENT) => -(((((f_agent(Var_ENTER,Var_COLLEGE)) & (f_patient(Var_ENTER,Var_STUDENT)))) => (( ? [Var_GRAD] : - (hasType(type_Graduation, Var_GRAD) & -(( ? [Var_SCHOOL] : - (hasType(type_HighSchool, Var_SCHOOL) & -(((f_agent(Var_GRAD,Var_SCHOOL)) & (((f_patient(Var_GRAD,Var_STUDENT)) & (f_earlier(f_WhenFn(Var_GRAD),f_WhenFn(Var_ENTER)))))))))))))))))))))))). - -fof(axMidLem414, axiom, - ( ! [Var_E] : - (hasType(type_Matriculation, Var_E) => -(( ! [Var_C] : - (hasType(type_College, Var_C) => -(( ! [Var_P] : - (hasType(type_Entity, Var_P) => -(((((f_agent(Var_E,Var_C)) & (f_patient(Var_E,Var_P)))) => (( ? [Var_G] : - (hasType(type_Graduation, Var_G) & -(( ? [Var_S] : - (hasType(type_SecondarySchool, Var_S) & -(((f_agent(Var_G,Var_S)) & (((f_patient(Var_G,Var_P)) & (f_earlier(f_WhenFn(Var_G),f_WhenFn(Var_E)))))))))))))))))))))))). - -fof(axMidLem415, axiom, - ( ! [Var_S] : - (hasType(type_GraduateSchool, Var_S) => -(( ? [Var_U] : - (hasType(type_University, Var_U) & -(f_part(Var_S,Var_U)))))))). - -fof(axMidLem416, axiom, - ( ! [Var_AS] : - (hasType(type_ArtSchool, Var_AS) => -(( ! [Var_P] : - (hasType(type_EducationalProcess, Var_P) => -(((f_located(Var_P,Var_AS)) => (( ? [Var_M] : - (hasType(type_Making, Var_M) & -(( ? [Var_ART] : - (hasType(type_ArtWork, Var_ART) & -(((f_patient(Var_M,Var_ART)) & (f_refers(Var_P,Var_M)))))))))))))))))). - -fof(axMidLem417, axiom, - ( ! [Var_DS] : - (hasType(type_DaySchool, Var_DS) => -(( ~ ( ? [Var_S] : - ((hasType(type_CognitiveAgent, Var_S) & hasType(type_Human, Var_S)) & -(((f_student(Var_DS,Var_S)) & (f_home(Var_S,Var_DS))))))))))). - -fof(axMidLem418, axiom, - ( ! [Var_AGENT] : - ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) => -(( ! [Var_ORG] : - ((hasType(type_EducationalOrganization, Var_ORG) & hasType(type_Object, Var_ORG)) => -(((f_student(Var_ORG,Var_AGENT)) => (( ? [Var_PROCESS] : - (hasType(type_EducationalProcess, Var_PROCESS) & -(((f_located(Var_PROCESS,Var_ORG)) & (f_destination(Var_PROCESS,Var_AGENT))))))))))))))). - -fof(axMidLem419, axiom, - ( ! [Var_AGENT] : - ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) => -(( ! [Var_ORG] : - ((hasType(type_EducationalOrganization, Var_ORG) & hasType(type_Object, Var_ORG)) => -(((f_teacher(Var_ORG,Var_AGENT)) => (( ? [Var_PROCESS] : - (hasType(type_EducationalProcess, Var_PROCESS) & -(((f_located(Var_PROCESS,Var_ORG)) & (f_agent(Var_PROCESS,Var_AGENT))))))))))))))). - -fof(axMidLem420, axiom, - ( ! [Var_TEL] : - (hasType(type_Telephoning, Var_TEL) => -(( ? [Var_DEVICE] : - (hasType(type_Telephone, Var_DEVICE) & -(f_instrument(Var_TEL,Var_DEVICE)))))))). - -fof(axMidLem421, axiom, - ( ! [Var_STRIKE] : - (hasType(type_LaborStriking, Var_STRIKE) => -(( ! [Var_PERSON] : - (hasType(type_Human, Var_PERSON) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((((f_agent(Var_STRIKE,Var_PERSON)) & (f_patient(Var_STRIKE,Var_ORG)))) => (f_employs(Var_ORG,Var_PERSON))))))))))))). - -fof(axMidLem422, axiom, - ( ! [Var_R] : - (hasType(type_Resigning, Var_R) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_CognitiveAgent, Var_A)) => -(((f_agent(Var_R,Var_A)) => (f_wants(Var_A,Var_R)))))))))). - -fof(axMidLem423, axiom, - ( ! [Var_T] : - (hasType(type_TransferringPosition, Var_T) => -(( ! [Var_H] : - ((hasType(type_Entity, Var_H) & hasType(type_Human, Var_H)) => -(((f_experiencer(Var_T,Var_H)) => (( ? [Var_ORG] : - (hasType(type_Organization, Var_ORG) & -(( ? [Var_P2] : - ((hasType(type_Position, Var_P2) & hasType(type_Entity, Var_P2)) & -(( ? [Var_P1] : - ((hasType(type_Position, Var_P1) & hasType(type_Entity, Var_P1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_T)),occupiesPosition(Var_H,Var_P1,Var_ORG))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_T)),occupiesPosition(Var_H,Var_P2,Var_ORG))) & (Var_P1 != Var_P2)))))))))))))))))))))). - -fof(axMidLem424, axiom, - ( ! [Var_MONEY] : - (hasType(type_CurrencyMeasure, Var_MONEY) => -(( ! [Var_TIME] : - (hasType(type_TimeDuration, Var_TIME) => -(( ! [Var_PERSON] : - ((hasType(type_Human, Var_PERSON) & hasType(type_CognitiveAgent, Var_PERSON)) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((f_monetaryWage(Var_ORG,Var_PERSON,Var_TIME,Var_MONEY)) => (f_employs(Var_ORG,Var_PERSON)))))))))))))))). - -fof(axMidLem425, axiom, - ( ! [Var_SHOT] : - (hasType(type_GameShot, Var_SHOT) => -(( ? [Var_PIECE] : - (hasType(type_GamePiece, Var_PIECE) & -(f_patient(Var_SHOT,Var_PIECE)))))))). - -fof(axMidLem426, axiom, - ( ! [Var_SHOT] : - (hasType(type_GameShot, Var_SHOT) => -(( ? [Var_GAME] : - (hasType(type_Game, Var_GAME) & -(f_subProcess(Var_SHOT,Var_GAME)))))))). - -fof(axMidLem427, axiom, - ( ! [Var_GOAL] : - (hasType(type_GameGoal, Var_GOAL) => -(( ! [Var_GAME] : - (hasType(type_Game, Var_GAME) => -(( ! [Var_SCORE] : - (hasType(type_Score, Var_SCORE) => -(((((f_instrument(Var_GAME,Var_GOAL)) & (f_subProcess(Var_SCORE,Var_GAME)))) => (( ? [Var_PIECE] : - (hasType(type_GamePiece, Var_PIECE) & -(( ? [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) & -(((f_patient(Var_SCORE,Var_PIECE)) & (((f_temporalPart(Var_TIME,f_WhenFn(Var_SCORE))) & (f_holdsDuring(Var_TIME,located(Var_PIECE,Var_GOAL)))))))))))))))))))))))). - -fof(axMidLem428, axiom, - ( ! [Var_SS] : - (hasType(type_SportServe, Var_SS) => -(( ? [Var_S] : - (hasType(type_Sport, Var_S) & -(((f_subProcess(Var_SS,Var_S)) & (f_starts(f_WhenFn(Var_SS),f_WhenFn(Var_S))))))))))). - -fof(axMidLem429, axiom, - ( ! [Var_THROW] : - (hasType(type_Throwing, Var_THROW) => -(( ? [Var_ARM] : - (hasType(type_Arm, Var_ARM) & -(f_instrument(Var_THROW,Var_ARM)))))))). - -fof(axMidLem430, axiom, - ( ! [Var_CATCH] : - (hasType(type_Catching, Var_CATCH) => -(( ! [Var_BALL] : - ((hasType(type_Entity, Var_BALL) & hasType(type_Object, Var_BALL)) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Animal, Var_AGENT)) => -(((((f_agent(Var_CATCH,Var_AGENT)) & (f_patient(Var_CATCH,Var_BALL)))) => (f_holdsDuring(f_EndFn(f_WhenFn(Var_CATCH)),grasps(Var_AGENT,Var_BALL)))))))))))))). - -fof(axMidLem431, axiom, - ( ! [Var_C] : - (hasType(type_PlayingCard, Var_C) => -(f_material(type_Paper,Var_C))))). - -fof(axMidLem432, axiom, - ( ! [Var_ACCELERATE] : - (hasType(type_Accelerating, Var_ACCELERATE) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_ACCELERATE,Var_AGENT)) => (( ? [Var_TIME2] : - ((hasType(type_TimeDuration, Var_TIME2) & hasType(type_Quantity, Var_TIME2)) & -(( ? [Var_TIME1] : - ((hasType(type_TimeDuration, Var_TIME1) & hasType(type_Quantity, Var_TIME1)) & -(( ? [Var_LENGTH2] : - ((hasType(type_LengthMeasure, Var_LENGTH2) & hasType(type_Quantity, Var_LENGTH2)) & -(( ? [Var_LENGTH1] : - ((hasType(type_LengthMeasure, Var_LENGTH1) & hasType(type_Quantity, Var_LENGTH1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_ACCELERATE)),measure(Var_AGENT,f_SpeedFn(Var_LENGTH1,Var_TIME1)))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_ACCELERATE)),measure(Var_AGENT,f_SpeedFn(Var_LENGTH2,Var_TIME2)))) & (((f_greaterThan(Var_LENGTH2,Var_LENGTH1)) | (f_greaterThan(Var_TIME2,Var_TIME1)))))))))))))))))))))))))))). - -fof(axMidLem433, axiom, - ( ! [Var_D] : - (hasType(type_Decelerating, Var_D) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Object, Var_A)) => -(((f_agent(Var_D,Var_A)) => (( ? [Var_T2] : - ((hasType(type_TimeDuration, Var_T2) & hasType(type_Quantity, Var_T2)) & -(( ? [Var_T1] : - ((hasType(type_TimeDuration, Var_T1) & hasType(type_Quantity, Var_T1)) & -(( ? [Var_L2] : - ((hasType(type_LengthMeasure, Var_L2) & hasType(type_Quantity, Var_L2)) & -(( ? [Var_L1] : - ((hasType(type_LengthMeasure, Var_L1) & hasType(type_Quantity, Var_L1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_D)),measure(Var_A,f_SpeedFn(Var_L1,Var_T1)))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_D)),measure(Var_A,f_SpeedFn(Var_L2,Var_T2)))) & (((f_greaterThan(Var_L1,Var_L2)) | (f_greaterThan(Var_T1,Var_T2)))))))))))))))))))))))))))). - -fof(axMidLem434, axiom, - ( ! [Var_S] : - (hasType(type_Shortening, Var_S) => -(( ! [Var_O] : - ((hasType(type_Entity, Var_O) & hasType(type_Object, Var_O)) => -(((f_patient(Var_S,Var_O)) => (( ? [Var_L2] : - ((hasType(type_PhysicalQuantity, Var_L2) & hasType(type_Quantity, Var_L2)) & -(( ? [Var_L1] : - ((hasType(type_PhysicalQuantity, Var_L1) & hasType(type_Quantity, Var_L1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_S)),length(Var_O,Var_L1))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_S)),length(Var_O,Var_L2))) & (f_greaterThan(Var_L1,Var_L2)))))))))))))))))))). - -fof(axMidLem435, axiom, - ( ! [Var_FLY] : - (hasType(type_Flying, Var_FLY) => -(( ? [Var_REGION] : - (hasType(type_AtmosphericRegion, Var_REGION) & -(f_located(Var_FLY,Var_REGION)))))))). - -fof(axMidLem436, axiom, - ( ! [Var_RETURN] : - (hasType(type_Returning, Var_RETURN) => -(( ! [Var_DEST] : - ((hasType(type_Entity, Var_DEST) & hasType(type_Object, Var_DEST)) => -(( ! [Var_AGENT] : - ((hasType(type_Entity, Var_AGENT) & hasType(type_Physical, Var_AGENT)) => -(((((f_experiencer(Var_RETURN,Var_AGENT)) & (f_destination(Var_RETURN,Var_DEST)))) => (( ? [Var_TIME] : - ((hasType(type_TimeInterval, Var_TIME) & hasType(type_TimePosition, Var_TIME)) & -(((f_earlier(Var_TIME,f_WhenFn(Var_RETURN))) & (f_holdsDuring(Var_TIME,located(Var_AGENT,Var_DEST))))))))))))))))))). - -fof(axMidLem437, axiom, - ( ! [Var_ESCAPE] : - (hasType(type_Escaping, Var_ESCAPE) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) => -(((f_agent(Var_ESCAPE,Var_AGENT)) => (( ? [Var_CONFINE] : - (hasType(type_Confining, Var_CONFINE) & -(((f_patient(Var_CONFINE,Var_AGENT)) & (f_meetsTemporally(f_WhenFn(Var_CONFINE),f_WhenFn(Var_ESCAPE)))))))))))))))). - -fof(axMidLem438, axiom, - ( ! [Var_ESCAPE] : - (hasType(type_Escaping, Var_ESCAPE) => -(( ! [Var_AGENT] : - (hasType(type_CognitiveAgent, Var_AGENT) => -(( ~ (f_holdsRight(agent(Var_ESCAPE,Var_AGENT),Var_AGENT)))))))))). - -fof(axMidLem439, axiom, - ( ! [Var_LEAVE] : - (hasType(type_Leaving, Var_LEAVE) => -(( ? [Var_GO] : - (hasType(type_Translocation, Var_GO) & -(((f_subProcess(Var_LEAVE,Var_GO)) & (f_starts(f_WhenFn(Var_LEAVE),f_WhenFn(Var_GO))))))))))). - -fof(axMidLem440, axiom, - ( ! [Var_ARRIVE] : - (hasType(type_Arriving, Var_ARRIVE) => -(( ? [Var_GO] : - (hasType(type_Translocation, Var_GO) & -(((f_subProcess(Var_ARRIVE,Var_GO)) & (f_finishes(f_WhenFn(Var_ARRIVE),f_WhenFn(Var_GO))))))))))). - -fof(axMidLem441, axiom, - ( ! [Var_I] : - (hasType(type_Immigrating, Var_I) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_SelfConnectedObject, Var_A) & hasType(type_Organism, Var_A)) => -(((f_agent(Var_I,Var_A)) => (( ? [Var_N1] : - (hasType(type_Nation, Var_N1) & -(( ? [Var_N2] : - (hasType(type_Nation, Var_N2) & -(((f_origin(Var_I,Var_N1)) & (((f_destination(Var_I,Var_N2)) & (((Var_N1 != Var_N2) & (((f_member(Var_A,f_CitizenryFn(Var_N1))) & (((( ~ (f_member(Var_A,f_CitizenryFn(Var_N2))))) & (f_hasPurpose(Var_I,inhabits(Var_A,Var_N2))))))))))))))))))))))))))). - -fof(axMidLem442, axiom, - ( ! [Var_V] : - ((hasType(type_Vehicle, Var_V) & hasType(type_SelfConnectedObject, Var_V)) => -(( ! [Var_O] : - ((hasType(type_SelfConnectedObject, Var_O) & hasType(type_Object, Var_O)) => -(((f_onboard(Var_O,Var_V)) => (f_contains(Var_V,Var_O)))))))))). - -fof(axMidLem443, axiom, - ( ! [Var_T] : - (hasType(type_Transportation, Var_T) => -(( ! [Var_V] : - ((hasType(type_Vehicle, Var_V) & hasType(type_Object, Var_V)) => -(( ! [Var_O] : - ((hasType(type_SelfConnectedObject, Var_O) & hasType(type_Entity, Var_O)) => -(((((f_onboard(Var_O,Var_V)) & (f_instrument(Var_T,Var_V)))) => (f_patient(Var_T,Var_O))))))))))))). - -fof(axMidLem444, axiom, - ( ! [Var_R] : - (hasType(type_Rotating, Var_R) => -(( ! [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_Physical, Var_A)) => -(((f_experiencer(Var_R,Var_A)) => (( ? [Var_L] : - (hasType(type_Object, Var_L) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_R)),located(Var_A,Var_L))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_R)),located(Var_A,Var_L)))))))))))))))). - -fof(axMidLem445, axiom, - ( ! [Var_CM] : - (hasType(type_CentrifugalMotion, Var_CM) => -(( ? [Var_R] : - (hasType(type_Rotating, Var_R) & -(( ? [Var_O2] : - (hasType(type_Entity, Var_O2) & -(( ? [Var_O1] : - ((hasType(type_Object, Var_O1) & hasType(type_Entity, Var_O1)) & -(( ? [Var_A] : - (hasType(type_Object, Var_A) & -(((f_axis(Var_A,Var_O1)) & (((f_origin(Var_CM,Var_A)) & (((f_experiencer(Var_R,Var_O1)) & (((f_experiencer(Var_CM,Var_O2)) & (f_causes(Var_R,Var_CM))))))))))))))))))))))))). - -fof(axMidLem446, axiom, - ( ! [Var_CM] : - (hasType(type_CentripetalMotion, Var_CM) => -(( ? [Var_R] : - (hasType(type_Rotating, Var_R) & -(( ? [Var_O2] : - (hasType(type_Entity, Var_O2) & -(( ? [Var_O1] : - ((hasType(type_Object, Var_O1) & hasType(type_Entity, Var_O1)) & -(( ? [Var_A] : - ((hasType(type_Object, Var_A) & hasType(type_Entity, Var_A)) & -(((f_axis(Var_A,Var_O1)) & (((f_destination(Var_CM,Var_A)) & (((f_experiencer(Var_R,Var_O1)) & (((f_experiencer(Var_CM,Var_O2)) & (f_causes(Var_R,Var_CM))))))))))))))))))))))))). - -fof(axMidLem447, axiom, - ( ! [Var_POUR] : - (hasType(type_Pouring, Var_POUR) => -(( ? [Var_LIQUID] : - (hasType(type_Substance, Var_LIQUID) & -(( ? [Var_CONTAINER1] : - (hasType(type_Container, Var_CONTAINER1) & -(( ? [Var_CONTAINER2] : - (hasType(type_Container, Var_CONTAINER2) & -(((f_origin(Var_POUR,Var_CONTAINER1)) & (((f_destination(Var_POUR,Var_CONTAINER2)) & (((Var_CONTAINER1 != Var_CONTAINER2) & (((f_patient(Var_POUR,Var_LIQUID)) & (f_attribute(Var_LIQUID,inst_Liquid)))))))))))))))))))))). - -fof(axMidLem448, axiom, - ( ! [Var_WAVE] : - (hasType(type_WaterWave, Var_WAVE) => -(( ? [Var_AREA] : - (hasType(type_WaterArea, Var_AREA) & -(f_located(Var_WAVE,Var_AREA)))))))). - -fof(axMidLem449, axiom, - ( ! [Var_F] : - (hasType(type_Flooding, Var_F) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_WaterArea, Var_P)) => -(((f_located(Var_F,Var_P)) => (( ? [Var_L2] : - ((hasType(type_LengthMeasure, Var_L2) & hasType(type_Quantity, Var_L2)) & -(( ? [Var_L1] : - ((hasType(type_LengthMeasure, Var_L1) & hasType(type_Quantity, Var_L1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_F)),waterDepth(Var_P,Var_L1))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_F)),waterDepth(Var_P,Var_L2))) & (f_greaterThan(Var_L2,Var_L1)))))))))))))))))))). - -fof(axMidLem450, axiom, - ( ! [Var_TT] : - (hasType(type_TractorTrailer, Var_TT) => -(( ? [Var_TRAC] : - (hasType(type_TruckTractor, Var_TRAC) & -(( ? [Var_TRAIL] : - (hasType(type_TruckTrailer, Var_TRAIL) & -(((f_part(Var_TRAC,Var_TT)) & (((f_part(Var_TRAIL,Var_TT)) & (f_connected(Var_TRAC,Var_TRAIL))))))))))))))). - -fof(axMidLem451, axiom, - ( ! [Var_TRANSPORT] : - (hasType(type_AirTransportation, Var_TRANSPORT) => -(( ? [Var_CRAFT] : - (hasType(type_Aircraft, Var_CRAFT) & -(( ? [Var_REGION] : - (hasType(type_AtmosphericRegion, Var_REGION) & -(((f_instrument(Var_TRANSPORT,Var_CRAFT)) & (f_located(Var_TRANSPORT,Var_REGION))))))))))))). - -fof(axMidLem452, axiom, - ( ! [Var_D] : - (hasType(type_ExplosiveDevice, Var_D) => -(( ? [Var_S] : - (hasType(type_ExplosiveSubstance, Var_S) & -(f_part(Var_S,Var_D)))))))). - -fof(axMidLem453, axiom, - ( ! [Var_LAND] : - (hasType(type_LandTransportation, Var_LAND) => -(( ? [Var_CRAFT] : - (hasType(type_LandVehicle, Var_CRAFT) & -(( ? [Var_AREA] : - (hasType(type_LandArea, Var_AREA) & -(((f_instrument(Var_LAND,Var_CRAFT)) & (f_located(Var_CRAFT,Var_AREA))))))))))))). - -fof(axMidLem454, axiom, - ( ! [Var_A] : - (hasType(type_Automobile, Var_A) => -(f_equipmentCount(Var_A,type_VehicleWheel,4))))). - -fof(axMidLem455, axiom, - ( ! [Var_A] : - (hasType(type_Automobile, Var_A) => -(f_equipmentCount(Var_A,type_Axle,2))))). - -fof(axMidLem456, axiom, - ( ! [Var_M] : - (hasType(type_Motorcycle, Var_M) => -(f_equipmentCount(Var_M,type_VehicleWheel,2))))). - -fof(axMidLem457, axiom, - ( ! [Var_TRANSPORT] : - (hasType(type_WaterTransportation, Var_TRANSPORT) => -(( ? [Var_CRAFT] : - (hasType(type_WaterVehicle, Var_CRAFT) & -(( ? [Var_AREA] : - (hasType(type_WaterArea, Var_AREA) & -(((f_instrument(Var_TRANSPORT,Var_CRAFT)) & (f_located(Var_TRANSPORT,Var_AREA))))))))))))). - -fof(axMidLem458, axiom, - ( ! [Var_R] : - (hasType(type_Rowing, Var_R) => -(( ? [Var_O] : - (hasType(type_Oar, Var_O) & -(f_instrument(Var_R,Var_O)))))))). - -fof(axMidLem459, axiom, - ( ! [Var_D] : - (hasType(type_BoatDeck, Var_D) => -(( ? [Var_B] : - (hasType(type_WaterVehicle, Var_B) & -(f_part(Var_D,Var_B)))))))). - -fof(axMidLem460, axiom, - ( ! [Var_TRANSPORT] : - (hasType(type_SpaceTransportation, Var_TRANSPORT) => -(( ? [Var_CRAFT] : - (hasType(type_Spacecraft, Var_CRAFT) & -(( ? [Var_REGION] : - (hasType(type_SpaceRegion, Var_REGION) & -(((f_instrument(Var_TRANSPORT,Var_CRAFT)) & (f_located(Var_TRANSPORT,Var_REGION))))))))))))). - -fof(axMidLem461, axiom, - ( ! [Var_M] : - (hasType(type_Missile, Var_M) => -(( ? [Var_B] : - (hasType(type_Bomb, Var_B) & -(f_part(Var_B,Var_M)))))))). - -fof(axMidLem462, axiom, - ( ! [Var_B] : - (hasType(type_Burying, Var_B) => -(( ? [Var_C] : - (hasType(type_Covering, Var_C) & -(( ? [Var_S] : - (hasType(type_Soil, Var_S) & -(((f_instrument(Var_C,Var_S)) & (f_subProcess(Var_C,Var_B))))))))))))). - -fof(axMidLem463, axiom, - ( ! [Var_D] : - (hasType(type_Digging, Var_D) => -(( ? [Var_S] : - (hasType(type_Soil, Var_S) & -(f_patient(Var_D,Var_S)))))))). - -fof(axMidLem464, axiom, - ( ! [Var_T] : - (hasType(type_Tilling, Var_T) => -(( ? [Var_A] : - (hasType(type_Agriculture, Var_A) & -(f_subProcess(Var_T,Var_A)))))))). - -fof(axMidLem465, axiom, - ( ! [Var_MOVE] : - (hasType(type_MovingResidence, Var_MOVE) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Human, Var_AGENT)) => -(((f_agent(Var_MOVE,Var_AGENT)) => (( ? [Var_HOME2] : - ((hasType(type_PermanentResidence, Var_HOME2) & hasType(type_Entity, Var_HOME2)) & -(( ? [Var_HOME1] : - ((hasType(type_PermanentResidence, Var_HOME1) & hasType(type_Entity, Var_HOME1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_MOVE)),home(Var_AGENT,Var_HOME1))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_MOVE)),home(Var_AGENT,Var_HOME2))) & (Var_HOME1 != Var_HOME2))))))))))))))))))). - -fof(axMidLem466, axiom, - ( ! [Var_H] : - (hasType(type_Harvesting, Var_H) => -(( ? [Var_A] : - (hasType(type_Agriculture, Var_A) & -(f_subProcess(Var_H,Var_A)))))))). - -fof(axMidLem467, axiom, - ( ! [Var_DREAM] : - (hasType(type_Dreaming, Var_DREAM) => -(( ! [Var_AGENT] : - ((hasType(type_Entity, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_experiencer(Var_DREAM,Var_AGENT)) => (f_holdsDuring(f_WhenFn(Var_DREAM),attribute(Var_AGENT,inst_Asleep))))))))))). - -fof(axMidLem468, axiom, - ( ! [Var_E] : - (hasType(type_Execution, Var_E) => -(( ? [Var_G] : - (hasType(type_Government, Var_G) & -(f_agent(Var_E,Var_G)))))))). - -fof(axMidLem469, axiom, - ( ! [Var_E] : - (hasType(type_Execution, Var_E) => -(( ? [Var_P] : - (hasType(type_Human, Var_P) & -(f_patient(Var_E,Var_P)))))))). - -fof(axMidLem470, axiom, - ( ! [Var_S] : - (hasType(type_Suicide, Var_S) => -(( ? [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Entity, Var_A)) & -(((f_agent(Var_S,Var_A)) & (f_experiencer(Var_S,Var_A)))))))))). - -fof(axMidLem471, axiom, - ( ! [Var_T] : - (hasType(type_Trespassing, Var_T) => -(( ! [Var_P] : - ((hasType(type_Entity, Var_P) & hasType(type_Object, Var_P)) => -(( ! [Var_H] : - ((hasType(type_Agent, Var_H) & hasType(type_Physical, Var_H)) => -(((((f_agent(Var_T,Var_H)) & (f_patient(Var_T,Var_P)))) => (((( ~ (f_possesses(Var_H,Var_P)))) & (f_modalAttribute(located(Var_H,Var_P),inst_Illegal))))))))))))))). - -fof(axMidLem472, axiom, - ( ! [Var_MURDER] : - (hasType(type_Murder, Var_MURDER) => -(( ? [Var_PERSON] : - (hasType(type_Human, Var_PERSON) & -(f_patient(Var_MURDER,Var_PERSON)))))))). - -fof(axMidLem473, axiom, - ( ! [Var_H] : - (hasType(type_Hanging, Var_H) => -(( ? [Var_S] : - (hasType(type_String, Var_S) & -(( ? [Var_N] : - (hasType(type_Neck, Var_N) & -(( ? [Var_P] : - (hasType(type_Human, Var_P) & -(((f_experiencer(Var_H,Var_P)) & (((f_properPart(Var_N,Var_P)) & (((f_instrument(Var_H,Var_S)) & (f_holdsDuring(f_WhenFn(Var_H),meetsSpatially(Var_S,Var_N))))))))))))))))))))). - -fof(axMidLem474, axiom, - ( ! [Var_CONDUCT] : - (hasType(type_OrchestralConducting, Var_CONDUCT) => -(( ? [Var_MUSIC] : - (hasType(type_Music, Var_MUSIC) & -(f_result(Var_CONDUCT,Var_MUSIC)))))))). - -fof(axMidLem475, axiom, - ( ! [Var_SHARE] : - (hasType(type_Sharing, Var_SHARE) => -(( ! [Var_OBJ] : - ((hasType(type_Entity, Var_OBJ) & hasType(type_Object, Var_OBJ)) => -(( ! [Var_AGENT2] : - (hasType(type_Entity, Var_AGENT2) => -(( ! [Var_AGENT1] : - (hasType(type_Agent, Var_AGENT1) => -(((((f_agent(Var_SHARE,Var_AGENT1)) & (((f_destination(Var_SHARE,Var_AGENT2)) & (f_patient(Var_SHARE,Var_OBJ)))))) => (( ? [Var_GIVE] : - (hasType(type_Giving, Var_GIVE) & -(( ? [Var_PART] : - ((hasType(type_Entity, Var_PART) & hasType(type_Object, Var_PART)) & -(((f_subProcess(Var_GIVE,Var_SHARE)) & (((f_patient(Var_GIVE,Var_PART)) & (((f_properPart(Var_PART,Var_OBJ)) & (((f_agent(Var_GIVE,Var_AGENT1)) & (f_destination(Var_GIVE,Var_AGENT2)))))))))))))))))))))))))))))). - -fof(axMidLem476, axiom, - ( ! [Var_STEAL] : - (hasType(type_Stealing, Var_STEAL) => -(( ! [Var_VICTIM] : - (hasType(type_CognitiveAgent, Var_VICTIM) => -(( ! [Var_AGENT] : - ((hasType(type_Entity, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) => -(((((f_destination(Var_STEAL,Var_AGENT)) & (f_origin(Var_STEAL,Var_VICTIM)))) => (( ~ (f_confersRight(destination(Var_STEAL,Var_AGENT),Var_VICTIM,Var_AGENT))))))))))))))). - -fof(axMidLem477, axiom, - ( ! [Var_INHERIT] : - (hasType(type_Inheriting, Var_INHERIT) => -(( ! [Var_PROPERTY] : - ((hasType(type_Entity, Var_PROPERTY) & hasType(type_Object, Var_PROPERTY)) => -(( ! [Var_PERSON] : - ((hasType(type_Object, Var_PERSON) & hasType(type_Entity, Var_PERSON) & hasType(type_Agent, Var_PERSON)) => -(( ! [Var_HEIR] : - ((hasType(type_Agent, Var_HEIR) & hasType(type_CognitiveAgent, Var_HEIR)) => -(((((f_agent(Var_INHERIT,Var_HEIR)) & (((f_origin(Var_INHERIT,Var_PERSON)) & (f_patient(Var_INHERIT,Var_PROPERTY)))))) => (( ? [Var_DEATH] : - (hasType(type_Death, Var_DEATH) & -(((f_experiencer(Var_DEATH,Var_PERSON)) & (((f_earlier(f_WhenFn(Var_DEATH),f_WhenFn(Var_INHERIT))) & (((f_holdsDuring(f_ImmediatePastFn(f_WhenFn(Var_DEATH)),possesses(Var_PERSON,Var_PROPERTY))) & (f_confersRight(possesses(Var_HEIR,Var_PROPERTY),Var_PERSON,Var_HEIR))))))))))))))))))))))))). - -fof(axMidLem478, axiom, - ( ! [Var_B] : - (hasType(type_Bequeathing, Var_B) => -(( ! [Var_PROP] : - ((hasType(type_Entity, Var_PROP) & hasType(type_Object, Var_PROP)) => -(( ! [Var_I] : - (hasType(type_Process, Var_I) => -(( ! [Var_H] : - ((hasType(type_Entity, Var_H) & hasType(type_Agent, Var_H)) => -(( ! [Var_P] : - ((hasType(type_Agent, Var_P) & hasType(type_Entity, Var_P)) => -(((((f_agent(Var_B,Var_P)) & (((f_destination(Var_B,Var_H)) & (f_patient(Var_I,Var_PROP)))))) => (( ? [Var_D] : - (hasType(type_Death, Var_D) & -(((f_experiencer(Var_D,Var_P)) & (((f_earlier(f_WhenFn(Var_D),f_WhenFn(Var_B))) & (((f_holdsDuring(f_ImmediatePastFn(f_WhenFn(Var_D)),possesses(Var_P,Var_PROP))) & (f_confersNorm(Var_P,possesses(Var_H,Var_PROP),inst_Permission)))))))))))))))))))))))))))). - -fof(axMidLem479, axiom, - ( ! [Var_ORG] : - ((hasType(type_Organization, Var_ORG) & hasType(type_EducationalOrganization, Var_ORG)) => -(( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_CognitiveAgent, Var_H)) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Position, Var_P)) => -(((((f_attribute(Var_P,inst_CollegeFreshman)) & (f_occupiesPosition(Var_H,Var_P,Var_ORG)))) => (( ? [Var_T] : - ((hasType(type_TimePosition, Var_T) & hasType(type_Quantity, Var_T)) & -(((f_holdsDuring(Var_T,student(Var_ORG,Var_H))) & (f_lessThan(Var_T,f_MeasureFn(1,inst_YearDuration))))))))))))))))))). - -fof(axMidLem480, axiom, - ( ! [Var_ORG] : - ((hasType(type_Organization, Var_ORG) & hasType(type_EducationalOrganization, Var_ORG)) => -(( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_CognitiveAgent, Var_H)) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Position, Var_P)) => -(((((f_attribute(Var_P,inst_CollegeJunior)) & (f_occupiesPosition(Var_H,Var_P,Var_ORG)))) => (( ? [Var_T] : - ((hasType(type_TimePosition, Var_T) & hasType(type_Quantity, Var_T)) & -(((f_holdsDuring(Var_T,student(Var_ORG,Var_H))) & (((f_greaterThanOrEqualTo(Var_T,f_MeasureFn(2,inst_YearDuration))) & (f_lessThan(Var_T,f_MeasureFn(3,inst_YearDuration))))))))))))))))))))). - -fof(axMidLem481, axiom, - ( ! [Var_ORG] : - ((hasType(type_Organization, Var_ORG) & hasType(type_EducationalOrganization, Var_ORG)) => -(( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_CognitiveAgent, Var_H)) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Position, Var_P)) => -(((((f_attribute(Var_P,inst_CollegeJunior)) & (f_occupiesPosition(Var_H,Var_P,Var_ORG)))) => (( ? [Var_T] : - ((hasType(type_TimePosition, Var_T) & hasType(type_Quantity, Var_T)) & -(((f_holdsDuring(Var_T,student(Var_ORG,Var_H))) & (((f_greaterThanOrEqualTo(Var_T,f_MeasureFn(3,inst_YearDuration))) & (f_lessThan(Var_T,f_MeasureFn(4,inst_YearDuration))))))))))))))))))))). - -fof(axMidLem482, axiom, - ( ! [Var_ORG] : - ((hasType(type_Organization, Var_ORG) & hasType(type_EducationalOrganization, Var_ORG)) => -(( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_CognitiveAgent, Var_H)) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Position, Var_P)) => -(((((f_attribute(Var_P,inst_CollegeSophomore)) & (f_occupiesPosition(Var_H,Var_P,Var_ORG)))) => (( ? [Var_T] : - ((hasType(type_TimePosition, Var_T) & hasType(type_Quantity, Var_T)) & -(((f_holdsDuring(Var_T,student(Var_ORG,Var_H))) & (((f_greaterThanOrEqualTo(Var_T,f_MeasureFn(2,inst_YearDuration))) & (f_lessThan(Var_T,f_MeasureFn(2,inst_YearDuration))))))))))))))))))))). - -fof(axMidLem483, axiom, - ( ! [Var_PREF] : - (hasType(type_Process, Var_PREF) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Agent, Var_P)) => -(((f_attribute(Var_P,inst_Comedian)) => (( ? [Var_PERF] : - (hasType(type_Performance, Var_PERF) & -(( ? [Var_L] : - (hasType(type_Laughing, Var_L) & -(((f_agent(Var_PREF,Var_P)) & (f_causes(Var_PERF,Var_L)))))))))))))))))). - -fof(axMidLem484, axiom, - ( ! [Var_H] : - ((hasType(type_Object, Var_H) & hasType(type_Agent, Var_H)) => -(((f_attribute(Var_H,inst_PresidentOfTheUnitedStates)) => (f_leader(Var_H,inst_UnitedStates))))))). - -fof(axMidLem485, axiom, - ( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Agent, Var_P)) => -(((f_attribute(Var_P,inst_Dentist)) => (( ? [Var_D] : - (hasType(type_DiagnosticProcess, Var_D) & -(( ? [Var_T] : - (hasType(type_Tooth, Var_T) & -(((f_agent(Var_D,Var_P)) & (f_patient(Var_D,Var_T))))))))))))))). - -fof(axMidLem486, axiom, - ( ! [Var_R] : - (hasType(type_Researcher, Var_R) => -(( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Human, Var_P)) => -(((f_attribute(Var_P,Var_R)) => (( ? [Var_S] : - (hasType(type_Science, Var_S) & -(f_hasExpertise(Var_P,Var_S))))))))))))). - -fof(axMidLem487, axiom, - ( ! [Var_OFFICER] : - (hasType(type_MilitaryOfficer, Var_OFFICER) => -(( ? [Var_MANAGE] : - (hasType(type_Managing, Var_MANAGE) & -(( ? [Var_PATIENT] : - ((hasType(type_MilitaryOrganization, Var_PATIENT) | hasType(type_Soldier, Var_PATIENT)) & -(((f_agent(Var_MANAGE,Var_OFFICER)) & (f_patient(Var_MANAGE,Var_PATIENT))))))))))))). - -fof(axMidLem488, axiom, - ( ! [Var_NUMBER] : - ((hasType(type_Entity, Var_NUMBER) & hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((Var_NUMBER = f_MultiplicationFn(1,Var_NUMBER)) => (f_MeasureFn(Var_NUMBER,inst_CenturyDuration) = f_MeasureFn(f_MultiplicationFn(Var_NUMBER,100),inst_YearDuration))))))). - -fof(axMidLem489, axiom, - ( ! [Var_NUMBER] : - ((hasType(type_Entity, Var_NUMBER) & hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((Var_NUMBER = f_MultiplicationFn(1,Var_NUMBER)) => (f_MeasureFn(Var_NUMBER,inst_DecadeDuration) = f_MeasureFn(f_MultiplicationFn(Var_NUMBER,10),inst_YearDuration))))))). - -fof(axMidLem490, axiom, - ( ! [Var_NUMBER] : - ((hasType(type_Entity, Var_NUMBER) & hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) => -(((Var_NUMBER = f_MultiplicationFn(1,Var_NUMBER)) => (f_MeasureFn(Var_NUMBER,inst_YardLength) = f_MeasureFn(f_MultiplicationFn(3,Var_NUMBER),inst_FootLength))))))). - -fof(axMidLem491, axiom, - ( ! [Var_NIGHT] : - (hasType(type_NightTime, Var_NIGHT) => -(( ? [Var_DAY1] : - (hasType(type_DayTime, Var_DAY1) & -(( ? [Var_DAY2] : - (hasType(type_DayTime, Var_DAY2) & -(((f_meetsTemporally(Var_NIGHT,Var_DAY1)) & (f_meetsTemporally(Var_DAY2,Var_NIGHT))))))))))))). - -fof(axMidLem492, axiom, - ( ! [Var_NIGHT] : - (hasType(type_NightTime, Var_NIGHT) => -(( ? [Var_RISE] : - (hasType(type_Sunrise, Var_RISE) & -(( ? [Var_SET] : - (hasType(type_Sunset, Var_SET) & -(((f_starts(Var_SET,Var_NIGHT)) & (f_finishes(Var_RISE,Var_NIGHT))))))))))))). - -fof(axMidLem493, axiom, - ( ! [Var_DAY] : - (hasType(type_DayTime, Var_DAY) => -(( ? [Var_NIGHT1] : - (hasType(type_NightTime, Var_NIGHT1) & -(( ? [Var_NIGHT2] : - (hasType(type_NightTime, Var_NIGHT2) & -(((f_meetsTemporally(Var_DAY,Var_NIGHT1)) & (f_meetsTemporally(Var_NIGHT2,Var_DAY))))))))))))). - -fof(axMidLem494, axiom, - ( ! [Var_DAY] : - (hasType(type_DayTime, Var_DAY) => -(( ? [Var_RISE] : - (hasType(type_Sunrise, Var_RISE) & -(( ? [Var_SET] : - (hasType(type_Sunset, Var_SET) & -(((f_starts(Var_RISE,Var_DAY)) & (f_finishes(Var_SET,Var_DAY))))))))))))). - -fof(axMidLem495, axiom, - ( ! [Var_WEEKEND] : - (hasType(type_Weekend, Var_WEEKEND) => -(( ? [Var_SATURDAY] : - (hasType(type_Saturday, Var_SATURDAY) & -(( ? [Var_SUNDAY] : - (hasType(type_Sunday, Var_SUNDAY) & -(((f_starts(Var_SATURDAY,Var_WEEKEND)) & (((f_finishes(Var_SUNDAY,Var_WEEKEND)) & (f_meetsTemporally(Var_SATURDAY,Var_SUNDAY))))))))))))))). - -fof(axMidLem496, axiom, - ( ! [Var_WINTER] : - (hasType(type_WinterSeason, Var_WINTER) => -(( ? [Var_SPRING] : - (hasType(type_SpringSeason, Var_SPRING) & -(f_meetsTemporally(Var_WINTER,Var_SPRING)))))))). - -fof(axMidLem497, axiom, - ( ! [Var_WINTER] : - (hasType(type_WinterSeason, Var_WINTER) => -(( ? [Var_AUTUMN] : - (hasType(type_FallSeason, Var_AUTUMN) & -(f_meetsTemporally(Var_AUTUMN,Var_WINTER)))))))). - -fof(axMidLem498, axiom, - ( ! [Var_SPRING] : - (hasType(type_SpringSeason, Var_SPRING) => -(( ? [Var_SUMMER] : - (hasType(type_SummerSeason, Var_SUMMER) & -(f_meetsTemporally(Var_SPRING,Var_SUMMER)))))))). - -fof(axMidLem499, axiom, - ( ! [Var_SPRING] : - (hasType(type_SpringSeason, Var_SPRING) => -(( ? [Var_WINTER] : - (hasType(type_WinterSeason, Var_WINTER) & -(f_meetsTemporally(Var_WINTER,Var_SPRING)))))))). - -fof(axMidLem500, axiom, - ( ! [Var_SUMMER] : - (hasType(type_SummerSeason, Var_SUMMER) => -(( ? [Var_SPRING] : - (hasType(type_SpringSeason, Var_SPRING) & -(f_meetsTemporally(Var_SPRING,Var_SUMMER)))))))). - -fof(axMidLem501, axiom, - ( ! [Var_SUMMER] : - (hasType(type_SummerSeason, Var_SUMMER) => -(( ? [Var_AUTUMN] : - (hasType(type_FallSeason, Var_AUTUMN) & -(f_meetsTemporally(Var_SUMMER,Var_AUTUMN)))))))). - -fof(axMidLem502, axiom, - ( ! [Var_AUTUMN] : - (hasType(type_FallSeason, Var_AUTUMN) => -(( ? [Var_SUMMER] : - (hasType(type_SummerSeason, Var_SUMMER) & -(f_meetsTemporally(Var_SUMMER,Var_AUTUMN)))))))). - -fof(axMidLem503, axiom, - ( ! [Var_AUTUMN] : - (hasType(type_FallSeason, Var_AUTUMN) => -(( ? [Var_WINTER] : - (hasType(type_WinterSeason, Var_WINTER) & -(f_meetsTemporally(Var_AUTUMN,Var_WINTER)))))))). - -fof(axMidLem504, axiom, - ( ! [Var_OBJ2] : - ((hasType(type_Object, Var_OBJ2) & hasType(type_Physical, Var_OBJ2)) => -(( ! [Var_OBJ1] : - ((hasType(type_Object, Var_OBJ1) & hasType(type_Physical, Var_OBJ1)) => -(((f_orientation(Var_OBJ1,Var_OBJ2,inst_Upstairs)) => (( ? [Var_LEVEL1] : - (hasType(type_BuildingLevel, Var_LEVEL1) & -(( ? [Var_LEVEL2] : - (hasType(type_BuildingLevel, Var_LEVEL2) & -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(((f_part(Var_LEVEL1,Var_BUILDING)) & (((f_part(Var_LEVEL2,Var_BUILDING)) & (((f_located(Var_OBJ1,Var_LEVEL1)) & (((f_located(Var_OBJ2,Var_LEVEL2)) & (f_orientation(Var_LEVEL1,Var_LEVEL2,inst_Above))))))))))))))))))))))))))). - -fof(axMidLem505, axiom, - ( ! [Var_OBJ2] : - ((hasType(type_Object, Var_OBJ2) & hasType(type_Physical, Var_OBJ2)) => -(( ! [Var_OBJ1] : - ((hasType(type_Object, Var_OBJ1) & hasType(type_Physical, Var_OBJ1)) => -(((f_orientation(Var_OBJ1,Var_OBJ2,inst_Downstairs)) => (( ? [Var_LEVEL1] : - (hasType(type_BuildingLevel, Var_LEVEL1) & -(( ? [Var_LEVEL2] : - (hasType(type_BuildingLevel, Var_LEVEL2) & -(( ? [Var_BUILDING] : - (hasType(type_Building, Var_BUILDING) & -(((f_part(Var_LEVEL1,Var_BUILDING)) & (((f_part(Var_LEVEL2,Var_BUILDING)) & (((f_located(Var_OBJ1,Var_LEVEL1)) & (((f_located(Var_OBJ2,Var_LEVEL2)) & (f_orientation(Var_LEVEL1,Var_LEVEL2,inst_Below))))))))))))))))))))))))))). - -fof(axMidLem506, axiom, - ( ! [Var_E] : - (hasType(type_Object, Var_E) => -(((f_attribute(Var_E,inst_Headache)) => (( ? [Var_H] : - (hasType(type_Head, Var_H) & -(((f_part(Var_H,Var_E)) & (f_attribute(Var_H,inst_Pain)))))))))))). - -fof(axMidLem507, axiom, - ( ! [Var_WORD] : - (hasType(type_Word, Var_WORD) => -(( ? [Var_SYLLABLE] : - (hasType(type_Syllable, Var_SYLLABLE) & -(f_part(Var_SYLLABLE,Var_WORD)))))))). - -fof(axMidLem508, axiom, - ( ! [Var_ATTR] : - (hasType(type_GameAttribute, Var_ATTR) => -(( ! [Var_THING] : - ((hasType(type_Entity, Var_THING) & hasType(type_Agent, Var_THING) & hasType(type_Process, Var_THING)) => -(((f_property(Var_THING,Var_ATTR)) => (( ? [Var_GAME] : - (hasType(type_Game, Var_GAME) & -(((f_agent(Var_GAME,Var_THING)) | (((f_patient(Var_GAME,Var_THING)) | (f_subProcess(Var_THING,Var_GAME))))))))))))))))). - -fof(axMidLem509, axiom, - ( ! [Var_ATTR] : - (hasType(type_SportsAttribute, Var_ATTR) => -(( ! [Var_THING] : - ((hasType(type_Entity, Var_THING) & hasType(type_Agent, Var_THING) & hasType(type_Process, Var_THING)) => -(((f_property(Var_THING,Var_ATTR)) => (( ? [Var_SPORT] : - (hasType(type_Game, Var_SPORT) & -(((f_agent(Var_SPORT,Var_THING)) | (((f_patient(Var_SPORT,Var_THING)) | (f_subProcess(Var_THING,Var_SPORT))))))))))))))))). - -fof(axMidLem510, axiom, - ( ! [Var_R] : - (hasType(type_ChemicalReduction, Var_R) => -(( ! [Var_G] : - ((hasType(type_Quantity, Var_G) & hasType(type_PositiveInteger, Var_G)) => -(( ! [Var_L] : - ((hasType(type_PositiveInteger, Var_L) & hasType(type_Quantity, Var_L)) => -(( ! [Var_S] : - ((hasType(type_Entity, Var_S) & hasType(type_PureSubstance, Var_S)) => -(((((f_patient(Var_R,Var_S)) & (f_holdsDuring(f_BeginFn(f_WhenFn(Var_R)),electronNumber(Var_S,Var_L))))) => (((f_greaterThan(Var_G,Var_L)) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_R)),electronNumber(Var_S,Var_G))))))))))))))))))). - -fof(axMidLem511, axiom, - ( ! [Var_O] : - (hasType(type_Oxidation, Var_O) => -(( ! [Var_G] : - ((hasType(type_PositiveInteger, Var_G) & hasType(type_Quantity, Var_G)) => -(( ! [Var_S] : - ((hasType(type_Entity, Var_S) & hasType(type_PureSubstance, Var_S)) => -(((((f_patient(Var_O,Var_S)) & (f_holdsDuring(f_BeginFn(f_WhenFn(Var_O)),electronNumber(Var_S,Var_G))))) => (( ? [Var_L] : - ((hasType(type_Quantity, Var_L) & hasType(type_PositiveInteger, Var_L)) & -(((f_lessThan(Var_L,Var_G)) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_O)),electronNumber(Var_S,Var_L))))))))))))))))))). - -fof(axMidLem512, axiom, - ( ! [Var_DIALYSIS] : - (hasType(type_Dialysis, Var_DIALYSIS) => -(( ? [Var_SOLUTION] : - (hasType(type_Solution, Var_SOLUTION) & -(( ? [Var_SUBSTANCE1] : - (hasType(type_PureSubstance, Var_SUBSTANCE1) & -(( ? [Var_SUBSTANCE2] : - (hasType(type_PureSubstance, Var_SUBSTANCE2) & -(((f_resourceS(Var_DIALYSIS,Var_SOLUTION)) & (((f_result(Var_DIALYSIS,Var_SUBSTANCE1)) & (((f_result(Var_DIALYSIS,Var_SUBSTANCE2)) & (Var_SUBSTANCE1 != Var_SUBSTANCE2))))))))))))))))))). - -fof(axMidLem513, axiom, - ( ! [Var_D] : - (hasType(type_Diluting, Var_D) => -(( ? [Var_S] : - (hasType(type_Solution, Var_S) & -(((f_patient(Var_D,Var_S)) & (f_attribute(Var_S,inst_Liquid)))))))))). - -fof(axMidLem514, axiom, - ( ! [Var_C] : - (hasType(type_Chromatography, Var_C) => -(( ? [Var_M] : - ((hasType(type_LiquidMixture, Var_M) | hasType(type_GasMixture, Var_M)) & -(f_resourceS(Var_C,Var_M)))))))). - -fof(axMidLem515, axiom, - ( ! [Var_C] : - (hasType(type_Chromatography, Var_C) => -(( ? [Var_S] : - (hasType(type_PureSubstance, Var_S) & -(f_result(Var_C,Var_S)))))))). - -fof(axMidLem516, axiom, - ( ! [Var_A] : - (hasType(type_RightAngle, Var_A) => -(f_angularMeasure(Var_A,f_MeasureFn(90,inst_AngularDegree)))))). - -fof(axMidLem517, axiom, - ( ! [Var_A] : - (hasType(type_AcuteAngle, Var_A) => -(( ! [Var_N] : - ((hasType(type_RealNumber, Var_N) & hasType(type_Quantity, Var_N)) => -(((f_angularMeasure(Var_A,f_MeasureFn(Var_N,inst_AngularDegree))) => (f_lessThan(Var_N,90)))))))))). - -fof(axMidLem518, axiom, - ( ! [Var_A] : - (hasType(type_ObliqueAngle, Var_A) => -(( ! [Var_N] : - ((hasType(type_RealNumber, Var_N) & hasType(type_Quantity, Var_N)) => -(((f_angularMeasure(Var_A,f_MeasureFn(Var_N,inst_AngularDegree))) => (f_greaterThan(Var_N,90)))))))))). - -fof(axMidLem519, axiom, - ( ! [Var_POLYGON] : - (hasType(type_Polygon, Var_POLYGON) => -(( ! [Var_PART] : - ((hasType(type_GeometricFigure, Var_PART) & hasType(type_OneDimensionalFigure, Var_PART)) => -(((f_geometricPart(Var_PART,Var_POLYGON)) => (((f_sideOfFigure(Var_PART,Var_POLYGON)) | (( ? [Var_SIDE] : - ((hasType(type_OneDimensionalFigure, Var_SIDE) & hasType(type_GeometricFigure, Var_SIDE)) & -(((f_sideOfFigure(Var_SIDE,Var_POLYGON)) & (f_geometricPart(Var_PART,Var_SIDE))))))))))))))))). - -fof(axMidLem520, axiom, - ( ! [Var_T] : - (hasType(type_RightTriangle, Var_T) => -(( ? [Var_A] : - (hasType(type_RightAngle, Var_A) & -(f_angleOfFigure(Var_A,Var_T)))))))). - -fof(axMidLem521, axiom, - ( ! [Var_SQUARE] : - (hasType(type_Square, Var_SQUARE) => -(( ? [Var_LENGTH] : - (hasType(type_LengthMeasure, Var_LENGTH) & -(( ! [Var_SIDE] : - (hasType(type_OneDimensionalFigure, Var_SIDE) => -(((f_sideOfFigure(Var_SIDE,Var_SQUARE)) => (f_lineMeasure(Var_SIDE,Var_LENGTH))))))))))))). - -fof(axMidLem522, axiom, - ( ! [Var_L] : - (hasType(type_Entity, Var_L) => -(( ! [Var_C] : - (hasType(type_Circle, Var_C) => -(((f_DiameterFn(Var_C) = Var_L) => (( ? [Var_R] : - ((hasType(type_Entity, Var_R) & hasType(type_Quantity, Var_R)) & -(((f_RadiusFn(Var_C) = Var_R) & (f_MultiplicationFn(Var_R,2) = Var_L)))))))))))))). - -fof(axMidLem523, axiom, - ( ! [Var_R] : - ((hasType(type_LengthMeasure, Var_R) & hasType(type_Entity, Var_R)) => -(( ! [Var_P2] : - ((hasType(type_GeometricFigure, Var_P2) & hasType(type_GeometricPoint, Var_P2)) => -(( ! [Var_P] : - ((hasType(type_Entity, Var_P) & hasType(type_GeometricPoint, Var_P)) => -(( ! [Var_C] : - ((hasType(type_Circle, Var_C) & hasType(type_GeometricFigure, Var_C)) => -(((((f_CenterOfCircleFn(Var_C) = Var_P) & (((f_pointOfFigure(Var_P2,Var_C)) & (f_geometricDistance(Var_P2,Var_P,Var_R)))))) => (f_RadiusFn(Var_C) = Var_R))))))))))))))). - -fof(axMidLem524, axiom, - ( ! [Var_CIRCLE] : - ((hasType(type_TwoDimensionalObject, Var_CIRCLE) & hasType(type_GeometricFigure, Var_CIRCLE)) => -(( ! [Var_LINE] : - ((hasType(type_OneDimensionalFigure, Var_LINE) & hasType(type_GeometricFigure, Var_LINE)) => -(((f_tangent(Var_LINE,Var_CIRCLE)) => (( ? [Var_POINT1] : - ((hasType(type_GeometricFigure, Var_POINT1) & hasType(type_Entity, Var_POINT1)) & -(((f_pointOfFigure(Var_POINT1,Var_LINE)) & (((f_pointOfFigure(Var_POINT1,Var_CIRCLE)) & (( ! [Var_POINT2] : - ((hasType(type_GeometricFigure, Var_POINT2) & hasType(type_Entity, Var_POINT2)) => -(((((f_pointOfFigure(Var_POINT2,Var_LINE)) & (f_pointOfFigure(Var_POINT2,Var_CIRCLE)))) => (Var_POINT1 = Var_POINT2))))))))))))))))))))). - -fof(axMidLem525, axiom, - ( ! [Var_WAR] : - (hasType(type_CivilWar, Var_WAR) => -(( ? [Var_NATION] : - (hasType(type_Nation, Var_NATION) & -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_GeopoliticalArea, Var_AGENT)) => -(((f_contestParticipant(Var_WAR,Var_AGENT)) => (f_geopoliticalSubdivision(Var_AGENT,Var_NATION))))))))))))). - -fof(axMidLem526, axiom, - ( ! [Var_H] : - (hasType(type_Object, Var_H) => -(((f_attribute(Var_H,inst_Pregnant)) => (f_attribute(Var_H,inst_Female))))))). - -fof(axMidLem527, axiom, - ( ! [Var_LIE] : - (hasType(type_LyingDown, Var_LIE) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_LIE,Var_AGENT)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_LIE)),attribute(Var_AGENT,inst_Sitting))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_LIE)),attribute(Var_AGENT,inst_Prostrate))))))))))))). - -fof(axMidLem528, axiom, - ( ! [Var_SIT] : - (hasType(type_SittingDown, Var_SIT) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_SIT,Var_AGENT)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_SIT)),attribute(Var_AGENT,inst_Standing))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_SIT)),attribute(Var_AGENT,inst_Sitting))))))))))))). - -fof(axMidLem529, axiom, - ( ! [Var_STAND] : - (hasType(type_StandingUp, Var_STAND) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_Object, Var_AGENT)) => -(((f_agent(Var_STAND,Var_AGENT)) => (((f_holdsDuring(f_BeginFn(f_WhenFn(Var_STAND)),attribute(Var_AGENT,inst_Sitting))) & (f_holdsDuring(f_EndFn(f_WhenFn(Var_STAND)),attribute(Var_AGENT,inst_Standing))))))))))))). - -fof(axMidLem530, axiom, - ( ! [Var_EM] : - (hasType(type_EyeMotion, Var_EM) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Object, Var_A)) => -(((f_agent(Var_EM,Var_A)) => (( ? [Var_E] : - (hasType(type_Eyelid, Var_E) & -(((f_part(Var_E,Var_A)) & (f_patient(Var_EM,Var_E))))))))))))))). - -fof(axMidLem531, axiom, - ( ! [Var_P] : - (hasType(type_ReflexiveProcess, Var_P) => -(( ? [Var_M] : - (hasType(type_Muscle, Var_M) & -(f_patient(Var_P,Var_M)))))))). - -fof(axMidLem532, axiom, - ( ! [Var_ANIMAL] : - (hasType(type_DomesticAnimal, Var_ANIMAL) => -(( ? [Var_KEEP] : - (hasType(type_Keeping, Var_KEEP) & -(( ? [Var_PERSON] : - (hasType(type_Human, Var_PERSON) & -(((f_agent(Var_KEEP,Var_PERSON)) & (f_patient(Var_KEEP,Var_ANIMAL))))))))))))). - -fof(axMidLem533, axiom, - ( ! [Var_MULE] : - (hasType(type_Mule, Var_MULE) => -(( ? [Var_DONKEY] : - (hasType(type_Donkey, Var_DONKEY) & -(( ? [Var_HORSE] : - (hasType(type_Horse, Var_HORSE) & -(((f_father(Var_MULE,Var_DONKEY)) & (f_mother(Var_MULE,Var_HORSE))))))))))))). - -fof(axMidLem534, axiom, - ( ! [Var_F] : - (hasType(type_Feather, Var_F) => -(( ? [Var_B] : - (hasType(type_Bird, Var_B) & -(f_part(Var_F,Var_B)))))))). - -fof(axMidLem535, axiom, - ( ! [Var_HAY] : - (hasType(type_Hay, Var_HAY) => -(( ? [Var_MAKE] : - (hasType(type_Making, Var_MAKE) & -(( ? [Var_GRASS] : - (hasType(type_Grass, Var_GRASS) & -(((f_resourceS(Var_MAKE,Var_GRASS)) & (f_result(Var_MAKE,Var_HAY))))))))))))). - -fof(axMidLem536, axiom, - ( ! [Var_VACATION] : - (hasType(type_Vacationing, Var_VACATION) => -(( ! [Var_WORK] : - (hasType(type_Working, Var_WORK) => -(( ! [Var_PERSON] : - (hasType(type_Human, Var_PERSON) => -(((((f_agent(Var_VACATION,Var_PERSON)) & (f_agent(Var_WORK,Var_PERSON)))) => (( ~ (f_overlapsTemporally(f_WhenFn(Var_VACATION),f_WhenFn(Var_WORK)))))))))))))))). - -fof(axMidLem537, axiom, - ( ! [Var_FARMING] : - (hasType(type_Farming, Var_FARMING) => -(( ! [Var_FARMER] : - ((hasType(type_Agent, Var_FARMER) & hasType(type_Physical, Var_FARMER)) => -(((f_agent(Var_FARMING,Var_FARMER)) => (( ? [Var_FARM] : - (hasType(type_Farm, Var_FARM) & -(f_holdsDuring(f_WhenFn(Var_FARMING),located(Var_FARMER,Var_FARM)))))))))))))). - -fof(axMidLem538, axiom, - ( ! [Var_W] : - ((hasType(type_Object, Var_W) & hasType(type_Woman, Var_W)) => -(((f_attribute(Var_W,inst_Housewife)) => (( ? [Var_H] : - (hasType(type_Man, Var_H) & -(f_wife(Var_W,Var_H)))))))))). - -fof(axMidLem539, axiom, - ( ! [Var_OCCUPATION] : - (hasType(type_SkilledOccupation, Var_OCCUPATION) => -(( ! [Var_PERSON] : - ((hasType(type_Object, Var_PERSON) & hasType(type_Entity, Var_PERSON)) => -(((f_attribute(Var_PERSON,Var_OCCUPATION)) => (( ? [Var_TRAINING] : - (hasType(type_EducationalProcess, Var_TRAINING) & -(f_destination(Var_TRAINING,Var_PERSON))))))))))))). - -fof(axMidLem540, axiom, - ( ! [Var_FM] : - (hasType(type_FilmMaking, Var_FM) => -(( ? [Var_M] : - (hasType(type_MotionPicture, Var_M) & -(( ? [Var_F] : - (hasType(type_PhotographicFilm, Var_F) & -(((f_result(Var_FM,Var_M)) & (f_resourceS(Var_FM,Var_F))))))))))))). - -fof(axMidLem541, axiom, - ( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Agent, Var_P)) => -(((f_attribute(Var_P,inst_Carpenter)) => (f_hasSkill(type_Carpentry,Var_P))))))). - -fof(axMidLem542, axiom, - ( ! [Var_C] : - (hasType(type_Carpentry, Var_C) => -(( ! [Var_W] : - (hasType(type_Wood, Var_W) => -(( ? [Var_B] : - (hasType(type_Building, Var_B) & -(((f_part(Var_W,Var_B)) & (f_result(Var_C,Var_B))))))))))))). - -fof(axMidLem543, axiom, - ( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Agent, Var_P)) => -(((f_attribute(Var_P,inst_FarmHand)) => (( ? [Var_F] : - (hasType(type_Agriculture, Var_F) & -(f_agent(Var_F,Var_P)))))))))). - -fof(axMidLem544, axiom, - ( ! [Var_H] : - ((hasType(type_Object, Var_H) & hasType(type_Agent, Var_H)) => -(((f_attribute(Var_H,inst_Potter)) => (( ? [Var_M] : - (hasType(type_Making, Var_M) & -(( ? [Var_P] : - (hasType(type_Pottery, Var_P) & -(((f_agent(Var_M,Var_H)) & (f_result(Var_M,Var_P))))))))))))))). - -fof(axMidLem545, axiom, - ( ! [Var_D] : - (hasType(type_Deacon, Var_D) => -(( ? [Var_O] : - (hasType(type_ReligiousOrganization, Var_O) & -(( ? [Var_C] : - (hasType(type_Cleric, Var_C) & -(f_subordinateInOrganization(Var_O,Var_D,Var_C))))))))))). - -fof(axMidLem546, axiom, - ( ! [Var_P] : - (hasType(type_PensionPlan, Var_P) => -(( ! [Var_O] : - ((hasType(type_Organization, Var_O) & hasType(type_FinancialCompany, Var_O)) => -(( ! [Var_A] : - (hasType(type_CognitiveAgent, Var_A) => -(((((f_accountHolder(Var_P,Var_A)) & (f_employs(Var_O,Var_A)))) => (f_financialAccount(Var_P,Var_O))))))))))))). - -fof(axMidLem547, axiom, - ( ! [Var_PSP] : - (hasType(type_ProfitSharingPlan, Var_PSP) => -(( ! [Var_P] : - ((hasType(type_CurrencyMeasure, Var_P) & hasType(type_Quantity, Var_P)) => -(( ! [Var_A] : - ((hasType(type_FinancialTransaction, Var_A) & hasType(type_Process, Var_A)) => -(( ! [Var_O] : - ((hasType(type_Organization, Var_O) & hasType(type_Agent, Var_O)) => -(( ! [Var_H] : - (hasType(type_CognitiveAgent, Var_H) => -(((((f_accountHolder(Var_PSP,Var_H)) & (((f_employs(Var_O,Var_H)) & (((f_profit(Var_A,Var_P)) & (f_agent(Var_A,Var_O)))))))) => (( ? [Var_PAY] : - (hasType(type_FinancialTransaction, Var_PAY) & -(( ? [Var_C] : - ((hasType(type_CurrencyMeasure, Var_C) & hasType(type_Quantity, Var_C)) & -(((f_transactionAmount(Var_PAY,Var_C)) & (((f_lessThan(Var_C,Var_P)) & (f_destination(Var_PAY,Var_PSP))))))))))))))))))))))))))))). - -fof(axMidLem548, axiom, - ( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Agent, Var_H)) => -(((f_hasExpertise(Var_H,inst_Architecture)) => (( ? [Var_D] : - (hasType(type_ContentDevelopment, Var_D) & -(( ? [Var_P] : - (hasType(type_Blueprint, Var_P) & -(( ? [Var_B] : - (hasType(type_Building, Var_B) & -(((f_agent(Var_D,Var_H)) & (((f_result(Var_D,Var_P)) & (f_represents(Var_P,Var_B)))))))))))))))))))). - -fof(axMidLem549, axiom, - ( ! [Var_FIELD] : - ((hasType(type_FieldOfStudy, Var_FIELD) & hasType(type_Proposition, Var_FIELD)) => -(( ! [Var_PERSON] : - ((hasType(type_Human, Var_PERSON) & hasType(type_Agent, Var_PERSON)) => -(((f_hasExpertise(Var_PERSON,Var_FIELD)) => (( ? [Var_LEARN] : - (hasType(type_Learning, Var_LEARN) & -(((f_agent(Var_LEARN,Var_PERSON)) & (f_realization(Var_LEARN,Var_FIELD))))))))))))))). - -fof(axMidLem550, axiom, - ( ! [Var_BLEED] : - (hasType(type_Bleeding, Var_BLEED) => -(( ? [Var_INJURY] : - (hasType(type_Injuring, Var_INJURY) & -(f_causes(Var_INJURY,Var_BLEED)))))))). - -fof(axMidLem551, axiom, - ( ! [Var_B] : - (hasType(type_Blushing, Var_B) => -(( ! [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_Object, Var_A)) => -(((f_experiencer(Var_B,Var_A)) => (( ? [Var_S1] : - (hasType(type_EmotionalState, Var_S1) & -(( ? [Var_S2] : - (hasType(type_EmotionalState, Var_S2) & -(( ? [Var_T2] : - ((hasType(type_TimePosition, Var_T2) & hasType(type_TimeInterval, Var_T2)) & -(( ? [Var_T1] : - ((hasType(type_TimePosition, Var_T1) & hasType(type_TimeInterval, Var_T1)) & -(((Var_S1 != Var_S2) & (((f_holdsDuring(Var_T1,attribute(Var_A,Var_S1))) & (((f_holdsDuring(Var_T2,attribute(Var_A,Var_S2))) & (((f_starts(f_WhenFn(Var_B),Var_T2)) & (f_finishes(f_WhenFn(Var_B),Var_T1)))))))))))))))))))))))))))))). - -fof(axMidLem552, axiom, - ( ! [Var_CLOSE] : - (hasType(type_ClosingContract, Var_CLOSE) => -(( ! [Var_CONTRACT] : - ((hasType(type_Entity, Var_CONTRACT) & hasType(type_Contract, Var_CONTRACT)) => -(( ! [Var_AGENT] : - ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) => -(((((f_agent(Var_CLOSE,Var_AGENT)) & (f_destination(Var_CLOSE,Var_CONTRACT)))) => (f_agreementMember(Var_CONTRACT,Var_AGENT))))))))))))). - -fof(axMidLem553, axiom, - ( ! [Var_D] : - (hasType(type_Diet, Var_D) => -(( ! [Var_P] : - (hasType(type_Process, Var_P) => -(((f_realization(Var_P,Var_D)) => (( ? [Var_E] : - (hasType(type_Eating, Var_E) & -(f_subProcess(Var_E,Var_P))))))))))))). - -fof(axMidLem554, axiom, - ( ! [Var_FOOD] : - (hasType(type_PreparedFood, Var_FOOD) => -(( ? [Var_COOK] : - (hasType(type_Cooking, Var_COOK) & -(f_result(Var_COOK,Var_FOOD)))))))). - -fof(axMidLem555, axiom, - ( ! [Var_B] : - (hasType(type_Baking, Var_B) => -(( ? [Var_O] : - (hasType(type_Oven, Var_O) & -(f_instrument(Var_B,Var_O)))))))). - -fof(axMidLem556, axiom, - ( ! [Var_B] : - (hasType(type_BreadOrBiscuit, Var_B) => -(( ? [Var_D] : - (hasType(type_Dough, Var_D) & -(( ? [Var_BAKE] : - (hasType(type_Baking, Var_BAKE) & -(((f_resourceS(Var_BAKE,Var_D)) & (f_result(Var_BAKE,Var_B))))))))))))). - -fof(axMidLem557, axiom, - ( ! [Var_S] : - (hasType(type_Sandwich, Var_S) => -(( ? [Var_B1] : - (hasType(type_BreadOrBiscuit, Var_B1) & -(( ? [Var_B2] : - (hasType(type_BreadOrBiscuit, Var_B2) & -(( ? [Var_F] : - (hasType(type_Food, Var_F) & -(((f_between(Var_B1,Var_F,Var_B2)) & (((Var_B1 != Var_B2) & (((Var_B1 != Var_F) & (((Var_B2 != Var_F) & (((f_part(Var_B1,Var_S)) & (((f_part(Var_B2,Var_S)) & (f_part(Var_F,Var_S)))))))))))))))))))))))))). - -fof(axMidLem558, axiom, - ( ! [Var_D] : - (hasType(type_Dough, Var_D) => -(( ? [Var_F] : - (hasType(type_Flour, Var_F) & -(( ? [Var_W] : - (hasType(type_Water, Var_W) & -(((f_part(Var_F,Var_D)) & (f_part(Var_W,Var_D))))))))))))). - -fof(axMidLem559, axiom, - ( ! [Var_B] : - (hasType(type_Butter, Var_B) => -(( ? [Var_C] : - (hasType(type_Cooking, Var_C) & -(( ? [Var_M] : - (hasType(type_Milk, Var_M) & -(((f_resourceS(Var_C,Var_M)) & (f_result(Var_C,Var_B))))))))))))). - -fof(axMidLem560, axiom, - ( ! [Var_F] : - (hasType(type_Flour, Var_F) => -(( ? [Var_P] : - (hasType(type_IntentionalProcess, Var_P) & -(( ? [Var_C] : - (hasType(type_CerealGrain, Var_C) & -(((f_resourceS(Var_P,Var_C)) & (f_result(Var_P,Var_F))))))))))))). - -fof(axMidLem561, axiom, - ( ! [Var_H] : - (hasType(type_Honey, Var_H) => -(( ? [Var_P] : - (hasType(type_PhysiologicProcess, Var_P) & -(( ? [Var_B] : - (hasType(type_Bee, Var_B) & -(((f_agent(Var_P,Var_B)) & (f_result(Var_P,Var_H))))))))))))). - -fof(axMidLem562, axiom, - ( ! [Var_G] : - (hasType(type_AtomicGroup, Var_G) => -(( ? [Var_ATOM1] : - (hasType(type_Atom, Var_ATOM1) & -(( ? [Var_ATOM2] : - (hasType(type_Atom, Var_ATOM2) & -(((Var_ATOM1 != Var_ATOM2) & (((f_part(Var_ATOM1,Var_G)) & (f_part(Var_ATOM2,Var_G))))))))))))))). - -fof(axMidLem563, axiom, - ( ! [Var_G] : - (hasType(type_AtomicGroup, Var_G) => -(( ? [Var_M] : - (hasType(type_Molecule, Var_M) & -(f_part(Var_G,Var_M)))))))). - -fof(axMidLem564, axiom, - ( ! [Var_M] : - (hasType(type_MilitaryManeuver, Var_M) => -(( ? [Var_B] : - (hasType(type_Battle, Var_B) & -(f_subProcess(Var_M,Var_B)))))))). - -fof(axMidLem565, axiom, - ( ! [Var_X] : - (hasType(type_Bombing, Var_X) => -(( ? [Var_BOMB] : - (hasType(type_Bomb, Var_BOMB) & -(f_instrument(Var_X,Var_BOMB)))))))). - -fof(axMidLem566, axiom, - ( ! [Var_X] : - (hasType(type_CarBombing, Var_X) => -(( ? [Var_BOMB] : - (hasType(type_Bomb, Var_BOMB) & -(( ? [Var_CAR] : - (hasType(type_TransportationDevice, Var_CAR) & -(((f_instrument(Var_X,Var_CAR)) & (((f_instrument(Var_X,Var_BOMB)) & (f_connected(Var_CAR,Var_BOMB))))))))))))))). - -fof(axMidLem567, axiom, - ( ! [Var_X] : - (hasType(type_ChemicalAttack, Var_X) => -(( ? [Var_CHEM] : - (hasType(type_Substance, Var_CHEM) & -(f_instrument(Var_X,Var_CHEM)))))))). - -fof(axMidLem568, axiom, - ( ! [Var_X] : - (hasType(type_HandGrenade, Var_X) => -(( ! [Var_N] : - ((hasType(type_RealNumber, Var_N) & hasType(type_Quantity, Var_N)) => -(((f_measure(Var_X,f_MeasureFn(Var_N,inst_PoundMass))) & (f_lessThan(Var_N,10)))))))))). - -fof(axMidLem569, axiom, - ( ! [Var_X] : - (hasType(type_HandgrenadeAttack, Var_X) => -(( ? [Var_HG] : - (hasType(type_HandGrenade, Var_HG) & -(f_instrument(Var_X,Var_HG)))))))). - -fof(axMidLem570, axiom, - ( ! [Var_H] : - (hasType(type_Hijacking, Var_H) => -(( ? [Var_V] : - (hasType(type_Vehicle, Var_V) & -(f_patient(Var_H,Var_V)))))))). - -fof(axMidLem571, axiom, - ( ! [Var_H] : - (hasType(type_Hijacking, Var_H) => -(( ? [Var_D] : - (hasType(type_Driving, Var_D) & -(f_subProcess(Var_D,Var_H)))))))). - -fof(axMidLem572, axiom, - ( ! [Var_X] : - (hasType(type_HostageTaking, Var_X) => -(( ? [Var_A] : - (hasType(type_SentientAgent, Var_A) & -(f_patient(Var_X,Var_A)))))))). - -fof(axMidLem573, axiom, - ( ! [Var_X] : - (hasType(type_Kidnapping, Var_X) => -(( ? [Var_A] : - (hasType(type_SentientAgent, Var_A) & -(( ? [Var_LOC1] : - (hasType(type_GeographicArea, Var_LOC1) & -(( ? [Var_LOC2] : - (hasType(type_GeographicArea, Var_LOC2) & -(((Var_LOC1 != Var_LOC2) & (((f_holdsDuring(f_ImmediatePastFn(f_WhenFn(Var_X)),located(Var_A,Var_LOC1))) & (f_holdsDuring(f_WhenFn(Var_X),located(Var_A,Var_LOC2))))))))))))))))))). - -fof(axMidLem574, axiom, - ( ! [Var_X] : - (hasType(type_KnifeAttack, Var_X) => -(( ? [Var_HG] : - (hasType(type_Knife, Var_HG) & -(f_instrument(Var_X,Var_HG)))))))). - -fof(axMidLem575, axiom, - ( ! [Var_X] : - (hasType(type_MortarAttack, Var_X) => -(( ? [Var_MA] : - (hasType(type_Mortar, Var_MA) & -(f_instrument(Var_X,Var_MA)))))))). - -fof(axMidLem576, axiom, - ( ! [Var_X] : - (hasType(type_Stoning, Var_X) => -(( ? [Var_ST] : - (hasType(type_Rock, Var_ST) & -(f_instrument(Var_X,Var_ST)))))))). - -fof(axMidLem577, axiom, - ( ! [Var_X] : - (hasType(type_SuicideBombing, Var_X) => -(( ? [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Object, Var_A)) & -(((f_agent(Var_X,Var_A)) & (f_holdsDuring(f_FutureFn(f_WhenFn(Var_X)),attribute(Var_A,inst_Dead))))))))))). - -fof(axMidLem578, axiom, - ( ! [Var_X] : - (hasType(type_SuicideBombing, Var_X) => -(( ! [Var_P] : - ((hasType(type_Agent, Var_P) & hasType(type_CognitiveAgent, Var_P)) => -(((f_agent(Var_X,Var_P)) => (f_believes(Var_P,holdsDuring(f_FutureFn(f_WhenFn(Var_X)),attribute(Var_P,inst_Dead)))))))))))). - -fof(axMidLem579, axiom, - ( ! [Var_X] : - (hasType(type_VehicleAttack, Var_X) => -(( ? [Var_V] : - (hasType(type_TransportationDevice, Var_V) & -(f_instrument(Var_X,Var_V)))))))). - -fof(axMidLem580, axiom, - ( ! [Var_X] : - (hasType(type_BusStop, Var_X) => -(( ? [Var_R] : - (hasType(type_Roadway, Var_R) & -(f_meetsSpatially(Var_X,Var_R)))))))). - -fof(axMidLem581, axiom, - ( ! [Var_B] : - (hasType(type_Burrow, Var_B) => -(( ? [Var_A] : - (hasType(type_Organism, Var_A) & -(f_hasPurpose(Var_B,inhabits(Var_A,Var_B))))))))). - -fof(axMidLem582, axiom, - ( ! [Var_X] : - ((hasType(type_Object, Var_X) & hasType(type_Agent, Var_X)) => -(((f_attribute(Var_X,inst_Musician)) => (f_hasSkill(type_MusicalPerformance,Var_X))))))). - -fof(axMidLem583, axiom, - ( ! [Var_H] : - (hasType(type_Object, Var_H) => -(( ! [Var_T1] : - ((hasType(type_TimePosition, Var_T1) & hasType(type_Physical, Var_T1)) => -(((f_holdsDuring(Var_T1,attribute(Var_H,inst_Veteran))) => (( ? [Var_P] : - (hasType(type_Soldier, Var_P) & -(( ? [Var_T2] : - (hasType(type_TimePosition, Var_T2) & -(((f_temporalPart(Var_T2,f_PastFn(f_WhenFn(Var_T1)))) & (((f_holdsDuring(Var_T2,attribute(Var_H,Var_P))) & (( ~ (f_holdsDuring(Var_T1,attribute(Var_H,Var_P))))))))))))))))))))))). - -fof(axMidLem584, axiom, - ( ! [Var_X] : - (hasType(type_Checkpoint, Var_X) => -(((( ? [Var_ROAD] : - (hasType(type_Road, Var_ROAD) & -(f_orientation(Var_ROAD,Var_X,inst_Near))))) | (( ? [Var_REG2] : - (hasType(type_GeographicArea, Var_REG2) & -(( ? [Var_REG1] : - (hasType(type_GeographicArea, Var_REG1) & -(f_orientation(f_BorderFn(Var_REG1,Var_REG2),Var_X,inst_Near))))))))))))). - -fof(axMidLem585, axiom, - ( ! [Var_P] : - ((hasType(type_Object, Var_P) & hasType(type_Human, Var_P)) => -(( ! [Var_NOW] : - ((hasType(type_TimePosition, Var_NOW) & hasType(type_TimeInterval, Var_NOW)) => -(((f_holdsDuring(Var_NOW,attribute(Var_P,inst_Widowed))) => (((( ? [Var_SPOUSE] : - ((hasType(type_Human, Var_SPOUSE) & hasType(type_Object, Var_SPOUSE)) & -(( ? [Var_BEFORE] : - ((hasType(type_TimeInterval, Var_BEFORE) & hasType(type_TimePosition, Var_BEFORE)) & -(((f_earlier(Var_BEFORE,Var_NOW)) & (((f_holdsDuring(Var_BEFORE,spouse(Var_SPOUSE,Var_P))) & (f_holdsDuring(Var_NOW,attribute(Var_SPOUSE,inst_Dead))))))))))))) & (( ~ ( ? [Var_OTHER] : - (hasType(type_Human, Var_OTHER) & -(f_holdsDuring(Var_NOW,spouse(Var_OTHER,Var_P))))))))))))))))). - -fof(axMidLem586, axiom, - ( ! [Var_C] : - (hasType(type_Convoy, Var_C) => -(( ! [Var_VEH] : - ((hasType(type_SelfConnectedObject, Var_VEH) & hasType(type_Entity, Var_VEH)) => -(((f_member(Var_VEH,Var_C)) => (( ? [Var_DRIVE] : - (hasType(type_Driving, Var_DRIVE) & -(((f_overlapsTemporally(f_WhenFn(Var_DRIVE),f_WhenFn(Var_C))) & (f_patient(Var_DRIVE,Var_VEH))))))))))))))). - -fof(axMidLem587, axiom, - ( ! [Var_C] : - (hasType(type_Convoy, Var_C) => -(f_attribute(Var_C,inst_LineFormation))))). - -fof(axMidLem588, axiom, - ( ! [Var_X] : - (hasType(type_EmbassyBuilding, Var_X) => -(( ? [Var_EGOV] : - (hasType(type_Nation, Var_EGOV) & -(( ? [Var_OTHERGOV] : - (hasType(type_Nation, Var_OTHERGOV) & -(((Var_EGOV != Var_OTHERGOV) & (((f_possesses(Var_EGOV,Var_X)) & (f_located(Var_X,Var_OTHERGOV))))))))))))))). - -fof(axMidLem589, axiom, - ( ! [Var_N] : - (hasType(type_EuropeanNation, Var_N) => -(f_part(Var_N,inst_Europe))))). - -fof(axMidLem590, axiom, - ( ! [Var_X] : - (hasType(type_GovernmentBuilding, Var_X) => -(( ? [Var_G] : - (hasType(type_Government, Var_G) & -(f_possesses(Var_G,Var_X)))))))). - -fof(axMidLem591, axiom, - ( ! [Var_X] : - ((hasType(type_Object, Var_X) & hasType(type_CognitiveAgent, Var_X)) => -(( ! [Var_T1] : - (hasType(type_TimePosition, Var_T1) => -(((f_holdsDuring(Var_T1,attribute(Var_X,inst_GovernmentPerson))) => (( ? [Var_GOV] : - (hasType(type_Government, Var_GOV) & -(f_holdsDuring(Var_T1,employs(Var_GOV,Var_X)))))))))))))). - -fof(axMidLem592, axiom, - ( ! [Var_R] : - (hasType(type_Renting, Var_R) => -(( ! [Var_O] : - ((hasType(type_Entity, Var_O) & hasType(type_Agent, Var_O)) => -(( ! [Var_A] : - ((hasType(type_Agent, Var_A) & hasType(type_Object, Var_A)) => -(((((f_agent(Var_R,Var_A)) & (f_patient(Var_R,Var_O)))) => (f_holdsDuring(f_WhenFn(Var_R),modalAttribute(uses(Var_A,Var_O),inst_Permission)))))))))))))). - -fof(axMidLem593, axiom, - ( ! [Var_X] : - ((hasType(type_Object, Var_X) & hasType(type_SelfConnectedObject, Var_X)) => -(( ! [Var_T1] : - (hasType(type_TimePosition, Var_T1) => -(((f_holdsDuring(Var_T1,attribute(Var_X,inst_MilitaryPerson))) => (( ? [Var_ORG] : - (hasType(type_MilitaryOrganization, Var_ORG) & -(f_holdsDuring(Var_T1,member(Var_X,Var_ORG)))))))))))))). - -fof(axMidLem594, axiom, - ( ! [Var_ORG] : - (hasType(type_MilitaryOrganization, Var_ORG) => -(( ! [Var_X] : - (hasType(type_Human, Var_X) => -(( ! [Var_T1] : - (hasType(type_TimePosition, Var_T1) => -(((f_holdsDuring(Var_T1,member(Var_X,Var_ORG))) => (f_holdsDuring(Var_T1,attribute(Var_X,inst_MilitaryPerson)))))))))))))). - -fof(axMidLem595, axiom, - ( ! [Var_X] : - (hasType(type_EducationalFacility, Var_X) => -(( ? [Var_ORG] : - (hasType(type_EducationalOrganization, Var_ORG) & -(f_possesses(Var_ORG,Var_X)))))))). - -fof(axMidLem596, axiom, - ( ! [Var_X] : - ((hasType(type_Object, Var_X) & hasType(type_Entity, Var_X)) => -(((f_attribute(Var_X,inst_Student)) => (( ? [Var_EV] : - (hasType(type_EducationalProcess, Var_EV) & -(f_patient(Var_EV,Var_X)))))))))). - -fof(axMidLem597, axiom, - ( ! [Var_X] : - (hasType(type_Subway, Var_X) => -(( ? [Var_SURF] : - ((hasType(type_SelfConnectedObject, Var_SURF) & hasType(type_Object, Var_SURF)) & -(((f_surface(Var_SURF,inst_PlanetEarth)) & (f_orientation(Var_X,Var_SURF,inst_Below)))))))))). - -fof(axMidLem598, axiom, - ( ! [Var_X] : - (hasType(type_TerroristOrganization, Var_X) => -(( ? [Var_EV] : - (hasType(type_ViolentContest, Var_EV) & -(f_agent(Var_EV,Var_X)))))))). - -fof(axMidLem599, axiom, - ( ! [Var_MEMBERS] : - ((hasType(type_Integer, Var_MEMBERS) & hasType(type_Quantity, Var_MEMBERS)) => -(( ! [Var_SEATS] : - ((hasType(type_Integer, Var_SEATS) & hasType(type_Quantity, Var_SEATS)) => -(( ! [Var_ORG] : - ((hasType(type_Organization, Var_ORG) & hasType(type_Collection, Var_ORG)) => -(((((f_seatsInOrganizationCount(Var_ORG,Var_SEATS)) & (f_memberCount(Var_ORG,Var_MEMBERS)))) => (f_greaterThanOrEqualTo(Var_SEATS,Var_MEMBERS))))))))))))). - -fof(axMidLem600, axiom, - ( ! [Var_NUMBER] : - ((hasType(type_NonnegativeInteger, Var_NUMBER) & hasType(type_Integer, Var_NUMBER)) => -(( ! [Var_TYPE] : - (hasType(type_SetOrClass, Var_TYPE) => -(( ! [Var_GROUP] : - (hasType(type_Collection, Var_GROUP) => -(((f_memberTypeCount(Var_GROUP,Var_TYPE,Var_NUMBER)) => (( ? [Var_SUBGROUP] : - (hasType(type_Collection, Var_SUBGROUP) & -(((f_subCollection(Var_SUBGROUP,Var_GROUP)) & (((f_memberCount(Var_SUBGROUP,Var_NUMBER)) & (f_memberType(Var_SUBGROUP,Var_TYPE)))))))))))))))))))). - -fof(axMidLem601, axiom, - ( ! [Var_NUMBER2] : - ((hasType(type_NonnegativeInteger, Var_NUMBER2) & hasType(type_Quantity, Var_NUMBER2)) => -(( ! [Var_TYPE] : - (hasType(type_SetOrClass, Var_TYPE) => -(( ! [Var_NUMBER1] : - ((hasType(type_Integer, Var_NUMBER1) & hasType(type_Quantity, Var_NUMBER1)) => -(( ! [Var_GROUP] : - (hasType(type_Collection, Var_GROUP) => -(((((f_memberCount(Var_GROUP,Var_NUMBER1)) & (f_memberTypeCount(Var_GROUP,Var_TYPE,Var_NUMBER2)))) => (f_greaterThanOrEqualTo(Var_NUMBER1,Var_NUMBER2)))))))))))))))). - -fof(axMidLem602, axiom, - ( ! [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) => -(( ! [Var_COLLECTION] : - (hasType(type_Collection, Var_COLLECTION) => -(( ! [Var_OBJ] : - (hasType(type_SelfConnectedObject, Var_OBJ) => -(((f_memberAtTime(Var_OBJ,Var_COLLECTION,Var_TIME)) <=> (f_holdsDuring(Var_TIME,member(Var_OBJ,Var_COLLECTION)))))))))))))). - -fof(axMidLem603, axiom, - ( ! [Var_OBJ] : - ((hasType(type_SelfConnectedObject, Var_OBJ) & hasType(type_Object, Var_OBJ)) => -(( ! [Var_PLACE] : - (hasType(type_Object, Var_PLACE) => -(( ! [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) => -(( ! [Var_COLLECTION] : - ((hasType(type_Object, Var_COLLECTION) & hasType(type_Collection, Var_COLLECTION)) => -(((((f_locatedAtTime(Var_COLLECTION,Var_TIME,Var_PLACE)) & (f_memberAtTime(Var_OBJ,Var_COLLECTION,Var_TIME)))) => (f_locatedAtTime(Var_OBJ,Var_TIME,Var_PLACE)))))))))))))))). - -fof(axMidLem604, axiom, - ( ! [Var_I] : - ((hasType(type_SelfConnectedObject, Var_I) & hasType(type_Entity, Var_I)) => -(( ! [Var_C] : - (hasType(type_Collection, Var_C) => -(( ! [Var_O] : - ((hasType(type_ContentBearingObject, Var_O) & hasType(type_Entity, Var_O)) => -(((((f_inventory(Var_O,Var_C)) & (f_member(Var_I,Var_C)))) => (f_refers(Var_O,Var_I))))))))))))). - -fof(axMidLem605, axiom, - ( ! [Var_PERSON2] : - (hasType(type_Human, Var_PERSON2) => -(( ! [Var_PERSON1] : - ((hasType(type_Human, Var_PERSON1) & hasType(type_CognitiveAgent, Var_PERSON1)) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((f_subordinateInOrganization(Var_ORG,Var_PERSON1,Var_PERSON2)) => (f_employs(Var_ORG,Var_PERSON1))))))))))))). - -fof(axMidLem606, axiom, - ( ! [Var_PERSON2] : - ((hasType(type_Human, Var_PERSON2) & hasType(type_CognitiveAgent, Var_PERSON2)) => -(( ! [Var_PERSON1] : - (hasType(type_Human, Var_PERSON1) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((f_subordinateInOrganization(Var_ORG,Var_PERSON1,Var_PERSON2)) => (f_employs(Var_ORG,Var_PERSON2))))))))))))). - -fof(axMidLem607, axiom, - ( ! [Var_PERSON1] : - (hasType(type_Human, Var_PERSON1) => -(( ! [Var_ROLE2] : - (hasType(type_Position, Var_ROLE2) => -(( ! [Var_ROLE1] : - (hasType(type_Position, Var_ROLE1) => -(( ! [Var_ORG] : - (hasType(type_Organization, Var_ORG) => -(((((f_subordinatePosition(Var_ORG,Var_ROLE1,Var_ROLE2)) & (f_occupiesPosition(Var_PERSON1,Var_ROLE1,Var_ORG)))) => (( ? [Var_PERSON2] : - (hasType(type_Human, Var_PERSON2) & -(((f_occupiesPosition(Var_PERSON2,Var_ROLE2,Var_ORG)) & (f_subordinateInOrganization(Var_ORG,Var_PERSON1,Var_PERSON2))))))))))))))))))))). - -fof(axMidLem608, axiom, - ( ! [Var_ONT] : - (hasType(type_Ontology, Var_ONT) => -(( ? [Var_TAX] : - (hasType(type_Taxonomy, Var_TAX) & -(f_abstractPart(Var_TAX,Var_ONT)))))))). - -fof(axMidLem609, axiom, - ( ! [Var_EVENT] : - (hasType(type_ServiceProcess, Var_EVENT) => -(( ? [Var_PROVIDER] : - (hasType(type_CognitiveAgent, Var_PROVIDER) & -(f_serviceProvider(Var_EVENT,Var_PROVIDER)))))))). - -fof(axMidLem610, axiom, - ( ! [Var_EVENT] : - (hasType(type_ServiceProcess, Var_EVENT) => -(( ? [Var_RECEIVER] : - (hasType(type_CognitiveAgent, Var_RECEIVER) & -(f_serviceRecipient(Var_EVENT,Var_RECEIVER)))))))). - -fof(axMidLem611, axiom, - ( ! [Var_AGENT] : - ((hasType(type_Physical, Var_AGENT) & hasType(type_Agent, Var_AGENT)) => -(( ! [Var_AGENT_END] : - ((hasType(type_Entity, Var_AGENT_END) & hasType(type_TimePoint, Var_AGENT_END)) => -(( ! [Var_PROCESS] : - ((hasType(type_Physical, Var_PROCESS) & hasType(type_Process, Var_PROCESS)) => -(( ! [Var_PROCESS_START] : - ((hasType(type_Entity, Var_PROCESS_START) & hasType(type_TimePoint, Var_PROCESS_START)) => -(((((Var_PROCESS_START = f_BeginFn(f_WhenFn(Var_PROCESS))) & (((Var_AGENT_END = f_EndFn(f_WhenFn(Var_AGENT))) & (f_benefits(Var_PROCESS,Var_AGENT)))))) => (f_before(Var_PROCESS_START,Var_AGENT_END)))))))))))))))). - -fof(axMidLem612, axiom, - ( ! [Var_PARENT] : - (hasType(type_Man, Var_PARENT) => -(( ! [Var_CHILD] : - (hasType(type_Organism, Var_CHILD) => -(((f_parent(Var_CHILD,Var_PARENT)) => (f_father(Var_CHILD,Var_PARENT)))))))))). - -fof(axMidLem613, axiom, - ( ! [Var_PARENT] : - (hasType(type_Woman, Var_PARENT) => -(( ! [Var_CHILD] : - (hasType(type_Organism, Var_CHILD) => -(((f_parent(Var_CHILD,Var_PARENT)) => (f_mother(Var_CHILD,Var_PARENT)))))))))). - -fof(axMidLem614, axiom, - ( ! [Var_CHILD] : - (hasType(type_Man, Var_CHILD) => -(( ! [Var_PARENT] : - (hasType(type_Organism, Var_PARENT) => -(((f_parent(Var_CHILD,Var_PARENT)) => (f_son(Var_CHILD,Var_PARENT)))))))))). - -fof(axMidLem615, axiom, - ( ! [Var_CHILD] : - (hasType(type_Woman, Var_CHILD) => -(( ! [Var_PARENT] : - (hasType(type_Organism, Var_PARENT) => -(((f_parent(Var_CHILD,Var_PARENT)) => (f_daughter(Var_CHILD,Var_PARENT)))))))))). - -fof(axMidLem616, axiom, - ( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Organism, Var_H)) => -(( ! [Var_A] : - (hasType(type_Woman, Var_A) => -(((f_aunt(Var_A,Var_H)) <=> (( ? [Var_P] : - ((hasType(type_Human, Var_P) & hasType(type_Organism, Var_P)) & -(((f_sister(Var_A,Var_P)) & (f_parent(Var_H,Var_P))))))))))))))). - -fof(axMidLem617, axiom, - ( ! [Var_P2] : - ((hasType(type_Human, Var_P2) & hasType(type_Organism, Var_P2)) => -(( ! [Var_P1] : - ((hasType(type_Human, Var_P1) & hasType(type_Organism, Var_P1)) => -(((f_cousin(Var_P1,Var_P2)) <=> (((( ? [Var_G2] : - (hasType(type_Man, Var_G2) & -(( ? [Var_G1] : - (hasType(type_Woman, Var_G1) & -(((f_grandmother(Var_P1,Var_G1)) & (((f_grandfather(Var_P1,Var_G2)) & (((f_grandmother(Var_P2,Var_G1)) & (f_grandfather(Var_P2,Var_G2)))))))))))))) & (( ~ ( ? [Var_F] : - (hasType(type_Organism, Var_F) & -(( ? [Var_M] : - (hasType(type_Organism, Var_M) & -(((f_mother(Var_P1,Var_M)) & (((f_father(Var_P1,Var_F)) & (((f_mother(Var_P2,Var_M)) & (f_father(Var_P2,Var_F))))))))))))))))))))))))). - -fof(axMidLem618, axiom, - ( ! [Var_P] : - ((hasType(type_Man, Var_P) & hasType(type_Organism, Var_P)) => -(( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Organism, Var_H)) => -(((f_grandfather(Var_H,Var_P)) => (( ? [Var_C] : - (hasType(type_Organism, Var_C) & -(((f_father(Var_C,Var_P)) & (f_parent(Var_H,Var_C))))))))))))))). - -fof(axMidLem619, axiom, - ( ! [Var_P] : - ((hasType(type_Woman, Var_P) & hasType(type_Organism, Var_P)) => -(( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Organism, Var_H)) => -(((f_grandmother(Var_H,Var_P)) => (( ? [Var_C] : - (hasType(type_Organism, Var_C) & -(((f_mother(Var_C,Var_P)) & (f_parent(Var_H,Var_C))))))))))))))). - -fof(axMidLem620, axiom, - ( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Organism, Var_H)) => -(( ! [Var_N] : - ((hasType(type_Man, Var_N) & hasType(type_Organism, Var_N)) => -(((f_nephew(Var_N,Var_H)) <=> (( ? [Var_S] : - (hasType(type_Organism, Var_S) & -(((f_sibling(Var_S,Var_H)) & (f_son(Var_N,Var_S))))))))))))))). - -fof(axMidLem621, axiom, - ( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Organism, Var_H)) => -(( ! [Var_N] : - ((hasType(type_Woman, Var_N) & hasType(type_Organism, Var_N)) => -(((f_niece(Var_N,Var_H)) <=> (( ? [Var_S] : - (hasType(type_Organism, Var_S) & -(((f_sibling(Var_S,Var_H)) & (f_daughter(Var_N,Var_S))))))))))))))). - -fof(axMidLem622, axiom, - ( ! [Var_H] : - ((hasType(type_Human, Var_H) & hasType(type_Organism, Var_H)) => -(( ! [Var_U] : - (hasType(type_Man, Var_U) => -(((f_uncle(Var_U,Var_H)) <=> (( ? [Var_P] : - ((hasType(type_Human, Var_P) & hasType(type_Organism, Var_P)) & -(((f_brother(Var_U,Var_P)) & (f_parent(Var_H,Var_P))))))))))))))). - -fof(axMidLem623, axiom, - ( ! [Var_F] : - ((hasType(type_Man, Var_F) & hasType(type_Human, Var_F) & hasType(type_Organism, Var_F)) => -(( ! [Var_P] : - ((hasType(type_Human, Var_P) & hasType(type_Organism, Var_P)) => -(((f_stepfather(Var_P,Var_F)) <=> (( ? [Var_M] : - ((hasType(type_Organism, Var_M) & hasType(type_Human, Var_M)) & -(((f_mother(Var_P,Var_M)) & (((f_spouse(Var_F,Var_M)) & (( ~ (f_father(Var_P,Var_F))))))))))))))))))). - -fof(axMidLem624, axiom, - ( ! [Var_M] : - ((hasType(type_Woman, Var_M) & hasType(type_Human, Var_M) & hasType(type_Organism, Var_M)) => -(( ! [Var_P] : - ((hasType(type_Human, Var_P) & hasType(type_Organism, Var_P)) => -(((f_stepmother(Var_P,Var_M)) <=> (( ? [Var_F] : - ((hasType(type_Organism, Var_F) & hasType(type_Human, Var_F)) & -(((f_father(Var_P,Var_F)) & (((f_spouse(Var_M,Var_F)) & (( ~ (f_mother(Var_P,Var_M))))))))))))))))))). - -fof(axMidLem625, axiom, - ( ! [Var_PLACE] : - (hasType(type_Object, Var_PLACE) => -(( ! [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) => -(( ! [Var_OBJ] : - ((hasType(type_Object, Var_OBJ) & hasType(type_Physical, Var_OBJ)) => -(((f_locatedAtTime(Var_OBJ,Var_TIME,Var_PLACE)) <=> (f_holdsDuring(Var_TIME,located(Var_OBJ,Var_PLACE)))))))))))))). - -fof(axMidLem626, axiom, - ( ! [Var_REGION] : - ((hasType(type_GeographicArea, Var_REGION) & hasType(type_Object, Var_REGION)) => -(( ! [Var_PLACE] : - ((hasType(type_Object, Var_PLACE) & hasType(type_GeographicArea, Var_PLACE)) => -(( ! [Var_TIME] : - (hasType(type_TimePosition, Var_TIME) => -(( ! [Var_OBJ] : - (hasType(type_Object, Var_OBJ) => -(((((f_locatedAtTime(Var_OBJ,Var_TIME,Var_PLACE)) & (f_geographicSubregion(Var_PLACE,Var_REGION)))) => (f_locatedAtTime(Var_OBJ,Var_TIME,Var_REGION)))))))))))))))). - -fof(axMidLem627, axiom, - ( ! [Var_S] : - (hasType(type_Seating, Var_S) => -(( ? [Var_P] : - (hasType(type_Seat, Var_P) & -(( ? [Var_H] : - (hasType(type_Human, Var_H) & -(((f_experiencer(Var_S,Var_H)) & (f_destination(Var_S,Var_P))))))))))))). - -fof(axMidLem628, axiom, - ( ! [Var_ARREST] : - (hasType(type_PlacingUnderArrest, Var_ARREST) => -(( ! [Var_AGENT] : - (hasType(type_GroupOfPeople, Var_AGENT) => -(( ! [Var_MEMBER] : - ((hasType(type_SelfConnectedObject, Var_MEMBER) & hasType(type_Agent, Var_MEMBER)) => -(((((f_arrested(Var_ARREST,Var_AGENT)) & (f_member(Var_MEMBER,Var_AGENT)))) => (( ? [Var_ARREST1] : - (hasType(type_PlacingUnderArrest, Var_ARREST1) & -(((f_arrested(Var_ARREST1,Var_MEMBER)) & (f_subProcess(Var_ARREST1,Var_ARREST)))))))))))))))))). - -fof(axMidLem629, axiom, - ( ! [Var_PROC] : - (hasType(type_Process, Var_PROC) => -(( ! [Var_SUB] : - ((hasType(type_Process, Var_SUB) & hasType(type_Physical, Var_SUB)) => -(( ! [Var_LOC] : - (hasType(type_Object, Var_LOC) => -(((((f_located(Var_PROC,Var_LOC)) & (f_subProcess(Var_SUB,Var_PROC)))) => (f_located(Var_SUB,Var_LOC))))))))))))). - -fof(axMidLem630, axiom, - ( ! [Var_IMPRISON] : - (hasType(type_Imprisoning, Var_IMPRISON) => -(( ! [Var_AGENT] : - (hasType(type_Human, Var_AGENT) => -(( ! [Var_INTERVAL] : - (hasType(type_TimeInterval, Var_INTERVAL) => -(((((f_detainee(Var_IMPRISON,Var_AGENT)) & (f_time(Var_IMPRISON,Var_INTERVAL)))) => (( ? [Var_ARREST] : - (hasType(type_PlacingUnderArrest, Var_ARREST) & -(( ? [Var_TIME] : - (hasType(type_TimeInterval, Var_TIME) & -(((f_time(Var_ARREST,Var_TIME)) & (((f_earlier(Var_TIME,Var_INTERVAL)) & (f_arrested(Var_ARREST,Var_AGENT))))))))))))))))))))))). - -fof(axMidLem631, axiom, - ( ! [Var_TRANSPORT] : - (hasType(type_TransportViaRoadVehicle, Var_TRANSPORT) => -(( ? [Var_DRIVING] : - (hasType(type_Driving, Var_DRIVING) & -(f_subProcess(Var_TRANSPORT,Var_DRIVING)))))))). - -fof(axMidLem632, axiom, - ( ! [Var_TRANSPORT] : - (hasType(type_Transportation, Var_TRANSPORT) => -(( ! [Var_DRIVE] : - (hasType(type_Driving, Var_DRIVE) => -(( ! [Var_VEHICLE] : - (hasType(type_TransportationDevice, Var_VEHICLE) => -(((((f_subProcess(Var_TRANSPORT,Var_DRIVE)) & (f_instrument(Var_TRANSPORT,Var_VEHICLE)))) => (f_patient(Var_DRIVE,Var_VEHICLE))))))))))))). - -fof(axMidLem633, axiom, - ( ! [Var_DRIVE] : - (hasType(type_Driving, Var_DRIVE) => -(( ! [Var_VEHICLE] : - (hasType(type_RoadVehicle, Var_VEHICLE) => -(((f_patient(Var_DRIVE,Var_VEHICLE)) => (( ? [Var_TRANSPORT] : - (hasType(type_TransportViaRoadVehicle, Var_TRANSPORT) & -(f_subProcess(Var_TRANSPORT,Var_DRIVE))))))))))))). - -fof(axMidLem634, axiom, - ( ! [Var_DRIVING] : - (hasType(type_Driving, Var_DRIVING) => -(( ! [Var_TRANSPORT] : - (hasType(type_Transportation, Var_TRANSPORT) => -(( ! [Var_DRIVER] : - ((hasType(type_Agent, Var_DRIVER) & hasType(type_Object, Var_DRIVER)) => -(((((f_subProcess(Var_TRANSPORT,Var_DRIVING)) & (f_agent(Var_DRIVING,Var_DRIVER)))) => (f_transported(Var_TRANSPORT,Var_DRIVER))))))))))))). - -fof(axMidLem635, axiom, - ( ! [Var_DRIVING] : - (hasType(type_Driving, Var_DRIVING) => -(( ! [Var_TRANSPORT] : - (hasType(type_Transportation, Var_TRANSPORT) => -(( ! [Var_DEST] : - (hasType(type_Entity, Var_DEST) => -(((((f_subProcess(Var_TRANSPORT,Var_DRIVING)) & (f_destination(Var_DRIVING,Var_DEST)))) => (f_destination(Var_TRANSPORT,Var_DEST))))))))))))). - -fof(axMidLem636, axiom, - ( ! [Var_DRIVING] : - (hasType(type_Driving, Var_DRIVING) => -(( ! [Var_TRANSPORT] : - (hasType(type_Transportation, Var_TRANSPORT) => -(( ! [Var_VEHICLE] : - (hasType(type_Vehicle, Var_VEHICLE) => -(((((f_subProcess(Var_TRANSPORT,Var_DRIVING)) & (f_patient(Var_DRIVING,Var_VEHICLE)))) => (f_conveyance(Var_TRANSPORT,Var_VEHICLE))))))))))))). - -fof(axMidLem637, axiom, - ( ! [Var_A] : - (hasType(type_Atrophy, Var_A) => -(( ? [Var_B] : - (hasType(type_BodyPart, Var_B) & -(f_experiencer(Var_A,Var_B)))))))). - -fof(axMidLem638, axiom, - ( ! [Var_L] : - (hasType(type_Lengthening, Var_L) => -(( ! [Var_O] : - ((hasType(type_Entity, Var_O) & hasType(type_Object, Var_O)) => -(((f_patient(Var_L,Var_O)) => (( ? [Var_L2] : - ((hasType(type_PhysicalQuantity, Var_L2) & hasType(type_Quantity, Var_L2)) & -(( ? [Var_L1] : - ((hasType(type_PhysicalQuantity, Var_L1) & hasType(type_Quantity, Var_L1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_L)),length(Var_O,Var_L1))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_L)),length(Var_O,Var_L2))) & (f_greaterThan(Var_L2,Var_L1)))))))))))))))))))). - -fof(axMidLem639, axiom, - ( ! [Var_S] : - (hasType(type_Saving, Var_S) => -(( ! [Var_A] : - (hasType(type_Agent, Var_A) => -(( ! [Var_O] : - ((hasType(type_Entity, Var_O) & hasType(type_Physical, Var_O) & hasType(type_Object, Var_O)) => -(((((f_patient(Var_S,Var_O)) & (f_agent(Var_S,Var_A)))) => (( ? [Var_Q2] : - ((hasType(type_CurrencyMeasure, Var_Q2) & hasType(type_Quantity, Var_Q2)) & -(( ? [Var_Q1] : - ((hasType(type_CurrencyMeasure, Var_Q1) & hasType(type_Quantity, Var_Q1)) & -(((f_holdsDuring(f_BeginFn(f_WhenFn(Var_S)),monetaryValue(Var_O,Var_Q1))) & (((f_holdsDuring(f_EndFn(f_WhenFn(Var_S)),monetaryValue(Var_O,Var_Q2))) & (((f_possesses(Var_A,Var_O)) & (f_lessThan(Var_Q1,Var_Q2))))))))))))))))))))))))). - -fof(axMidLem640, axiom, - ( ! [Var_A] : - ((hasType(type_Object, Var_A) & hasType(type_Physical, Var_A)) => -(( ! [Var_P] : - (hasType(type_Agent, Var_P) => -(((f_financialAsset(Var_P,Var_A)) => (( ? [Var_V] : - (hasType(type_CurrencyMeasure, Var_V) & -(f_monetaryValue(Var_A,Var_V))))))))))))). - -fof(axMidLem641, axiom, - ( ! [Var_B] : - (hasType(type_Barking, Var_B) => -(( ? [Var_D] : - (hasType(type_Canine, Var_D) & -(f_agent(Var_B,Var_D)))))))). - -fof(axMidLem642, axiom, - ( ! [Var_P] : - (hasType(type_Organification, Var_P) => -(( ? [Var_O] : - (hasType(type_Organ, Var_O) & -(f_result(Var_P,Var_O)))))))). - -fof(axMidLem643, axiom, - ( ! [Var_SR] : - (hasType(type_SexualReproduction, Var_SR) => -(( ? [Var_C] : - (hasType(type_BiologicalConception, Var_C) & -(f_subProcess(Var_C,Var_SR)))))))). - -fof(axMidLem644, axiom, - ( ! [Var_E] : - (hasType(type_BirdEgg, Var_E) => -(( ? [Var_SR] : - (hasType(type_SexualReproduction, Var_SR) & -(( ? [Var_B] : - (hasType(type_Bird, Var_B) & -(((f_agent(Var_SR,Var_B)) & (f_result(Var_SR,Var_E))))))))))))). - -fof(axMidLem645, axiom, - ( ! [Var_R] : - (hasType(type_Raping, Var_R) => -(( ? [Var_A] : - ((hasType(type_Entity, Var_A) & hasType(type_CognitiveAgent, Var_A)) & -(((f_experiencer(Var_R,Var_A)) & (( ~ (f_wants(Var_A,Var_R)))))))))))). - -fof(axMidLem646, axiom, - ( ! [Var_PLACE] : - (hasType(type_Object, Var_PLACE) => -(( ! [Var_INDIV] : - ((hasType(type_Animal, Var_INDIV) & hasType(type_Entity, Var_INDIV)) => -(((f_birthplace(Var_INDIV,Var_PLACE)) => (( ? [Var_BIRTH] : - (hasType(type_Birth, Var_BIRTH) & -(((f_experiencer(Var_BIRTH,Var_INDIV)) & (f_located(Var_BIRTH,Var_PLACE))))))))))))))). - -fof(axMidLem647, axiom, - ( ! [Var_D] : - (hasType(type_Day, Var_D) => -(( ! [Var_P] : - ((hasType(type_Human, Var_P) & hasType(type_Entity, Var_P)) => -(((f_birthdate(Var_P,Var_D)) => (( ? [Var_B] : - (hasType(type_Birth, Var_B) & -(((f_experiencer(Var_B,Var_P)) & (f_date(Var_B,Var_D))))))))))))))). - -fof(axMidLem648, axiom, - ( ! [Var_T] : - (hasType(type_Day, Var_T) => -(( ! [Var_P] : - ((hasType(type_Human, Var_P) & hasType(type_Entity, Var_P)) => -(((f_deathdate(Var_P,Var_T)) => (( ? [Var_D] : - (hasType(type_Death, Var_D) & -(((f_experiencer(Var_D,Var_P)) & (f_date(Var_D,Var_T))))))))))))))). - -fof(axMidLem649, axiom, - ( ! [Var_L] : - (hasType(type_Object, Var_L) => -(( ! [Var_P] : - ((hasType(type_Animal, Var_P) & hasType(type_Entity, Var_P)) => -(((f_deathplace(Var_P,Var_L)) => (( ? [Var_D] : - (hasType(type_Death, Var_D) & -(((f_experiencer(Var_D,Var_P)) & (f_located(Var_D,Var_L))))))))))))))). - -fof(axMidLem650, axiom, - ( ! [Var_S] : - (hasType(type_TransitSystem, Var_S) => -(( ! [Var_P] : - ((hasType(type_Transitway, Var_P) & hasType(type_Object, Var_P)) => -(((f_pathInSystem(Var_P,Var_S)) => (((f_routeInSystem(Var_P,Var_S)) | (( ? [Var_R2] : - ((hasType(type_Transitway, Var_R2) & hasType(type_Object, Var_R2)) & -(( ? [Var_R1] : - ((hasType(type_Transitway, Var_R1) & hasType(type_Object, Var_R1)) & -(((f_routeInSystem(Var_R1,Var_S)) & (((f_routeInSystem(Var_R2,Var_S)) & (((f_part(Var_R1,Var_P)) & (((f_part(Var_R2,Var_P)) & (f_connected(Var_R1,Var_R2)))))))))))))))))))))))))). - -fof(axMidLem651, axiom, - ( ! [Var_P] : - (hasType(type_Transitway, Var_P) => -(( ! [Var_T] : - ((hasType(type_PhysicalSystem, Var_T) & hasType(type_TransitSystem, Var_T)) => -(( ! [Var_S] : - ((hasType(type_PhysicalSystem, Var_S) & hasType(type_TransitSystem, Var_S)) => -(((((f_subSystem(Var_S,Var_T)) & (f_routeInSystem(Var_P,Var_S)))) => (f_routeInSystem(Var_P,Var_T))))))))))))). - -- cgit v1.2.3