%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : CSR126^2 : TPTP v6.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n190.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:21:03 EDT 2014 % Result : Timeout 300.10s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : CSR126^2 : TPTP v6.1.0. Released v4.1.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n190.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 10:05:41 CDT 2014 % % CPUTime : 300.10 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x2500488>, <kernel.Type object at 0x25003b0>) of role type named numbers % Using role type % Declaring num:Type % FOF formula (<kernel.Constant object at 0x2775560>, <kernel.Constant object at 0x2500560>) of role type named agent_THFTYPE_i % Using role type % Declaring agent_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2775560>, <kernel.Single object at 0x2500908>) of role type named attribute_THFTYPE_i % Using role type % Declaring attribute_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2500050>, <kernel.DependentProduct object at 0x251ff80>) of role type named disjointRelation_THFTYPE_IiioI % Using role type % Declaring disjointRelation_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2500908>, <kernel.DependentProduct object at 0x251f9e0>) of role type named disjoint_THFTYPE_IiioI % Using role type % Declaring disjoint_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x251ff80>, <kernel.Single object at 0x2500050>) of role type named documentation_THFTYPE_i % Using role type % Declaring documentation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x25003b0>, <kernel.DependentProduct object at 0x25008c0>) of role type named domainSubclass_THFTYPE_IIiioIiioI % Using role type % Declaring domainSubclass_THFTYPE_IIiioIiioI:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x25003b0>, <kernel.DependentProduct object at 0x2520c68>) of role type named domainSubclass_THFTYPE_IiiioI % Using role type % Declaring domainSubclass_THFTYPE_IiiioI:(fofType->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x25003b0>, <kernel.DependentProduct object at 0x2520c68>) of role type named domain_THFTYPE_IIIiioIIiioIoIiioI % Using role type % Declaring domain_THFTYPE_IIIiioIIiioIoIiioI:(((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop))->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x2500488>, <kernel.DependentProduct object at 0x2520a70>) of role type named domain_THFTYPE_IIiiIiioI % Using role type % Declaring domain_THFTYPE_IIiiIiioI:((fofType->fofType)->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x25003b0>, <kernel.DependentProduct object at 0x2520c68>) of role type named domain_THFTYPE_IIiiioIiioI % Using role type % Declaring domain_THFTYPE_IIiiioIiioI:((fofType->(fofType->(fofType->Prop)))->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x2500248>, <kernel.DependentProduct object at 0x25208c0>) of role type named domain_THFTYPE_IIiioIiioI % Using role type % Declaring domain_THFTYPE_IIiioIiioI:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x25003b0>, <kernel.DependentProduct object at 0x2520b90>) of role type named domain_THFTYPE_IiiioI % Using role type % Declaring domain_THFTYPE_IiiioI:(fofType->(fofType->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x25003b0>, <kernel.DependentProduct object at 0x2520b00>) of role type named duration_THFTYPE_IiioI % Using role type % Declaring duration_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520a70>, <kernel.Single object at 0x2520488>) of role type named equal_THFTYPE_i % Using role type % Declaring equal_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520290>, <kernel.Single object at 0x2520c68>) of role type named greaterThan_THFTYPE_i % Using role type % Declaring greaterThan_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x25204d0>, <kernel.DependentProduct object at 0x2520ab8>) of role type named holdsDuring_THFTYPE_IiooI % Using role type % Declaring holdsDuring_THFTYPE_IiooI:(fofType->(Prop->Prop)) % FOF formula (<kernel.Constant object at 0x25204d0>, <kernel.DependentProduct object at 0x2520b90>) of role type named instance_THFTYPE_IIIiioIiioIioI % Using role type % Declaring instance_THFTYPE_IIIiioIiioIioI:(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520c68>, <kernel.DependentProduct object at 0x25200e0>) of role type named instance_THFTYPE_IIiiIioI % Using role type % Declaring instance_THFTYPE_IIiiIioI:((fofType->fofType)->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520290>, <kernel.DependentProduct object at 0x2520bd8>) of role type named instance_THFTYPE_IIiiiIioI % Using role type % Declaring instance_THFTYPE_IIiiiIioI:((fofType->(fofType->fofType))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520ab8>, <kernel.DependentProduct object at 0x2520c20>) of role type named instance_THFTYPE_IIiiioIioI % Using role type % Declaring instance_THFTYPE_IIiiioIioI:((fofType->(fofType->(fofType->Prop)))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520cb0>, <kernel.DependentProduct object at 0x2520bd8>) of role type named instance_THFTYPE_IIiioIioI % Using role type % Declaring instance_THFTYPE_IIiioIioI:((fofType->(fofType->Prop))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520c68>, <kernel.DependentProduct object at 0x25204d0>) of role type named instance_THFTYPE_IIiooIioI % Using role type % Declaring instance_THFTYPE_IIiooIioI:((fofType->(Prop->Prop))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520290>, <kernel.DependentProduct object at 0x2520cb0>) of role type named instance_THFTYPE_IiioI % Using role type % Declaring instance_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2520b90>, <kernel.Single object at 0x2520ab8>) of role type named instrument_THFTYPE_i % Using role type % Declaring instrument_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520c68>, <kernel.Single object at 0x2520a70>) of role type named lAdditionFn_THFTYPE_i % Using role type % Declaring lAdditionFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520c68>, <kernel.Single object at 0x2520a70>) of role type named lAsymmetricRelation_THFTYPE_i % Using role type % Declaring lAsymmetricRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520248>, <kernel.DependentProduct object at 0x25205a8>) of role type named lBeginFn_THFTYPE_IiiI % Using role type % Declaring lBeginFn_THFTYPE_IiiI:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x2520b90>, <kernel.Single object at 0x2520c68>) of role type named lBill_THFTYPE_i % Using role type % Declaring lBill_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520680>, <kernel.Single object at 0x25204d0>) of role type named lBinaryFunction_THFTYPE_i % Using role type % Declaring lBinaryFunction_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520248>, <kernel.Single object at 0x25203b0>) of role type named lBinaryPredicate_THFTYPE_i % Using role type % Declaring lBinaryPredicate_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520b90>, <kernel.DependentProduct object at 0x2520170>) of role type named lCardinalityFn_THFTYPE_IiiI % Using role type % Declaring lCardinalityFn_THFTYPE_IiiI:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x2520320>, <kernel.Single object at 0x25203b0>) of role type named lDayDuration_THFTYPE_i % Using role type % Declaring lDayDuration_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520248>, <kernel.Single object at 0x2520a70>) of role type named lDay_THFTYPE_i % Using role type % Declaring lDay_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520b90>, <kernel.DependentProduct object at 0x24b8560>) of role type named lEndFn_THFTYPE_IiiI % Using role type % Declaring lEndFn_THFTYPE_IiiI:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x2520680>, <kernel.Single object at 0x2520a70>) of role type named lEntity_THFTYPE_i % Using role type % Declaring lEntity_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520680>, <kernel.Single object at 0x2520a70>) of role type named lInheritableRelation_THFTYPE_i % Using role type % Declaring lInheritableRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520290>, <kernel.Single object at 0x2520320>) of role type named lInteger_THFTYPE_i % Using role type % Declaring lInteger_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520320>, <kernel.Single object at 0x2520680>) of role type named lIrreflexiveRelation_THFTYPE_i % Using role type % Declaring lIrreflexiveRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x24b81b8>, <kernel.Single object at 0x2520290>) of role type named lMary_THFTYPE_i % Using role type % Declaring lMary_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x25207a0>, <kernel.DependentProduct object at 0x2777908>) of role type named lMeasureFn_THFTYPE_IiiiI % Using role type % Declaring lMeasureFn_THFTYPE_IiiiI:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x2520680>, <kernel.Single object at 0x25207a0>) of role type named lMonthFn_THFTYPE_i % Using role type % Declaring lMonthFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520320>, <kernel.Single object at 0x2520290>) of role type named lMonth_THFTYPE_i % Using role type % Declaring lMonth_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x25207a0>, <kernel.Single object at 0x2777908>) of role type named lMultiplicationFn_THFTYPE_i % Using role type % Declaring lMultiplicationFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520290>, <kernel.Single object at 0x2777830>) of role type named lObject_THFTYPE_i % Using role type % Declaring lObject_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2520290>, <kernel.Single object at 0x27779e0>) of role type named lProcess_THFTYPE_i % Using role type % Declaring lProcess_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777ab8>, <kernel.Single object at 0x2777320>) of role type named lQuantity_THFTYPE_i % Using role type % Declaring lQuantity_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a28>, <kernel.Single object at 0x2777998>) of role type named lRelationExtendedToQuantities_THFTYPE_i % Using role type % Declaring lRelationExtendedToQuantities_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a70>, <kernel.Single object at 0x2777128>) of role type named lRelation_THFTYPE_i % Using role type % Declaring lRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777ab8>, <kernel.Single object at 0x2777b90>) of role type named lSetOrClass_THFTYPE_i % Using role type % Declaring lSetOrClass_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a28>, <kernel.Single object at 0x2777bd8>) of role type named lSubtractionFn_THFTYPE_i % Using role type % Declaring lSubtractionFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a70>, <kernel.Single object at 0x2777a28>) of role type named lSue_THFTYPE_i % Using role type % Declaring lSue_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777ab8>, <kernel.DependentProduct object at 0x251ecb0>) of role type named lTemporalCompositionFn_THFTYPE_IiiiI % Using role type % Declaring lTemporalCompositionFn_THFTYPE_IiiiI:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x251e5a8>, <kernel.Single object at 0x2777a70>) of role type named lTemporalCompositionFn_THFTYPE_i % Using role type % Declaring lTemporalCompositionFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a28>, <kernel.Single object at 0x251e950>) of role type named lTemporalRelation_THFTYPE_i % Using role type % Declaring lTemporalRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a70>, <kernel.Single object at 0x251e5a8>) of role type named lTernaryPredicate_THFTYPE_i % Using role type % Declaring lTernaryPredicate_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2777a70>, <kernel.Single object at 0x251e488>) of role type named lTimeInterval_THFTYPE_i % Using role type % Declaring lTimeInterval_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251e5f0>, <kernel.Single object at 0x251e488>) of role type named lTotalValuedRelation_THFTYPE_i % Using role type % Declaring lTotalValuedRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251ec20>, <kernel.Single object at 0x251e5f0>) of role type named lTransitiveRelation_THFTYPE_i % Using role type % Declaring lTransitiveRelation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251ecb0>, <kernel.Single object at 0x251e440>) of role type named lUnaryFunction_THFTYPE_i % Using role type % Declaring lUnaryFunction_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251e488>, <kernel.DependentProduct object at 0x23227e8>) of role type named lWhenFn_THFTYPE_IiiI % Using role type % Declaring lWhenFn_THFTYPE_IiiI:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x251ecb0>, <kernel.Single object at 0x251e488>) of role type named lWhenFn_THFTYPE_i % Using role type % Declaring lWhenFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251ec20>, <kernel.DependentProduct object at 0x2322758>) of role type named lYearFn_THFTYPE_IiiI % Using role type % Declaring lYearFn_THFTYPE_IiiI:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x251e440>, <kernel.Single object at 0x2322908>) of role type named lYearFn_THFTYPE_i % Using role type % Declaring lYearFn_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251ec20>, <kernel.Single object at 0x2322878>) of role type named lYear_THFTYPE_i % Using role type % Declaring lYear_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x251ec20>, <kernel.Single object at 0x2322758>) of role type named lessThan_THFTYPE_i % Using role type % Declaring lessThan_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23228c0>, <kernel.DependentProduct object at 0x2322830>) of role type named likes_THFTYPE_IiioI % Using role type % Declaring likes_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x23227a0>, <kernel.DependentProduct object at 0x2322950>) of role type named located_THFTYPE_IiioI % Using role type % Declaring located_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x23227a0>, <kernel.DependentProduct object at 0x2322908>) of role type named meetsTemporally_THFTYPE_IiioI % Using role type % Declaring meetsTemporally_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2322830>, <kernel.DependentProduct object at 0x2322908>) of role type named minus_THFTYPE_IiiiI % Using role type % Declaring minus_THFTYPE_IiiiI:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x23228c0>, <kernel.Single object at 0x23225f0>) of role type named n12_THFTYPE_i % Using role type % Declaring n12_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23225a8>, <kernel.Single object at 0x2322758>) of role type named n1_THFTYPE_i % Using role type % Declaring n1_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2322830>, <kernel.Single object at 0x23227a0>) of role type named n2009_THFTYPE_i % Using role type % Declaring n2009_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23228c0>, <kernel.Single object at 0x2322488>) of role type named n2_THFTYPE_i % Using role type % Declaring n2_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23225a8>, <kernel.Single object at 0x2322560>) of role type named n3_THFTYPE_i % Using role type % Declaring n3_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2322830>, <kernel.Single object at 0x23226c8>) of role type named orientation_THFTYPE_i % Using role type % Declaring orientation_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23228c0>, <kernel.DependentProduct object at 0x23225a8>) of role type named part_THFTYPE_IiioI % Using role type % Declaring part_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x23223f8>, <kernel.Single object at 0x2322440>) of role type named patient_THFTYPE_i % Using role type % Declaring patient_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2322830>, <kernel.DependentProduct object at 0x23228c0>) of role type named rangeSubclass_THFTYPE_IiioI % Using role type % Declaring rangeSubclass_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x23226c8>, <kernel.DependentProduct object at 0x23223f8>) of role type named range_THFTYPE_IiioI % Using role type % Declaring range_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x23224d0>, <kernel.DependentProduct object at 0x2322440>) of role type named relatedInternalConcept_THFTYPE_IIiioIIiioIoI % Using role type % Declaring relatedInternalConcept_THFTYPE_IIiioIIiioIoI:((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop)) % FOF formula (<kernel.Constant object at 0x2322a70>, <kernel.DependentProduct object at 0x2322bd8>) of role type named relatedInternalConcept_THFTYPE_IiIiiIoI % Using role type % Declaring relatedInternalConcept_THFTYPE_IiIiiIoI:(fofType->((fofType->fofType)->Prop)) % FOF formula (<kernel.Constant object at 0x23223f8>, <kernel.DependentProduct object at 0x23224d0>) of role type named relatedInternalConcept_THFTYPE_IiioI % Using role type % Declaring relatedInternalConcept_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2322ab8>, <kernel.Single object at 0x2322440>) of role type named result_THFTYPE_i % Using role type % Declaring result_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x2322a70>, <kernel.DependentProduct object at 0x23223f8>) of role type named subProcess_THFTYPE_IiioI % Using role type % Declaring subProcess_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2322bd8>, <kernel.DependentProduct object at 0x2322ab8>) of role type named subclass_THFTYPE_IiioI % Using role type % Declaring subclass_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2322bd8>, <kernel.DependentProduct object at 0x2322d88>) of role type named subrelation_THFTYPE_IIioIIioIoI % Using role type % Declaring subrelation_THFTYPE_IIioIIioIoI:((fofType->Prop)->((fofType->Prop)->Prop)) % FOF formula (<kernel.Constant object at 0x23223f8>, <kernel.DependentProduct object at 0x2322d88>) of role type named subrelation_THFTYPE_IiioI % Using role type % Declaring subrelation_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2322a70>, <kernel.DependentProduct object at 0x2322ab8>) of role type named temporalPart_THFTYPE_IiioI % Using role type % Declaring temporalPart_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (forall (REL2:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and ((rangeSubclass_THFTYPE_IiioI REL1) CLASS1)) ((rangeSubclass_THFTYPE_IiioI REL2) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) of role axiom named ax % A new axiom: (forall (REL2:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and ((rangeSubclass_THFTYPE_IiioI REL1) CLASS1)) ((rangeSubclass_THFTYPE_IiioI REL2) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) % FOF formula ((subclass_THFTYPE_IiioI lInheritableRelation_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_001 % A new axiom: ((subclass_THFTYPE_IiioI lInheritableRelation_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((subclass_THFTYPE_IiioI X) Y)) ((instance_THFTYPE_IiioI Z) X))->((instance_THFTYPE_IiioI Z) Y))) of role axiom named ax_002 % A new axiom: (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((subclass_THFTYPE_IiioI X) Y)) ((instance_THFTYPE_IiioI Z) X))->((instance_THFTYPE_IiioI Z) Y))) % FOF formula (forall (X:fofType) (Y:fofType), (((subclass_THFTYPE_IiioI X) Y)->((and ((instance_THFTYPE_IiioI X) lSetOrClass_THFTYPE_i)) ((instance_THFTYPE_IiioI Y) lSetOrClass_THFTYPE_i)))) of role axiom named ax_003 % A new axiom: (forall (X:fofType) (Y:fofType), (((subclass_THFTYPE_IiioI X) Y)->((and ((instance_THFTYPE_IiioI X) lSetOrClass_THFTYPE_i)) ((instance_THFTYPE_IiioI Y) lSetOrClass_THFTYPE_i)))) % FOF formula (forall (THING:fofType), ((instance_THFTYPE_IiioI THING) lEntity_THFTYPE_i)) of role axiom named ax_004 % A new axiom: (forall (THING:fofType), ((instance_THFTYPE_IiioI THING) lEntity_THFTYPE_i)) % FOF formula (forall (X:fofType), ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) (((likes_THFTYPE_IiioI lMary_THFTYPE_i) X)->((likes_THFTYPE_IiioI lSue_THFTYPE_i) X)))) of role axiom named ax_005 % A new axiom: (forall (X:fofType), ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) (((likes_THFTYPE_IiioI lMary_THFTYPE_i) X)->((likes_THFTYPE_IiioI lSue_THFTYPE_i) X)))) % FOF formula (forall (X:fofType), ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) (((likes_THFTYPE_IiioI lMary_THFTYPE_i) X)->((likes_THFTYPE_IiioI lSue_THFTYPE_i) X)))) of role axiom named ax_006 % A new axiom: (forall (X:fofType), ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) (((likes_THFTYPE_IiioI lMary_THFTYPE_i) X)->((likes_THFTYPE_IiioI lSue_THFTYPE_i) X)))) % FOF formula (forall (NUMBER:fofType) (MONTH:fofType), (((and ((instance_THFTYPE_IiioI MONTH) lMonth_THFTYPE_i)) ((duration_THFTYPE_IiioI MONTH) ((lMeasureFn_THFTYPE_IiiiI NUMBER) lDayDuration_THFTYPE_i)))->(((eq fofType) (lCardinalityFn_THFTYPE_IiiI ((lTemporalCompositionFn_THFTYPE_IiiiI MONTH) lDay_THFTYPE_i))) NUMBER))) of role axiom named ax_007 % A new axiom: (forall (NUMBER:fofType) (MONTH:fofType), (((and ((instance_THFTYPE_IiioI MONTH) lMonth_THFTYPE_i)) ((duration_THFTYPE_IiioI MONTH) ((lMeasureFn_THFTYPE_IiiiI NUMBER) lDayDuration_THFTYPE_i)))->(((eq fofType) (lCardinalityFn_THFTYPE_IiiI ((lTemporalCompositionFn_THFTYPE_IiiiI MONTH) lDay_THFTYPE_i))) NUMBER))) % FOF formula (forall (OBJ1:fofType) (OBJ2:fofType), (((located_THFTYPE_IiioI OBJ1) OBJ2)->(forall (SUB:fofType), (((part_THFTYPE_IiioI SUB) OBJ1)->((located_THFTYPE_IiioI SUB) OBJ2))))) of role axiom named ax_008 % A new axiom: (forall (OBJ1:fofType) (OBJ2:fofType), (((located_THFTYPE_IiioI OBJ1) OBJ2)->(forall (SUB:fofType), (((part_THFTYPE_IiioI SUB) OBJ1)->((located_THFTYPE_IiioI SUB) OBJ2))))) % FOF formula ((subclass_THFTYPE_IiioI lAsymmetricRelation_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) of role axiom named ax_009 % A new axiom: ((subclass_THFTYPE_IiioI lAsymmetricRelation_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) % FOF formula ((subclass_THFTYPE_IiioI lTotalValuedRelation_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_010 % A new axiom: ((subclass_THFTYPE_IiioI lTotalValuedRelation_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula (forall (NUMBER:fofType) (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and (((domainSubclass_THFTYPE_IiiioI REL) NUMBER) CLASS1)) (((domainSubclass_THFTYPE_IiiioI REL) NUMBER) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) of role axiom named ax_011 % A new axiom: (forall (NUMBER:fofType) (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and (((domainSubclass_THFTYPE_IiiioI REL) NUMBER) CLASS1)) (((domainSubclass_THFTYPE_IiiioI REL) NUMBER) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) % FOF formula (forall (DAY:fofType), (((instance_THFTYPE_IiioI DAY) lDay_THFTYPE_i)->((duration_THFTYPE_IiioI DAY) ((lMeasureFn_THFTYPE_IiiiI n1_THFTYPE_i) lDayDuration_THFTYPE_i)))) of role axiom named ax_012 % A new axiom: (forall (DAY:fofType), (((instance_THFTYPE_IiioI DAY) lDay_THFTYPE_i)->((duration_THFTYPE_IiioI DAY) ((lMeasureFn_THFTYPE_IiiiI n1_THFTYPE_i) lDayDuration_THFTYPE_i)))) % FOF formula (forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and (((domainSubclass_THFTYPE_IiiioI REL1) NUMBER) CLASS1)) (((domainSubclass_THFTYPE_IiiioI REL2) NUMBER) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) of role axiom named ax_013 % A new axiom: (forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and (((domainSubclass_THFTYPE_IiiioI REL1) NUMBER) CLASS1)) (((domainSubclass_THFTYPE_IiiioI REL2) NUMBER) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) % FOF formula ((subclass_THFTYPE_IiioI lTemporalRelation_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_014 % A new axiom: ((subclass_THFTYPE_IiioI lTemporalRelation_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((subclass_THFTYPE_IiioI lYear_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_015 % A new axiom: ((subclass_THFTYPE_IiioI lYear_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (forall (NUMBER:fofType) (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and (((domain_THFTYPE_IiiioI REL) NUMBER) CLASS1)) (((domain_THFTYPE_IiiioI REL) NUMBER) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) of role axiom named ax_016 % A new axiom: (forall (NUMBER:fofType) (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and (((domain_THFTYPE_IiiioI REL) NUMBER) CLASS1)) (((domain_THFTYPE_IiiioI REL) NUMBER) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) % FOF formula (forall (REL:(fofType->(fofType->Prop))), ((iff ((instance_THFTYPE_IIiioIioI REL) lTransitiveRelation_THFTYPE_i)) (forall (INST1:fofType) (INST2:fofType) (INST3:fofType), (((and ((REL INST1) INST2)) ((REL INST2) INST3))->((REL INST1) INST3))))) of role axiom named ax_017 % A new axiom: (forall (REL:(fofType->(fofType->Prop))), ((iff ((instance_THFTYPE_IIiioIioI REL) lTransitiveRelation_THFTYPE_i)) (forall (INST1:fofType) (INST2:fofType) (INST3:fofType), (((and ((REL INST1) INST2)) ((REL INST2) INST3))->((REL INST1) INST3))))) % FOF formula ((rangeSubclass_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_018 % A new axiom: ((rangeSubclass_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (forall (REL2:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and ((range_THFTYPE_IiioI REL1) CLASS1)) ((range_THFTYPE_IiioI REL2) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) of role axiom named ax_019 % A new axiom: (forall (REL2:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and ((range_THFTYPE_IiioI REL1) CLASS1)) ((range_THFTYPE_IiioI REL2) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) % FOF formula ((subclass_THFTYPE_IiioI lRelationExtendedToQuantities_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_020 % A new axiom: ((subclass_THFTYPE_IiioI lRelationExtendedToQuantities_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((subclass_THFTYPE_IiioI lMonth_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_021 % A new axiom: ((subclass_THFTYPE_IiioI lMonth_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (forall (TIME:fofType) (SITUATION:Prop), (((holdsDuring_THFTYPE_IiooI TIME) (not SITUATION))->(not ((holdsDuring_THFTYPE_IiooI TIME) SITUATION)))) of role axiom named ax_022 % A new axiom: (forall (TIME:fofType) (SITUATION:Prop), (((holdsDuring_THFTYPE_IiooI TIME) (not SITUATION))->(not ((holdsDuring_THFTYPE_IiooI TIME) SITUATION)))) % FOF formula (forall (T:fofType), ((holdsDuring_THFTYPE_IiooI T) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) of role axiom named ax_023 % A new axiom: (forall (T:fofType), ((holdsDuring_THFTYPE_IiooI T) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) % FOF formula (forall (T:fofType), ((holdsDuring_THFTYPE_IiooI T) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) of role axiom named ax_024 % A new axiom: (forall (T:fofType), ((holdsDuring_THFTYPE_IiooI T) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) % FOF formula ((range_THFTYPE_IiioI lWhenFn_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_025 % A new axiom: ((range_THFTYPE_IiioI lWhenFn_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (forall (INTERVAL1:fofType) (INTERVAL2:fofType), ((iff ((meetsTemporally_THFTYPE_IiioI INTERVAL1) INTERVAL2)) (((eq fofType) (lEndFn_THFTYPE_IiiI INTERVAL1)) (lBeginFn_THFTYPE_IiiI INTERVAL2)))) of role axiom named ax_026 % A new axiom: (forall (INTERVAL1:fofType) (INTERVAL2:fofType), ((iff ((meetsTemporally_THFTYPE_IiioI INTERVAL1) INTERVAL2)) (((eq fofType) (lEndFn_THFTYPE_IiiI INTERVAL1)) (lBeginFn_THFTYPE_IiiI INTERVAL2)))) % FOF formula (forall (SITUATION:Prop) (TIME2:fofType) (TIME1:fofType), (((and ((holdsDuring_THFTYPE_IiooI TIME1) SITUATION)) ((temporalPart_THFTYPE_IiioI TIME2) TIME1))->((holdsDuring_THFTYPE_IiooI TIME2) SITUATION))) of role axiom named ax_027 % A new axiom: (forall (SITUATION:Prop) (TIME2:fofType) (TIME1:fofType), (((and ((holdsDuring_THFTYPE_IiooI TIME1) SITUATION)) ((temporalPart_THFTYPE_IiioI TIME2) TIME1))->((holdsDuring_THFTYPE_IiooI TIME2) SITUATION))) % FOF formula ((range_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_028 % A new axiom: ((range_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula ((ex fofType) (fun (THING:fofType)=> ((instance_THFTYPE_IiioI THING) lEntity_THFTYPE_i))) of role axiom named ax_029 % A new axiom: ((ex fofType) (fun (THING:fofType)=> ((instance_THFTYPE_IiioI THING) lEntity_THFTYPE_i))) % FOF formula (forall (REL:(fofType->(fofType->Prop))), ((iff ((instance_THFTYPE_IIiioIioI REL) lIrreflexiveRelation_THFTYPE_i)) (forall (INST:fofType), (not ((REL INST) INST))))) of role axiom named ax_030 % A new axiom: (forall (REL:(fofType->(fofType->Prop))), ((iff ((instance_THFTYPE_IIiioIioI REL) lIrreflexiveRelation_THFTYPE_i)) (forall (INST:fofType), (not ((REL INST) INST))))) % FOF formula ((subclass_THFTYPE_IiioI lBinaryFunction_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_031 % A new axiom: ((subclass_THFTYPE_IiioI lBinaryFunction_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula (forall (NUMBER:fofType) (PRED1:fofType) (CLASS1:fofType) (PRED2:fofType), (((and ((subrelation_THFTYPE_IiioI PRED1) PRED2)) (((domain_THFTYPE_IiiioI PRED2) NUMBER) CLASS1))->(((domain_THFTYPE_IiiioI PRED1) NUMBER) CLASS1))) of role axiom named ax_032 % A new axiom: (forall (NUMBER:fofType) (PRED1:fofType) (CLASS1:fofType) (PRED2:fofType), (((and ((subrelation_THFTYPE_IiioI PRED1) PRED2)) (((domain_THFTYPE_IiiioI PRED2) NUMBER) CLASS1))->(((domain_THFTYPE_IiiioI PRED1) NUMBER) CLASS1))) % FOF formula ((subclass_THFTYPE_IiioI lTotalValuedRelation_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_033 % A new axiom: ((subclass_THFTYPE_IiioI lTotalValuedRelation_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((subclass_THFTYPE_IiioI lTernaryPredicate_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_034 % A new axiom: ((subclass_THFTYPE_IiioI lTernaryPredicate_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula ((subclass_THFTYPE_IiioI lRelationExtendedToQuantities_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_035 % A new axiom: ((subclass_THFTYPE_IiioI lRelationExtendedToQuantities_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula (forall (YEAR:fofType), (((instance_THFTYPE_IiioI YEAR) lYear_THFTYPE_i)->(((eq fofType) (lCardinalityFn_THFTYPE_IiiI ((lTemporalCompositionFn_THFTYPE_IiiiI YEAR) lMonth_THFTYPE_i))) n12_THFTYPE_i))) of role axiom named ax_036 % A new axiom: (forall (YEAR:fofType), (((instance_THFTYPE_IiioI YEAR) lYear_THFTYPE_i)->(((eq fofType) (lCardinalityFn_THFTYPE_IiiI ((lTemporalCompositionFn_THFTYPE_IiiiI YEAR) lMonth_THFTYPE_i))) n12_THFTYPE_i))) % FOF formula (forall (CLASS1:fofType) (CLASS2:fofType), ((((eq fofType) CLASS1) CLASS2)->(forall (THING:fofType), ((iff ((instance_THFTYPE_IiioI THING) CLASS1)) ((instance_THFTYPE_IiioI THING) CLASS2))))) of role axiom named ax_037 % A new axiom: (forall (CLASS1:fofType) (CLASS2:fofType), ((((eq fofType) CLASS1) CLASS2)->(forall (THING:fofType), ((iff ((instance_THFTYPE_IiioI THING) CLASS1)) ((instance_THFTYPE_IiioI THING) CLASS2))))) % FOF formula (forall (REL2:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) ((rangeSubclass_THFTYPE_IiioI REL2) CLASS1))->((rangeSubclass_THFTYPE_IiioI REL1) CLASS1))) of role axiom named ax_038 % A new axiom: (forall (REL2:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) ((rangeSubclass_THFTYPE_IiioI REL2) CLASS1))->((rangeSubclass_THFTYPE_IiioI REL1) CLASS1))) % FOF formula (forall (YEAR2:fofType) (YEAR1:fofType), (((and ((and ((instance_THFTYPE_IiioI YEAR1) lYear_THFTYPE_i)) ((instance_THFTYPE_IiioI YEAR2) lYear_THFTYPE_i))) (((eq fofType) ((minus_THFTYPE_IiiiI YEAR2) YEAR1)) n1_THFTYPE_i))->((meetsTemporally_THFTYPE_IiioI YEAR1) YEAR2))) of role axiom named ax_039 % A new axiom: (forall (YEAR2:fofType) (YEAR1:fofType), (((and ((and ((instance_THFTYPE_IiioI YEAR1) lYear_THFTYPE_i)) ((instance_THFTYPE_IiioI YEAR2) lYear_THFTYPE_i))) (((eq fofType) ((minus_THFTYPE_IiiiI YEAR2) YEAR1)) n1_THFTYPE_i))->((meetsTemporally_THFTYPE_IiioI YEAR1) YEAR2))) % FOF formula (forall (REL2:(fofType->Prop)) (ROW:fofType) (REL1:(fofType->Prop)), (((and ((subrelation_THFTYPE_IIioIIioIoI REL1) REL2)) (REL1 ROW))->(REL2 ROW))) of role axiom named ax_040 % A new axiom: (forall (REL2:(fofType->Prop)) (ROW:fofType) (REL1:(fofType->Prop)), (((and ((subrelation_THFTYPE_IIioIIioIoI REL1) REL2)) (REL1 ROW))->(REL2 ROW))) % FOF formula (forall (THING2:fofType) (THING1:fofType), ((((eq fofType) THING1) THING2)->(forall (CLASS:fofType), ((iff ((instance_THFTYPE_IiioI THING1) CLASS)) ((instance_THFTYPE_IiioI THING2) CLASS))))) of role axiom named ax_041 % A new axiom: (forall (THING2:fofType) (THING1:fofType), ((((eq fofType) THING1) THING2)->(forall (CLASS:fofType), ((iff ((instance_THFTYPE_IiioI THING1) CLASS)) ((instance_THFTYPE_IiioI THING2) CLASS))))) % FOF formula (forall (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and ((range_THFTYPE_IiioI REL) CLASS1)) ((range_THFTYPE_IiioI REL) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) of role axiom named ax_042 % A new axiom: (forall (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and ((range_THFTYPE_IiioI REL) CLASS1)) ((range_THFTYPE_IiioI REL) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) % FOF formula (forall (CLASS1:fofType) (CLASS2:fofType), ((iff ((disjoint_THFTYPE_IiioI CLASS1) CLASS2)) (forall (INST:fofType), (not ((and ((instance_THFTYPE_IiioI INST) CLASS1)) ((instance_THFTYPE_IiioI INST) CLASS2)))))) of role axiom named ax_043 % A new axiom: (forall (CLASS1:fofType) (CLASS2:fofType), ((iff ((disjoint_THFTYPE_IiioI CLASS1) CLASS2)) (forall (INST:fofType), (not ((and ((instance_THFTYPE_IiioI INST) CLASS1)) ((instance_THFTYPE_IiioI INST) CLASS2)))))) % FOF formula (forall (SUBPROC:fofType) (PROC:fofType), (((subProcess_THFTYPE_IiioI SUBPROC) PROC)->((temporalPart_THFTYPE_IiioI (lWhenFn_THFTYPE_IiiI SUBPROC)) (lWhenFn_THFTYPE_IiiI PROC)))) of role axiom named ax_044 % A new axiom: (forall (SUBPROC:fofType) (PROC:fofType), (((subProcess_THFTYPE_IiioI SUBPROC) PROC)->((temporalPart_THFTYPE_IiioI (lWhenFn_THFTYPE_IiiI SUBPROC)) (lWhenFn_THFTYPE_IiiI PROC)))) % FOF formula ((rangeSubclass_THFTYPE_IiioI lMonthFn_THFTYPE_i) lMonth_THFTYPE_i) of role axiom named ax_045 % A new axiom: ((rangeSubclass_THFTYPE_IiioI lMonthFn_THFTYPE_i) lMonth_THFTYPE_i) % FOF formula (forall (INTERVAL1:fofType) (INTERVAL2:fofType), (((and (((eq fofType) (lBeginFn_THFTYPE_IiiI INTERVAL1)) (lBeginFn_THFTYPE_IiiI INTERVAL2))) (((eq fofType) (lEndFn_THFTYPE_IiiI INTERVAL1)) (lEndFn_THFTYPE_IiiI INTERVAL2)))->(((eq fofType) INTERVAL1) INTERVAL2))) of role axiom named ax_046 % A new axiom: (forall (INTERVAL1:fofType) (INTERVAL2:fofType), (((and (((eq fofType) (lBeginFn_THFTYPE_IiiI INTERVAL1)) (lBeginFn_THFTYPE_IiiI INTERVAL2))) (((eq fofType) (lEndFn_THFTYPE_IiiI INTERVAL1)) (lEndFn_THFTYPE_IiiI INTERVAL2)))->(((eq fofType) INTERVAL1) INTERVAL2))) % FOF formula (forall (REL2:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) ((range_THFTYPE_IiioI REL2) CLASS1))->((range_THFTYPE_IiioI REL1) CLASS1))) of role axiom named ax_047 % A new axiom: (forall (REL2:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) ((range_THFTYPE_IiioI REL2) CLASS1))->((range_THFTYPE_IiioI REL1) CLASS1))) % FOF formula ((subclass_THFTYPE_IiioI lTemporalRelation_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_048 % A new axiom: ((subclass_THFTYPE_IiioI lTemporalRelation_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula (forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) (((domainSubclass_THFTYPE_IiiioI REL2) NUMBER) CLASS1))->(((domainSubclass_THFTYPE_IiiioI REL1) NUMBER) CLASS1))) of role axiom named ax_049 % A new axiom: (forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) (((domainSubclass_THFTYPE_IiiioI REL2) NUMBER) CLASS1))->(((domainSubclass_THFTYPE_IiiioI REL1) NUMBER) CLASS1))) % FOF formula (forall (SUBPROC:fofType) (PROC:fofType), (((subProcess_THFTYPE_IiioI SUBPROC) PROC)->(forall (REGION:fofType), (((located_THFTYPE_IiioI PROC) REGION)->((located_THFTYPE_IiioI SUBPROC) REGION))))) of role axiom named ax_050 % A new axiom: (forall (SUBPROC:fofType) (PROC:fofType), (((subProcess_THFTYPE_IiioI SUBPROC) PROC)->(forall (REGION:fofType), (((located_THFTYPE_IiioI PROC) REGION)->((located_THFTYPE_IiioI SUBPROC) REGION))))) % FOF formula ((range_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_051 % A new axiom: ((range_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula ((range_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_052 % A new axiom: ((range_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (forall (OBJ:fofType) (PROCESS:fofType), (((located_THFTYPE_IiioI PROCESS) OBJ)->(forall (SUB:fofType), (((subProcess_THFTYPE_IiioI SUB) PROCESS)->((located_THFTYPE_IiioI SUB) OBJ))))) of role axiom named ax_053 % A new axiom: (forall (OBJ:fofType) (PROCESS:fofType), (((located_THFTYPE_IiioI PROCESS) OBJ)->(forall (SUB:fofType), (((subProcess_THFTYPE_IiioI SUB) PROCESS)->((located_THFTYPE_IiioI SUB) OBJ))))) % FOF formula ((subclass_THFTYPE_IiioI lUnaryFunction_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_054 % A new axiom: ((subclass_THFTYPE_IiioI lUnaryFunction_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula ((subclass_THFTYPE_IiioI lDay_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_055 % A new axiom: ((subclass_THFTYPE_IiioI lDay_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and (((domain_THFTYPE_IiiioI REL1) NUMBER) CLASS1)) (((domain_THFTYPE_IiiioI REL2) NUMBER) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) of role axiom named ax_056 % A new axiom: (forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and (((domain_THFTYPE_IiiioI REL1) NUMBER) CLASS1)) (((domain_THFTYPE_IiiioI REL2) NUMBER) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))) % FOF formula ((rangeSubclass_THFTYPE_IiioI lYearFn_THFTYPE_i) lYear_THFTYPE_i) of role axiom named ax_057 % A new axiom: ((rangeSubclass_THFTYPE_IiioI lYearFn_THFTYPE_i) lYear_THFTYPE_i) % FOF formula (forall (CLASS:fofType) (PRED1:fofType) (PRED2:fofType), (((and ((and ((subrelation_THFTYPE_IiioI PRED1) PRED2)) ((instance_THFTYPE_IiioI PRED2) CLASS))) ((subclass_THFTYPE_IiioI CLASS) lInheritableRelation_THFTYPE_i))->((instance_THFTYPE_IiioI PRED1) CLASS))) of role axiom named ax_058 % A new axiom: (forall (CLASS:fofType) (PRED1:fofType) (PRED2:fofType), (((and ((and ((subrelation_THFTYPE_IiioI PRED1) PRED2)) ((instance_THFTYPE_IiioI PRED2) CLASS))) ((subclass_THFTYPE_IiioI CLASS) lInheritableRelation_THFTYPE_i))->((instance_THFTYPE_IiioI PRED1) CLASS))) % FOF formula (forall (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and ((rangeSubclass_THFTYPE_IiioI REL) CLASS1)) ((rangeSubclass_THFTYPE_IiioI REL) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) of role axiom named ax_059 % A new axiom: (forall (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and ((rangeSubclass_THFTYPE_IiioI REL) CLASS1)) ((rangeSubclass_THFTYPE_IiioI REL) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))) % FOF formula ((subclass_THFTYPE_IiioI lBinaryPredicate_THFTYPE_i) lInheritableRelation_THFTYPE_i) of role axiom named ax_060 % A new axiom: ((subclass_THFTYPE_IiioI lBinaryPredicate_THFTYPE_i) lInheritableRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lTemporalRelation_THFTYPE_i) of role axiom named ax_061 % A new axiom: ((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lTemporalRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_062 % A new axiom: ((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lTotalValuedRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) of role axiom named ax_063 % A new axiom: ((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI range_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_064 % A new axiom: ((instance_THFTYPE_IIiioIioI range_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lMonthFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) of role axiom named ax_065 % A new axiom: ((instance_THFTYPE_IiioI lMonthFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI disjointRelation_THFTYPE_IiioI) n2_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_066 % A new axiom: (((domain_THFTYPE_IIiioIiioI disjointRelation_THFTYPE_IiioI) n2_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_067 % A new axiom: ((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) % FOF formula (((domainSubclass_THFTYPE_IiiioI lMonthFn_THFTYPE_i) n2_THFTYPE_i) lYear_THFTYPE_i) of role axiom named ax_068 % A new axiom: (((domainSubclass_THFTYPE_IiiioI lMonthFn_THFTYPE_i) n2_THFTYPE_i) lYear_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI subProcess_THFTYPE_IiioI) n1_THFTYPE_i) lProcess_THFTYPE_i) of role axiom named ax_069 % A new axiom: (((domain_THFTYPE_IIiioIiioI subProcess_THFTYPE_IiioI) n1_THFTYPE_i) lProcess_THFTYPE_i) % FOF formula ((relatedInternalConcept_THFTYPE_IiioI lMonth_THFTYPE_i) lMonthFn_THFTYPE_i) of role axiom named ax_070 % A new axiom: ((relatedInternalConcept_THFTYPE_IiioI lMonth_THFTYPE_i) lMonthFn_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lBinaryPredicate_THFTYPE_i) of role axiom named ax_071 % A new axiom: ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lBinaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI meetsTemporally_THFTYPE_IiioI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_072 % A new axiom: (((domain_THFTYPE_IIiioIiioI meetsTemporally_THFTYPE_IiioI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI equal_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_073 % A new axiom: (((domain_THFTYPE_IiiioI equal_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI disjoint_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_074 % A new axiom: (((domain_THFTYPE_IIiioIiioI disjoint_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_075 % A new axiom: ((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI subProcess_THFTYPE_IiioI) n2_THFTYPE_i) lProcess_THFTYPE_i) of role axiom named ax_076 % A new axiom: (((domain_THFTYPE_IIiioIiioI subProcess_THFTYPE_IiioI) n2_THFTYPE_i) lProcess_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI agent_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) of role axiom named ax_077 % A new axiom: (((domain_THFTYPE_IiiioI agent_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI relatedInternalConcept_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_078 % A new axiom: ((instance_THFTYPE_IIiioIioI relatedInternalConcept_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI equal_THFTYPE_i) lBinaryPredicate_THFTYPE_i) of role axiom named ax_079 % A new axiom: ((instance_THFTYPE_IiioI equal_THFTYPE_i) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) of role axiom named ax_080 % A new axiom: ((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) of role axiom named ax_081 % A new axiom: ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI disjointRelation_THFTYPE_IiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_082 % A new axiom: (((domain_THFTYPE_IIiioIiioI disjointRelation_THFTYPE_IiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI greaterThan_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_083 % A new axiom: (((domain_THFTYPE_IiiioI greaterThan_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI range_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_084 % A new axiom: (((domain_THFTYPE_IIiioIiioI range_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI subrelation_THFTYPE_IiioI) n2_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_085 % A new axiom: (((domain_THFTYPE_IIiioIiioI subrelation_THFTYPE_IiioI) n2_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lYearFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) of role axiom named ax_086 % A new axiom: ((instance_THFTYPE_IIiiIioI lYearFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI attribute_THFTYPE_i) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_087 % A new axiom: ((instance_THFTYPE_IiioI attribute_THFTYPE_i) lAsymmetricRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) of role axiom named ax_088 % A new axiom: ((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) % FOF formula ((subrelation_THFTYPE_IiioI result_THFTYPE_i) patient_THFTYPE_i) of role axiom named ax_089 % A new axiom: ((subrelation_THFTYPE_IiioI result_THFTYPE_i) patient_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lMultiplicationFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_090 % A new axiom: (((domain_THFTYPE_IiiioI lMultiplicationFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI patient_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) of role axiom named ax_091 % A new axiom: (((domain_THFTYPE_IiiioI patient_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) of role axiom named ax_092 % A new axiom: ((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) of role axiom named ax_093 % A new axiom: ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_094 % A new axiom: ((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI patient_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_095 % A new axiom: (((domain_THFTYPE_IiiioI patient_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI documentation_THFTYPE_i) lTernaryPredicate_THFTYPE_i) of role axiom named ax_096 % A new axiom: ((instance_THFTYPE_IiioI documentation_THFTYPE_i) lTernaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_097 % A new axiom: ((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI orientation_THFTYPE_i) lTernaryPredicate_THFTYPE_i) of role axiom named ax_098 % A new axiom: ((instance_THFTYPE_IiioI orientation_THFTYPE_i) lTernaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiioIiioI domain_THFTYPE_IiiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_099 % A new axiom: (((domain_THFTYPE_IIiiioIiioI domain_THFTYPE_IiiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) of role axiom named ax_100 % A new axiom: ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI result_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_101 % A new axiom: (((domain_THFTYPE_IiiioI result_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) of role axiom named ax_102 % A new axiom: ((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lTemporalRelation_THFTYPE_i) of role axiom named ax_103 % A new axiom: ((instance_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lTemporalRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI relatedInternalConcept_THFTYPE_IiioI) n2_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_104 % A new axiom: (((domain_THFTYPE_IIiioIiioI relatedInternalConcept_THFTYPE_IiioI) n2_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI subrelation_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_105 % A new axiom: ((instance_THFTYPE_IIiioIioI subrelation_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((relatedInternalConcept_THFTYPE_IIiioIIiioIoI disjointRelation_THFTYPE_IiioI) disjoint_THFTYPE_IiioI) of role axiom named ax_106 % A new axiom: ((relatedInternalConcept_THFTYPE_IIiioIIiioIoI disjointRelation_THFTYPE_IiioI) disjoint_THFTYPE_IiioI) % FOF formula (((domain_THFTYPE_IiiioI greaterThan_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_107 % A new axiom: (((domain_THFTYPE_IiiioI greaterThan_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI part_THFTYPE_IiioI) n1_THFTYPE_i) lObject_THFTYPE_i) of role axiom named ax_108 % A new axiom: (((domain_THFTYPE_IIiioIiioI part_THFTYPE_IiioI) n1_THFTYPE_i) lObject_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) of role axiom named ax_109 % A new axiom: ((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiIiioI lBeginFn_THFTYPE_IiiI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_110 % A new axiom: (((domain_THFTYPE_IIiiIiioI lBeginFn_THFTYPE_IiiI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) of role axiom named ax_111 % A new axiom: ((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI instance_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_112 % A new axiom: ((instance_THFTYPE_IIiioIioI instance_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI attribute_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) of role axiom named ax_113 % A new axiom: ((instance_THFTYPE_IiioI attribute_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lessThan_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_114 % A new axiom: (((domain_THFTYPE_IiiioI lessThan_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI instance_THFTYPE_IiioI) n1_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_115 % A new axiom: (((domain_THFTYPE_IIiioIiioI instance_THFTYPE_IiioI) n1_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiooIioI holdsDuring_THFTYPE_IiooI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_116 % A new axiom: ((instance_THFTYPE_IIiooIioI holdsDuring_THFTYPE_IiooI) lBinaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI part_THFTYPE_IiioI) n2_THFTYPE_i) lObject_THFTYPE_i) of role axiom named ax_117 % A new axiom: (((domain_THFTYPE_IIiioIiioI part_THFTYPE_IiioI) n2_THFTYPE_i) lObject_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI temporalPart_THFTYPE_IiioI) lTemporalRelation_THFTYPE_i) of role axiom named ax_118 % A new axiom: ((instance_THFTYPE_IIiioIioI temporalPart_THFTYPE_IiioI) lTemporalRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI instrument_THFTYPE_i) n2_THFTYPE_i) lObject_THFTYPE_i) of role axiom named ax_119 % A new axiom: (((domain_THFTYPE_IiiioI instrument_THFTYPE_i) n2_THFTYPE_i) lObject_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lAdditionFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_120 % A new axiom: (((domain_THFTYPE_IiiioI lAdditionFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiIiioI lYearFn_THFTYPE_IiiI) n1_THFTYPE_i) lInteger_THFTYPE_i) of role axiom named ax_121 % A new axiom: (((domain_THFTYPE_IIiiIiioI lYearFn_THFTYPE_IiiI) n1_THFTYPE_i) lInteger_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI range_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_122 % A new axiom: ((instance_THFTYPE_IIiioIioI range_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIIiioIiioIioI domain_THFTYPE_IIiioIiioI) lTernaryPredicate_THFTYPE_i) of role axiom named ax_123 % A new axiom: ((instance_THFTYPE_IIIiioIiioIioI domain_THFTYPE_IIiioIiioI) lTernaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiioIiioI domain_THFTYPE_IiiioI) n3_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_124 % A new axiom: (((domain_THFTYPE_IIiiioIiioI domain_THFTYPE_IiiioI) n3_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_125 % A new axiom: ((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI documentation_THFTYPE_i) n1_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_126 % A new axiom: (((domain_THFTYPE_IiiioI documentation_THFTYPE_i) n1_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI rangeSubclass_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_127 % A new axiom: ((instance_THFTYPE_IIiioIioI rangeSubclass_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) % FOF formula ((relatedInternalConcept_THFTYPE_IiIiiIoI lYear_THFTYPE_i) lYearFn_THFTYPE_IiiI) of role axiom named ax_128 % A new axiom: ((relatedInternalConcept_THFTYPE_IiIiiIoI lYear_THFTYPE_i) lYearFn_THFTYPE_IiiI) % FOF formula (((domain_THFTYPE_IiiioI equal_THFTYPE_i) n1_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_129 % A new axiom: (((domain_THFTYPE_IiiioI equal_THFTYPE_i) n1_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_130 % A new axiom: ((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lAsymmetricRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI disjoint_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_131 % A new axiom: ((instance_THFTYPE_IIiioIioI disjoint_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI temporalPart_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_132 % A new axiom: ((instance_THFTYPE_IIiioIioI temporalPart_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) of role axiom named ax_133 % A new axiom: ((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI subProcess_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_134 % A new axiom: ((instance_THFTYPE_IIiioIioI subProcess_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lTransitiveRelation_THFTYPE_i) of role axiom named ax_135 % A new axiom: ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lTransitiveRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI disjointRelation_THFTYPE_IiioI) lIrreflexiveRelation_THFTYPE_i) of role axiom named ax_136 % A new axiom: ((instance_THFTYPE_IIiioIioI disjointRelation_THFTYPE_IiioI) lIrreflexiveRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lMonthFn_THFTYPE_i) lTemporalRelation_THFTYPE_i) of role axiom named ax_137 % A new axiom: ((instance_THFTYPE_IiioI lMonthFn_THFTYPE_i) lTemporalRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lBinaryPredicate_THFTYPE_i) of role axiom named ax_138 % A new axiom: ((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lBinaryPredicate_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) of role axiom named ax_139 % A new axiom: ((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiiIioI lMeasureFn_THFTYPE_IiiiI) lBinaryFunction_THFTYPE_i) of role axiom named ax_140 % A new axiom: ((instance_THFTYPE_IIiiiIioI lMeasureFn_THFTYPE_IiiiI) lBinaryFunction_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lMultiplicationFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_141 % A new axiom: (((domain_THFTYPE_IiiioI lMultiplicationFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_142 % A new axiom: ((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_143 % A new axiom: ((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula (((domainSubclass_THFTYPE_IiiioI lMonthFn_THFTYPE_i) n1_THFTYPE_i) lMonth_THFTYPE_i) of role axiom named ax_144 % A new axiom: (((domainSubclass_THFTYPE_IiiioI lMonthFn_THFTYPE_i) n1_THFTYPE_i) lMonth_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI subclass_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_145 % A new axiom: ((instance_THFTYPE_IIiioIioI subclass_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI result_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) of role axiom named ax_146 % A new axiom: (((domain_THFTYPE_IiiioI result_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) of role axiom named ax_147 % A new axiom: ((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI subclass_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_148 % A new axiom: (((domain_THFTYPE_IIiioIiioI subclass_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) of role axiom named ax_149 % A new axiom: ((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lTemporalCompositionFn_THFTYPE_i) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_150 % A new axiom: (((domain_THFTYPE_IiiioI lTemporalCompositionFn_THFTYPE_i) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIIiioIIiioIoIiioI relatedInternalConcept_THFTYPE_IIiioIIiioIoI) n1_THFTYPE_i) lEntity_THFTYPE_i) of role axiom named ax_151 % A new axiom: (((domain_THFTYPE_IIIiioIIiioIoIiioI relatedInternalConcept_THFTYPE_IIiioIIiioIoI) n1_THFTYPE_i) lEntity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) of role axiom named ax_152 % A new axiom: ((instance_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI subclass_THFTYPE_IiioI) n1_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_153 % A new axiom: (((domain_THFTYPE_IIiioIiioI subclass_THFTYPE_IiioI) n1_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lSubtractionFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_154 % A new axiom: (((domain_THFTYPE_IiiioI lSubtractionFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI equal_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) of role axiom named ax_155 % A new axiom: ((instance_THFTYPE_IiioI equal_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) % FOF formula (((domainSubclass_THFTYPE_IiiioI lTemporalCompositionFn_THFTYPE_i) n2_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_156 % A new axiom: (((domainSubclass_THFTYPE_IiiioI lTemporalCompositionFn_THFTYPE_i) n2_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lYearFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) of role axiom named ax_157 % A new axiom: ((instance_THFTYPE_IIiiIioI lYearFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI orientation_THFTYPE_i) n2_THFTYPE_i) lObject_THFTYPE_i) of role axiom named ax_158 % A new axiom: (((domain_THFTYPE_IiiioI orientation_THFTYPE_i) n2_THFTYPE_i) lObject_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiioIiioI domainSubclass_THFTYPE_IiiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_159 % A new axiom: (((domain_THFTYPE_IIiiioIiioI domainSubclass_THFTYPE_IiiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((relatedInternalConcept_THFTYPE_IiioI lDay_THFTYPE_i) lDayDuration_THFTYPE_i) of role axiom named ax_160 % A new axiom: ((relatedInternalConcept_THFTYPE_IiioI lDay_THFTYPE_i) lDayDuration_THFTYPE_i) % FOF formula ((disjointRelation_THFTYPE_IiioI result_THFTYPE_i) instrument_THFTYPE_i) of role axiom named ax_161 % A new axiom: ((disjointRelation_THFTYPE_IiioI result_THFTYPE_i) instrument_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiiIioI lMeasureFn_THFTYPE_IiiiI) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_162 % A new axiom: ((instance_THFTYPE_IIiiiIioI lMeasureFn_THFTYPE_IiiiI) lTotalValuedRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI instrument_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) of role axiom named ax_163 % A new axiom: (((domain_THFTYPE_IiiioI instrument_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_164 % A new axiom: ((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_165 % A new axiom: ((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) of role axiom named ax_166 % A new axiom: ((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI instance_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_167 % A new axiom: (((domain_THFTYPE_IIiioIiioI instance_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lSubtractionFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_168 % A new axiom: (((domain_THFTYPE_IiiioI lSubtractionFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI duration_THFTYPE_IiioI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_169 % A new axiom: (((domain_THFTYPE_IIiioIiioI duration_THFTYPE_IiioI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI subrelation_THFTYPE_IiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) of role axiom named ax_170 % A new axiom: (((domain_THFTYPE_IIiioIiioI subrelation_THFTYPE_IiioI) n1_THFTYPE_i) lRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_171 % A new axiom: ((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiioIioI domainSubclass_THFTYPE_IiiioI) lTernaryPredicate_THFTYPE_i) of role axiom named ax_172 % A new axiom: ((instance_THFTYPE_IIiiioIioI domainSubclass_THFTYPE_IiiioI) lTernaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI meetsTemporally_THFTYPE_IiioI) n2_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_173 % A new axiom: (((domain_THFTYPE_IIiioIiioI meetsTemporally_THFTYPE_IiioI) n2_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lessThan_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_174 % A new axiom: (((domain_THFTYPE_IiiioI lessThan_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiooIioI holdsDuring_THFTYPE_IiooI) lAsymmetricRelation_THFTYPE_i) of role axiom named ax_175 % A new axiom: ((instance_THFTYPE_IIiooIioI holdsDuring_THFTYPE_IiooI) lAsymmetricRelation_THFTYPE_i) % FOF formula (((domainSubclass_THFTYPE_IIiioIiioI rangeSubclass_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_176 % A new axiom: (((domainSubclass_THFTYPE_IIiioIiioI rangeSubclass_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lTransitiveRelation_THFTYPE_i) of role axiom named ax_177 % A new axiom: ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lTransitiveRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiioIiioI disjoint_THFTYPE_IiioI) n1_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_178 % A new axiom: (((domain_THFTYPE_IIiioIiioI disjoint_THFTYPE_IiioI) n1_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula ((subrelation_THFTYPE_IiioI instrument_THFTYPE_i) patient_THFTYPE_i) of role axiom named ax_179 % A new axiom: ((subrelation_THFTYPE_IiioI instrument_THFTYPE_i) patient_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiIiioI lEndFn_THFTYPE_IiiI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) of role axiom named ax_180 % A new axiom: (((domain_THFTYPE_IIiiIiioI lEndFn_THFTYPE_IiiI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI disjointRelation_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_181 % A new axiom: ((instance_THFTYPE_IIiioIioI disjointRelation_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI orientation_THFTYPE_i) n1_THFTYPE_i) lObject_THFTYPE_i) of role axiom named ax_182 % A new axiom: (((domain_THFTYPE_IiiioI orientation_THFTYPE_i) n1_THFTYPE_i) lObject_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) of role axiom named ax_183 % A new axiom: ((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) of role axiom named ax_184 % A new axiom: ((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI attribute_THFTYPE_i) n1_THFTYPE_i) lObject_THFTYPE_i) of role axiom named ax_185 % A new axiom: (((domain_THFTYPE_IiiioI attribute_THFTYPE_i) n1_THFTYPE_i) lObject_THFTYPE_i) % FOF formula (((domain_THFTYPE_IiiioI lAdditionFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) of role axiom named ax_186 % A new axiom: (((domain_THFTYPE_IiiioI lAdditionFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI located_THFTYPE_IiioI) lTransitiveRelation_THFTYPE_i) of role axiom named ax_187 % A new axiom: ((instance_THFTYPE_IIiioIioI located_THFTYPE_IiioI) lTransitiveRelation_THFTYPE_i) % FOF formula (((domain_THFTYPE_IIiiioIiioI domainSubclass_THFTYPE_IiiioI) n3_THFTYPE_i) lSetOrClass_THFTYPE_i) of role axiom named ax_188 % A new axiom: (((domain_THFTYPE_IIiiioIiioI domainSubclass_THFTYPE_IiiioI) n3_THFTYPE_i) lSetOrClass_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) of role axiom named ax_189 % A new axiom: ((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i) % FOF formula ((instance_THFTYPE_IIiioIioI rangeSubclass_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) of role axiom named ax_190 % A new axiom: ((instance_THFTYPE_IIiioIioI rangeSubclass_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i) % FOF formula ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) of role conjecture named con % Conjecture to prove = ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)):Prop % Parameter num_DUMMY:num. % We need to prove ['((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i))'] % Parameter num:Type. % Parameter fofType:Type. % Parameter agent_THFTYPE_i:fofType. % Parameter attribute_THFTYPE_i:fofType. % Parameter disjointRelation_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter disjoint_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter documentation_THFTYPE_i:fofType. % Parameter domainSubclass_THFTYPE_IIiioIiioI:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Parameter domainSubclass_THFTYPE_IiiioI:(fofType->(fofType->(fofType->Prop))). % Parameter domain_THFTYPE_IIIiioIIiioIoIiioI:(((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop))->(fofType->(fofType->Prop))). % Parameter domain_THFTYPE_IIiiIiioI:((fofType->fofType)->(fofType->(fofType->Prop))). % Parameter domain_THFTYPE_IIiiioIiioI:((fofType->(fofType->(fofType->Prop)))->(fofType->(fofType->Prop))). % Parameter domain_THFTYPE_IIiioIiioI:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Parameter domain_THFTYPE_IiiioI:(fofType->(fofType->(fofType->Prop))). % Parameter duration_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter equal_THFTYPE_i:fofType. % Parameter greaterThan_THFTYPE_i:fofType. % Parameter holdsDuring_THFTYPE_IiooI:(fofType->(Prop->Prop)). % Parameter instance_THFTYPE_IIIiioIiioIioI:(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->(fofType->Prop)). % Parameter instance_THFTYPE_IIiiIioI:((fofType->fofType)->(fofType->Prop)). % Parameter instance_THFTYPE_IIiiiIioI:((fofType->(fofType->fofType))->(fofType->Prop)). % Parameter instance_THFTYPE_IIiiioIioI:((fofType->(fofType->(fofType->Prop)))->(fofType->Prop)). % Parameter instance_THFTYPE_IIiioIioI:((fofType->(fofType->Prop))->(fofType->Prop)). % Parameter instance_THFTYPE_IIiooIioI:((fofType->(Prop->Prop))->(fofType->Prop)). % Parameter instance_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter instrument_THFTYPE_i:fofType. % Parameter lAdditionFn_THFTYPE_i:fofType. % Parameter lAsymmetricRelation_THFTYPE_i:fofType. % Parameter lBeginFn_THFTYPE_IiiI:(fofType->fofType). % Parameter lBill_THFTYPE_i:fofType. % Parameter lBinaryFunction_THFTYPE_i:fofType. % Parameter lBinaryPredicate_THFTYPE_i:fofType. % Parameter lCardinalityFn_THFTYPE_IiiI:(fofType->fofType). % Parameter lDayDuration_THFTYPE_i:fofType. % Parameter lDay_THFTYPE_i:fofType. % Parameter lEndFn_THFTYPE_IiiI:(fofType->fofType). % Parameter lEntity_THFTYPE_i:fofType. % Parameter lInheritableRelation_THFTYPE_i:fofType. % Parameter lInteger_THFTYPE_i:fofType. % Parameter lIrreflexiveRelation_THFTYPE_i:fofType. % Parameter lMary_THFTYPE_i:fofType. % Parameter lMeasureFn_THFTYPE_IiiiI:(fofType->(fofType->fofType)). % Parameter lMonthFn_THFTYPE_i:fofType. % Parameter lMonth_THFTYPE_i:fofType. % Parameter lMultiplicationFn_THFTYPE_i:fofType. % Parameter lObject_THFTYPE_i:fofType. % Parameter lProcess_THFTYPE_i:fofType. % Parameter lQuantity_THFTYPE_i:fofType. % Parameter lRelationExtendedToQuantities_THFTYPE_i:fofType. % Parameter lRelation_THFTYPE_i:fofType. % Parameter lSetOrClass_THFTYPE_i:fofType. % Parameter lSubtractionFn_THFTYPE_i:fofType. % Parameter lSue_THFTYPE_i:fofType. % Parameter lTemporalCompositionFn_THFTYPE_IiiiI:(fofType->(fofType->fofType)). % Parameter lTemporalCompositionFn_THFTYPE_i:fofType. % Parameter lTemporalRelation_THFTYPE_i:fofType. % Parameter lTernaryPredicate_THFTYPE_i:fofType. % Parameter lTimeInterval_THFTYPE_i:fofType. % Parameter lTotalValuedRelation_THFTYPE_i:fofType. % Parameter lTransitiveRelation_THFTYPE_i:fofType. % Parameter lUnaryFunction_THFTYPE_i:fofType. % Parameter lWhenFn_THFTYPE_IiiI:(fofType->fofType). % Parameter lWhenFn_THFTYPE_i:fofType. % Parameter lYearFn_THFTYPE_IiiI:(fofType->fofType). % Parameter lYearFn_THFTYPE_i:fofType. % Parameter lYear_THFTYPE_i:fofType. % Parameter lessThan_THFTYPE_i:fofType. % Parameter likes_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter located_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter meetsTemporally_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter minus_THFTYPE_IiiiI:(fofType->(fofType->fofType)). % Parameter n12_THFTYPE_i:fofType. % Parameter n1_THFTYPE_i:fofType. % Parameter n2009_THFTYPE_i:fofType. % Parameter n2_THFTYPE_i:fofType. % Parameter n3_THFTYPE_i:fofType. % Parameter orientation_THFTYPE_i:fofType. % Parameter part_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter patient_THFTYPE_i:fofType. % Parameter rangeSubclass_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter range_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter relatedInternalConcept_THFTYPE_IIiioIIiioIoI:((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop)). % Parameter relatedInternalConcept_THFTYPE_IiIiiIoI:(fofType->((fofType->fofType)->Prop)). % Parameter relatedInternalConcept_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter result_THFTYPE_i:fofType. % Parameter subProcess_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter subclass_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter subrelation_THFTYPE_IIioIIioIoI:((fofType->Prop)->((fofType->Prop)->Prop)). % Parameter subrelation_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter temporalPart_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Axiom ax:(forall (REL2:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and ((rangeSubclass_THFTYPE_IiioI REL1) CLASS1)) ((rangeSubclass_THFTYPE_IiioI REL2) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))). % Axiom ax_001:((subclass_THFTYPE_IiioI lInheritableRelation_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_002:(forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((subclass_THFTYPE_IiioI X) Y)) ((instance_THFTYPE_IiioI Z) X))->((instance_THFTYPE_IiioI Z) Y))). % Axiom ax_003:(forall (X:fofType) (Y:fofType), (((subclass_THFTYPE_IiioI X) Y)->((and ((instance_THFTYPE_IiioI X) lSetOrClass_THFTYPE_i)) ((instance_THFTYPE_IiioI Y) lSetOrClass_THFTYPE_i)))). % Axiom ax_004:(forall (THING:fofType), ((instance_THFTYPE_IiioI THING) lEntity_THFTYPE_i)). % Axiom ax_005:(forall (X:fofType), ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) (((likes_THFTYPE_IiioI lMary_THFTYPE_i) X)->((likes_THFTYPE_IiioI lSue_THFTYPE_i) X)))). % Axiom ax_006:(forall (X:fofType), ((holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i)) (((likes_THFTYPE_IiioI lMary_THFTYPE_i) X)->((likes_THFTYPE_IiioI lSue_THFTYPE_i) X)))). % Axiom ax_007:(forall (NUMBER:fofType) (MONTH:fofType), (((and ((instance_THFTYPE_IiioI MONTH) lMonth_THFTYPE_i)) ((duration_THFTYPE_IiioI MONTH) ((lMeasureFn_THFTYPE_IiiiI NUMBER) lDayDuration_THFTYPE_i)))->(((eq fofType) (lCardinalityFn_THFTYPE_IiiI ((lTemporalCompositionFn_THFTYPE_IiiiI MONTH) lDay_THFTYPE_i))) NUMBER))). % Axiom ax_008:(forall (OBJ1:fofType) (OBJ2:fofType), (((located_THFTYPE_IiioI OBJ1) OBJ2)->(forall (SUB:fofType), (((part_THFTYPE_IiioI SUB) OBJ1)->((located_THFTYPE_IiioI SUB) OBJ2))))). % Axiom ax_009:((subclass_THFTYPE_IiioI lAsymmetricRelation_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i). % Axiom ax_010:((subclass_THFTYPE_IiioI lTotalValuedRelation_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_011:(forall (NUMBER:fofType) (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and (((domainSubclass_THFTYPE_IiiioI REL) NUMBER) CLASS1)) (((domainSubclass_THFTYPE_IiiioI REL) NUMBER) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))). % Axiom ax_012:(forall (DAY:fofType), (((instance_THFTYPE_IiioI DAY) lDay_THFTYPE_i)->((duration_THFTYPE_IiioI DAY) ((lMeasureFn_THFTYPE_IiiiI n1_THFTYPE_i) lDayDuration_THFTYPE_i)))). % Axiom ax_013:(forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and (((domainSubclass_THFTYPE_IiiioI REL1) NUMBER) CLASS1)) (((domainSubclass_THFTYPE_IiiioI REL2) NUMBER) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))). % Axiom ax_014:((subclass_THFTYPE_IiioI lTemporalRelation_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_015:((subclass_THFTYPE_IiioI lYear_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_016:(forall (NUMBER:fofType) (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and (((domain_THFTYPE_IiiioI REL) NUMBER) CLASS1)) (((domain_THFTYPE_IiiioI REL) NUMBER) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))). % Axiom ax_017:(forall (REL:(fofType->(fofType->Prop))), ((iff ((instance_THFTYPE_IIiioIioI REL) lTransitiveRelation_THFTYPE_i)) (forall (INST1:fofType) (INST2:fofType) (INST3:fofType), (((and ((REL INST1) INST2)) ((REL INST2) INST3))->((REL INST1) INST3))))). % Axiom ax_018:((rangeSubclass_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_019:(forall (REL2:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and ((range_THFTYPE_IiioI REL1) CLASS1)) ((range_THFTYPE_IiioI REL2) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))). % Axiom ax_020:((subclass_THFTYPE_IiioI lRelationExtendedToQuantities_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_021:((subclass_THFTYPE_IiioI lMonth_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_022:(forall (TIME:fofType) (SITUATION:Prop), (((holdsDuring_THFTYPE_IiooI TIME) (not SITUATION))->(not ((holdsDuring_THFTYPE_IiooI TIME) SITUATION)))). % Axiom ax_023:(forall (T:fofType), ((holdsDuring_THFTYPE_IiooI T) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))). % Axiom ax_024:(forall (T:fofType), ((holdsDuring_THFTYPE_IiooI T) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))). % Axiom ax_025:((range_THFTYPE_IiioI lWhenFn_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_026:(forall (INTERVAL1:fofType) (INTERVAL2:fofType), ((iff ((meetsTemporally_THFTYPE_IiioI INTERVAL1) INTERVAL2)) (((eq fofType) (lEndFn_THFTYPE_IiiI INTERVAL1)) (lBeginFn_THFTYPE_IiiI INTERVAL2)))). % Axiom ax_027:(forall (SITUATION:Prop) (TIME2:fofType) (TIME1:fofType), (((and ((holdsDuring_THFTYPE_IiooI TIME1) SITUATION)) ((temporalPart_THFTYPE_IiioI TIME2) TIME1))->((holdsDuring_THFTYPE_IiooI TIME2) SITUATION))). % Axiom ax_028:((range_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_029:((ex fofType) (fun (THING:fofType)=> ((instance_THFTYPE_IiioI THING) lEntity_THFTYPE_i))). % Axiom ax_030:(forall (REL:(fofType->(fofType->Prop))), ((iff ((instance_THFTYPE_IIiioIioI REL) lIrreflexiveRelation_THFTYPE_i)) (forall (INST:fofType), (not ((REL INST) INST))))). % Axiom ax_031:((subclass_THFTYPE_IiioI lBinaryFunction_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_032:(forall (NUMBER:fofType) (PRED1:fofType) (CLASS1:fofType) (PRED2:fofType), (((and ((subrelation_THFTYPE_IiioI PRED1) PRED2)) (((domain_THFTYPE_IiiioI PRED2) NUMBER) CLASS1))->(((domain_THFTYPE_IiiioI PRED1) NUMBER) CLASS1))). % Axiom ax_033:((subclass_THFTYPE_IiioI lTotalValuedRelation_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_034:((subclass_THFTYPE_IiioI lTernaryPredicate_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_035:((subclass_THFTYPE_IiioI lRelationExtendedToQuantities_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_036:(forall (YEAR:fofType), (((instance_THFTYPE_IiioI YEAR) lYear_THFTYPE_i)->(((eq fofType) (lCardinalityFn_THFTYPE_IiiI ((lTemporalCompositionFn_THFTYPE_IiiiI YEAR) lMonth_THFTYPE_i))) n12_THFTYPE_i))). % Axiom ax_037:(forall (CLASS1:fofType) (CLASS2:fofType), ((((eq fofType) CLASS1) CLASS2)->(forall (THING:fofType), ((iff ((instance_THFTYPE_IiioI THING) CLASS1)) ((instance_THFTYPE_IiioI THING) CLASS2))))). % Axiom ax_038:(forall (REL2:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) ((rangeSubclass_THFTYPE_IiioI REL2) CLASS1))->((rangeSubclass_THFTYPE_IiioI REL1) CLASS1))). % Axiom ax_039:(forall (YEAR2:fofType) (YEAR1:fofType), (((and ((and ((instance_THFTYPE_IiioI YEAR1) lYear_THFTYPE_i)) ((instance_THFTYPE_IiioI YEAR2) lYear_THFTYPE_i))) (((eq fofType) ((minus_THFTYPE_IiiiI YEAR2) YEAR1)) n1_THFTYPE_i))->((meetsTemporally_THFTYPE_IiioI YEAR1) YEAR2))). % Axiom ax_040:(forall (REL2:(fofType->Prop)) (ROW:fofType) (REL1:(fofType->Prop)), (((and ((subrelation_THFTYPE_IIioIIioIoI REL1) REL2)) (REL1 ROW))->(REL2 ROW))). % Axiom ax_041:(forall (THING2:fofType) (THING1:fofType), ((((eq fofType) THING1) THING2)->(forall (CLASS:fofType), ((iff ((instance_THFTYPE_IiioI THING1) CLASS)) ((instance_THFTYPE_IiioI THING2) CLASS))))). % Axiom ax_042:(forall (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and ((range_THFTYPE_IiioI REL) CLASS1)) ((range_THFTYPE_IiioI REL) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))). % Axiom ax_043:(forall (CLASS1:fofType) (CLASS2:fofType), ((iff ((disjoint_THFTYPE_IiioI CLASS1) CLASS2)) (forall (INST:fofType), (not ((and ((instance_THFTYPE_IiioI INST) CLASS1)) ((instance_THFTYPE_IiioI INST) CLASS2)))))). % Axiom ax_044:(forall (SUBPROC:fofType) (PROC:fofType), (((subProcess_THFTYPE_IiioI SUBPROC) PROC)->((temporalPart_THFTYPE_IiioI (lWhenFn_THFTYPE_IiiI SUBPROC)) (lWhenFn_THFTYPE_IiiI PROC)))). % Axiom ax_045:((rangeSubclass_THFTYPE_IiioI lMonthFn_THFTYPE_i) lMonth_THFTYPE_i). % Axiom ax_046:(forall (INTERVAL1:fofType) (INTERVAL2:fofType), (((and (((eq fofType) (lBeginFn_THFTYPE_IiiI INTERVAL1)) (lBeginFn_THFTYPE_IiiI INTERVAL2))) (((eq fofType) (lEndFn_THFTYPE_IiiI INTERVAL1)) (lEndFn_THFTYPE_IiiI INTERVAL2)))->(((eq fofType) INTERVAL1) INTERVAL2))). % Axiom ax_047:(forall (REL2:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) ((range_THFTYPE_IiioI REL2) CLASS1))->((range_THFTYPE_IiioI REL1) CLASS1))). % Axiom ax_048:((subclass_THFTYPE_IiioI lTemporalRelation_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_049:(forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (REL1:fofType), (((and ((subrelation_THFTYPE_IiioI REL1) REL2)) (((domainSubclass_THFTYPE_IiiioI REL2) NUMBER) CLASS1))->(((domainSubclass_THFTYPE_IiiioI REL1) NUMBER) CLASS1))). % Axiom ax_050:(forall (SUBPROC:fofType) (PROC:fofType), (((subProcess_THFTYPE_IiioI SUBPROC) PROC)->(forall (REGION:fofType), (((located_THFTYPE_IiioI PROC) REGION)->((located_THFTYPE_IiioI SUBPROC) REGION))))). % Axiom ax_051:((range_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_052:((range_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_053:(forall (OBJ:fofType) (PROCESS:fofType), (((located_THFTYPE_IiioI PROCESS) OBJ)->(forall (SUB:fofType), (((subProcess_THFTYPE_IiioI SUB) PROCESS)->((located_THFTYPE_IiioI SUB) OBJ))))). % Axiom ax_054:((subclass_THFTYPE_IiioI lUnaryFunction_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_055:((subclass_THFTYPE_IiioI lDay_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_056:(forall (REL2:fofType) (NUMBER:fofType) (CLASS1:fofType) (CLASS2:fofType) (REL1:fofType), (((and ((and (((domain_THFTYPE_IiiioI REL1) NUMBER) CLASS1)) (((domain_THFTYPE_IiiioI REL2) NUMBER) CLASS2))) ((disjoint_THFTYPE_IiioI CLASS1) CLASS2))->((disjointRelation_THFTYPE_IiioI REL1) REL2))). % Axiom ax_057:((rangeSubclass_THFTYPE_IiioI lYearFn_THFTYPE_i) lYear_THFTYPE_i). % Axiom ax_058:(forall (CLASS:fofType) (PRED1:fofType) (PRED2:fofType), (((and ((and ((subrelation_THFTYPE_IiioI PRED1) PRED2)) ((instance_THFTYPE_IiioI PRED2) CLASS))) ((subclass_THFTYPE_IiioI CLASS) lInheritableRelation_THFTYPE_i))->((instance_THFTYPE_IiioI PRED1) CLASS))). % Axiom ax_059:(forall (CLASS1:fofType) (REL:fofType) (CLASS2:fofType), (((and ((rangeSubclass_THFTYPE_IiioI REL) CLASS1)) ((rangeSubclass_THFTYPE_IiioI REL) CLASS2))->((or ((subclass_THFTYPE_IiioI CLASS1) CLASS2)) ((subclass_THFTYPE_IiioI CLASS2) CLASS1)))). % Axiom ax_060:((subclass_THFTYPE_IiioI lBinaryPredicate_THFTYPE_i) lInheritableRelation_THFTYPE_i). % Axiom ax_061:((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lTemporalRelation_THFTYPE_i). % Axiom ax_062:((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lTotalValuedRelation_THFTYPE_i). % Axiom ax_063:((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i). % Axiom ax_064:((instance_THFTYPE_IIiioIioI range_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i). % Axiom ax_065:((instance_THFTYPE_IiioI lMonthFn_THFTYPE_i) lBinaryFunction_THFTYPE_i). % Axiom ax_066:(((domain_THFTYPE_IIiioIiioI disjointRelation_THFTYPE_IiioI) n2_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_067:((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i). % Axiom ax_068:(((domainSubclass_THFTYPE_IiiioI lMonthFn_THFTYPE_i) n2_THFTYPE_i) lYear_THFTYPE_i). % Axiom ax_069:(((domain_THFTYPE_IIiioIiioI subProcess_THFTYPE_IiioI) n1_THFTYPE_i) lProcess_THFTYPE_i). % Axiom ax_070:((relatedInternalConcept_THFTYPE_IiioI lMonth_THFTYPE_i) lMonthFn_THFTYPE_i). % Axiom ax_071:((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lBinaryPredicate_THFTYPE_i). % Axiom ax_072:(((domain_THFTYPE_IIiioIiioI meetsTemporally_THFTYPE_IiioI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_073:(((domain_THFTYPE_IiiioI equal_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_074:(((domain_THFTYPE_IIiioIiioI disjoint_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_075:((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i). % Axiom ax_076:(((domain_THFTYPE_IIiioIiioI subProcess_THFTYPE_IiioI) n2_THFTYPE_i) lProcess_THFTYPE_i). % Axiom ax_077:(((domain_THFTYPE_IiiioI agent_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i). % Axiom ax_078:((instance_THFTYPE_IIiioIioI relatedInternalConcept_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_079:((instance_THFTYPE_IiioI equal_THFTYPE_i) lBinaryPredicate_THFTYPE_i). % Axiom ax_080:((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i). % Axiom ax_081:((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i). % Axiom ax_082:(((domain_THFTYPE_IIiioIiioI disjointRelation_THFTYPE_IiioI) n1_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_083:(((domain_THFTYPE_IiiioI greaterThan_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_084:(((domain_THFTYPE_IIiioIiioI range_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_085:(((domain_THFTYPE_IIiioIiioI subrelation_THFTYPE_IiioI) n2_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_086:((instance_THFTYPE_IIiiIioI lYearFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i). % Axiom ax_087:((instance_THFTYPE_IiioI attribute_THFTYPE_i) lAsymmetricRelation_THFTYPE_i). % Axiom ax_088:((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i). % Axiom ax_089:((subrelation_THFTYPE_IiioI result_THFTYPE_i) patient_THFTYPE_i). % Axiom ax_090:(((domain_THFTYPE_IiiioI lMultiplicationFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_091:(((domain_THFTYPE_IiiioI patient_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i). % Axiom ax_092:((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i). % Axiom ax_093:((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i). % Axiom ax_094:((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i). % Axiom ax_095:(((domain_THFTYPE_IiiioI patient_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_096:((instance_THFTYPE_IiioI documentation_THFTYPE_i) lTernaryPredicate_THFTYPE_i). % Axiom ax_097:((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_098:((instance_THFTYPE_IiioI orientation_THFTYPE_i) lTernaryPredicate_THFTYPE_i). % Axiom ax_099:(((domain_THFTYPE_IIiiioIiioI domain_THFTYPE_IiiioI) n1_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_100:((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i). % Axiom ax_101:(((domain_THFTYPE_IiiioI result_THFTYPE_i) n2_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_102:((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i). % Axiom ax_103:((instance_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lTemporalRelation_THFTYPE_i). % Axiom ax_104:(((domain_THFTYPE_IIiioIiioI relatedInternalConcept_THFTYPE_IiioI) n2_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_105:((instance_THFTYPE_IIiioIioI subrelation_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_106:((relatedInternalConcept_THFTYPE_IIiioIIiioIoI disjointRelation_THFTYPE_IiioI) disjoint_THFTYPE_IiioI). % Axiom ax_107:(((domain_THFTYPE_IiiioI greaterThan_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_108:(((domain_THFTYPE_IIiioIiioI part_THFTYPE_IiioI) n1_THFTYPE_i) lObject_THFTYPE_i). % Axiom ax_109:((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i). % Axiom ax_110:(((domain_THFTYPE_IIiiIiioI lBeginFn_THFTYPE_IiiI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_111:((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i). % Axiom ax_112:((instance_THFTYPE_IIiioIioI instance_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_113:((instance_THFTYPE_IiioI attribute_THFTYPE_i) lIrreflexiveRelation_THFTYPE_i). % Axiom ax_114:(((domain_THFTYPE_IiiioI lessThan_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_115:(((domain_THFTYPE_IIiioIiioI instance_THFTYPE_IiioI) n1_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_116:((instance_THFTYPE_IIiooIioI holdsDuring_THFTYPE_IiooI) lBinaryPredicate_THFTYPE_i). % Axiom ax_117:(((domain_THFTYPE_IIiioIiioI part_THFTYPE_IiioI) n2_THFTYPE_i) lObject_THFTYPE_i). % Axiom ax_118:((instance_THFTYPE_IIiioIioI temporalPart_THFTYPE_IiioI) lTemporalRelation_THFTYPE_i). % Axiom ax_119:(((domain_THFTYPE_IiiioI instrument_THFTYPE_i) n2_THFTYPE_i) lObject_THFTYPE_i). % Axiom ax_120:(((domain_THFTYPE_IiiioI lAdditionFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_121:(((domain_THFTYPE_IIiiIiioI lYearFn_THFTYPE_IiiI) n1_THFTYPE_i) lInteger_THFTYPE_i). % Axiom ax_122:((instance_THFTYPE_IIiioIioI range_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_123:((instance_THFTYPE_IIIiioIiioIioI domain_THFTYPE_IIiioIiioI) lTernaryPredicate_THFTYPE_i). % Axiom ax_124:(((domain_THFTYPE_IIiiioIiioI domain_THFTYPE_IiiioI) n3_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_125:((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i). % Axiom ax_126:(((domain_THFTYPE_IiiioI documentation_THFTYPE_i) n1_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_127:((instance_THFTYPE_IIiioIioI rangeSubclass_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i). % Axiom ax_128:((relatedInternalConcept_THFTYPE_IiIiiIoI lYear_THFTYPE_i) lYearFn_THFTYPE_IiiI). % Axiom ax_129:(((domain_THFTYPE_IiiioI equal_THFTYPE_i) n1_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_130:((instance_THFTYPE_IIiiIioI lCardinalityFn_THFTYPE_IiiI) lAsymmetricRelation_THFTYPE_i). % Axiom ax_131:((instance_THFTYPE_IIiioIioI disjoint_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_132:((instance_THFTYPE_IIiioIioI temporalPart_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_133:((instance_THFTYPE_IiioI lMultiplicationFn_THFTYPE_i) lBinaryFunction_THFTYPE_i). % Axiom ax_134:((instance_THFTYPE_IIiioIioI subProcess_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_135:((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lTransitiveRelation_THFTYPE_i). % Axiom ax_136:((instance_THFTYPE_IIiioIioI disjointRelation_THFTYPE_IiioI) lIrreflexiveRelation_THFTYPE_i). % Axiom ax_137:((instance_THFTYPE_IiioI lMonthFn_THFTYPE_i) lTemporalRelation_THFTYPE_i). % Axiom ax_138:((instance_THFTYPE_IiioI greaterThan_THFTYPE_i) lBinaryPredicate_THFTYPE_i). % Axiom ax_139:((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i). % Axiom ax_140:((instance_THFTYPE_IIiiiIioI lMeasureFn_THFTYPE_IiiiI) lBinaryFunction_THFTYPE_i). % Axiom ax_141:(((domain_THFTYPE_IiiioI lMultiplicationFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_142:((instance_THFTYPE_IIiiIioI lBeginFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i). % Axiom ax_143:((instance_THFTYPE_IIiioIioI meetsTemporally_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_144:(((domainSubclass_THFTYPE_IiiioI lMonthFn_THFTYPE_i) n1_THFTYPE_i) lMonth_THFTYPE_i). % Axiom ax_145:((instance_THFTYPE_IIiioIioI subclass_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_146:(((domain_THFTYPE_IiiioI result_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i). % Axiom ax_147:((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i). % Axiom ax_148:(((domain_THFTYPE_IIiioIiioI subclass_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_149:((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lTemporalRelation_THFTYPE_i). % Axiom ax_150:(((domain_THFTYPE_IiiioI lTemporalCompositionFn_THFTYPE_i) n1_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_151:(((domain_THFTYPE_IIIiioIIiioIoIiioI relatedInternalConcept_THFTYPE_IIiioIIiioIoI) n1_THFTYPE_i) lEntity_THFTYPE_i). % Axiom ax_152:((instance_THFTYPE_IiioI lTemporalCompositionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i). % Axiom ax_153:(((domain_THFTYPE_IIiioIiioI subclass_THFTYPE_IiioI) n1_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_154:(((domain_THFTYPE_IiiioI lSubtractionFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_155:((instance_THFTYPE_IiioI equal_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i). % Axiom ax_156:(((domainSubclass_THFTYPE_IiiioI lTemporalCompositionFn_THFTYPE_i) n2_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_157:((instance_THFTYPE_IIiiIioI lYearFn_THFTYPE_IiiI) lUnaryFunction_THFTYPE_i). % Axiom ax_158:(((domain_THFTYPE_IiiioI orientation_THFTYPE_i) n2_THFTYPE_i) lObject_THFTYPE_i). % Axiom ax_159:(((domain_THFTYPE_IIiiioIiioI domainSubclass_THFTYPE_IiiioI) n1_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_160:((relatedInternalConcept_THFTYPE_IiioI lDay_THFTYPE_i) lDayDuration_THFTYPE_i). % Axiom ax_161:((disjointRelation_THFTYPE_IiioI result_THFTYPE_i) instrument_THFTYPE_i). % Axiom ax_162:((instance_THFTYPE_IIiiiIioI lMeasureFn_THFTYPE_IiiiI) lTotalValuedRelation_THFTYPE_i). % Axiom ax_163:(((domain_THFTYPE_IiiioI instrument_THFTYPE_i) n1_THFTYPE_i) lProcess_THFTYPE_i). % Axiom ax_164:((instance_THFTYPE_IIiioIioI duration_THFTYPE_IiioI) lAsymmetricRelation_THFTYPE_i). % Axiom ax_165:((instance_THFTYPE_IiioI lAdditionFn_THFTYPE_i) lTotalValuedRelation_THFTYPE_i). % Axiom ax_166:((instance_THFTYPE_IiioI lSubtractionFn_THFTYPE_i) lBinaryFunction_THFTYPE_i). % Axiom ax_167:(((domain_THFTYPE_IIiioIiioI instance_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_168:(((domain_THFTYPE_IiiioI lSubtractionFn_THFTYPE_i) n1_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_169:(((domain_THFTYPE_IIiioIiioI duration_THFTYPE_IiioI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_170:(((domain_THFTYPE_IIiioIiioI subrelation_THFTYPE_IiioI) n1_THFTYPE_i) lRelation_THFTYPE_i). % Axiom ax_171:((instance_THFTYPE_IIiiIioI lEndFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i). % Axiom ax_172:((instance_THFTYPE_IIiiioIioI domainSubclass_THFTYPE_IiiioI) lTernaryPredicate_THFTYPE_i). % Axiom ax_173:(((domain_THFTYPE_IIiioIiioI meetsTemporally_THFTYPE_IiioI) n2_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_174:(((domain_THFTYPE_IiiioI lessThan_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_175:((instance_THFTYPE_IIiooIioI holdsDuring_THFTYPE_IiooI) lAsymmetricRelation_THFTYPE_i). % Axiom ax_176:(((domainSubclass_THFTYPE_IIiioIiioI rangeSubclass_THFTYPE_IiioI) n2_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_177:((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lTransitiveRelation_THFTYPE_i). % Axiom ax_178:(((domain_THFTYPE_IIiioIiioI disjoint_THFTYPE_IiioI) n1_THFTYPE_i) lSetOrClass_THFTYPE_i). % Axiom ax_179:((subrelation_THFTYPE_IiioI instrument_THFTYPE_i) patient_THFTYPE_i). % Axiom ax_180:(((domain_THFTYPE_IIiiIiioI lEndFn_THFTYPE_IiiI) n1_THFTYPE_i) lTimeInterval_THFTYPE_i). % Axiom ax_181:((instance_THFTYPE_IIiioIioI disjointRelation_THFTYPE_IiioI) lBinaryPredicate_THFTYPE_i). % Axiom ax_182:(((domain_THFTYPE_IiiioI orientation_THFTYPE_i) n1_THFTYPE_i) lObject_THFTYPE_i). % Axiom ax_183:((instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI) lTotalValuedRelation_THFTYPE_i). % Axiom ax_184:((instance_THFTYPE_IiioI lessThan_THFTYPE_i) lRelationExtendedToQuantities_THFTYPE_i). % Axiom ax_185:(((domain_THFTYPE_IiiioI attribute_THFTYPE_i) n1_THFTYPE_i) lObject_THFTYPE_i). % Axiom ax_186:(((domain_THFTYPE_IiiioI lAdditionFn_THFTYPE_i) n2_THFTYPE_i) lQuantity_THFTYPE_i). % Axiom ax_187:((instance_THFTYPE_IIiioIioI located_THFTYPE_IiioI) lTransitiveRelation_THFTYPE_i). % Axiom ax_188:(((domain_THFTYPE_IIiiioIiioI domainSubclass_ % EOF %------------------------------------------------------------------------------