%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : CSR125^2 : TPTP v9.2.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n028.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:13:01 AM UTC 2026 % Result : Theorem 1.53s 1.72s % Output : Proof 1.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR125^2 : TPTP v9.2.1. Released v4.1.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n028.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon Jun 1 21:57:20 EDT 2026 % 0.16/0.34 % CPUTime : % 0.31/0.54 %----Proving TH0 % 1.53/1.72 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 1.53/1.72 % SZS status Theorem % 1.53/1.72 % SZS output start Proof % 1.53/1.72 ( % 1.53/1.72 (declare-sort $$unsorted 0) % 1.53/1.72 (declare-const tptp.subrelation_THFTYPE_IIoooIIiioIoI (-> (-> Bool Bool Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 1.53/1.72 (declare-const tptp.domainSubclass_THFTYPE_IIiioIiioI (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIIioIiioIioI (-> (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIIioIiioIiioI (-> (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domainSubclass_THFTYPE_IIiiiIiioI (-> (-> $$unsorted $$unsorted $$unsorted) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIiiiIiioI (-> (-> $$unsorted $$unsorted $$unsorted) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.relatedInternalConcept_THFTYPE_IiIiiIoI (-> $$unsorted (-> $$unsorted $$unsorted) Bool)) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIIiioIiioIioI (-> (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lInteger_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lTemporalCompositionFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lText_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lContentBearingObject_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lIntentionalProcess_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lProcess_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lYear_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIiioIioI (-> (-> $$unsorted $$unsorted Bool) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lTemporalRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.truth_THFTYPE_IoooI (-> Bool Bool Bool)) % 1.53/1.72 (declare-const tptp.duration_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lTransitiveRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IoioI (-> Bool $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lTotalValuedRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lAsymmetricRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.range_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lListFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lList_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lTruthValue_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.contraryAttribute_THFTYPE_IioI (-> $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.n2009_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lProposition_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.inList_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lListFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lSentence_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lFormula_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lSetOrClass_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.orientation_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.disjointRelation_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.temporalPart_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.subclass_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.disjoint_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.part_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.located_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lPositionalAttribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lCardinalityFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.domainSubclass_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.partition_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.documentation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lTemporalCompositionFn_THFTYPE_IiiiI (-> $$unsorted $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.n1_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lDirectionalAttribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lIrreflexiveRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.rangeSubclass_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.containsInformation_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 1.53/1.72 (declare-const tptp.n12_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lAttribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.subAttribute_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lMonth_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lTimeInterval_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.property_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lInternalAttribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lRelationalAttribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lEntity_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lInheritableRelation_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lDay_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lDayDuration_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lMeasureFn_THFTYPE_IiiiI (-> $$unsorted $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lAgent_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.knows_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 1.53/1.72 (declare-const tptp.agent_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.meetsTemporally_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lCognitiveAgent_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lHuman_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lRelationExtendedToQuantities_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lLinguisticExpression_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.holdsDuring_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 1.53/1.72 (declare-const tptp.lListOrderFn_THFTYPE_IiiiI (-> $$unsorted $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lBill_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lMary_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.likes_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lWhenFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lBeginFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lEndFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lQuantity_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lMultiplicationFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.contraryAttribute_THFTYPE_IoooI (-> Bool Bool Bool)) % 1.53/1.72 (declare-const tptp.n3_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lListOrderFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lBinaryFunction_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.subrelation_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIoooIiioI (-> (-> Bool Bool Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domainSubclass_THFTYPE_IIioIiioI (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lTernaryPredicate_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lObject_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lSelfConnectedObject_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIioIiioI (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.minus_THFTYPE_IiiiI (-> $$unsorted $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.subrelation_THFTYPE_IIioIIioIoI (-> (-> $$unsorted Bool) (-> $$unsorted Bool) Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIiioIiioI (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.believes_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 1.53/1.72 (declare-const tptp.modalAttribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.member_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.attribute_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lOrganization_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lSue_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lYearFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.lOrganism_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lWhenFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 1.53/1.72 (declare-const tptp.subProcess_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIiiIiioI (-> (-> $$unsorted $$unsorted) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lMonthFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lSubtractionFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lAdditionFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lUnaryFunction_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lYearFn_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.lBinaryPredicate_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIiooIioI (-> (-> $$unsorted Bool Bool) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.n2_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.relatedInternalConcept_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.lessThan_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.equal_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIiiiIioI (-> (-> $$unsorted $$unsorted $$unsorted) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.relatedInternalConcept_THFTYPE_IiIiooIoI (-> $$unsorted (-> $$unsorted Bool Bool) Bool)) % 1.53/1.72 (declare-const tptp.greaterThan_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIiiIioI (-> (-> $$unsorted $$unsorted) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.patient_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.result_THFTYPE_i $$unsorted) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIiooIiioI (-> (-> $$unsorted Bool Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.domain_THFTYPE_IIiiioIiioI (-> (-> $$unsorted $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.instance_THFTYPE_IIiiioIioI (-> (-> $$unsorted $$unsorted $$unsorted Bool) $$unsorted Bool)) % 1.53/1.72 (declare-const tptp.relatedInternalConcept_THFTYPE_IIiioIIiioIoI (-> (-> $$unsorted $$unsorted Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 1.53/1.72 (declare-const tptp.subrelation_THFTYPE_IIiioIIiioIoI (-> (-> $$unsorted $$unsorted Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 1.53/1.72 (declare-const tptp.subrelation_THFTYPE_IiIiioIoI (-> $$unsorted (-> $$unsorted $$unsorted Bool) Bool)) % 1.53/1.72 (declare-const tptp.instrument_THFTYPE_i $$unsorted) % 1.53/1.72 (define @t1 () (@var "REL2" $$unsorted)) % 1.53/1.72 (define @t2 () (@var "REL1" $$unsorted)) % 1.53/1.72 (define @t3 () (_ (_ tptp.disjointRelation_THFTYPE_IiioI @t2) @t1)) % 1.53/1.72 (define @t4 () (@var "CLASS2" $$unsorted)) % 1.53/1.72 (define @t5 () (@var "CLASS1" $$unsorted)) % 1.53/1.72 (define @t6 () (_ (_ tptp.disjoint_THFTYPE_IiioI @t5) @t4)) % 1.53/1.72 (define @t7 () (_ tptp.rangeSubclass_THFTYPE_IiioI @t1)) % 1.53/1.72 (define @t8 () (_ (_ tptp.rangeSubclass_THFTYPE_IiioI @t2) @t5)) % 1.53/1.72 (define @t9 () (@list @t1 @t5 @t4 @t2)) % 1.53/1.72 (define @t10 () (@var "Y" $$unsorted)) % 1.53/1.72 (define @t11 () (@var "Z" $$unsorted)) % 1.53/1.72 (define @t12 () (_ tptp.instance_THFTYPE_IiioI @t11)) % 1.53/1.72 (define @t13 () (@var "X" $$unsorted)) % 1.53/1.72 (define @t14 () (_ (_ tptp.subclass_THFTYPE_IiioI @t13) @t10)) % 1.53/1.72 (define @t15 () (@var "THING" $$unsorted)) % 1.53/1.72 (define @t16 () (_ tptp.instance_THFTYPE_IiioI @t15)) % 1.53/1.72 (define @t17 () (_ @t16 tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (define @t18 () (@list @t15)) % 1.53/1.72 (define @t19 () (@var "OBJ2" $$unsorted)) % 1.53/1.72 (define @t20 () (@var "SUB" $$unsorted)) % 1.53/1.72 (define @t21 () (_ tptp.located_THFTYPE_IiioI @t20)) % 1.53/1.72 (define @t22 () (@var "OBJ1" $$unsorted)) % 1.53/1.72 (define @t23 () (@list @t20)) % 1.53/1.72 (define @t24 () (@var "NUMBER" $$unsorted)) % 1.53/1.72 (define @t25 () (@var "MONTH" $$unsorted)) % 1.53/1.72 (define @t26 () (@var "AGENT" $$unsorted)) % 1.53/1.72 (define @t27 () (@var "PROC" $$unsorted)) % 1.53/1.72 (define @t28 () (_ (_ tptp.agent_THFTYPE_IiioI @t27) @t26)) % 1.53/1.72 (define @t29 () (@list @t27)) % 1.53/1.72 (define @t30 () (_ tptp.instance_THFTYPE_IiioI @t26)) % 1.53/1.72 (define @t31 () (_ @t30 tptp.lAgent_THFTYPE_i)) % 1.53/1.72 (define @t32 () (@list @t26)) % 1.53/1.72 (define @t33 () (@var "ATTR2" $$unsorted)) % 1.53/1.72 (define @t34 () (_ (_ tptp.orientation_THFTYPE_IiiioI @t22) @t19)) % 1.53/1.72 (define @t35 () (not (_ @t34 @t33))) % 1.53/1.72 (define @t36 () (@var "ATTR1" $$unsorted)) % 1.53/1.72 (define @t37 () (= @t36 @t33)) % 1.53/1.72 (define @t38 () (not @t37)) % 1.53/1.72 (define @t39 () (@var "ROW" $$unsorted)) % 1.53/1.72 (define @t40 () (_ tptp.lListFn_THFTYPE_IiiI @t39)) % 1.53/1.72 (define @t41 () (_ tptp.contraryAttribute_THFTYPE_IioI @t39)) % 1.53/1.72 (define @t42 () (_ @t34 @t36)) % 1.53/1.72 (define @t43 () (@var "CLASS" $$unsorted)) % 1.53/1.72 (define @t44 () (_ tptp.instance_THFTYPE_IiioI @t36)) % 1.53/1.72 (define @t45 () (_ tptp.instance_THFTYPE_IiioI @t33)) % 1.53/1.72 (define @t46 () (_ (_ tptp.subAttribute_THFTYPE_IiioI @t36) @t33)) % 1.53/1.72 (define @t47 () (_ tptp.subclass_THFTYPE_IiioI tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (define @t48 () (@var "PROP" Bool)) % 1.53/1.72 (define @t49 () (@var "SENT" $$unsorted)) % 1.53/1.72 (define @t50 () (or (_ (_ tptp.subclass_THFTYPE_IiioI @t5) @t4) (_ (_ tptp.subclass_THFTYPE_IiioI @t4) @t5))) % 1.53/1.72 (define @t51 () (@var "REL" $$unsorted)) % 1.53/1.72 (define @t52 () (_ (_ tptp.domainSubclass_THFTYPE_IiiioI @t51) @t24)) % 1.53/1.72 (define @t53 () (@list @t24 @t5 @t51 @t4)) % 1.53/1.72 (define @t54 () (@var "DAY" $$unsorted)) % 1.53/1.72 (define @t55 () (@var "FORMULA" Bool)) % 1.53/1.72 (define @t56 () (_ (_ tptp.knows_THFTYPE_IiooI @t26) @t55)) % 1.53/1.72 (define @t57 () (@list @t55 @t26)) % 1.53/1.72 (define @t58 () (_ (_ tptp.domainSubclass_THFTYPE_IiiioI @t1) @t24)) % 1.53/1.72 (define @t59 () (_ (_ (_ tptp.domainSubclass_THFTYPE_IiiioI @t2) @t24) @t5)) % 1.53/1.72 (define @t60 () (@list @t1 @t24 @t5 @t4 @t2)) % 1.53/1.72 (define @t61 () (_ tptp.subclass_THFTYPE_IiioI tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (define @t62 () (_ (_ tptp.domain_THFTYPE_IiiioI @t51) @t24)) % 1.53/1.72 (define @t63 () (_ tptp.subclass_THFTYPE_IiioI tptp.lText_THFTYPE_i)) % 1.53/1.72 (define @t64 () (@var "INST3" $$unsorted)) % 1.53/1.72 (define @t65 () (@var "INST1" $$unsorted)) % 1.53/1.72 (define @t66 () (@var "REL" (-> $$unsorted $$unsorted Bool))) % 1.53/1.72 (define @t67 () (_ @t66 @t65)) % 1.53/1.72 (define @t68 () (@var "INST2" $$unsorted)) % 1.53/1.72 (define @t69 () (_ tptp.instance_THFTYPE_IIiioIioI @t66)) % 1.53/1.72 (define @t70 () (@list @t66)) % 1.53/1.72 (define @t71 () (@var "ATTR" $$unsorted)) % 1.53/1.72 (define @t72 () (@var "THING2" $$unsorted)) % 1.53/1.72 (define @t73 () (@var "THING1" $$unsorted)) % 1.53/1.72 (define @t74 () (= @t73 @t72)) % 1.53/1.72 (define @t75 () (@list @t72 @t73)) % 1.53/1.72 (define @t76 () (_ tptp.range_THFTYPE_IiioI @t1)) % 1.53/1.72 (define @t77 () (_ (_ tptp.range_THFTYPE_IiioI @t2) @t5)) % 1.53/1.72 (define @t78 () (_ tptp.subclass_THFTYPE_IiioI tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (define @t79 () (@var "SITUATION" Bool)) % 1.53/1.72 (define @t80 () (@var "TIME" $$unsorted)) % 1.53/1.72 (define @t81 () (_ tptp.holdsDuring_THFTYPE_IiooI @t80)) % 1.53/1.72 (define @t82 () (@var "LIST2" $$unsorted)) % 1.53/1.72 (define @t83 () (@var "LIST1" $$unsorted)) % 1.53/1.72 (define @t84 () (= @t83 @t82)) % 1.53/1.72 (define @t85 () (@list @t24)) % 1.53/1.72 (define @t86 () (@var "INTERVAL2" $$unsorted)) % 1.53/1.72 (define @t87 () (_ tptp.lBeginFn_THFTYPE_IiiI @t86)) % 1.53/1.72 (define @t88 () (@var "INTERVAL1" $$unsorted)) % 1.53/1.72 (define @t89 () (_ tptp.lEndFn_THFTYPE_IiiI @t88)) % 1.53/1.72 (define @t90 () (@list @t88 @t86)) % 1.53/1.72 (define @t91 () (@var "TIME2" $$unsorted)) % 1.53/1.72 (define @t92 () (@var "TIME1" $$unsorted)) % 1.53/1.72 (define @t93 () (@var "INST" $$unsorted)) % 1.53/1.72 (define @t94 () (@list @t93)) % 1.53/1.72 (define @t95 () (@var "PRED1" $$unsorted)) % 1.53/1.72 (define @t96 () (@var "PRED2" $$unsorted)) % 1.53/1.72 (define @t97 () (_ (_ tptp.subrelation_THFTYPE_IiioI @t95) @t96)) % 1.53/1.72 (define @t98 () (_ tptp.lListOrderFn_THFTYPE_IiiiI @t40)) % 1.53/1.72 (define @t99 () (_ @t98 @t24)) % 1.53/1.72 (define @t100 () (@var "REL" (-> $$unsorted Bool))) % 1.53/1.72 (define @t101 () (_ @t100 @t39)) % 1.53/1.72 (define @t102 () (@list @t24 @t43 @t100 @t39)) % 1.53/1.72 (define @t103 () (@var "YEAR" $$unsorted)) % 1.53/1.72 (define @t104 () (@list @t5 @t4)) % 1.53/1.72 (define @t105 () (_ (_ tptp.subrelation_THFTYPE_IiioI @t2) @t1)) % 1.53/1.72 (define @t106 () (@list @t1 @t5 @t2)) % 1.53/1.72 (define @t107 () (@var "ITEM" $$unsorted)) % 1.53/1.72 (define @t108 () (_ tptp.instance_THFTYPE_IiioI @t107)) % 1.53/1.72 (define @t109 () (@var "VALUE" $$unsorted)) % 1.53/1.72 (define @t110 () (@var "YEAR2" $$unsorted)) % 1.53/1.72 (define @t111 () (@var "YEAR1" $$unsorted)) % 1.53/1.72 (define @t112 () (@var "REL2" (-> $$unsorted Bool))) % 1.53/1.72 (define @t113 () (@var "REL1" (-> $$unsorted Bool))) % 1.53/1.72 (define @t114 () (@var "ORG" $$unsorted)) % 1.53/1.72 (define @t115 () (_ tptp.range_THFTYPE_IiioI @t51)) % 1.53/1.72 (define @t116 () (@list @t5 @t51 @t4)) % 1.53/1.72 (define @t117 () (_ tptp.likes_THFTYPE_IiioI tptp.lSue_THFTYPE_i)) % 1.53/1.72 (define @t118 () (_ @t117 @t13)) % 1.53/1.72 (define @t119 () (not @t118)) % 1.53/1.72 (define @t120 () (_ tptp.lYearFn_THFTYPE_IiiI tptp.n2009_THFTYPE_i)) % 1.53/1.72 (define @t121 () (_ tptp.holdsDuring_THFTYPE_IiooI @t120)) % 1.53/1.72 (define @t122 () (_ @t121 @t119)) % 1.53/1.72 (define @t123 () (@list @t13)) % 1.53/1.72 (define @t124 () (forall @t123 @t122)) % 1.53/1.72 (define @t125 () (_ tptp.instance_THFTYPE_IiioI @t93)) % 1.53/1.72 (define @t126 () (@var "SUBPROC" $$unsorted)) % 1.53/1.72 (define @t127 () (_ (_ tptp.subProcess_THFTYPE_IiioI @t126) @t27)) % 1.53/1.72 (define @t128 () (@list @t126 @t27)) % 1.53/1.72 (define @t129 () (@var "OBJ" $$unsorted)) % 1.53/1.72 (define @t130 () (_ tptp.property_THFTYPE_IiioI @t129)) % 1.53/1.72 (define @t131 () (_ @t130 @t33)) % 1.53/1.72 (define @t132 () (_ @t130 @t36)) % 1.53/1.72 (define @t133 () (@var "NUMBER2" $$unsorted)) % 1.53/1.72 (define @t134 () (@var "NUMBER1" $$unsorted)) % 1.53/1.72 (define @t135 () (_ tptp.property_THFTYPE_IiioI @t15)) % 1.53/1.72 (define @t136 () (@list @t33 @t36)) % 1.53/1.72 (define @t137 () (_ @t117 tptp.lBill_THFTYPE_i)) % 1.53/1.72 (define @t138 () (@var "REGION" $$unsorted)) % 1.53/1.72 (define @t139 () (@var "PART" $$unsorted)) % 1.53/1.72 (define @t140 () (@var "TEXT" $$unsorted)) % 1.53/1.72 (define @t141 () (@var "ELEMENT" $$unsorted)) % 1.53/1.72 (define @t142 () (@var "PROCESS" $$unsorted)) % 1.53/1.72 (define @t143 () (@var "ROW2" $$unsorted)) % 1.53/1.72 (define @t144 () (_ tptp.lListFn_THFTYPE_IiiI @t143)) % 1.53/1.72 (define @t145 () (@var "ROW1" $$unsorted)) % 1.53/1.72 (define @t146 () (_ tptp.lListFn_THFTYPE_IiiI @t145)) % 1.53/1.72 (define @t147 () (@var "LIST" $$unsorted)) % 1.53/1.72 (define @t148 () (_ tptp.rangeSubclass_THFTYPE_IiioI @t51)) % 1.53/1.72 (define @t149 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.meetsTemporally_THFTYPE_IiioI)) % 1.53/1.72 (define @t150 () (_ tptp.instance_THFTYPE_IIiooIioI tptp.containsInformation_THFTYPE_IiooI)) % 1.53/1.72 (define @t151 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.duration_THFTYPE_IiioI)) % 1.53/1.72 (define @t152 () (_ tptp.instance_THFTYPE_IiioI tptp.lAdditionFn_THFTYPE_i)) % 1.53/1.72 (define @t153 () (_ tptp.instance_THFTYPE_IiioI tptp.lMonthFn_THFTYPE_i)) % 1.53/1.72 (define @t154 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.range_THFTYPE_IiioI)) % 1.53/1.72 (define @t155 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.disjointRelation_THFTYPE_IiioI)) % 1.53/1.72 (define @t156 () (_ tptp.domainSubclass_THFTYPE_IiiioI tptp.lMonthFn_THFTYPE_i)) % 1.53/1.72 (define @t157 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subProcess_THFTYPE_IiioI)) % 1.53/1.72 (define @t158 () (_ tptp.instance_THFTYPE_IiioI tptp.lessThan_THFTYPE_i)) % 1.53/1.72 (define @t159 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.meetsTemporally_THFTYPE_IiioI)) % 1.53/1.72 (define @t160 () (_ tptp.domain_THFTYPE_IiiioI tptp.equal_THFTYPE_i)) % 1.53/1.72 (define @t161 () (_ tptp.domain_THFTYPE_IIoooIiioI tptp.truth_THFTYPE_IoooI)) % 1.53/1.72 (define @t162 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.disjoint_THFTYPE_IiioI)) % 1.53/1.72 (define @t163 () (_ tptp.instance_THFTYPE_IiioI tptp.lSubtractionFn_THFTYPE_i)) % 1.53/1.72 (define @t164 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.agent_THFTYPE_IiioI)) % 1.53/1.72 (define @t165 () (_ tptp.instance_THFTYPE_IiioI tptp.equal_THFTYPE_i)) % 1.53/1.72 (define @t166 () (_ tptp.domain_THFTYPE_IiiioI tptp.greaterThan_THFTYPE_i)) % 1.53/1.72 (define @t167 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subrelation_THFTYPE_IiioI)) % 1.53/1.72 (define @t168 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lYearFn_THFTYPE_IiiI)) % 1.53/1.72 (define @t169 () (_ tptp.instance_THFTYPE_IiioI tptp.attribute_THFTYPE_i)) % 1.53/1.72 (define @t170 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lWhenFn_THFTYPE_IiiI)) % 1.53/1.72 (define @t171 () (_ tptp.instance_THFTYPE_IiioI tptp.modalAttribute_THFTYPE_i)) % 1.53/1.72 (define @t172 () (_ tptp.domain_THFTYPE_IiiioI tptp.patient_THFTYPE_i)) % 1.53/1.72 (define @t173 () (_ tptp.domain_THFTYPE_IiiioI tptp.lMultiplicationFn_THFTYPE_i)) % 1.53/1.72 (define @t174 () (_ tptp.domain_THFTYPE_IIiooIiioI tptp.believes_THFTYPE_IiooI)) % 1.53/1.72 (define @t175 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lCardinalityFn_THFTYPE_IiiI)) % 1.53/1.72 (define @t176 () (_ tptp.instance_THFTYPE_IiioI tptp.greaterThan_THFTYPE_i)) % 1.53/1.72 (define @t177 () (_ tptp.instance_THFTYPE_IiioI tptp.lMultiplicationFn_THFTYPE_i)) % 1.53/1.72 (define @t178 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.property_THFTYPE_IiioI)) % 1.53/1.72 (define @t179 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subAttribute_THFTYPE_IiioI)) % 1.53/1.72 (define @t180 () (_ tptp.domain_THFTYPE_IIiiioIiioI tptp.orientation_THFTYPE_IiiioI)) % 1.53/1.72 (define @t181 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.inList_THFTYPE_IiioI)) % 1.53/1.72 (define @t182 () (_ tptp.domain_THFTYPE_IIiooIiioI tptp.knows_THFTYPE_IiooI)) % 1.53/1.72 (define @t183 () (_ tptp.domain_THFTYPE_IIiiioIiioI tptp.domain_THFTYPE_IiiioI)) % 1.53/1.72 (define @t184 () (_ tptp.domain_THFTYPE_IiiioI tptp.result_THFTYPE_i)) % 1.53/1.72 (define @t185 () (_ tptp.instance_THFTYPE_IIiiiIioI tptp.lTemporalCompositionFn_THFTYPE_IiiiI)) % 1.53/1.72 (define @t186 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.relatedInternalConcept_THFTYPE_IiioI)) % 1.53/1.72 (define @t187 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.part_THFTYPE_IiioI)) % 1.53/1.72 (define @t188 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lBeginFn_THFTYPE_IiiI)) % 1.53/1.72 (define @t189 () (_ tptp.instance_THFTYPE_IIiooIioI tptp.holdsDuring_THFTYPE_IiooI)) % 1.53/1.72 (define @t190 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.instance_THFTYPE_IiioI)) % 1.53/1.72 (define @t191 () (_ tptp.domain_THFTYPE_IiiioI tptp.lessThan_THFTYPE_i)) % 1.53/1.72 (define @t192 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.temporalPart_THFTYPE_IiioI)) % 1.53/1.72 (define @t193 () (_ tptp.domain_THFTYPE_IiiioI tptp.instrument_THFTYPE_i)) % 1.53/1.72 (define @t194 () (_ tptp.domain_THFTYPE_IiiioI tptp.lAdditionFn_THFTYPE_i)) % 1.53/1.72 (define @t195 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.rangeSubclass_THFTYPE_IiioI)) % 1.53/1.72 (define @t196 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.inList_THFTYPE_IiioI)) % 1.53/1.72 (define @t197 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.disjointRelation_THFTYPE_IiioI)) % 1.53/1.72 (define @t198 () (_ tptp.instance_THFTYPE_IIiiiIioI tptp.lMeasureFn_THFTYPE_IiiiI)) % 1.53/1.72 (define @t199 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lEndFn_THFTYPE_IiiI)) % 1.53/1.72 (define @t200 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subclass_THFTYPE_IiioI)) % 1.53/1.72 (define @t201 () (_ tptp.domain_THFTYPE_IiiioI tptp.lSubtractionFn_THFTYPE_i)) % 1.53/1.72 (define @t202 () (_ tptp.domain_THFTYPE_IIIioIiioIiioI tptp.domainSubclass_THFTYPE_IIioIiioI)) % 1.53/1.72 (define @t203 () (not (_ @t121 false))) % 1.53/1.72 (define @t204 () (@purify false)) % 1.53/1.72 (define @t205 () (tptp.lYearFn_THFTYPE_IiiI tptp.n2009_THFTYPE_i)) % 1.53/1.72 (define @t206 () (tptp.holdsDuring_THFTYPE_IiooI @t205 @t204)) % 1.53/1.72 (define @t207 () (_ tptp.holdsDuring_THFTYPE_IiooI @t205)) % 1.53/1.72 (define @t208 () (tptp.likes_THFTYPE_IiioI tptp.lSue_THFTYPE_i tptp.lBill_THFTYPE_i)) % 1.53/1.72 (define @t209 () (not @t208)) % 1.53/1.72 (define @t210 () (@purify @t209)) % 1.53/1.72 (define @t211 () (@list false)) % 1.53/1.72 (define @t212 () (tptp.holdsDuring_THFTYPE_IiooI @t205 @t210)) % 1.53/1.72 (define @t213 () (tptp.likes_THFTYPE_IiioI tptp.lSue_THFTYPE_i @t13)) % 1.53/1.72 (define @t214 () (not @t213)) % 1.53/1.72 (define @t215 () (tptp.holdsDuring_THFTYPE_IiooI @t205 @t214)) % 1.53/1.72 (define @t216 () (tptp.holdsDuring_THFTYPE_IiooI @t205 @t209)) % 1.53/1.72 (define @t217 () (forall @t123 @t215)) % 1.53/1.72 (assume @p1 (_ (_ (_ tptp.partition_THFTYPE_IiiioI tptp.lAttribute_THFTYPE_i) tptp.lInternalAttribute_THFTYPE_i) tptp.lRelationalAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p2 (forall @t9 (=> (and @t8 (_ @t7 @t4) @t6) @t3))) % 1.53/1.72 (assume @p3 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lInheritableRelation_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p4 (forall (@list @t13 @t10 @t11) (=> (and @t14 (_ @t12 @t13)) (_ @t12 @t10)))) % 1.53/1.72 (assume @p5 (forall (@list @t13 @t10) (=> @t14 (and (_ (_ tptp.instance_THFTYPE_IiioI @t13) tptp.lSetOrClass_THFTYPE_i) (_ (_ tptp.instance_THFTYPE_IiioI @t10) tptp.lSetOrClass_THFTYPE_i))))) % 1.53/1.72 (assume @p6 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lFormula_THFTYPE_i) tptp.lSentence_THFTYPE_i)) % 1.53/1.72 (assume @p7 (forall @t18 @t17)) % 1.53/1.72 (assume @p8 (forall (@list @t22 @t19) (=> (_ (_ tptp.located_THFTYPE_IiioI @t22) @t19) (forall @t23 (=> (_ (_ tptp.part_THFTYPE_IiioI @t20) @t22) (_ @t21 @t19)))))) % 1.53/1.72 (assume @p9 (forall (@list @t24 @t25) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t25) tptp.lMonth_THFTYPE_i) (_ (_ tptp.duration_THFTYPE_IiioI @t25) (_ (_ tptp.lMeasureFn_THFTYPE_IiiiI @t24) tptp.lDayDuration_THFTYPE_i))) (= (_ tptp.lCardinalityFn_THFTYPE_IiiI (_ (_ tptp.lTemporalCompositionFn_THFTYPE_IiiiI @t25) tptp.lDay_THFTYPE_i)) @t24)))) % 1.53/1.72 (assume @p10 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lDirectionalAttribute_THFTYPE_i) tptp.lPositionalAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p11 (forall @t32 (= @t31 (exists @t29 @t28)))) % 1.53/1.72 (assume @p12 (forall (@list @t33 @t22 @t39 @t19 @t36) (=> (and @t42 @t41 (_ (_ tptp.inList_THFTYPE_IiioI @t36) @t40) (_ (_ tptp.inList_THFTYPE_IiioI @t33) @t40) @t38) @t35))) % 1.53/1.72 (assume @p13 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lTruthValue_THFTYPE_i) tptp.lRelationalAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p14 (forall (@list @t43 @t33 @t36) (=> (and @t46 (_ @t45 @t43)) (_ @t44 @t43)))) % 1.53/1.72 (assume @p15 (_ (_ tptp.range_THFTYPE_IiioI tptp.lListFn_THFTYPE_i) tptp.lList_THFTYPE_i)) % 1.53/1.72 (assume @p16 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lAsymmetricRelation_THFTYPE_i) tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p17 (_ @t47 tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p18 (forall (@list @t49) (=> (_ (_ tptp.instance_THFTYPE_IiioI @t49) tptp.lSentence_THFTYPE_i) (exists (@list @t48) (and (_ (_ tptp.instance_THFTYPE_IoioI @t48) tptp.lProposition_THFTYPE_i) (_ (_ tptp.containsInformation_THFTYPE_IiooI @t49) @t48)))))) % 1.53/1.72 (assume @p19 (forall @t53 (=> (and (_ @t52 @t5) (_ @t52 @t4)) @t50))) % 1.53/1.72 (assume @p20 (forall (@list @t54) (=> (_ (_ tptp.instance_THFTYPE_IiioI @t54) tptp.lDay_THFTYPE_i) (_ (_ tptp.duration_THFTYPE_IiioI @t54) (_ (_ tptp.lMeasureFn_THFTYPE_IiiiI tptp.n1_THFTYPE_i) tptp.lDayDuration_THFTYPE_i))))) % 1.53/1.72 (assume @p21 (forall @t57 (=> @t56 (_ (_ tptp.truth_THFTYPE_IoooI @t55) true)))) % 1.53/1.72 (assume @p22 (forall @t60 (=> (and @t59 (_ @t58 @t4) @t6) @t3))) % 1.53/1.72 (assume @p23 (_ @t61 tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p24 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lYear_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p25 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lIntentionalProcess_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p26 (forall @t53 (=> (and (_ @t62 @t5) (_ @t62 @t4)) @t50))) % 1.53/1.72 (assume @p27 (_ @t63 tptp.lContentBearingObject_THFTYPE_i)) % 1.53/1.72 (assume @p28 (forall @t70 (= (_ @t69 tptp.lTransitiveRelation_THFTYPE_i) (forall (@list @t65 @t68 @t64) (=> (and (_ @t67 @t68) (_ (_ @t66 @t68) @t64)) (_ @t67 @t64)))))) % 1.53/1.72 (assume @p29 (forall @t75 (=> @t74 (forall (@list @t71) (= (_ (_ tptp.property_THFTYPE_IiioI @t73) @t71) (_ (_ tptp.property_THFTYPE_IiioI @t72) @t71)))))) % 1.53/1.72 (assume @p30 (forall (@list @t33 @t22 @t19 @t36) (=> (and @t42 (_ @t44 tptp.lDirectionalAttribute_THFTYPE_i) (_ @t45 tptp.lDirectionalAttribute_THFTYPE_i) @t38) @t35))) % 1.53/1.72 (assume @p31 (_ (_ tptp.rangeSubclass_THFTYPE_IiioI tptp.lTemporalCompositionFn_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p32 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lList_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p33 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lHuman_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 1.53/1.72 (assume @p34 (forall @t9 (=> (and @t77 (_ @t76 @t4) @t6) @t3))) % 1.53/1.72 (assume @p35 (_ @t78 tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p36 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lMonth_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p37 (_ @t63 tptp.lLinguisticExpression_THFTYPE_i)) % 1.53/1.72 (assume @p38 (forall (@list @t80 @t79) (=> (_ @t81 (not @t79)) (not (_ @t81 @t79))))) % 1.53/1.72 (assume @p39 (forall (@list @t82 @t83) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t83) tptp.lList_THFTYPE_i) (_ (_ tptp.instance_THFTYPE_IiioI @t82) tptp.lList_THFTYPE_i) (forall @t85 (= (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t83) @t24) (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t82) @t24)))) @t84))) % 1.53/1.72 (assume @p40 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lPositionalAttribute_THFTYPE_i) tptp.lRelationalAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p41 (_ (_ tptp.likes_THFTYPE_IiioI tptp.lMary_THFTYPE_i) tptp.lBill_THFTYPE_i)) % 1.53/1.72 (assume @p42 (_ (_ tptp.range_THFTYPE_IiioI tptp.lWhenFn_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p43 (forall @t90 (= (_ (_ tptp.meetsTemporally_THFTYPE_IiioI @t88) @t86) (= @t89 @t87)))) % 1.53/1.72 (assume @p44 (forall (@list @t79 @t91 @t92) (=> (and (_ (_ tptp.holdsDuring_THFTYPE_IiooI @t92) @t79) (_ (_ tptp.temporalPart_THFTYPE_IiioI @t91) @t92)) (_ (_ tptp.holdsDuring_THFTYPE_IiooI @t91) @t79)))) % 1.53/1.72 (assume @p45 (_ (_ tptp.range_THFTYPE_IiioI tptp.lMultiplicationFn_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p46 (_ (_ tptp.contraryAttribute_THFTYPE_IoooI false) true)) % 1.53/1.72 (assume @p47 (exists @t18 @t17)) % 1.53/1.72 (assume @p48 (_ (_ tptp.range_THFTYPE_IiioI tptp.lListOrderFn_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p49 (forall @t70 (= (_ @t69 tptp.lIrreflexiveRelation_THFTYPE_i) (forall @t94 (not (_ (_ @t66 @t93) @t93)))))) % 1.53/1.72 (assume @p50 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lBinaryFunction_THFTYPE_i) tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p51 (forall (@list @t24 @t95 @t5 @t96) (=> (and @t97 (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t96) @t24) @t5)) (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t95) @t24) @t5)))) % 1.53/1.72 (assume @p52 (_ @t47 tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p53 (forall @t102 (=> (and (_ (_ (_ tptp.domainSubclass_THFTYPE_IIioIiioI @t100) @t24) @t43) @t101) (_ (_ tptp.subclass_THFTYPE_IiioI @t99) @t43)))) % 1.53/1.72 (assume @p54 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lTernaryPredicate_THFTYPE_i) tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p55 (_ @t78 tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p56 (forall (@list @t103) (=> (_ (_ tptp.instance_THFTYPE_IiioI @t103) tptp.lYear_THFTYPE_i) (= (_ tptp.lCardinalityFn_THFTYPE_IiiI (_ (_ tptp.lTemporalCompositionFn_THFTYPE_IiiiI @t103) tptp.lMonth_THFTYPE_i)) tptp.n12_THFTYPE_i)))) % 1.53/1.72 (assume @p57 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lSelfConnectedObject_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p58 (forall @t104 (=> (= @t5 @t4) (forall @t18 (= (_ @t16 @t5) (_ @t16 @t4)))))) % 1.53/1.72 (assume @p59 (forall @t106 (=> (and @t105 (_ @t7 @t5)) @t8))) % 1.53/1.72 (assume @p60 (forall (@list @t109 @t107) (=> (and (_ (_ tptp.property_THFTYPE_IiioI @t107) @t109) (_ (_ tptp.instance_THFTYPE_IiioI @t109) tptp.lTruthValue_THFTYPE_i)) (or (_ @t108 tptp.lSentence_THFTYPE_i) (_ @t108 tptp.lProposition_THFTYPE_i))))) % 1.53/1.72 (assume @p61 (forall @t102 (=> (and (_ (_ (_ tptp.domain_THFTYPE_IIioIiioI @t100) @t24) @t43) @t101) (_ (_ tptp.instance_THFTYPE_IiioI @t99) @t43)))) % 1.53/1.72 (assume @p62 (forall (@list @t110 @t111) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t111) tptp.lYear_THFTYPE_i) (_ (_ tptp.instance_THFTYPE_IiioI @t110) tptp.lYear_THFTYPE_i) (= (_ (_ tptp.minus_THFTYPE_IiiiI @t110) @t111) tptp.n1_THFTYPE_i)) (_ (_ tptp.meetsTemporally_THFTYPE_IiioI @t111) @t110)))) % 1.53/1.72 (assume @p63 (forall (@list @t112 @t39 @t113) (=> (and (_ (_ tptp.subrelation_THFTYPE_IIioIIioIoI @t113) @t112) (_ @t113 @t39)) (_ @t112 @t39)))) % 1.53/1.72 (assume @p64 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lRelationalAttribute_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p65 (forall @t57 (=> @t56 (_ (_ tptp.believes_THFTYPE_IiooI @t26) @t55)))) % 1.53/1.72 (assume @p66 (forall @t75 (=> @t74 (forall (@list @t43) (= (_ (_ tptp.instance_THFTYPE_IiioI @t73) @t43) (_ (_ tptp.instance_THFTYPE_IiioI @t72) @t43)))))) % 1.53/1.72 (assume @p67 (forall (@list @t114 @t26) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t114) tptp.lOrganization_THFTYPE_i) (_ (_ tptp.member_THFTYPE_IiioI @t26) @t114)) @t31))) % 1.53/1.72 (assume @p68 (forall @t116 (=> (and (_ @t115 @t5) (_ @t115 @t4)) @t50))) % 1.53/1.72 (assume @p69 @t124) % 1.53/1.72 (assume @p70 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lOrganism_THFTYPE_i) tptp.lAgent_THFTYPE_i)) % 1.53/1.72 (assume @p71 (forall @t104 (= @t6 (forall @t94 (not (and (_ @t125 @t5) (_ @t125 @t4))))))) % 1.53/1.72 (assume @p72 (forall @t128 (=> @t127 (_ (_ tptp.temporalPart_THFTYPE_IiioI (_ tptp.lWhenFn_THFTYPE_IiiI @t126)) (_ tptp.lWhenFn_THFTYPE_IiiI @t27))))) % 1.53/1.72 (assume @p73 (_ (_ tptp.rangeSubclass_THFTYPE_IiioI tptp.lMonthFn_THFTYPE_i) tptp.lMonth_THFTYPE_i)) % 1.53/1.72 (assume @p74 (forall @t90 (=> (and (= (_ tptp.lBeginFn_THFTYPE_IiiI @t88) @t87) (= @t89 (_ tptp.lEndFn_THFTYPE_IiiI @t86))) (= @t88 @t86)))) % 1.53/1.72 (assume @p75 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lOrganization_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 1.53/1.72 (assume @p76 (forall @t106 (=> (and @t105 (_ @t76 @t5)) @t77))) % 1.53/1.72 (assume @p77 (forall (@list @t129 @t133 @t39 @t134) (=> @t41 (forall (@list @t36 @t33) (=> (and (= @t36 (_ @t98 @t134)) (= @t33 (_ @t98 @t133)) (not (= @t134 @t133))) (=> @t132 (not @t131))))))) % 1.53/1.72 (assume @p78 (_ @t61 tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p79 (forall @t29 (=> (_ (_ tptp.instance_THFTYPE_IiioI @t27) tptp.lIntentionalProcess_THFTYPE_i) (exists @t32 (and (_ @t30 tptp.lCognitiveAgent_THFTYPE_i) @t28))))) % 1.53/1.72 (assume @p80 (forall (@list @t1 @t24 @t5 @t2) (=> (and @t105 (_ @t58 @t5)) @t59))) % 1.53/1.72 (assume @p81 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lAgent_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p82 (forall @t136 (=> @t37 (forall @t18 (= (_ @t135 @t36) (_ @t135 @t33)))))) % 1.53/1.72 (assume @p83 @t137) % 1.53/1.72 (assume @p84 (forall @t128 (=> @t127 (forall (@list @t138) (=> (_ (_ tptp.located_THFTYPE_IiioI @t27) @t138) (_ (_ tptp.located_THFTYPE_IiioI @t126) @t138)))))) % 1.53/1.72 (assume @p85 (_ (_ tptp.range_THFTYPE_IiioI tptp.lSubtractionFn_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p86 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lInternalAttribute_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p87 (forall @t136 (=> @t46 (forall (@list @t129) (=> @t132 @t131))))) % 1.53/1.72 (assume @p88 (_ (_ tptp.range_THFTYPE_IiioI tptp.lAdditionFn_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p89 (forall (@list @t140) (=> (_ (_ tptp.instance_THFTYPE_IiioI @t140) tptp.lText_THFTYPE_i) (exists (@list @t139) (and (_ (_ tptp.part_THFTYPE_IiioI @t139) @t140) (_ (_ tptp.instance_THFTYPE_IiioI @t139) tptp.lLinguisticExpression_THFTYPE_i)))))) % 1.53/1.72 (assume @p90 (forall (@list @t39 @t141) (=> @t41 (=> (_ (_ tptp.inList_THFTYPE_IiioI @t141) @t40) (_ (_ tptp.instance_THFTYPE_IiioI @t141) tptp.lAttribute_THFTYPE_i))))) % 1.53/1.72 (assume @p91 (forall (@list @t129 @t142) (=> (_ (_ tptp.located_THFTYPE_IiioI @t142) @t129) (forall @t23 (=> (_ (_ tptp.subProcess_THFTYPE_IiioI @t20) @t142) (_ @t21 @t129)))))) % 1.53/1.72 (assume @p92 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lUnaryFunction_THFTYPE_i) tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p93 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lDay_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p94 (forall (@list @t143 @t82 @t83 @t145) (=> @t84 (=> (and (= @t83 @t146) (= @t82 @t144)) (forall @t85 (= (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t146) @t24) (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t144) @t24))))))) % 1.53/1.72 (assume @p95 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lSentence_THFTYPE_i) tptp.lLinguisticExpression_THFTYPE_i)) % 1.53/1.72 (assume @p96 (forall @t60 (=> (and (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t2) @t24) @t5) (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t1) @t24) @t4) @t6) @t3))) % 1.53/1.72 (assume @p97 (_ (_ tptp.rangeSubclass_THFTYPE_IiioI tptp.lYearFn_THFTYPE_i) tptp.lYear_THFTYPE_i)) % 1.53/1.72 (assume @p98 (forall (@list @t43 @t95 @t96) (=> (and @t97 (_ (_ tptp.instance_THFTYPE_IiioI @t96) @t43) (_ (_ tptp.subclass_THFTYPE_IiioI @t43) tptp.lInheritableRelation_THFTYPE_i)) (_ (_ tptp.instance_THFTYPE_IiioI @t95) @t43)))) % 1.53/1.72 (assume @p99 (forall (@list @t107 @t147) (=> (_ (_ tptp.inList_THFTYPE_IiioI @t107) @t147) (exists @t85 (= (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t147) @t24) @t107))))) % 1.53/1.72 (assume @p100 (forall @t116 (=> (and (_ @t148 @t5) (_ @t148 @t4)) @t50))) % 1.53/1.72 (assume @p101 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lBinaryPredicate_THFTYPE_i) tptp.lInheritableRelation_THFTYPE_i)) % 1.53/1.72 (assume @p102 (_ @t149 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p103 (_ @t150 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p104 (_ @t151 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p105 (_ @t152 tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p106 (_ @t153 tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p107 (_ @t154 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p108 (_ (_ @t155 tptp.n2_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p109 (_ @t149 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p110 (_ (_ @t156 tptp.n2_THFTYPE_i) tptp.lYear_THFTYPE_i)) % 1.53/1.72 (assume @p111 (_ (_ @t157 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p112 (_ (_ tptp.relatedInternalConcept_THFTYPE_IiioI tptp.lMonth_THFTYPE_i) tptp.lMonthFn_THFTYPE_i)) % 1.53/1.72 (assume @p113 (_ @t158 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p114 (_ (_ @t159 tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p115 (_ (_ @t160 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p116 (_ (_ @t161 tptp.n1_THFTYPE_i) tptp.lSentence_THFTYPE_i)) % 1.53/1.72 (assume @p117 (_ (_ @t162 tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p118 (_ @t163 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p119 (_ (_ @t157 tptp.n2_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p120 (_ (_ @t164 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p121 (_ @t165 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p122 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.relatedInternalConcept_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p123 (_ @t152 tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (assume @p124 (_ (_ tptp.instance_THFTYPE_IIiiiIioI tptp.lListOrderFn_THFTYPE_IiiiI) tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p125 (_ @t158 tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p126 (_ (_ tptp.relatedInternalConcept_THFTYPE_IiIiooIoI tptp.lContentBearingObject_THFTYPE_i) tptp.containsInformation_THFTYPE_IiooI)) % 1.53/1.72 (assume @p127 (_ (_ @t155 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p128 (_ (_ @t166 tptp.n2_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p129 (_ (_ (_ tptp.domain_THFTYPE_IIiioIiioI tptp.range_THFTYPE_IiioI) tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p130 (_ (_ @t167 tptp.n2_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p131 (_ @t168 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p132 (_ @t150 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p133 (_ @t169 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p134 (_ @t170 tptp.lUnaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p135 (_ @t171 tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p136 (_ (_ tptp.subrelation_THFTYPE_IiioI tptp.result_THFTYPE_i) tptp.patient_THFTYPE_i)) % 1.53/1.72 (assume @p137 (_ (_ @t172 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p138 (_ (_ @t173 tptp.n1_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p139 (_ (_ @t174 tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 1.53/1.72 (assume @p140 (_ @t175 tptp.lUnaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p141 (_ @t176 tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (assume @p142 (_ @t177 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p143 (_ (_ @t178 tptp.n2_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p144 (_ (_ @t172 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p145 (_ (_ (_ tptp.domain_THFTYPE_IIiioIiioI tptp.member_THFTYPE_IiioI) tptp.n1_THFTYPE_i) tptp.lSelfConnectedObject_THFTYPE_i)) % 1.53/1.72 (assume @p146 (_ (_ @t179 tptp.n1_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p147 (_ (_ @t180 tptp.n3_THFTYPE_i) tptp.lPositionalAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p148 (_ (_ tptp.instance_THFTYPE_IiioI tptp.documentation_THFTYPE_i) tptp.lTernaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p149 (_ @t181 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p150 (_ @t151 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p151 (_ (_ @t182 tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 1.53/1.72 (assume @p152 (_ (_ tptp.instance_THFTYPE_IIiiioIioI tptp.orientation_THFTYPE_IiiioI) tptp.lTernaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p153 (_ (_ @t183 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p154 (_ @t176 tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p155 (_ (_ tptp.instance_THFTYPE_IIiooIioI tptp.knows_THFTYPE_IiooI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p156 (_ (_ @t184 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p157 (_ @t177 tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (assume @p158 (_ @t185 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p159 (_ (_ @t186 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p160 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subrelation_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p161 (_ (_ tptp.relatedInternalConcept_THFTYPE_IIiioIIiioIoI tptp.disjointRelation_THFTYPE_IiioI) tptp.disjoint_THFTYPE_IiioI)) % 1.53/1.72 (assume @p162 (_ (_ @t166 tptp.n1_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p163 (_ (_ tptp.subrelation_THFTYPE_IIiioIIiioIoI tptp.member_THFTYPE_IiioI) tptp.part_THFTYPE_IiioI)) % 1.53/1.72 (assume @p164 (_ (_ @t187 tptp.n1_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p165 (_ @t188 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p166 (_ (_ (_ tptp.domain_THFTYPE_IIiiIiioI tptp.lBeginFn_THFTYPE_IiiI) tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p167 (_ @t163 tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (assume @p168 (_ (_ @t178 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p169 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.instance_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p170 (_ @t169 tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p171 (_ @t189 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p172 (_ (_ @t190 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p173 (_ (_ @t191 tptp.n1_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p174 (_ (_ tptp.instance_THFTYPE_IoioI true) tptp.lTruthValue_THFTYPE_i)) % 1.53/1.72 (assume @p175 (_ (_ @t187 tptp.n2_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p176 (_ @t192 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p177 (_ (_ tptp.subrelation_THFTYPE_IiIiioIoI tptp.modalAttribute_THFTYPE_i) tptp.property_THFTYPE_IiioI)) % 1.53/1.72 (assume @p178 (_ (_ @t193 tptp.n2_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p179 (_ (_ @t194 tptp.n1_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p180 (_ (_ (_ tptp.domain_THFTYPE_IIiiIiioI tptp.lYearFn_THFTYPE_IiiI) tptp.n1_THFTYPE_i) tptp.lInteger_THFTYPE_i)) % 1.53/1.72 (assume @p181 (_ @t154 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p182 (_ (_ tptp.instance_THFTYPE_IIIiioIiioIioI tptp.domain_THFTYPE_IIiioIiioI) tptp.lTernaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p183 (_ (_ @t183 tptp.n3_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p184 (_ @t181 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p185 (_ @t175 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p186 (_ (_ (_ tptp.domain_THFTYPE_IiiioI tptp.documentation_THFTYPE_i) tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p187 (_ @t195 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p188 (_ (_ tptp.relatedInternalConcept_THFTYPE_IiIiiIoI tptp.lYear_THFTYPE_i) tptp.lYearFn_THFTYPE_IiiI)) % 1.53/1.72 (assume @p189 (_ (_ @t160 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p190 (_ @t175 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p191 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.disjoint_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p192 (_ (_ tptp.subrelation_THFTYPE_IiIiioIoI tptp.attribute_THFTYPE_i) tptp.property_THFTYPE_IiioI)) % 1.53/1.72 (assume @p193 (_ @t192 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p194 (_ @t177 tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p195 (_ (_ @t196 tptp.n2_THFTYPE_i) tptp.lList_THFTYPE_i)) % 1.53/1.72 (assume @p196 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subProcess_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p197 (_ @t176 tptp.lTransitiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p198 (_ (_ tptp.instance_THFTYPE_IoioI false) tptp.lTruthValue_THFTYPE_i)) % 1.53/1.72 (assume @p199 (_ @t197 tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p200 (_ @t153 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p201 (_ (_ (_ tptp.domain_THFTYPE_IIiooIiioI tptp.holdsDuring_THFTYPE_IiooI) tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 1.53/1.72 (assume @p202 (_ @t176 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p203 (_ @t188 tptp.lUnaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p204 (_ @t198 tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p205 (_ (_ @t196 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p206 (_ (_ @t173 tptp.n2_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p207 (_ @t188 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p208 (_ @t149 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p209 (_ (_ @t156 tptp.n1_THFTYPE_i) tptp.lMonth_THFTYPE_i)) % 1.53/1.72 (assume @p210 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subclass_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p211 (_ (_ @t179 tptp.n2_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 1.53/1.72 (assume @p212 (_ (_ @t184 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p213 (_ @t199 tptp.lUnaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p214 (_ @t181 tptp.lIrreflexiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p215 (_ (_ @t200 tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p216 (_ (_ tptp.instance_THFTYPE_IIiooIioI tptp.believes_THFTYPE_IiooI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p217 (_ (_ @t174 tptp.n1_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 1.53/1.72 (assume @p218 (_ @t199 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p219 (_ (_ (_ tptp.domain_THFTYPE_IIiiiIiioI tptp.lTemporalCompositionFn_THFTYPE_IiiiI) tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p220 (_ (_ @t186 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 1.53/1.72 (assume @p221 (_ @t185 tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p222 (_ (_ @t200 tptp.n1_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p223 (_ (_ @t201 tptp.n2_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p224 (_ @t165 tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (assume @p225 (_ (_ (_ tptp.domainSubclass_THFTYPE_IIiiiIiioI tptp.lTemporalCompositionFn_THFTYPE_IiiiI) tptp.n2_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p226 (_ (_ (_ tptp.domain_THFTYPE_IIiooIiioI tptp.containsInformation_THFTYPE_IiooI) tptp.n2_THFTYPE_i) tptp.lProposition_THFTYPE_i)) % 1.53/1.72 (assume @p227 (_ @t168 tptp.lUnaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p228 (_ (_ @t180 tptp.n2_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p229 (_ (_ tptp.relatedInternalConcept_THFTYPE_IiioI tptp.lDay_THFTYPE_i) tptp.lDayDuration_THFTYPE_i)) % 1.53/1.72 (assume @p230 (_ (_ @t202 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p231 (_ (_ tptp.disjointRelation_THFTYPE_IiioI tptp.result_THFTYPE_i) tptp.instrument_THFTYPE_i)) % 1.53/1.72 (assume @p232 (_ @t198 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p233 (_ (_ @t193 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 1.53/1.72 (assume @p234 (_ @t151 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p235 (_ @t152 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p236 (_ (_ @t161 tptp.n2_THFTYPE_i) tptp.lTruthValue_THFTYPE_i)) % 1.53/1.72 (assume @p237 (_ @t163 tptp.lBinaryFunction_THFTYPE_i)) % 1.53/1.72 (assume @p238 (_ (_ @t190 tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p239 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subAttribute_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p240 (_ (_ @t201 tptp.n1_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p241 (_ (_ (_ tptp.domain_THFTYPE_IIiioIiioI tptp.duration_THFTYPE_IiioI) tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p242 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.member_THFTYPE_IiioI) tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p243 (_ (_ @t167 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 1.53/1.72 (assume @p244 (_ @t199 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p245 (_ (_ tptp.instance_THFTYPE_IIIioIiioIioI tptp.domainSubclass_THFTYPE_IIioIiioI) tptp.lTernaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p246 (_ (_ @t164 tptp.n2_THFTYPE_i) tptp.lAgent_THFTYPE_i)) % 1.53/1.72 (assume @p247 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.property_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p248 (_ (_ (_ tptp.domain_THFTYPE_IIiiiIiioI tptp.lListOrderFn_THFTYPE_IiiiI) tptp.n1_THFTYPE_i) tptp.lList_THFTYPE_i)) % 1.53/1.72 (assume @p249 (_ (_ @t159 tptp.n2_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p250 (_ (_ @t191 tptp.n2_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p251 (_ @t189 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p252 (_ (_ (_ tptp.domainSubclass_THFTYPE_IIiioIiioI tptp.rangeSubclass_THFTYPE_IiioI) tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p253 (_ @t158 tptp.lTransitiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p254 (_ (_ tptp.relatedInternalConcept_THFTYPE_IIiioIIiioIoI tptp.member_THFTYPE_IiioI) tptp.instance_THFTYPE_IiioI)) % 1.53/1.72 (assume @p255 (_ (_ (_ tptp.domain_THFTYPE_IiiioI tptp.modalAttribute_THFTYPE_i) tptp.n1_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 1.53/1.72 (assume @p256 (_ (_ @t162 tptp.n1_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p257 (_ (_ tptp.subrelation_THFTYPE_IiioI tptp.instrument_THFTYPE_i) tptp.patient_THFTYPE_i)) % 1.53/1.72 (assume @p258 (_ (_ @t182 tptp.n1_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 1.53/1.72 (assume @p259 (_ (_ (_ tptp.domain_THFTYPE_IIiiIiioI tptp.lEndFn_THFTYPE_IiiI) tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 1.53/1.72 (assume @p260 (_ @t197 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p261 (_ (_ @t180 tptp.n1_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p262 (_ @t170 tptp.lTotalValuedRelation_THFTYPE_i)) % 1.53/1.72 (assume @p263 (_ @t158 tptp.lRelationExtendedToQuantities_THFTYPE_i)) % 1.53/1.72 (assume @p264 (_ @t171 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p265 (_ (_ (_ tptp.domain_THFTYPE_IiiioI tptp.attribute_THFTYPE_i) tptp.n1_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 1.53/1.72 (assume @p266 (_ (_ tptp.subrelation_THFTYPE_IIoooIIiioIoI tptp.truth_THFTYPE_IoooI) tptp.property_THFTYPE_IiioI)) % 1.53/1.72 (assume @p267 (_ (_ @t194 tptp.n2_THFTYPE_i) tptp.lQuantity_THFTYPE_i)) % 1.53/1.72 (assume @p268 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.located_THFTYPE_IiioI) tptp.lTransitiveRelation_THFTYPE_i)) % 1.53/1.72 (assume @p269 (_ @t171 tptp.lAsymmetricRelation_THFTYPE_i)) % 1.53/1.72 (assume @p270 (_ (_ @t202 tptp.n3_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 1.53/1.72 (assume @p271 (_ @t195 tptp.lBinaryPredicate_THFTYPE_i)) % 1.53/1.72 (assume @p272 (_ @t170 tptp.lTemporalRelation_THFTYPE_i)) % 1.53/1.72 (assume @p273 @t203) % 1.53/1.72 (assume @p274 true) % 1.53/1.72 (step @p275 :rule evaluate :args ((= true false))) % 1.53/1.72 (step @p276 :rule refl :args ((tptp.holdsDuring_THFTYPE_IiooI @t120 @t204))) % 1.53/1.72 (step @p277 :rule refl :args (@t204)) % 1.53/1.72 (step @p278 :rule refl :args (@t205)) % 1.53/1.72 (step @p279 :rule cong :premises (@p278 @p277) :args (@t206)) % 1.53/1.72 (step @p280 :rule trans :premises (@p279 @p276)) % 1.53/1.72 (step @p281 :rule refl :args (tptp.holdsDuring_THFTYPE_IiooI)) % 1.53/1.72 (step @p282 :rule ho_cong :premises (@p281 @p278)) % 1.53/1.72 (step @p283 :rule ho_cong :premises (@p282 @p277)) % 1.53/1.72 (step @p284 :rule cong :premises (@p283 @p280) :args ((= (_ @t207 @t204) @t206))) % 1.53/1.72 (step @p285 :rule symm :premises (@p284)) % 1.53/1.72 (step @p286 :rule refl :args ((_ @t121 @t204))) % 1.53/1.72 (step @p287 :rule eq_resolve :premises (@p286 @p285)) % 1.53/1.72 (step @p288 :rule evaluate :args ((not false))) % 1.53/1.73 (step @p289 :rule skolem_intro :args (@t204)) % 1.53/1.73 (step @p290 :rule cong :premises (@p289) :args ((not @t204))) % 1.53/1.73 (step @p291 :rule bool-eq-false :args (@t204)) % 1.53/1.73 (step @p292 :rule eq-symm :args (false @t204)) % 1.53/1.73 (step @p293 :rule trans :premises (@p292 @p291)) % 1.53/1.73 (step @p294 :rule trans :premises (@p293 @p290 @p288)) % 1.53/1.73 (step @p295 :rule true_elim :premises (@p294)) % 1.53/1.73 (step @p296 :rule refl :args (@t120)) % 1.53/1.73 (step @p297 :rule cong :premises (@p296 @p278) :args ((= @t120 @t205))) % 1.53/1.73 (step @p298 :rule symm :premises (@p297)) % 1.53/1.73 (step @p299 :rule eq_resolve :premises (@p296 @p298)) % 1.53/1.73 (step @p300 :rule refl :args (tptp.holdsDuring_THFTYPE_IiooI)) % 1.53/1.73 (step @p301 :rule ho_cong :premises (@p300 @p299)) % 1.53/1.73 (step @p302 :rule ho_cong :premises (@p301 @p295)) % 1.53/1.73 (step @p303 :rule trans :premises (@p302 @p287)) % 1.53/1.73 (step @p304 :rule cong :premises (@p303) :args (@t203)) % 1.53/1.73 (step @p305 :rule eq_resolve :premises (@p273 @p304)) % 1.53/1.73 (step @p306 :rule false_intro :premises (@p305)) % 1.53/1.73 (step @p307 :rule refl :args (@t208)) % 1.53/1.73 (step @p308 :rule refl :args (@t137)) % 1.53/1.73 (step @p309 :rule cong :premises (@p308 @p307) :args ((= @t137 @t208))) % 1.53/1.73 (step @p310 :rule symm :premises (@p309)) % 1.53/1.73 (step @p311 :rule eq_resolve :premises (@p308 @p310)) % 1.53/1.73 (step @p312 :rule eq_resolve :premises (@p83 @p311)) % 1.53/1.73 (step @p313 :rule eq-refl :args (@t209)) % 1.53/1.73 (step @p314 :rule skolem_intro :args (@t210)) % 1.53/1.73 (step @p315 :rule refl :args (@t209)) % 1.53/1.73 (step @p316 :rule cong :premises (@p315 @p314) :args ((= @t209 @t210))) % 1.53/1.73 (step @p317 :rule trans :premises (@p316 @p313)) % 1.53/1.73 (step @p318 :rule true_elim :premises (@p317)) % 1.53/1.73 (step @p319 :rule equiv_elim2 :premises (@p318)) % 1.53/1.73 (step @p320 :rule chain_m_resolution :premises (@p319 @p312) :args ((not @t210) @t211 (@list @t208))) % 1.53/1.73 (step @p321 :rule false_intro :premises (@p320)) % 1.53/1.73 (step @p322 :rule trans :premises (@p321 @p295)) % 1.53/1.73 (step @p323 :rule refl :args (@t205)) % 1.53/1.73 (step @p324 :rule cong :premises (@p323 @p322) :args (@t212)) % 1.53/1.73 (step @p325 :rule refl :args ((tptp.holdsDuring_THFTYPE_IiooI @t120 @t119))) % 1.53/1.73 (step @p326 :rule refl :args (@t213)) % 1.53/1.73 (step @p327 :rule cong :premises (@p326) :args (@t214)) % 1.53/1.73 (step @p328 :rule cong :premises (@p278 @p327) :args (@t215)) % 1.53/1.73 (step @p329 :rule trans :premises (@p328 @p325)) % 1.53/1.73 (step @p330 :rule ho_cong :premises (@p282 @p327)) % 1.53/1.73 (step @p331 :rule cong :premises (@p330 @p329) :args ((= (_ @t207 @t214) @t215))) % 1.53/1.73 (step @p332 :rule symm :premises (@p331)) % 1.53/1.73 (step @p333 :rule refl :args (@t122)) % 1.53/1.73 (step @p334 :rule eq_resolve :premises (@p333 @p332)) % 1.53/1.73 (step @p335 :rule refl :args (@t118)) % 1.53/1.73 (step @p336 :rule cong :premises (@p335 @p326) :args ((= @t118 @t213))) % 1.53/1.73 (step @p337 :rule symm :premises (@p336)) % 1.53/1.73 (step @p338 :rule eq_resolve :premises (@p335 @p337)) % 1.53/1.73 (step @p339 :rule cong :premises (@p338) :args (@t119)) % 1.53/1.73 (step @p340 :rule eq_resolve :premises (@p296 @p298)) % 1.53/1.73 (step @p341 :rule ho_cong :premises (@p281 @p340)) % 1.53/1.73 (step @p342 :rule ho_cong :premises (@p341 @p339)) % 1.53/1.73 (step @p343 :rule trans :premises (@p342 @p334)) % 1.53/1.73 (step @p344 :rule cong :premises (@p343) :args (@t124)) % 1.53/1.73 (step @p345 :rule eq_resolve :premises (@p69 @p344)) % 1.53/1.73 (step @p346 :rule cong :premises (@p323 @p318) :args (@t216)) % 1.53/1.73 (step @p347 :rule refl :args (@t217)) % 1.53/1.73 (step @p348 :rule cong :premises (@p347 @p346) :args ((=> @t217 @t216))) % 1.53/1.73 (assume-push @p360 @t217) % 1.53/1.73 (step @p350 :rule instantiate :premises (@p345) :args ((@list tptp.lBill_THFTYPE_i))) % 1.53/1.73 (step-pop @p361 :rule scope :premises (@p350)) % 1.53/1.73 (step @p351 :rule process_scope :premises (@p361) :args (@t216)) % 1.53/1.73 (step @p353 :rule eq_resolve :premises (@p351 @p348)) % 1.53/1.73 (step @p354 :rule implies_elim :premises (@p353)) % 1.53/1.73 (step @p355 :rule chain_m_resolution :premises (@p354 @p345) :args (@t212 @t211 (@list @t217))) % 1.53/1.73 (step @p356 :rule true_intro :premises (@p355)) % 1.53/1.73 (step @p357 :rule symm :premises (@p356)) % 1.53/1.73 (step @p358 :rule trans :premises (@p357 @p324 @p306)) % 1.53/1.73 (step @p359 false :rule eq_resolve :premises (@p358 @p275)) % 1.53/1.73 ) % 1.53/1.73 % SZS output end Proof % 1.53/1.73 % cvc5 exiting %------------------------------------------------------------------------------