%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : CSR138^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 : n023.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:04 AM UTC 2026 % Result : Theorem 151.25s 151.52s % Output : Proof 151.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR138^2 : TPTP v9.2.1. Released v4.1.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n023.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon Jun 1 21:58:28 EDT 2026 % 0.17/0.35 % CPUTime : % 0.32/0.53 %----Proving TH0 % 151.25/151.52 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 151.25/151.52 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --mbqi-enum-choice-grammar-all --no-cegqi --no-sygus-inst at 30s... % 151.25/151.52 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-mbqi-nested-check --no-cegqi --no-sygus-inst at 30s... % 151.25/151.52 --- Run --ho-elim --full-saturate-quant at 18s... % 151.25/151.52 % SZS status Theorem % 151.25/151.52 % SZS output start Proof % 151.25/151.52 ( % 151.25/151.52 (declare-sort $$unsorted 0) % 151.25/151.52 (declare-const tptp.subrelation_THFTYPE_IIoooIIiioIoI (-> (-> Bool Bool Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.52 (declare-const tptp.domain_THFTYPE_IIiiiIiioI (-> (-> $$unsorted $$unsorted $$unsorted) $$unsorted $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.instance_THFTYPE_IIIioIiioIioI (-> (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool) $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.domain_THFTYPE_IIIioIiioIiioI (-> (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.lMeasureFn_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.instance_THFTYPE_IIIiioIiioIioI (-> (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool) $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.disjointRelation_THFTYPE_IiIiioIoI (-> $$unsorted (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.52 (declare-const tptp.subrelation_THFTYPE_IiIiioIoI (-> $$unsorted (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.52 (declare-const tptp.partition_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.domain_THFTYPE_IIiiIiioI (-> (-> $$unsorted $$unsorted) $$unsorted $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.subrelation_THFTYPE_IIiioIIiioIoI (-> (-> $$unsorted $$unsorted Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.52 (declare-const tptp.relatedInternalConcept_THFTYPE_IIioIIiioIoI (-> (-> $$unsorted Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.52 (declare-const tptp.relatedInternalConcept_THFTYPE_IIiioIIiioIoI (-> (-> $$unsorted $$unsorted Bool) (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.52 (declare-const tptp.instance_THFTYPE_IIiooIioI (-> (-> $$unsorted Bool Bool) $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.domain_THFTYPE_IIiiioIiioI (-> (-> $$unsorted $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.instance_THFTYPE_IIiiioIioI (-> (-> $$unsorted $$unsorted $$unsorted Bool) $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.lTernaryPredicate_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.lMultiplicationFn_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.n3_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.domain_THFTYPE_IIiooIiioI (-> (-> $$unsorted Bool Bool) $$unsorted $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.lFormula_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.result_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.patient_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.modalAttribute_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.instance_THFTYPE_IIiiIioI (-> (-> $$unsorted $$unsorted) $$unsorted Bool)) % 151.25/151.52 (declare-const tptp.lUnaryFunction_THFTYPE_i $$unsorted) % 151.25/151.52 (declare-const tptp.instance_THFTYPE_IIiiiIioI (-> (-> $$unsorted $$unsorted $$unsorted) $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lBinaryFunction_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.instance_THFTYPE_IIiIiioIoIioI (-> (-> $$unsorted (-> $$unsorted $$unsorted Bool) Bool) $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.relatedInternalConcept_THFTYPE_IiIiioIoI (-> $$unsorted (-> $$unsorted $$unsorted Bool) Bool)) % 151.25/151.53 (declare-const tptp.relatedExternalConcept_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.relatedInternalConcept_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.equal_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.n1_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lBinaryPredicate_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.domain_THFTYPE_IIiioIiioI (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.n2_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lKappaFn_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lAttribute_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.instrument_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.disjointDecomposition_THFTYPE_IioI (-> $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lWhenFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 151.25/151.53 (declare-const tptp.lBob_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lOrganization_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.member_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.subrelation_THFTYPE_IIiioIioI (-> (-> $$unsorted $$unsorted Bool) $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.believes_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 151.25/151.53 (declare-const tptp.domain_THFTYPE_IIioIiioI (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lSue_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lSelfConnectedObject_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lObject_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lAsymmetricRelation_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.property_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.range_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lListFn_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lEntity_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.attribute_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.subclass_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.subAttribute_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lContentBearingObject_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.inList_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lSymbolicString_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lListFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 151.25/151.53 (declare-const tptp.disjointRelation_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.subrelation_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lList_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.orientation_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.instance_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.subProcess_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.agent_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lBeginFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 151.25/151.53 (declare-const tptp.lAgent_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.part_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.knows_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 151.25/151.53 (declare-const tptp.lAnna_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.temporalPart_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.disjoint_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lMary_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.parent_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lBen_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lClass_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.disjointDecomposition_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.located_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lLanguage_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.subrelation_THFTYPE_IIioIIioIoI (-> (-> $$unsorted Bool) (-> $$unsorted Bool) Bool)) % 151.25/151.53 (declare-const tptp.contraryAttribute_THFTYPE_IioI (-> $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lSetOrClass_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.domainSubclass_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lIrreflexiveRelation_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.likes_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lLinguisticExpression_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.documentation_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.truth_THFTYPE_IoooI (-> Bool Bool Bool)) % 151.25/151.53 (declare-const tptp.lListOrderFn_THFTYPE_IiiiI (-> $$unsorted $$unsorted $$unsorted)) % 151.25/151.53 (declare-const tptp.lRelation_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lTemporalRelation_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lProcess_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lIntentionalProcess_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.domainSubclass_THFTYPE_IIioIiioI (-> (-> $$unsorted Bool) $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.domain_THFTYPE_IiiioI (-> $$unsorted $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lText_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lCognitiveAgent_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lHuman_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lOrganism_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.holdsDuring_THFTYPE_IiooI (-> $$unsorted Bool Bool)) % 151.25/151.53 (declare-const tptp.lBill_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lTimeInterval_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lWhenFn_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lEndFn_THFTYPE_IiiI (-> $$unsorted $$unsorted)) % 151.25/151.53 (declare-const tptp.meetsTemporally_THFTYPE_IiioI (-> $$unsorted $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lListOrderFn_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.instance_THFTYPE_IIiioIioI (-> (-> $$unsorted $$unsorted Bool) $$unsorted Bool)) % 151.25/151.53 (declare-const tptp.lTotalValuedRelation_THFTYPE_i $$unsorted) % 151.25/151.53 (declare-const tptp.lHumanLanguage_THFTYPE_i $$unsorted) % 151.25/151.53 (define @t1 () (_ tptp.parent_THFTYPE_IiioI tptp.lMary_THFTYPE_i)) % 151.25/151.53 (define @t2 () (_ @t1 tptp.lAnna_THFTYPE_i)) % 151.25/151.53 (define @t3 () (@var "Y" $$unsorted)) % 151.25/151.53 (define @t4 () (@var "Z" $$unsorted)) % 151.25/151.53 (define @t5 () (_ tptp.instance_THFTYPE_IiioI @t4)) % 151.25/151.53 (define @t6 () (@var "X" $$unsorted)) % 151.25/151.53 (define @t7 () (_ (_ tptp.subclass_THFTYPE_IiioI @t6) @t3)) % 151.25/151.53 (define @t8 () (@list @t6 @t3)) % 151.25/151.53 (define @t9 () (_ (_ tptp.likes_THFTYPE_IiioI @t6) @t3)) % 151.25/151.53 (define @t10 () (not @t9)) % 151.25/151.53 (define @t11 () (exists @t8 @t10)) % 151.25/151.53 (define @t12 () (@var "CLASS" $$unsorted)) % 151.25/151.53 (define @t13 () (_ tptp.subclass_THFTYPE_IiioI @t12)) % 151.25/151.53 (define @t14 () (@list @t12)) % 151.25/151.53 (define @t15 () (@var "THING" $$unsorted)) % 151.25/151.53 (define @t16 () (_ tptp.instance_THFTYPE_IiioI @t15)) % 151.25/151.53 (define @t17 () (_ @t16 tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (define @t18 () (@list @t15)) % 151.25/151.53 (define @t19 () (@var "OBJ2" $$unsorted)) % 151.25/151.53 (define @t20 () (@var "SUB" $$unsorted)) % 151.25/151.53 (define @t21 () (_ tptp.located_THFTYPE_IiioI @t20)) % 151.25/151.53 (define @t22 () (@var "OBJ1" $$unsorted)) % 151.25/151.53 (define @t23 () (@list @t20)) % 151.25/151.53 (define @t24 () (@var "AGENT" $$unsorted)) % 151.25/151.53 (define @t25 () (@var "PROC" $$unsorted)) % 151.25/151.53 (define @t26 () (_ (_ tptp.agent_THFTYPE_IiioI @t25) @t24)) % 151.25/151.53 (define @t27 () (@list @t25)) % 151.25/151.53 (define @t28 () (_ tptp.instance_THFTYPE_IiioI @t24)) % 151.25/151.53 (define @t29 () (_ @t28 tptp.lAgent_THFTYPE_i)) % 151.25/151.53 (define @t30 () (@list @t24)) % 151.25/151.53 (define @t31 () (@var "ATTR2" $$unsorted)) % 151.25/151.53 (define @t32 () (_ (_ tptp.orientation_THFTYPE_IiiioI @t22) @t19)) % 151.25/151.53 (define @t33 () (@var "ATTR1" $$unsorted)) % 151.25/151.53 (define @t34 () (= @t33 @t31)) % 151.25/151.53 (define @t35 () (@var "ROW" $$unsorted)) % 151.25/151.53 (define @t36 () (_ tptp.lListFn_THFTYPE_IiiI @t35)) % 151.25/151.53 (define @t37 () (_ tptp.contraryAttribute_THFTYPE_IioI @t35)) % 151.25/151.53 (define @t38 () (_ (_ tptp.subAttribute_THFTYPE_IiioI @t33) @t31)) % 151.25/151.53 (define @t39 () (@var "CLASS1" $$unsorted)) % 151.25/151.53 (define @t40 () (@var "CLASS2" $$unsorted)) % 151.25/151.53 (define @t41 () (or (_ (_ tptp.subclass_THFTYPE_IiioI @t39) @t40) (_ (_ tptp.subclass_THFTYPE_IiioI @t40) @t39))) % 151.25/151.53 (define @t42 () (@var "NUMBER" $$unsorted)) % 151.25/151.53 (define @t43 () (@var "REL" $$unsorted)) % 151.25/151.53 (define @t44 () (_ (_ tptp.domainSubclass_THFTYPE_IiiioI @t43) @t42)) % 151.25/151.53 (define @t45 () (@list @t42 @t39 @t43 @t40)) % 151.25/151.53 (define @t46 () (@var "REL2" $$unsorted)) % 151.25/151.53 (define @t47 () (@var "REL1" $$unsorted)) % 151.25/151.53 (define @t48 () (_ (_ tptp.disjointRelation_THFTYPE_IiioI @t47) @t46)) % 151.25/151.53 (define @t49 () (_ (_ tptp.disjoint_THFTYPE_IiioI @t39) @t40)) % 151.25/151.53 (define @t50 () (_ (_ tptp.domainSubclass_THFTYPE_IiiioI @t46) @t42)) % 151.25/151.53 (define @t51 () (_ (_ (_ tptp.domainSubclass_THFTYPE_IiiioI @t47) @t42) @t39)) % 151.25/151.53 (define @t52 () (@list @t46 @t42 @t39 @t40 @t47)) % 151.25/151.53 (define @t53 () (@var "FORMULA" Bool)) % 151.25/151.53 (define @t54 () (_ (_ tptp.knows_THFTYPE_IiooI @t24) @t53)) % 151.25/151.53 (define @t55 () (@list @t53 @t24)) % 151.25/151.53 (define @t56 () (_ (_ tptp.domain_THFTYPE_IiiioI @t43) @t42)) % 151.25/151.53 (define @t57 () (_ tptp.subclass_THFTYPE_IiioI tptp.lText_THFTYPE_i)) % 151.25/151.53 (define @t58 () (@var "ATTR" $$unsorted)) % 151.25/151.53 (define @t59 () (@var "THING2" $$unsorted)) % 151.25/151.53 (define @t60 () (@var "THING1" $$unsorted)) % 151.25/151.53 (define @t61 () (= @t60 @t59)) % 151.25/151.53 (define @t62 () (@list @t59 @t60)) % 151.25/151.53 (define @t63 () (_ (_ tptp.parent_THFTYPE_IiioI @t6) @t3)) % 151.25/151.53 (define @t64 () (not @t63)) % 151.25/151.53 (define @t65 () (exists @t8 @t64)) % 151.25/151.53 (define @t66 () (_ tptp.range_THFTYPE_IiioI @t46)) % 151.25/151.53 (define @t67 () (_ (_ tptp.range_THFTYPE_IiioI @t47) @t39)) % 151.25/151.53 (define @t68 () (@var "PARENT" $$unsorted)) % 151.25/151.53 (define @t69 () (@var "ORGANISM" $$unsorted)) % 151.25/151.53 (define @t70 () (@var "SITUATION" Bool)) % 151.25/151.53 (define @t71 () (@var "TIME" $$unsorted)) % 151.25/151.53 (define @t72 () (_ tptp.holdsDuring_THFTYPE_IiooI @t71)) % 151.25/151.53 (define @t73 () (@var "LIST2" $$unsorted)) % 151.25/151.53 (define @t74 () (@var "LIST1" $$unsorted)) % 151.25/151.53 (define @t75 () (= @t74 @t73)) % 151.25/151.53 (define @t76 () (@list @t42)) % 151.25/151.53 (define @t77 () (_ (_ tptp.likes_THFTYPE_IiioI tptp.lMary_THFTYPE_i) tptp.lBill_THFTYPE_i)) % 151.25/151.53 (define @t78 () (@var "INTERVAL2" $$unsorted)) % 151.25/151.53 (define @t79 () (_ tptp.lBeginFn_THFTYPE_IiiI @t78)) % 151.25/151.53 (define @t80 () (@var "INTERVAL1" $$unsorted)) % 151.25/151.53 (define @t81 () (_ tptp.lEndFn_THFTYPE_IiiI @t80)) % 151.25/151.53 (define @t82 () (@list @t80 @t78)) % 151.25/151.53 (define @t83 () (@var "TIME2" $$unsorted)) % 151.25/151.53 (define @t84 () (@var "TIME1" $$unsorted)) % 151.25/151.53 (define @t85 () (@var "ITEM" $$unsorted)) % 151.25/151.53 (define @t86 () (_ tptp.inList_THFTYPE_IiioI @t85)) % 151.25/151.53 (define @t87 () (_ (_ tptp.disjointDecomposition_THFTYPE_IiioI @t12) @t35)) % 151.25/151.53 (define @t88 () (@list @t12 @t35)) % 151.25/151.53 (define @t89 () (@var "INST" $$unsorted)) % 151.25/151.53 (define @t90 () (@var "REL" (-> $$unsorted $$unsorted Bool))) % 151.25/151.53 (define @t91 () (@list @t89)) % 151.25/151.53 (define @t92 () (@var "PRED1" $$unsorted)) % 151.25/151.53 (define @t93 () (@var "PRED2" $$unsorted)) % 151.25/151.53 (define @t94 () (_ tptp.lListOrderFn_THFTYPE_IiiiI @t36)) % 151.25/151.53 (define @t95 () (_ @t94 @t42)) % 151.25/151.53 (define @t96 () (@var "REL" (-> $$unsorted Bool))) % 151.25/151.53 (define @t97 () (_ @t96 @t35)) % 151.25/151.53 (define @t98 () (@list @t42 @t12 @t96 @t35)) % 151.25/151.53 (define @t99 () (@list @t39 @t40)) % 151.25/151.53 (define @t100 () (_ tptp.parent_THFTYPE_IiioI tptp.lSue_THFTYPE_i)) % 151.25/151.53 (define @t101 () (@var "REL2" (-> $$unsorted Bool))) % 151.25/151.53 (define @t102 () (@var "REL1" (-> $$unsorted Bool))) % 151.25/151.53 (define @t103 () (@var "ORG" $$unsorted)) % 151.25/151.53 (define @t104 () (_ tptp.range_THFTYPE_IiioI @t43)) % 151.25/151.53 (define @t105 () (_ tptp.instance_THFTYPE_IiioI @t89)) % 151.25/151.53 (define @t106 () (@var "SUBPROC" $$unsorted)) % 151.25/151.53 (define @t107 () (_ (_ tptp.subProcess_THFTYPE_IiioI @t106) @t25)) % 151.25/151.53 (define @t108 () (@list @t106 @t25)) % 151.25/151.53 (define @t109 () (@var "CHILD" $$unsorted)) % 151.25/151.53 (define @t110 () (_ (_ tptp.subrelation_THFTYPE_IiioI @t47) @t46)) % 151.25/151.53 (define @t111 () (@var "ELEMENT" $$unsorted)) % 151.25/151.53 (define @t112 () (_ tptp.instance_THFTYPE_IiioI @t111)) % 151.25/151.53 (define @t113 () (_ (_ tptp.inList_THFTYPE_IiioI @t111) @t36)) % 151.25/151.53 (define @t114 () (@list @t35 @t111)) % 151.25/151.53 (define @t115 () (@var "OBJ" $$unsorted)) % 151.25/151.53 (define @t116 () (_ tptp.property_THFTYPE_IiioI @t115)) % 151.25/151.53 (define @t117 () (_ @t116 @t31)) % 151.25/151.53 (define @t118 () (_ @t116 @t33)) % 151.25/151.53 (define @t119 () (@var "NUMBER2" $$unsorted)) % 151.25/151.53 (define @t120 () (@var "NUMBER1" $$unsorted)) % 151.25/151.53 (define @t121 () (_ tptp.property_THFTYPE_IiioI @t15)) % 151.25/151.53 (define @t122 () (@list @t31 @t33)) % 151.25/151.53 (define @t123 () (@var "REGION" $$unsorted)) % 151.25/151.53 (define @t124 () (@var "LANG" $$unsorted)) % 151.25/151.53 (define @t125 () (@var "PART" $$unsorted)) % 151.25/151.53 (define @t126 () (@var "TEXT" $$unsorted)) % 151.25/151.53 (define @t127 () (@var "PROCESS" $$unsorted)) % 151.25/151.53 (define @t128 () (@var "ROW2" $$unsorted)) % 151.25/151.53 (define @t129 () (_ tptp.lListFn_THFTYPE_IiiI @t128)) % 151.25/151.53 (define @t130 () (@var "ROW1" $$unsorted)) % 151.25/151.53 (define @t131 () (_ tptp.lListFn_THFTYPE_IiiI @t130)) % 151.25/151.53 (define @t132 () (@var "ITEM2" $$unsorted)) % 151.25/151.53 (define @t133 () (@var "ITEM1" $$unsorted)) % 151.25/151.53 (define @t134 () (@var "LIST" $$unsorted)) % 151.25/151.53 (define @t135 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.meetsTemporally_THFTYPE_IiioI)) % 151.25/151.53 (define @t136 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.range_THFTYPE_IiioI)) % 151.25/151.53 (define @t137 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.disjointRelation_THFTYPE_IiioI)) % 151.25/151.53 (define @t138 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.parent_THFTYPE_IiioI)) % 151.25/151.53 (define @t139 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subProcess_THFTYPE_IiioI)) % 151.25/151.53 (define @t140 () (_ tptp.domain_THFTYPE_IiiioI tptp.lKappaFn_THFTYPE_i)) % 151.25/151.53 (define @t141 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.meetsTemporally_THFTYPE_IiioI)) % 151.25/151.53 (define @t142 () (_ tptp.domain_THFTYPE_IiiioI tptp.equal_THFTYPE_i)) % 151.25/151.53 (define @t143 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.disjoint_THFTYPE_IiioI)) % 151.25/151.53 (define @t144 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.agent_THFTYPE_IiioI)) % 151.25/151.53 (define @t145 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subrelation_THFTYPE_IiioI)) % 151.25/151.53 (define @t146 () (_ tptp.instance_THFTYPE_IiioI tptp.attribute_THFTYPE_i)) % 151.25/151.53 (define @t147 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lWhenFn_THFTYPE_IiiI)) % 151.25/151.53 (define @t148 () (_ tptp.instance_THFTYPE_IiioI tptp.modalAttribute_THFTYPE_i)) % 151.25/151.53 (define @t149 () (_ tptp.domain_THFTYPE_IiiioI tptp.patient_THFTYPE_i)) % 151.25/151.53 (define @t150 () (_ tptp.domain_THFTYPE_IIiooIiioI tptp.believes_THFTYPE_IiooI)) % 151.25/151.53 (define @t151 () (_ tptp.domain_THFTYPE_IiiioI tptp.documentation_THFTYPE_i)) % 151.25/151.53 (define @t152 () (_ tptp.instance_THFTYPE_IiioI tptp.lMultiplicationFn_THFTYPE_i)) % 151.25/151.53 (define @t153 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.property_THFTYPE_IiioI)) % 151.25/151.53 (define @t154 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subAttribute_THFTYPE_IiioI)) % 151.25/151.53 (define @t155 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.inList_THFTYPE_IiioI)) % 151.25/151.53 (define @t156 () (_ tptp.domain_THFTYPE_IIiooIiioI tptp.knows_THFTYPE_IiooI)) % 151.25/151.53 (define @t157 () (_ tptp.domain_THFTYPE_IIiiioIiioI tptp.domain_THFTYPE_IiiioI)) % 151.25/151.53 (define @t158 () (_ tptp.domain_THFTYPE_IiiioI tptp.result_THFTYPE_i)) % 151.25/151.53 (define @t159 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.relatedInternalConcept_THFTYPE_IiioI)) % 151.25/151.53 (define @t160 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.part_THFTYPE_IiioI)) % 151.25/151.53 (define @t161 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lBeginFn_THFTYPE_IiiI)) % 151.25/151.53 (define @t162 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.instance_THFTYPE_IiioI)) % 151.25/151.53 (define @t163 () (_ tptp.instance_THFTYPE_IIiooIioI tptp.holdsDuring_THFTYPE_IiooI)) % 151.25/151.53 (define @t164 () (_ tptp.instance_THFTYPE_IIiioIioI tptp.temporalPart_THFTYPE_IiioI)) % 151.25/151.53 (define @t165 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.instrument_THFTYPE_IiioI)) % 151.25/151.53 (define @t166 () (_ tptp.domain_THFTYPE_IiiioI tptp.relatedExternalConcept_THFTYPE_i)) % 151.25/151.53 (define @t167 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.inList_THFTYPE_IiioI)) % 151.25/151.53 (define @t168 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.parent_THFTYPE_IiioI)) % 151.25/151.53 (define @t169 () (_ tptp.instance_THFTYPE_IiioI tptp.lMeasureFn_THFTYPE_i)) % 151.25/151.53 (define @t170 () (_ tptp.instance_THFTYPE_IIiiIioI tptp.lEndFn_THFTYPE_IiiI)) % 151.25/151.53 (define @t171 () (_ tptp.domain_THFTYPE_IIiioIiioI tptp.subclass_THFTYPE_IiioI)) % 151.25/151.53 (define @t172 () (_ tptp.domain_THFTYPE_IIiiioIiioI tptp.orientation_THFTYPE_IiiioI)) % 151.25/151.53 (define @t173 () (_ tptp.domain_THFTYPE_IIIioIiioIiioI tptp.domainSubclass_THFTYPE_IIioIiioI)) % 151.25/151.53 (define @t174 () (@var "W" $$unsorted)) % 151.25/151.53 (define @t175 () (lambda (@list @t4 @t174) true)) % 151.25/151.53 (define @t176 () (@var "Q" (-> $$unsorted $$unsorted Bool))) % 151.25/151.53 (define @t177 () (= @t176 @t175)) % 151.25/151.53 (define @t178 () (not @t177)) % 151.25/151.53 (define @t179 () (@var "R" (-> $$unsorted $$unsorted Bool))) % 151.25/151.53 (define @t180 () (= @t179 @t175)) % 151.25/151.53 (define @t181 () (not @t180)) % 151.25/151.53 (define @t182 () (_ (_ @t176 @t3) tptp.lAnna_THFTYPE_i)) % 151.25/151.53 (define @t183 () (_ (_ @t179 @t3) tptp.lBill_THFTYPE_i)) % 151.25/151.53 (define @t184 () (and @t183 @t182 @t181 @t178)) % 151.25/151.53 (define @t185 () (@list @t176 @t179 @t3)) % 151.25/151.53 (define @t186 () (exists @t185 @t184)) % 151.25/151.53 (define @t187 () (not @t186)) % 151.25/151.53 (define @t188 () (@const 0 (@ho-elim-sort (-> $$unsorted $$unsorted Bool)))) % 151.25/151.53 (define @t189 () (@const 1 (-> (@ho-elim-sort (-> $$unsorted $$unsorted Bool)) $$unsorted (@ho-elim-sort (-> $$unsorted Bool))))) % 151.25/151.53 (define @t190 () (@const 2 (-> (@ho-elim-sort (-> $$unsorted Bool)) $$unsorted Bool))) % 151.25/151.53 (define @t191 () (forall @t8 (_ @t190 (_ @t189 @t188 @t6) @t3))) % 151.25/151.53 (define @t192 () (tptp.likes_THFTYPE_IiioI @t6 @t3)) % 151.25/151.53 (define @t193 () (forall @t8 (not @t10))) % 151.25/151.53 (define @t194 () (not @t193)) % 151.25/151.53 (define @t195 () (@var "BOUND_VARIABLE_10806" (@ho-elim-sort (-> $$unsorted $$unsorted Bool)))) % 151.25/151.53 (define @t196 () (@const 3 (@ho-elim-sort (-> $$unsorted $$unsorted Bool)))) % 151.25/151.53 (define @t197 () (@var "BOUND_VARIABLE_10808" (@ho-elim-sort (-> $$unsorted $$unsorted Bool)))) % 151.25/151.53 (define @t198 () (not (_ @t190 (_ @t189 @t195 @t3) tptp.lAnna_THFTYPE_i))) % 151.25/151.53 (define @t199 () (not (_ @t190 (_ @t189 @t197 @t3) tptp.lBill_THFTYPE_i))) % 151.25/151.53 (define @t200 () (or @t199 @t198 (= @t197 @t196) (= @t195 @t196))) % 151.25/151.53 (define @t201 () (@list @t195 @t197 @t3)) % 151.25/151.53 (define @t202 () (forall @t201 @t200)) % 151.25/151.53 (define @t203 () (@const 4 (-> $$unsorted $$unsorted Bool))) % 151.25/151.53 (define @t204 () (_ @t176 @t3 tptp.lAnna_THFTYPE_i)) % 151.25/151.53 (define @t205 () (not @t204)) % 151.25/151.53 (define @t206 () (_ @t179 @t3 tptp.lBill_THFTYPE_i)) % 151.25/151.53 (define @t207 () (not @t206)) % 151.25/151.53 (define @t208 () (forall @t185 (or @t207 @t205 (= @t179 @t203) (= @t176 @t203)))) % 151.25/151.53 (define @t209 () (@var "BOUND_VARIABLE_9395" $$unsorted)) % 151.25/151.53 (define @t210 () (@var "BOUND_VARIABLE_9393" $$unsorted)) % 151.25/151.53 (define @t211 () (lambda (@list @t210 @t209) true)) % 151.25/151.53 (define @t212 () (= @t176 @t211)) % 151.25/151.53 (define @t213 () (= @t179 @t211)) % 151.25/151.53 (define @t214 () (forall @t185 (or @t207 @t205 @t213 @t212))) % 151.25/151.53 (define @t215 () (not @t182)) % 151.25/151.53 (define @t216 () (not @t183)) % 151.25/151.53 (define @t217 () (or @t216 @t215 @t213 @t212)) % 151.25/151.53 (define @t218 () (not @t212)) % 151.25/151.53 (define @t219 () (not @t218)) % 151.25/151.53 (define @t220 () (not @t213)) % 151.25/151.53 (define @t221 () (not @t220)) % 151.25/151.53 (define @t222 () (or @t216 @t215 @t221 @t219)) % 151.25/151.53 (define @t223 () (and @t183 @t182 @t220 @t218)) % 151.25/151.53 (define @t224 () (forall @t185 (not @t223))) % 151.25/151.53 (define @t225 () (not @t224)) % 151.25/151.53 (define @t226 () (@const 5 (@ho-elim-sort (-> $$unsorted $$unsorted Bool)))) % 151.25/151.53 (define @t227 () (_ @t190 (_ @t189 @t226 tptp.lMary_THFTYPE_i) tptp.lAnna_THFTYPE_i)) % 151.25/151.53 (define @t228 () (not @t227)) % 151.25/151.53 (define @t229 () (_ @t190 (_ @t189 @t188 tptp.lMary_THFTYPE_i) tptp.lBill_THFTYPE_i)) % 151.25/151.53 (define @t230 () (not @t229)) % 151.25/151.53 (define @t231 () (or @t230 @t228 (= @t196 @t188) (= @t196 @t226))) % 151.25/151.53 (define @t232 () (forall @t201 (or @t199 @t198 (= @t196 @t197) (= @t196 @t195)))) % 151.25/151.53 (define @t233 () (= @t226 @t196)) % 151.25/151.53 (define @t234 () (= @t188 @t196)) % 151.25/151.53 (define @t235 () (or @t230 @t228 @t234 @t233)) % 151.25/151.53 (define @t236 () (@var "BOUND_VARIABLE_9407" $$unsorted)) % 151.25/151.53 (define @t237 () (@var "BOUND_VARIABLE_9406" $$unsorted)) % 151.25/151.53 (define @t238 () (@list @t237 @t236)) % 151.25/151.53 (define @t239 () (forall @t238 (_ @t203 @t237 @t236))) % 151.25/151.53 (define @t240 () (forall @t8 (_ @t190 (_ @t189 @t226 @t6) @t3))) % 151.25/151.53 (define @t241 () (@quantifiers_skolemize @t240 1)) % 151.25/151.53 (define @t242 () (@quantifiers_skolemize @t240 0)) % 151.25/151.53 (define @t243 () (tptp.parent_THFTYPE_IiioI @t6 @t3)) % 151.25/151.53 (define @t244 () (forall @t8 (not @t64))) % 151.25/151.53 (define @t245 () (not @t244)) % 151.25/151.53 (define @t246 () (_ @t189 @t196 @t242)) % 151.25/151.53 (define @t247 () (_ @t190 @t246 @t241)) % 151.25/151.53 (define @t248 () (not @t247)) % 151.25/151.53 (define @t249 () (not @t233)) % 151.25/151.53 (define @t250 () (_ @t190 (_ @t189 @t226 @t242) @t241)) % 151.25/151.53 (define @t251 () (not @t250)) % 151.25/151.53 (define @t252 () (@quantifiers_skolemize @t191 1)) % 151.25/151.53 (define @t253 () (@quantifiers_skolemize @t191 0)) % 151.25/151.53 (define @t254 () (_ @t190 (_ @t189 @t196 @t253) @t252)) % 151.25/151.53 (define @t255 () (not @t254)) % 151.25/151.53 (define @t256 () (not @t234)) % 151.25/151.53 (define @t257 () (_ @t189 @t188 @t253)) % 151.25/151.53 (define @t258 () (_ @t190 @t257 @t252)) % 151.25/151.53 (define @t259 () (not @t258)) % 151.25/151.53 (define @t260 () (and @t254 @t234 @t259)) % 151.25/151.53 (assume @p1 @t2) % 151.25/151.53 (assume @p2 (forall (@list @t6 @t3 @t4) (=> (and @t7 (_ @t5 @t6)) (_ @t5 @t3)))) % 151.25/151.53 (assume @p3 (forall @t8 (=> @t7 (and (_ (_ tptp.instance_THFTYPE_IiioI @t6) tptp.lSetOrClass_THFTYPE_i) (_ (_ tptp.instance_THFTYPE_IiioI @t3) tptp.lSetOrClass_THFTYPE_i))))) % 151.25/151.53 (assume @p4 @t11) % 151.25/151.53 (assume @p5 (_ @t1 tptp.lBen_THFTYPE_i)) % 151.25/151.53 (assume @p6 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lLanguage_THFTYPE_i) tptp.lLinguisticExpression_THFTYPE_i)) % 151.25/151.53 (assume @p7 (forall @t14 (= (_ (_ tptp.instance_THFTYPE_IiioI @t12) tptp.lClass_THFTYPE_i) (_ @t13 tptp.lEntity_THFTYPE_i)))) % 151.25/151.53 (assume @p8 (forall @t18 @t17)) % 151.25/151.53 (assume @p9 (forall (@list @t22 @t19) (=> (_ (_ tptp.located_THFTYPE_IiioI @t22) @t19) (forall @t23 (=> (_ (_ tptp.part_THFTYPE_IiioI @t20) @t22) (_ @t21 @t19)))))) % 151.25/151.53 (assume @p10 (forall @t30 (= @t29 (exists @t27 @t26)))) % 151.25/151.53 (assume @p11 (forall (@list @t31 @t22 @t35 @t19 @t33) (=> (and (_ @t32 @t33) @t37 (_ (_ tptp.inList_THFTYPE_IiioI @t33) @t36) (_ (_ tptp.inList_THFTYPE_IiioI @t31) @t36) (not @t34)) (not (_ @t32 @t31))))) % 151.25/151.53 (assume @p12 (forall (@list @t12 @t31 @t33) (=> (and @t38 (_ (_ tptp.instance_THFTYPE_IiioI @t31) @t12)) (_ (_ tptp.instance_THFTYPE_IiioI @t33) @t12)))) % 151.25/151.53 (assume @p13 (_ (_ tptp.range_THFTYPE_IiioI tptp.lListFn_THFTYPE_i) tptp.lList_THFTYPE_i)) % 151.25/151.53 (assume @p14 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lAsymmetricRelation_THFTYPE_i) tptp.lIrreflexiveRelation_THFTYPE_i)) % 151.25/151.53 (assume @p15 (forall @t45 (=> (and (_ @t44 @t39) (_ @t44 @t40)) @t41))) % 151.25/151.53 (assume @p16 (forall @t52 (=> (and @t51 (_ @t50 @t40) @t49) @t48))) % 151.25/151.53 (assume @p17 (forall @t55 (=> @t54 (_ (_ tptp.truth_THFTYPE_IoooI @t53) true)))) % 151.25/151.53 (assume @p18 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lTemporalRelation_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p19 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lIntentionalProcess_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p20 (forall @t45 (=> (and (_ @t56 @t39) (_ @t56 @t40)) @t41))) % 151.25/151.53 (assume @p21 (_ @t57 tptp.lContentBearingObject_THFTYPE_i)) % 151.25/151.53 (assume @p22 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lClass_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p23 (forall @t62 (=> @t61 (forall (@list @t58) (= (_ (_ tptp.property_THFTYPE_IiioI @t60) @t58) (_ (_ tptp.property_THFTYPE_IiioI @t59) @t58)))))) % 151.25/151.53 (assume @p24 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lList_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p25 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lHuman_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 151.25/151.53 (assume @p26 @t65) % 151.25/151.53 (assume @p27 (forall (@list @t46 @t39 @t40 @t47) (=> (and @t67 (_ @t66 @t40) @t49) @t48))) % 151.25/151.53 (assume @p28 (forall (@list @t69) (=> (_ (_ tptp.instance_THFTYPE_IiioI @t69) tptp.lOrganism_THFTYPE_i) (exists (@list @t68) (_ (_ tptp.parent_THFTYPE_IiioI @t69) @t68))))) % 151.25/151.53 (assume @p29 (_ @t57 tptp.lLinguisticExpression_THFTYPE_i)) % 151.25/151.53 (assume @p30 (forall (@list @t71 @t70) (=> (_ @t72 (not @t70)) (not (_ @t72 @t70))))) % 151.25/151.53 (assume @p31 (forall (@list @t73 @t74) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t74) tptp.lList_THFTYPE_i) (_ (_ tptp.instance_THFTYPE_IiioI @t73) tptp.lList_THFTYPE_i) (forall @t76 (= (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t74) @t42) (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t73) @t42)))) @t75))) % 151.25/151.53 (assume @p32 @t77) % 151.25/151.53 (assume @p33 (_ (_ tptp.range_THFTYPE_IiioI tptp.lWhenFn_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 151.25/151.53 (assume @p34 (forall @t82 (= (_ (_ tptp.meetsTemporally_THFTYPE_IiioI @t80) @t78) (= @t81 @t79)))) % 151.25/151.53 (assume @p35 (forall (@list @t70 @t83 @t84) (=> (and (_ (_ tptp.holdsDuring_THFTYPE_IiooI @t84) @t70) (_ (_ tptp.temporalPart_THFTYPE_IiioI @t83) @t84)) (_ (_ tptp.holdsDuring_THFTYPE_IiooI @t83) @t70)))) % 151.25/151.53 (assume @p36 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lSymbolicString_THFTYPE_i) tptp.lContentBearingObject_THFTYPE_i)) % 151.25/151.53 (assume @p37 (exists @t18 @t17)) % 151.25/151.53 (assume @p38 (forall @t88 (=> @t87 (forall (@list @t85) (=> (_ @t86 @t36) (_ (_ tptp.subclass_THFTYPE_IiioI @t85) @t12)))))) % 151.25/151.53 (assume @p39 (_ (_ tptp.range_THFTYPE_IiioI tptp.lListOrderFn_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p40 (forall (@list @t90) (= (_ (_ tptp.instance_THFTYPE_IIiioIioI @t90) tptp.lIrreflexiveRelation_THFTYPE_i) (forall @t91 (not (_ (_ @t90 @t89) @t89)))))) % 151.25/151.53 (assume @p41 (forall (@list @t42 @t92 @t39 @t93) (=> (and (_ (_ tptp.subrelation_THFTYPE_IiioI @t92) @t93) (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t93) @t42) @t39)) (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t92) @t42) @t39)))) % 151.25/151.53 (assume @p42 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lTotalValuedRelation_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p43 (forall @t98 (=> (and (_ (_ (_ tptp.domainSubclass_THFTYPE_IIioIiioI @t96) @t42) @t12) @t97) (_ (_ tptp.subclass_THFTYPE_IiioI @t95) @t12)))) % 151.25/151.53 (assume @p44 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lHumanLanguage_THFTYPE_i) tptp.lLanguage_THFTYPE_i)) % 151.25/151.53 (assume @p45 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lSelfConnectedObject_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p46 (forall @t99 (=> (= @t39 @t40) (forall @t18 (= (_ @t16 @t39) (_ @t16 @t40)))))) % 151.25/151.53 (assume @p47 (_ @t100 tptp.lAnna_THFTYPE_i)) % 151.25/151.53 (assume @p48 (forall @t98 (=> (and (_ (_ (_ tptp.domain_THFTYPE_IIioIiioI @t96) @t42) @t12) @t97) (_ (_ tptp.instance_THFTYPE_IiioI @t95) @t12)))) % 151.25/151.53 (assume @p49 (forall (@list @t101 @t35 @t102) (=> (and (_ (_ tptp.subrelation_THFTYPE_IIioIIioIoI @t102) @t101) (_ @t102 @t35)) (_ @t101 @t35)))) % 151.25/151.53 (assume @p50 (forall @t55 (=> @t54 (_ (_ tptp.believes_THFTYPE_IiooI @t24) @t53)))) % 151.25/151.53 (assume @p51 (forall (@list @t103 @t24) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t103) tptp.lOrganization_THFTYPE_i) (_ (_ tptp.member_THFTYPE_IiioI @t24) @t103)) @t29))) % 151.25/151.53 (assume @p52 (forall @t62 (=> @t61 (forall @t14 (= (_ (_ tptp.instance_THFTYPE_IiioI @t60) @t12) (_ (_ tptp.instance_THFTYPE_IiioI @t59) @t12)))))) % 151.25/151.53 (assume @p53 (forall (@list @t39 @t43 @t40) (=> (and (_ @t104 @t39) (_ @t104 @t40)) @t41))) % 151.25/151.53 (assume @p54 (forall @t99 (= @t49 (forall @t91 (not (and (_ @t105 @t39) (_ @t105 @t40))))))) % 151.25/151.53 (assume @p55 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lOrganism_THFTYPE_i) tptp.lAgent_THFTYPE_i)) % 151.25/151.53 (assume @p56 (_ (_ tptp.likes_THFTYPE_IiioI tptp.lBob_THFTYPE_i) tptp.lBill_THFTYPE_i)) % 151.25/151.53 (assume @p57 (forall @t108 (=> @t107 (_ (_ tptp.temporalPart_THFTYPE_IiioI (_ tptp.lWhenFn_THFTYPE_IiiI @t106)) (_ tptp.lWhenFn_THFTYPE_IiiI @t25))))) % 151.25/151.53 (assume @p58 (forall (@list @t12 @t109 @t68) (=> (and (_ (_ tptp.parent_THFTYPE_IiioI @t109) @t68) (_ @t13 tptp.lOrganism_THFTYPE_i) (_ (_ tptp.instance_THFTYPE_IiioI @t68) @t12)) (_ (_ tptp.instance_THFTYPE_IiioI @t109) @t12)))) % 151.25/151.53 (assume @p59 (forall @t82 (=> (and (= (_ tptp.lBeginFn_THFTYPE_IiiI @t80) @t79) (= @t81 (_ tptp.lEndFn_THFTYPE_IiiI @t78))) (= @t80 @t78)))) % 151.25/151.53 (assume @p60 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lOrganization_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 151.25/151.53 (assume @p61 (forall (@list @t46 @t39 @t47) (=> (and @t110 (_ @t66 @t39)) @t67))) % 151.25/151.53 (assume @p62 (forall @t114 (=> (_ tptp.disjointDecomposition_THFTYPE_IioI @t35) (=> @t113 (_ @t112 tptp.lClass_THFTYPE_i))))) % 151.25/151.53 (assume @p63 (forall (@list @t115 @t119 @t35 @t120) (=> @t37 (forall (@list @t33 @t31) (=> (and (= @t33 (_ @t94 @t120)) (= @t31 (_ @t94 @t119)) (not (= @t120 @t119))) (=> @t118 (not @t117))))))) % 151.25/151.53 (assume @p64 (forall @t27 (=> (_ (_ tptp.instance_THFTYPE_IiioI @t25) tptp.lIntentionalProcess_THFTYPE_i) (exists @t30 (and (_ @t28 tptp.lCognitiveAgent_THFTYPE_i) @t26))))) % 151.25/151.53 (assume @p65 (forall (@list @t46 @t42 @t39 @t47) (=> (and @t110 (_ @t50 @t39)) @t51))) % 151.25/151.53 (assume @p66 (_ (_ tptp.subclass_THFTYPE_IiioI tptp.lAgent_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p67 (forall @t122 (=> @t34 (forall @t18 (= (_ @t121 @t33) (_ @t121 @t31)))))) % 151.25/151.53 (assume @p68 (_ (_ tptp.likes_THFTYPE_IiioI tptp.lSue_THFTYPE_i) tptp.lBill_THFTYPE_i)) % 151.25/151.53 (assume @p69 (forall @t108 (=> @t107 (forall (@list @t123) (=> (_ (_ tptp.located_THFTYPE_IiioI @t25) @t123) (_ (_ tptp.located_THFTYPE_IiioI @t106) @t123)))))) % 151.25/151.53 (assume @p70 (forall (@list @t124 @t24 @t25) (=> (and (_ (_ tptp.instance_THFTYPE_IiioI @t124) tptp.lHumanLanguage_THFTYPE_i) @t26 (_ (_ tptp.instrument_THFTYPE_IiioI @t25) @t124)) (_ @t28 tptp.lHuman_THFTYPE_i)))) % 151.25/151.53 (assume @p71 (forall @t122 (=> @t38 (forall (@list @t115) (=> @t118 @t117))))) % 151.25/151.53 (assume @p72 (forall (@list @t126) (=> (_ (_ tptp.instance_THFTYPE_IiioI @t126) tptp.lText_THFTYPE_i) (exists (@list @t125) (and (_ (_ tptp.part_THFTYPE_IiioI @t125) @t126) (_ (_ tptp.instance_THFTYPE_IiioI @t125) tptp.lLinguisticExpression_THFTYPE_i)))))) % 151.25/151.53 (assume @p73 (forall @t114 (=> @t37 (=> @t113 (_ @t112 tptp.lAttribute_THFTYPE_i))))) % 151.25/151.53 (assume @p74 (forall (@list @t115 @t127) (=> (_ (_ tptp.located_THFTYPE_IiioI @t127) @t115) (forall @t23 (=> (_ (_ tptp.subProcess_THFTYPE_IiioI @t20) @t127) (_ @t21 @t115)))))) % 151.25/151.53 (assume @p75 (_ (_ tptp.range_THFTYPE_IiioI tptp.lKappaFn_THFTYPE_i) tptp.lClass_THFTYPE_i)) % 151.25/151.53 (assume @p76 (forall (@list @t128 @t73 @t74 @t130) (=> @t75 (=> (and (= @t74 @t131) (= @t73 @t129)) (forall @t76 (= (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t131) @t42) (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t129) @t42))))))) % 151.25/151.53 (assume @p77 (forall @t52 (=> (and (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t47) @t42) @t39) (_ (_ (_ tptp.domain_THFTYPE_IiiioI @t46) @t42) @t40) @t49) @t48))) % 151.25/151.53 (assume @p78 (forall @t88 (=> @t87 (forall (@list @t133 @t132) (=> (and (_ (_ tptp.inList_THFTYPE_IiioI @t133) @t36) (_ (_ tptp.inList_THFTYPE_IiioI @t132) @t36) (not (= @t133 @t132))) (_ (_ tptp.disjoint_THFTYPE_IiioI @t133) @t132)))))) % 151.25/151.53 (assume @p79 (forall (@list @t85 @t134) (=> (_ @t86 @t134) (exists @t76 (= (_ (_ tptp.lListOrderFn_THFTYPE_IiiiI @t134) @t42) @t85))))) % 151.25/151.53 (assume @p80 (_ @t100 tptp.lBen_THFTYPE_i)) % 151.25/151.53 (assume @p81 (_ @t135 tptp.lTemporalRelation_THFTYPE_i)) % 151.25/151.53 (assume @p82 (_ @t136 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p83 (_ (_ @t137 tptp.n2_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p84 (_ @t138 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p85 (_ @t135 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p86 (_ (_ @t139 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p87 (_ (_ @t140 tptp.n1_THFTYPE_i) tptp.lSymbolicString_THFTYPE_i)) % 151.25/151.53 (assume @p88 (_ (_ @t141 tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 151.25/151.53 (assume @p89 (_ (_ @t142 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p90 (_ (_ tptp.relatedInternalConcept_THFTYPE_IiIiioIoI tptp.relatedExternalConcept_THFTYPE_i) tptp.relatedInternalConcept_THFTYPE_IiioI)) % 151.25/151.53 (assume @p91 (_ (_ @t143 tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p92 (_ (_ @t139 tptp.n2_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p93 (_ (_ (_ tptp.domain_THFTYPE_IIiioIiioI tptp.disjointDecomposition_THFTYPE_IiioI) tptp.n1_THFTYPE_i) tptp.lClass_THFTYPE_i)) % 151.25/151.53 (assume @p94 (_ (_ @t144 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p95 (_ (_ tptp.instance_THFTYPE_IiioI tptp.equal_THFTYPE_i) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p96 (_ (_ tptp.instance_THFTYPE_IIiIiioIoIioI tptp.relatedInternalConcept_THFTYPE_IiIiioIoI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p97 (_ (_ tptp.instance_THFTYPE_IIiiiIioI tptp.lListOrderFn_THFTYPE_IiiiI) tptp.lBinaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p98 (_ (_ @t137 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p99 (_ (_ @t145 tptp.n2_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p100 (_ (_ (_ tptp.domain_THFTYPE_IIiioIiioI tptp.range_THFTYPE_IiioI) tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p101 (_ @t146 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p102 (_ @t147 tptp.lUnaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p103 (_ @t148 tptp.lIrreflexiveRelation_THFTYPE_i)) % 151.25/151.53 (assume @p104 (_ (_ tptp.subrelation_THFTYPE_IiioI tptp.result_THFTYPE_i) tptp.patient_THFTYPE_i)) % 151.25/151.53 (assume @p105 (_ (_ @t149 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p106 (_ @t138 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p107 (_ (_ @t150 tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 151.25/151.53 (assume @p108 (_ (_ @t151 tptp.n3_THFTYPE_i) tptp.lSymbolicString_THFTYPE_i)) % 151.25/151.53 (assume @p109 (_ @t152 tptp.lTotalValuedRelation_THFTYPE_i)) % 151.25/151.53 (assume @p110 (_ (_ @t153 tptp.n2_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 151.25/151.53 (assume @p111 (_ (_ @t149 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p112 (_ (_ (_ tptp.domain_THFTYPE_IIiioIiioI tptp.member_THFTYPE_IiioI) tptp.n1_THFTYPE_i) tptp.lSelfConnectedObject_THFTYPE_i)) % 151.25/151.53 (assume @p113 (_ (_ @t154 tptp.n1_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 151.25/151.53 (assume @p114 (_ (_ tptp.instance_THFTYPE_IiioI tptp.documentation_THFTYPE_i) tptp.lTernaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p115 (_ @t155 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p116 (_ (_ @t156 tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 151.25/151.53 (assume @p117 (_ (_ tptp.instance_THFTYPE_IIiiioIioI tptp.orientation_THFTYPE_IiiioI) tptp.lTernaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p118 (_ (_ @t157 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p119 (_ (_ tptp.instance_THFTYPE_IIiooIioI tptp.knows_THFTYPE_IiooI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p120 (_ (_ tptp.instance_THFTYPE_IiioI tptp.relatedExternalConcept_THFTYPE_i) tptp.lTernaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p121 (_ (_ tptp.instance_THFTYPE_IiioI tptp.lKappaFn_THFTYPE_i) tptp.lBinaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p122 (_ (_ @t158 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p123 (_ (_ @t159 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p124 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subrelation_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p125 (_ (_ tptp.relatedInternalConcept_THFTYPE_IIiioIIiioIoI tptp.disjointRelation_THFTYPE_IiioI) tptp.disjoint_THFTYPE_IiioI)) % 151.25/151.53 (assume @p126 (_ (_ tptp.relatedInternalConcept_THFTYPE_IIioIIiioIoI tptp.disjointDecomposition_THFTYPE_IioI) tptp.disjoint_THFTYPE_IiioI)) % 151.25/151.53 (assume @p127 (_ (_ tptp.subrelation_THFTYPE_IIiioIIiioIoI tptp.member_THFTYPE_IiioI) tptp.part_THFTYPE_IiioI)) % 151.25/151.53 (assume @p128 (_ (_ @t160 tptp.n1_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p129 (_ @t161 tptp.lTemporalRelation_THFTYPE_i)) % 151.25/151.53 (assume @p130 (_ (_ (_ tptp.domain_THFTYPE_IIiiIiioI tptp.lBeginFn_THFTYPE_IiiI) tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 151.25/151.53 (assume @p131 (_ (_ @t153 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p132 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.instance_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p133 (_ @t146 tptp.lIrreflexiveRelation_THFTYPE_i)) % 151.25/151.53 (assume @p134 (_ (_ @t162 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p135 (_ @t163 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p136 (_ (_ (_ tptp.domain_THFTYPE_IiiioI tptp.partition_THFTYPE_i) tptp.n1_THFTYPE_i) tptp.lClass_THFTYPE_i)) % 151.25/151.53 (assume @p137 (_ (_ @t160 tptp.n2_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p138 (_ @t164 tptp.lTemporalRelation_THFTYPE_i)) % 151.25/151.53 (assume @p139 (_ (_ tptp.subrelation_THFTYPE_IiIiioIoI tptp.modalAttribute_THFTYPE_i) tptp.property_THFTYPE_IiioI)) % 151.25/151.53 (assume @p140 (_ (_ @t165 tptp.n2_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p141 (_ @t136 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p142 (_ (_ @t166 tptp.n1_THFTYPE_i) tptp.lSymbolicString_THFTYPE_i)) % 151.25/151.53 (assume @p143 (_ (_ tptp.instance_THFTYPE_IIIiioIiioIioI tptp.domain_THFTYPE_IIiioIiioI) tptp.lTernaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p144 (_ (_ @t157 tptp.n3_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p145 (_ @t155 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p146 (_ (_ @t151 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p147 (_ (_ @t142 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p148 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.disjoint_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p149 (_ @t164 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p150 (_ (_ tptp.subrelation_THFTYPE_IiIiioIoI tptp.attribute_THFTYPE_i) tptp.property_THFTYPE_IiioI)) % 151.25/151.53 (assume @p151 (_ (_ @t166 tptp.n3_THFTYPE_i) tptp.lLanguage_THFTYPE_i)) % 151.25/151.53 (assume @p152 (_ (_ @t166 tptp.n2_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p153 (_ @t152 tptp.lBinaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p154 (_ (_ @t151 tptp.n2_THFTYPE_i) tptp.lHumanLanguage_THFTYPE_i)) % 151.25/151.53 (assume @p155 (_ (_ @t167 tptp.n2_THFTYPE_i) tptp.lList_THFTYPE_i)) % 151.25/151.53 (assume @p156 (_ (_ @t168 tptp.n1_THFTYPE_i) tptp.lOrganism_THFTYPE_i)) % 151.25/151.53 (assume @p157 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subProcess_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p158 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.disjointRelation_THFTYPE_IiioI) tptp.lIrreflexiveRelation_THFTYPE_i)) % 151.25/151.53 (assume @p159 (_ (_ (_ tptp.domain_THFTYPE_IIiooIiioI tptp.holdsDuring_THFTYPE_IiooI) tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 151.25/151.53 (assume @p160 (_ @t161 tptp.lUnaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p161 (_ @t169 tptp.lBinaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p162 (_ (_ @t168 tptp.n2_THFTYPE_i) tptp.lOrganism_THFTYPE_i)) % 151.25/151.53 (assume @p163 (_ (_ @t167 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p164 (_ @t161 tptp.lTotalValuedRelation_THFTYPE_i)) % 151.25/151.53 (assume @p165 (_ @t135 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p166 (_ (_ @t140 tptp.n2_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 151.25/151.53 (assume @p167 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subclass_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p168 (_ (_ @t154 tptp.n2_THFTYPE_i) tptp.lAttribute_THFTYPE_i)) % 151.25/151.53 (assume @p169 (_ (_ @t158 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p170 (_ @t170 tptp.lUnaryFunction_THFTYPE_i)) % 151.25/151.53 (assume @p171 (_ @t155 tptp.lIrreflexiveRelation_THFTYPE_i)) % 151.25/151.53 (assume @p172 (_ (_ @t171 tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p173 (_ (_ tptp.instance_THFTYPE_IIiooIioI tptp.believes_THFTYPE_IiooI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p174 (_ (_ @t150 tptp.n1_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 151.25/151.53 (assume @p175 (_ @t170 tptp.lTemporalRelation_THFTYPE_i)) % 151.25/151.53 (assume @p176 (_ (_ @t159 tptp.n1_THFTYPE_i) tptp.lEntity_THFTYPE_i)) % 151.25/151.53 (assume @p177 (_ (_ @t171 tptp.n1_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p178 (_ (_ @t172 tptp.n2_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p179 (_ (_ @t173 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p180 (_ (_ tptp.disjointRelation_THFTYPE_IiIiioIoI tptp.result_THFTYPE_i) tptp.instrument_THFTYPE_IiioI)) % 151.25/151.53 (assume @p181 (_ @t169 tptp.lTotalValuedRelation_THFTYPE_i)) % 151.25/151.53 (assume @p182 (_ (_ @t165 tptp.n1_THFTYPE_i) tptp.lProcess_THFTYPE_i)) % 151.25/151.53 (assume @p183 (_ (_ @t162 tptp.n2_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p184 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.subAttribute_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p185 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.member_THFTYPE_IiioI) tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p186 (_ (_ @t145 tptp.n1_THFTYPE_i) tptp.lRelation_THFTYPE_i)) % 151.25/151.53 (assume @p187 (_ (_ tptp.instance_THFTYPE_IIIioIiioIioI tptp.domainSubclass_THFTYPE_IIioIiioI) tptp.lTernaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p188 (_ @t170 tptp.lTotalValuedRelation_THFTYPE_i)) % 151.25/151.53 (assume @p189 (_ (_ @t144 tptp.n2_THFTYPE_i) tptp.lAgent_THFTYPE_i)) % 151.25/151.53 (assume @p190 (_ (_ tptp.instance_THFTYPE_IIiioIioI tptp.property_THFTYPE_IiioI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p191 (_ (_ (_ tptp.domain_THFTYPE_IIiiiIiioI tptp.lListOrderFn_THFTYPE_IiiiI) tptp.n1_THFTYPE_i) tptp.lList_THFTYPE_i)) % 151.25/151.53 (assume @p192 (_ (_ @t141 tptp.n2_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 151.25/151.53 (assume @p193 (_ @t163 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p194 (_ (_ tptp.relatedInternalConcept_THFTYPE_IIiioIIiioIoI tptp.member_THFTYPE_IiioI) tptp.instance_THFTYPE_IiioI)) % 151.25/151.53 (assume @p195 (_ (_ (_ tptp.domain_THFTYPE_IiiioI tptp.modalAttribute_THFTYPE_i) tptp.n1_THFTYPE_i) tptp.lFormula_THFTYPE_i)) % 151.25/151.53 (assume @p196 (_ (_ @t143 tptp.n1_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p197 (_ (_ tptp.subrelation_THFTYPE_IIiioIioI tptp.instrument_THFTYPE_IiioI) tptp.patient_THFTYPE_i)) % 151.25/151.53 (assume @p198 (_ (_ @t156 tptp.n1_THFTYPE_i) tptp.lCognitiveAgent_THFTYPE_i)) % 151.25/151.53 (assume @p199 (_ (_ (_ tptp.domain_THFTYPE_IIiiIiioI tptp.lEndFn_THFTYPE_IiiI) tptp.n1_THFTYPE_i) tptp.lTimeInterval_THFTYPE_i)) % 151.25/151.53 (assume @p200 (_ (_ tptp.instance_THFTYPE_IIiIiioIoIioI tptp.disjointRelation_THFTYPE_IiIiioIoI) tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p201 (_ (_ @t172 tptp.n1_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p202 (_ @t147 tptp.lTotalValuedRelation_THFTYPE_i)) % 151.25/151.53 (assume @p203 (_ @t148 tptp.lBinaryPredicate_THFTYPE_i)) % 151.25/151.53 (assume @p204 (_ (_ (_ tptp.domain_THFTYPE_IiiioI tptp.attribute_THFTYPE_i) tptp.n1_THFTYPE_i) tptp.lObject_THFTYPE_i)) % 151.25/151.53 (assume @p205 (_ (_ tptp.subrelation_THFTYPE_IIoooIIiioIoI tptp.truth_THFTYPE_IoooI) tptp.property_THFTYPE_IiioI)) % 151.25/151.53 (assume @p206 (_ @t148 tptp.lAsymmetricRelation_THFTYPE_i)) % 151.25/151.53 (assume @p207 (_ (_ @t173 tptp.n3_THFTYPE_i) tptp.lSetOrClass_THFTYPE_i)) % 151.25/151.53 (assume @p208 (_ @t147 tptp.lTemporalRelation_THFTYPE_i)) % 151.25/151.53 (assume @p209 @t187) % 151.25/151.53 (assume @p210 true) % 151.25/151.53 ; WARNING: add trust step for TRUST % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p211 :rule trust :premises () :args ((= (not (forall @t8 @t192)) (not @t191)))) % 151.25/151.53 (step @p212 :rule refl :args (@t192)) % 151.25/151.53 (step @p213 :rule refl :args (@t9)) % 151.25/151.53 (step @p214 :rule cong :premises (@p213 @p212) :args ((= @t9 @t192))) % 151.25/151.53 (step @p215 :rule symm :premises (@p214)) % 151.25/151.53 (step @p216 :rule eq_resolve :premises (@p213 @p215)) % 151.25/151.53 (step @p217 :rule cong :premises (@p216) :args ((forall @t8 @t9))) % 151.25/151.53 (step @p218 :rule bool-double-not-elim :args (@t9)) % 151.25/151.53 (step @p219 :rule cong :premises (@p218) :args (@t193)) % 151.25/151.53 (step @p220 :rule trans :premises (@p219 @p217)) % 151.25/151.53 (step @p221 :rule cong :premises (@p220) :args (@t194)) % 151.25/151.53 (step @p222 :rule exists-elim :args ((= @t11 @t194))) % 151.25/151.53 (step @p223 :rule trans :premises (@p222 @p221)) % 151.25/151.53 (step @p224 :rule trans :premises (@p223 @p211)) % 151.25/151.53 (step @p225 :rule eq_resolve :premises (@p4 @p224)) % 151.25/151.53 (step @p226 :rule skolemize :premises (@p225)) % 151.25/151.53 (step @p227 :rule eq-symm :args (@t195 @t196)) % 151.25/151.53 (step @p228 :rule eq-symm :args (@t197 @t196)) % 151.25/151.53 (step @p229 :rule refl :args (@t198)) % 151.25/151.53 (step @p230 :rule refl :args (@t199)) % 151.25/151.53 (step @p231 :rule nary_cong :premises (@p230 @p229 @p228 @p227) :args (@t200)) % 151.25/151.53 (step @p232 :rule cong :premises (@p231) :args (@t202)) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p233 :rule trust :premises () :args ((= @t208 @t202))) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p234 :rule trust :premises () :args ((= @t214 @t208))) % 151.25/151.53 (step @p235 :rule bool-double-not-elim :args (@t214)) % 151.25/151.53 (step @p236 :rule refl :args (@t212)) % 151.25/151.53 (step @p237 :rule refl :args (@t213)) % 151.25/151.53 (step @p238 :rule refl :args (@t204)) % 151.25/151.53 (step @p239 :rule refl :args (@t182)) % 151.25/151.53 (step @p240 :rule cong :premises (@p239 @p238) :args ((= @t182 @t204))) % 151.25/151.53 (step @p241 :rule symm :premises (@p240)) % 151.25/151.53 (step @p242 :rule eq_resolve :premises (@p239 @p241)) % 151.25/151.53 (step @p243 :rule cong :premises (@p242) :args (@t215)) % 151.25/151.53 (step @p244 :rule refl :args (@t206)) % 151.25/151.53 (step @p245 :rule refl :args (@t183)) % 151.25/151.53 (step @p246 :rule cong :premises (@p245 @p244) :args ((= @t183 @t206))) % 151.25/151.53 (step @p247 :rule symm :premises (@p246)) % 151.25/151.53 (step @p248 :rule eq_resolve :premises (@p245 @p247)) % 151.25/151.53 (step @p249 :rule cong :premises (@p248) :args (@t216)) % 151.25/151.53 (step @p250 :rule nary_cong :premises (@p249 @p243 @p237 @p236) :args (@t217)) % 151.25/151.53 (step @p251 :rule cong :premises (@p250) :args ((forall @t185 @t217))) % 151.25/151.53 (step @p252 :rule bool-double-not-elim :args (@t212)) % 151.25/151.53 (step @p253 :rule bool-double-not-elim :args (@t213)) % 151.25/151.53 (step @p254 :rule refl :args (@t215)) % 151.25/151.53 (step @p255 :rule refl :args (@t216)) % 151.25/151.53 (step @p256 :rule nary_cong :premises (@p255 @p254 @p253 @p252) :args (@t222)) % 151.25/151.53 (step @p257 :rule aci_norm :args ((= (or @t216 (or @t215 (or @t221 @t219))) @t222))) % 151.25/151.53 (step @p258 :rule trans :premises (@p257 @p256)) % 151.25/151.53 (step @p259 :rule bool-and-de-morgan :args (@t220 @t218 true)) % 151.25/151.53 (step @p260 :rule nary_cong :premises (@p254 @p259) :args ((or @t215 (not (and @t220 @t218))))) % 151.25/151.53 (step @p261 :rule bool-and-de-morgan :args (@t182 @t220 (and @t218))) % 151.25/151.53 (step @p262 :rule trans :premises (@p261 @p260)) % 151.25/151.53 (step @p263 :rule nary_cong :premises (@p255 @p262) :args ((or @t216 (not (and @t182 @t220 @t218))))) % 151.25/151.53 (step @p264 :rule bool-and-de-morgan :args (@t183 @t182 (and @t220 @t218))) % 151.25/151.53 (step @p265 :rule trans :premises (@p264 @p263)) % 151.25/151.53 (step @p266 :rule trans :premises (@p265 @p258)) % 151.25/151.53 (step @p267 :rule cong :premises (@p266) :args (@t224)) % 151.25/151.53 (step @p268 :rule trans :premises (@p267 @p251)) % 151.25/151.53 (step @p269 :rule cong :premises (@p268) :args (@t225)) % 151.25/151.53 (step @p270 :rule exists-elim :args ((= (exists @t185 @t223) @t225))) % 151.25/151.53 (step @p271 :rule trans :premises (@p270 @p269)) % 151.25/151.53 (step @p272 :rule refl :args (@t211)) % 151.25/151.53 (step @p273 :rule symm :premises (@p272)) % 151.25/151.53 (step @p274 :rule alpha_equiv :args (@t175 (@list @t4 @t174) (@list @t210 @t209))) % 151.25/151.53 (step @p275 :rule trans :premises (@p274 @p273)) % 151.25/151.53 (step @p276 :rule refl :args (@t176)) % 151.25/151.53 (step @p277 :rule cong :premises (@p276 @p275) :args (@t177)) % 151.25/151.53 (step @p278 :rule cong :premises (@p277) :args (@t178)) % 151.25/151.53 (step @p279 :rule refl :args (@t179)) % 151.25/151.53 (step @p280 :rule cong :premises (@p279 @p275) :args (@t180)) % 151.25/151.53 (step @p281 :rule cong :premises (@p280) :args (@t181)) % 151.25/151.53 (step @p282 :rule refl :args (@t182)) % 151.25/151.53 (step @p283 :rule refl :args (@t183)) % 151.25/151.53 (step @p284 :rule nary_cong :premises (@p283 @p282 @p281 @p278) :args (@t184)) % 151.25/151.53 (step @p285 :rule cong :premises (@p284) :args (@t186)) % 151.25/151.53 (step @p286 :rule trans :premises (@p285 @p271)) % 151.25/151.53 (step @p287 :rule cong :premises (@p286) :args (@t187)) % 151.25/151.53 (step @p288 :rule trans :premises (@p287 @p235)) % 151.25/151.53 (step @p289 :rule trans :premises (@p288 @p234 @p233 @p232)) % 151.25/151.53 (step @p290 :rule eq_resolve :premises (@p209 @p289)) % 151.25/151.53 (step @p291 :rule eq-symm :args (@t196 @t226)) % 151.25/151.53 (step @p292 :rule eq-symm :args (@t196 @t188)) % 151.25/151.53 (step @p293 :rule refl :args (@t228)) % 151.25/151.53 (step @p294 :rule refl :args (@t230)) % 151.25/151.53 (step @p295 :rule nary_cong :premises (@p294 @p293 @p292 @p291) :args (@t231)) % 151.25/151.53 (step @p296 :rule refl :args (@t232)) % 151.25/151.53 (step @p297 :rule cong :premises (@p296 @p295) :args ((=> @t232 @t231))) % 151.25/151.53 (assume-push @p392 @t232) % 151.25/151.53 (step @p299 :rule instantiate :premises (@p290) :args ((@list @t226 @t188 tptp.lMary_THFTYPE_i))) % 151.25/151.53 (step-pop @p393 :rule scope :premises (@p299)) % 151.25/151.53 (step @p300 :rule process_scope :premises (@p393) :args (@t231)) % 151.25/151.53 (step @p302 :rule eq_resolve :premises (@p300 @p297)) % 151.25/151.53 (step @p303 :rule implies_elim :premises (@p302)) % 151.25/151.53 (step @p304 :rule chain_m_resolution :premises (@p303 @p290) :args (@t235 (@list false) (@list @t232))) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p305 :rule trust :premises () :args ((= @t239 (forall @t238 (_ @t190 (_ @t189 @t196 @t237) @t236))))) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM_LEMMA % 151.25/151.53 (step @p306 :rule trust :premises () :args (@t239)) % 151.25/151.53 (step @p307 :rule eq_resolve :premises (@p306 @p305)) % 151.25/151.53 (step @p308 :rule instantiate :premises (@p307) :args ((@list @t242 @t241))) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p309 :rule trust :premises () :args ((= (not (forall @t8 @t243)) (not @t240)))) % 151.25/151.53 (step @p310 :rule refl :args (@t243)) % 151.25/151.53 (step @p311 :rule refl :args (@t63)) % 151.25/151.53 (step @p312 :rule cong :premises (@p311 @p310) :args ((= @t63 @t243))) % 151.25/151.53 (step @p313 :rule symm :premises (@p312)) % 151.25/151.53 (step @p314 :rule eq_resolve :premises (@p311 @p313)) % 151.25/151.53 (step @p315 :rule cong :premises (@p314) :args ((forall @t8 @t63))) % 151.25/151.53 (step @p316 :rule bool-double-not-elim :args (@t63)) % 151.25/151.53 (step @p317 :rule cong :premises (@p316) :args (@t244)) % 151.25/151.53 (step @p318 :rule trans :premises (@p317 @p315)) % 151.25/151.53 (step @p319 :rule cong :premises (@p318) :args (@t245)) % 151.25/151.53 (step @p320 :rule exists-elim :args ((= @t65 @t245))) % 151.25/151.53 (step @p321 :rule trans :premises (@p320 @p319)) % 151.25/151.53 (step @p322 :rule trans :premises (@p321 @p309)) % 151.25/151.53 (step @p323 :rule eq_resolve :premises (@p26 @p322)) % 151.25/151.53 (step @p324 :rule skolemize :premises (@p323)) % 151.25/151.53 (step @p325 :rule refl :args (@t248)) % 151.25/151.53 (step @p326 :rule refl :args (@t249)) % 151.25/151.53 (step @p327 :rule bool-double-not-elim :args (@t250)) % 151.25/151.53 (step @p328 :rule nary_cong :premises (@p327 @p326 @p325) :args ((or (not @t251) @t249 @t248))) % 151.25/151.53 (assume-push @p394 @t251) % 151.25/151.53 (assume-push @p395 @t233) % 151.25/151.53 (assume-push @p396 @t247) % 151.25/151.53 (step @p332 :rule evaluate :args ((= true false))) % 151.25/151.53 (step @p333 :rule false_intro :premises (@p324)) % 151.25/151.53 (step @p334 :rule refl :args (@t241)) % 151.25/151.53 (step @p335 :rule refl :args (@t242)) % 151.25/151.53 (step @p336 :rule symm :premises (@p395)) % 151.25/151.53 (step @p337 :rule cong :premises (@p336 @p335) :args (@t246)) % 151.25/151.53 (step @p338 :rule cong :premises (@p337 @p334) :args (@t247)) % 151.25/151.53 (step @p339 :rule true_intro :premises (@p308)) % 151.25/151.53 (step @p340 :rule symm :premises (@p339)) % 151.25/151.53 (step @p341 :rule trans :premises (@p340 @p338 @p333)) % 151.25/151.53 (step @p342 false :rule eq_resolve :premises (@p341 @p332)) % 151.25/151.53 (step-pop @p397 :rule scope :premises (@p342)) % 151.25/151.53 (step-pop @p398 :rule scope :premises (@p397)) % 151.25/151.53 (step-pop @p399 :rule scope :premises (@p398)) % 151.25/151.53 (step @p343 :rule process_scope :premises (@p399) :args (false)) % 151.25/151.53 (step @p347 :rule not_and :premises (@p343)) % 151.25/151.53 (step @p348 :rule eq_resolve :premises (@p347 @p328)) % 151.25/151.53 (step @p349 :rule chain_m_resolution :premises (@p348 @p324 @p308) :args (@t249 (@list true false) (@list @t250 @t247))) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p350 :rule trust :premises () :args ((= @t77 @t229))) % 151.25/151.53 (step @p351 :rule eq_resolve :premises (@p32 @p350)) % 151.25/151.53 ; trust TRUST PREPROCESS_HO_ELIM % 151.25/151.53 (step @p352 :rule trust :premises () :args ((= @t2 @t227))) % 151.25/151.53 (step @p353 :rule eq_resolve :premises (@p1 @p352)) % 151.25/151.53 (step @p354 :rule cnf_or_pos :args (@t235)) % 151.25/151.53 (step @p355 :rule reordering :premises (@p354) :args ((or @t228 @t230 @t233 @t234 (not @t235)))) % 151.25/151.53 (step @p356 :rule chain_m_resolution :premises (@p355 @p353 @p351 @p349 @p304) :args (@t234 (@list false false true false) (@list @t227 @t229 @t233 @t235))) % 151.25/151.53 (step @p357 :rule instantiate :premises (@p307) :args ((@list @t253 @t252))) % 151.25/151.53 (step @p358 :rule refl :args (@t255)) % 151.25/151.53 (step @p359 :rule refl :args (@t256)) % 151.25/151.53 (step @p360 :rule bool-double-not-elim :args (@t258)) % 151.25/151.53 (step @p361 :rule nary_cong :premises (@p360 @p359 @p358) :args ((or (not @t259) @t256 @t255))) % 151.25/151.53 (assume-push @p400 @t254) % 151.25/151.53 (assume-push @p401 @t234) % 151.25/151.53 (assume-push @p402 @t259) % 151.25/151.53 (step @p365 :rule evaluate :args ((= false true))) % 151.25/151.53 (step @p366 :rule true_intro :premises (@p357)) % 151.25/151.53 (step @p367 :rule refl :args (@t252)) % 151.25/151.53 (step @p368 :rule refl :args (@t253)) % 151.25/151.53 (step @p369 :rule cong :premises (@p401 @p368) :args (@t257)) % 151.25/151.53 (step @p370 :rule cong :premises (@p369 @p367) :args (@t258)) % 151.25/151.53 (step @p371 :rule false_intro :premises (@p226)) % 151.25/151.53 (step @p372 :rule symm :premises (@p371)) % 151.25/151.53 (step @p373 :rule trans :premises (@p372 @p370 @p366)) % 151.25/151.53 (step @p374 false :rule eq_resolve :premises (@p373 @p365)) % 151.25/151.53 (step-pop @p403 :rule scope :premises (@p374)) % 151.25/151.53 (step-pop @p404 :rule scope :premises (@p403)) % 151.25/151.53 (step-pop @p405 :rule scope :premises (@p404)) % 151.25/151.53 (step @p375 :rule process_scope :premises (@p405) :args (false)) % 151.25/151.53 (assume-push @p406 @t259) % 151.25/151.53 (assume-push @p407 @t234) % 151.25/151.53 (assume-push @p408 @t254) % 151.25/151.53 (step @p382 :rule and_intro :premises (@p357 @p407 @p226)) % 151.25/151.53 (step-pop @p409 :rule scope :premises (@p382)) % 151.25/151.53 (step-pop @p410 :rule scope :premises (@p409)) % 151.25/151.53 (step-pop @p411 :rule scope :premises (@p410)) % 151.25/151.53 (step @p383 :rule process_scope :premises (@p411) :args (@t260)) % 151.25/151.53 (step @p387 :rule implies_elim :premises (@p383)) % 151.25/151.53 (step @p388 :rule resolution :premises (@p387 @p375) :args (true @t260)) % 151.25/151.53 (step @p389 :rule not_and :premises (@p388)) % 151.25/151.53 (step @p390 :rule eq_resolve :premises (@p389 @p361)) % 151.25/151.53 (step @p391 false :rule chain_m_resolution :premises (@p390 @p357 @p356 @p226) :args (false (@list false false true) (@list @t254 @t234 @t258))) % 151.25/151.53 ) % 151.25/151.53 % SZS output end Proof % 151.25/151.53 % cvc5 exiting %------------------------------------------------------------------------------