%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV919-1 : 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 : n001.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 09:02:37 AM UTC 2026 % Result : Unsatisfiable 93.39s 93.62s % Output : Proof 93.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV919-1 : 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.16/0.35 % Computer : n001.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Tue Jun 2 21:22:20 EDT 2026 % 0.16/0.35 % CPUTime : % 0.39/0.62 %----Proving TF0_NAR, FOF, or CNF % 0.46/0.63 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 15.51/15.74 --- Run --no-e-matching --full-saturate-quant at 6... % 21.53/21.79 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 6... % 27.62/27.83 --- Run --finite-model-find --uf-ss=no-minimal at 6... % 33.61/33.88 --- Run --multi-trigger-when-single --full-saturate-quant at 30... % 63.69/63.99 --- Run --trigger-sel=max --full-saturate-quant at 15... % 78.81/79.07 --- Run --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant at 33... % 93.39/93.62 % SZS status Unsatisfiable % 93.39/93.62 % SZS output start Proof % 93.39/93.65 ( % 93.39/93.65 (declare-sort $$unsorted 0) % 93.39/93.65 (declare-const tptp.v_E____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_Objects_Oinit__fields (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_v____ $$unsorted) % 93.39/93.65 (declare-const tptp.t_c $$unsorted) % 93.39/93.65 (declare-const tptp.v_C____ $$unsorted) % 93.39/93.65 (declare-const tptp.v_F____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_Product__Type_Oprod_Oprod__case (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Product__Type_Oprod__fun (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_fequal (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_xa $$unsorted) % 93.39/93.65 (declare-const tptp.v_P $$unsorted) % 93.39/93.65 (declare-const tptp.c_Option_Ois__none (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_fst (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Product__Type_Oprod_Oprod__rec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Option_Othe (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_snd (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Product__Type_Oapfst (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_Expr_Oexp (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Map_Omap__comp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Map_Osko__Map__Xmap__comp__None__iff__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_split (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_T____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_Map_Omap__le (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Map_Omap__upds (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Product__Type_Ointernal__split (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_TypeRel_Osko__TypeRel__Xhas__field__def__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_TypeRel_Ohas__field (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.class_OrderedGroup_Ocomm__monoid__mult (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Conform_Ooconf (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Finite__Set_Osetprod (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_Type_Oty $$unsorted) % 93.39/93.65 (declare-const tptp.c_Conform_Osko__Conform__Xconf__def__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.class_OrderedGroup_Ocomm__monoid__add (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Finite__Set_Osetsum (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Option_Ooption_OSome (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_TypeRel_OFields (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_curry (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_Option_Ooption (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Option_Ooption_Ooption__rec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_sko__Option__Xoption__Xsplit__asm__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Progress_OWTrt_H (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Expr_Oexp_OFAss (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.t_a $$unsorted) % 93.39/93.65 (declare-const tptp.class_Orderings_Otop (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_List_Oset (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_List_Olist (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Nat_Osize__class_Osize (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_String_Ochar $$unsorted) % 93.39/93.65 (declare-const tptp.c_Map_Oran (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Map_Orestrict__map (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_WellTypeRT_OWTrt (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Objects_Otypeof__h (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_BigStep_Oeval (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.class_OrderedGroup_Oab__group__add (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Value_Oval_OAddr (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Product__Type_Oapsnd (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Map_Odom (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_SmallStep_Oredp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Conform_Oconf (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Expr_Oexp_OFAcc (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Option_Ooption_ONone (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Set_Oimage (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Fun_Oinj__on (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Exceptions_Opreallocated (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.tc_bool $$unsorted) % 93.39/93.65 (declare-const tptp.c_Fun_Oswap (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Map_Omap__add (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Fun_Ofun__upd (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Orderings_Obot__class_Obot (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_ATP__Linkup_Osko__Product__Type__Xsplit__paired__Ex__1__3 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_COMBI (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Orderings_Otop__class_Otop (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Set_Oinsert (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Fun_Ocomp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Expr_Oexp_OVal (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.hBOOL (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.v_TF____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_List_Olist_OCons (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Objects_Osko__Objects__Xhext__def__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Option_Oset (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_HOL_Ominus__class_Ominus (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.class_HOL_Ominus (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.v_fs____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_List_Ozip (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Fun_Ooverride__on (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_x $$unsorted) % 93.39/93.65 (declare-const tptp.c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Fun_Othe__inv__into (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.class_Orderings_Obot (-> $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Map_Omap__of (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Conform_Ohconf (-> $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.hAPP (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Product__Type_Oscomp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_in (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Fun_Oid (-> $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_Tv____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_List_Ofilter (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_TypeRel_Owiden (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Objects_Ohext (-> $$unsorted $$unsorted Bool)) % 93.39/93.65 (declare-const tptp.c_Option_Omap (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_sko__Option__Xoption__Xsplit__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_ATP__Linkup_Osko__Product__Type__Xsplit__paired__All__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_a____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_Objects_Osko__Objects__Xhext__objD__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_nat $$unsorted) % 93.39/93.65 (declare-const tptp.t_b $$unsorted) % 93.39/93.65 (declare-const tptp.tc_Value_Oval $$unsorted) % 93.39/93.65 (declare-const tptp.c_Option_Ooption_Ooption__case (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_ha____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_ATP__Linkup_Osko__Option__Xospec__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_prod (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Value_Oval_OUnit $$unsorted) % 93.39/93.65 (declare-const tptp.c_Hilbert__Choice_Oinv__into (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.v_D____ $$unsorted) % 93.39/93.65 (declare-const tptp.c_Pair (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.tc_fun (-> $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_Map_Osko__Map__Xdom__eq__singleton__conv__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (declare-const tptp.c_COMBK (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 93.39/93.65 (define @t1 () (@var "T_a" $$unsorted)) % 93.39/93.65 (define @t2 () (@var "V_A" $$unsorted)) % 93.39/93.65 (define @t3 () (@var "V_x" $$unsorted)) % 93.39/93.65 (define @t4 () (tptp.hBOOL (tptp.c_in @t3 @t2 @t1))) % 93.39/93.65 (define @t5 () (tptp.tc_fun @t1 tptp.tc_bool)) % 93.39/93.65 (define @t6 () (tptp.c_Orderings_Obot__class_Obot @t5)) % 93.39/93.65 (define @t7 () (tptp.c_Set_Oinsert @t3 @t6 @t1)) % 93.39/93.65 (define @t8 () (tptp.c_Set_Oinsert @t3 @t2 @t1)) % 93.39/93.65 (define @t9 () (@list @t3 @t2 @t1)) % 93.39/93.65 (define @t10 () (@var "T_b" $$unsorted)) % 93.39/93.65 (define @t11 () (@var "V_B" $$unsorted)) % 93.39/93.65 (define @t12 () (tptp.tc_fun tptp.t_a @t10)) % 93.39/93.65 (define @t13 () (tptp.c_Orderings_Otop__class_Otop @t5)) % 93.39/93.65 (define @t14 () (@var "V_f" $$unsorted)) % 93.39/93.65 (define @t15 () (tptp.c_Fun_Oinj__on @t14 @t13 @t1 @t10)) % 93.39/93.65 (define @t16 () (not @t15)) % 93.39/93.65 (define @t17 () (tptp.tc_fun @t10 tptp.tc_bool)) % 93.39/93.65 (define @t18 () (tptp.c_Set_Oimage @t14 @t11 @t1 @t10)) % 93.39/93.65 (define @t19 () (tptp.c_Set_Oimage @t14 @t2 @t1 @t10)) % 93.39/93.65 (define @t20 () (tptp.c_HOL_Ominus__class_Ominus @t2 @t11 @t5)) % 93.39/93.65 (define @t21 () (@list @t14 @t2 @t11 @t1 @t10)) % 93.39/93.65 (define @t22 () (@var "V_c" $$unsorted)) % 93.39/93.65 (define @t23 () (tptp.hBOOL (tptp.c_in @t22 @t2 @t1))) % 93.39/93.65 (define @t24 () (tptp.hBOOL (tptp.c_in @t22 @t11 @t1))) % 93.39/93.65 (define @t25 () (tptp.hBOOL (tptp.c_in @t22 @t20 @t1))) % 93.39/93.65 (define @t26 () (@var "V_a" $$unsorted)) % 93.39/93.65 (define @t27 () (tptp.c_Set_Oinsert @t26 @t2 @t1)) % 93.39/93.65 (define @t28 () (tptp.c_Set_Oinsert @t26 @t6 @t1)) % 93.39/93.65 (define @t29 () (tptp.c_HOL_Ominus__class_Ominus @t2 @t28 @t5)) % 93.39/93.65 (define @t30 () (tptp.c_Set_Oinsert @t26 @t29 @t1)) % 93.39/93.65 (define @t31 () (@list @t26 @t2 @t1)) % 93.39/93.65 (define @t32 () (@var "V_val" $$unsorted)) % 93.39/93.65 (define @t33 () (tptp.c_Expr_Oexp_OVal @t32 @t1)) % 93.39/93.65 (define @t34 () (@var "V_list2_H" $$unsorted)) % 93.39/93.65 (define @t35 () (@var "V_list1_H" $$unsorted)) % 93.39/93.65 (define @t36 () (@var "V_exp_H" $$unsorted)) % 93.39/93.65 (define @t37 () (tptp.c_Expr_Oexp_OFAcc @t36 @t35 @t34 @t1)) % 93.39/93.65 (define @t38 () (@var "V_y_H" $$unsorted)) % 93.39/93.65 (define @t39 () (@var "V_x_H" $$unsorted)) % 93.39/93.65 (define @t40 () (tptp.c_HOL_Ominus__class_Ominus @t3 @t3 @t1)) % 93.39/93.65 (define @t41 () (not (tptp.class_OrderedGroup_Oab__group__add @t1))) % 93.39/93.65 (define @t42 () (@var "V_y" $$unsorted)) % 93.39/93.65 (define @t43 () (@var "V_xa" $$unsorted)) % 93.39/93.65 (define @t44 () (@var "V_s_H" $$unsorted)) % 93.39/93.65 (define @t45 () (@var "V_e_H" $$unsorted)) % 93.39/93.65 (define @t46 () (@var "V_s" $$unsorted)) % 93.39/93.65 (define @t47 () (@var "V_e" $$unsorted)) % 93.39/93.65 (define @t48 () (@var "V_P" $$unsorted)) % 93.39/93.65 (define @t49 () (not (tptp.c_SmallStep_Oredp @t48 @t47 @t46 @t45 @t44))) % 93.39/93.65 (define @t50 () (tptp.tc_List_Olist tptp.tc_String_Ochar)) % 93.39/93.65 (define @t51 () (@var "V_D" $$unsorted)) % 93.39/93.65 (define @t52 () (@var "V_F" $$unsorted)) % 93.39/93.65 (define @t53 () (tptp.c_Expr_Oexp_OFAcc @t47 @t52 @t51 @t50)) % 93.39/93.65 (define @t54 () (tptp.c_Map_Odom @t14 @t10 @t1)) % 93.39/93.65 (define @t55 () (tptp.c_Option_Ooption_ONone @t1)) % 93.39/93.65 (define @t56 () (tptp.hAPP @t14 @t3)) % 93.39/93.65 (define @t57 () (tptp.c_Fun_Oinj__on @t14 @t2 @t1 @t10)) % 93.39/93.65 (define @t58 () (not @t57)) % 93.39/93.65 (define @t59 () (tptp.c_Set_Oinsert @t26 @t11 @t1)) % 93.39/93.65 (define @t60 () (tptp.c_HOL_Ominus__class_Ominus @t2 @t59 @t5)) % 93.39/93.65 (define @t61 () (@list @t2 @t26 @t11 @t1)) % 93.39/93.65 (define @t62 () (not @t25)) % 93.39/93.65 (define @t63 () (@var "V_list2" $$unsorted)) % 93.39/93.65 (define @t64 () (= @t63 @t34)) % 93.39/93.65 (define @t65 () (@var "V_list1" $$unsorted)) % 93.39/93.65 (define @t66 () (@var "V_exp" $$unsorted)) % 93.39/93.65 (define @t67 () (tptp.c_Expr_Oexp_OFAcc @t66 @t65 @t63 @t1)) % 93.39/93.65 (define @t68 () (not (= @t67 @t37))) % 93.39/93.65 (define @t69 () (@list @t66 @t65 @t63 @t1 @t36 @t35 @t34)) % 93.39/93.66 (define @t70 () (= @t65 @t35)) % 93.39/93.66 (define @t71 () (@list @t2 @t1)) % 93.39/93.66 (define @t72 () (@list @t1 @t2)) % 93.39/93.66 (define @t73 () (@var "V_exp2_H" $$unsorted)) % 93.39/93.66 (define @t74 () (@var "V_exp1_H" $$unsorted)) % 93.39/93.66 (define @t75 () (tptp.c_Expr_Oexp_OFAss @t74 @t35 @t34 @t73 @t1)) % 93.39/93.66 (define @t76 () (tptp.hBOOL (tptp.c_in @t26 @t2 @t1))) % 93.39/93.66 (define @t77 () (not @t76)) % 93.39/93.66 (define @t78 () (tptp.hBOOL (tptp.c_in @t3 @t11 @t1))) % 93.39/93.66 (define @t79 () (tptp.c_HOL_Ominus__class_Ominus @t8 @t11 @t5)) % 93.39/93.66 (define @t80 () (@list @t3 @t2 @t1 @t11)) % 93.39/93.66 (define @t81 () (tptp.tc_Option_Ooption @t10)) % 93.39/93.66 (define @t82 () (@var "V_m" $$unsorted)) % 93.39/93.66 (define @t83 () (tptp.c_Map_Orestrict__map @t82 (tptp.c_HOL_Ominus__class_Ominus @t51 @t7 @t5) @t1 @t10)) % 93.39/93.66 (define @t84 () (tptp.c_Fun_Ofun__upd @t83 @t3 @t42 @t1 @t81)) % 93.39/93.66 (define @t85 () (tptp.c_Map_Orestrict__map @t82 @t51 @t1 @t10)) % 93.39/93.66 (define @t86 () (= (tptp.c_Fun_Ofun__upd @t85 @t3 @t42 @t1 @t81) @t84)) % 93.39/93.66 (define @t87 () (@list @t82 @t51 @t1 @t10 @t3 @t42)) % 93.39/93.66 (define @t88 () (tptp.c_Fun_Oinj__on @t14 @t27 @t1 @t10)) % 93.39/93.66 (define @t89 () (not @t88)) % 93.39/93.66 (define @t90 () (tptp.hAPP @t14 @t26)) % 93.39/93.66 (define @t91 () (tptp.hBOOL (tptp.c_in @t90 (tptp.c_Set_Oimage @t14 @t29 @t1 @t10) @t10))) % 93.39/93.66 (define @t92 () (@list @t14 @t26 @t2 @t1 @t10)) % 93.39/93.66 (define @t93 () (tptp.hBOOL (tptp.c_in @t3 @t2 @t10))) % 93.39/93.66 (define @t94 () (not @t93)) % 93.39/93.66 (define @t95 () (tptp.c_Orderings_Obot__class_Obot @t17)) % 93.39/93.66 (define @t96 () (tptp.c_Fun_Ofun__upd @t14 @t3 @t42 @t10 @t1)) % 93.39/93.66 (define @t97 () (tptp.c_Set_Oimage @t96 @t2 @t10 @t1)) % 93.39/93.66 (define @t98 () (@list @t14 @t3 @t42 @t10 @t1 @t2)) % 93.39/93.66 (define @t99 () (tptp.hBOOL (tptp.c_in @t3 @t51 @t1))) % 93.39/93.66 (define @t100 () (not @t99)) % 93.39/93.66 (define @t101 () (tptp.c_Map_Orestrict__map (tptp.c_Fun_Ofun__upd @t82 @t3 @t42 @t1 @t81) @t51 @t1 @t10)) % 93.39/93.66 (define @t102 () (@list @t82 @t3 @t42 @t1 @t10 @t51)) % 93.39/93.66 (define @t103 () (@var "V_xs" $$unsorted)) % 93.39/93.66 (define @t104 () (tptp.c_List_Oset @t103 @t1)) % 93.39/93.66 (define @t105 () (tptp.hBOOL (tptp.c_in @t3 @t104 @t1))) % 93.39/93.66 (define @t106 () (tptp.tc_List_Olist @t10)) % 93.39/93.66 (define @t107 () (@var "V_ys" $$unsorted)) % 93.39/93.66 (define @t108 () (tptp.tc_List_Olist @t1)) % 93.39/93.66 (define @t109 () (not (= (tptp.c_Nat_Osize__class_Osize @t103 @t108) (tptp.c_Nat_Osize__class_Osize @t107 @t106)))) % 93.39/93.66 (define @t110 () (tptp.c_Option_Ooption_OSome @t10)) % 93.39/93.66 (define @t111 () (tptp.hAPP @t110 @t43)) % 93.39/93.66 (define @t112 () (tptp.c_List_Ozip @t103 @t107 @t1 @t10)) % 93.39/93.66 (define @t113 () (tptp.hAPP (tptp.c_Map_Omap__of @t112 @t1 @t10) @t3)) % 93.39/93.66 (define @t114 () (tptp.c_Map_Odom @t14 @t1 @t10)) % 93.39/93.66 (define @t115 () (tptp.c_Option_Ooption_ONone @t10)) % 93.39/93.66 (define @t116 () (tptp.c_Fun_Ofun__upd @t14 @t3 @t115 @t1 @t81)) % 93.39/93.66 (define @t117 () (@list @t14 @t3 @t10 @t1)) % 93.39/93.66 (define @t118 () (not @t105)) % 93.39/93.66 (define @t119 () (= @t113 @t115)) % 93.39/93.66 (define @t120 () (tptp.c_Fun_Oid @t1)) % 93.39/93.66 (define @t121 () (tptp.hBOOL (tptp.hAPP @t48 @t3))) % 93.39/93.66 (define @t122 () (tptp.c_List_Ofilter @t48 @t107 @t1)) % 93.39/93.66 (define @t123 () (tptp.c_List_Olist_OCons @t3 @t103 @t1)) % 93.39/93.66 (define @t124 () (tptp.c_Set_Oimage @t14 @t95 @t10 @t1)) % 93.39/93.66 (define @t125 () (@list @t14 @t10 @t1)) % 93.39/93.66 (define @t126 () (@list @t14 @t1 @t10)) % 93.39/93.66 (define @t127 () (@var "V_T" $$unsorted)) % 93.39/93.66 (define @t128 () (@var "V_U" $$unsorted)) % 93.39/93.66 (define @t129 () (@var "V_S" $$unsorted)) % 93.39/93.66 (define @t130 () (@var "V_v" $$unsorted)) % 93.39/93.66 (define @t131 () (@var "V_h" $$unsorted)) % 93.39/93.66 (define @t132 () (tptp.c_Conform_Oconf @t48 @t131 @t130 @t127 @t1)) % 93.39/93.66 (define @t133 () (not @t132)) % 93.39/93.66 (define @t134 () (@var "V_T_H" $$unsorted)) % 93.39/93.66 (define @t135 () (@var "V_b" $$unsorted)) % 93.39/93.66 (define @t136 () (= @t26 @t135)) % 93.39/93.66 (define @t137 () (tptp.c_Set_Oinsert @t135 @t6 @t1)) % 93.39/93.66 (define @t138 () (not (tptp.hBOOL (tptp.c_in @t3 @t6 @t1)))) % 93.39/93.66 (define @t139 () (not @t121)) % 93.39/93.66 (define @t140 () (@list @t48 @t3 @t1)) % 93.39/93.66 (define @t141 () (@list @t1)) % 93.39/93.66 (define @t142 () (not (tptp.c_Fun_Oinj__on @t14 @t2 @t1 @t1))) % 93.39/93.66 (define @t143 () (@var "V_g" $$unsorted)) % 93.39/93.66 (define @t144 () (tptp.c_Fun_Oinj__on @t143 @t2 @t1 @t10)) % 93.39/93.66 (define @t145 () (not @t144)) % 93.39/93.66 (define @t146 () (tptp.c_Fun_Oinj__on @t143 (tptp.c_Set_Oimage @t14 @t2 @t1 @t1) @t1 @t10)) % 93.39/93.66 (define @t147 () (tptp.c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2 @t2 @t14 @t143 @t1 @t10)) % 93.39/93.66 (define @t148 () (tptp.c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1 @t2 @t14 @t143 @t1 @t10)) % 93.39/93.66 (define @t149 () (= (tptp.hAPP @t143 (tptp.hAPP @t14 @t148)) (tptp.hAPP @t143 (tptp.hAPP @t14 @t147)))) % 93.39/93.66 (define @t150 () (not @t149)) % 93.39/93.66 (define @t151 () (= (tptp.hAPP @t143 @t148) (tptp.hAPP @t143 @t147))) % 93.39/93.66 (define @t152 () (not @t151)) % 93.39/93.66 (define @t153 () (@list @t143 @t2 @t14 @t1 @t10)) % 93.39/93.66 (define @t154 () (not @t146)) % 93.39/93.66 (define @t155 () (@list @t143 @t14 @t2 @t1 @t10)) % 93.39/93.66 (define @t156 () (@list @t143 @t2 @t1 @t10 @t14)) % 93.39/93.66 (define @t157 () (tptp.c_Exceptions_Opreallocated @t131)) % 93.39/93.66 (define @t158 () (not @t157)) % 93.39/93.66 (define @t159 () (@var "V_h_H" $$unsorted)) % 93.39/93.66 (define @t160 () (tptp.c_Objects_Ohext @t131 @t159)) % 93.39/93.66 (define @t161 () (not @t160)) % 93.39/93.66 (define @t162 () (tptp.hAPP @t26 (tptp.hAPP @t135 @t130))) % 93.39/93.66 (define @t163 () (tptp.c_Fun_Oid @t10)) % 93.39/93.66 (define @t164 () (@var "T_c" $$unsorted)) % 93.39/93.66 (define @t165 () (tptp.c_Fun_Ocomp @t26 @t135 @t164 @t10 @t1)) % 93.39/93.66 (define @t166 () (@list @t1 @t14 @t10 @t3)) % 93.39/93.66 (define @t167 () (tptp.c_Expr_Oexp_OVal @t130 @t50)) % 93.39/93.66 (define @t168 () (not (tptp.c_BigStep_Oeval @t48 @t167 @t46 @t45 @t44))) % 93.39/93.66 (define @t169 () (@var "V_f1" $$unsorted)) % 93.39/93.66 (define @t170 () (tptp.hBOOL (tptp.hAPP @t48 @t169))) % 93.39/93.66 (define @t171 () (not @t170)) % 93.39/93.66 (define @t172 () (@var "V_f2" $$unsorted)) % 93.39/93.66 (define @t173 () (tptp.v_sko__Option__Xoption__Xsplit__1 @t48 @t172 @t3)) % 93.39/93.66 (define @t174 () (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP @t172 @t173))))) % 93.39/93.66 (define @t175 () (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_Option_Ooption_Ooption__case @t169 @t172 @t3 tptp.t_a tptp.t_b)))) % 93.39/93.66 (define @t176 () (@list @t48 @t169 @t172 @t3)) % 93.39/93.66 (define @t177 () (@var "V_Y" $$unsorted)) % 93.39/93.66 (define @t178 () (@list @t1 @t177)) % 93.39/93.66 (define @t179 () (@var "V_nat_H" $$unsorted)) % 93.39/93.66 (define @t180 () (tptp.c_Value_Oval_OAddr @t179)) % 93.39/93.66 (define @t181 () (@list @t179)) % 93.39/93.66 (define @t182 () (@var "V_X" $$unsorted)) % 93.39/93.66 (define @t183 () (tptp.c_Hilbert__Choice_Oinv__into @t13 @t14 @t1 @t10)) % 93.39/93.66 (define @t184 () (@list @t1 @t14 @t10)) % 93.39/93.66 (define @t185 () (@list @t1 @t3)) % 93.39/93.66 (define @t186 () (@list @t14 @t143 @t1 @t10)) % 93.39/93.66 (define @t187 () (@var "V_l" $$unsorted)) % 93.39/93.66 (define @t188 () (tptp.tc_Option_Ooption tptp.tc_Value_Oval)) % 93.39/93.66 (define @t189 () (tptp.tc_prod @t50 @t50)) % 93.39/93.66 (define @t190 () (tptp.tc_fun @t189 @t188)) % 93.39/93.66 (define @t191 () (tptp.tc_prod @t50 @t190)) % 93.39/93.66 (define @t192 () (tptp.tc_Option_Ooption @t191)) % 93.39/93.66 (define @t193 () (tptp.c_Pair (tptp.tc_fun tptp.tc_nat @t192) (tptp.tc_fun @t50 @t188))) % 93.39/93.66 (define @t194 () (tptp.hAPP (tptp.hAPP @t193 @t131) @t187)) % 93.39/93.66 (define @t195 () (@var "V_s_092_060_094isub_0620" $$unsorted)) % 93.39/93.66 (define @t196 () (tptp.c_Expr_Oexp_OVal (tptp.c_Value_Oval_OAddr @t26) @t50)) % 93.39/93.66 (define @t197 () (@var "V_fs" $$unsorted)) % 93.39/93.66 (define @t198 () (@var "V_C" $$unsorted)) % 93.39/93.66 (define @t199 () (tptp.c_Pair @t50 @t190)) % 93.39/93.66 (define @t200 () (tptp.hAPP @t199 @t198)) % 93.39/93.66 (define @t201 () (tptp.hAPP @t200 @t197)) % 93.39/93.66 (define @t202 () (tptp.c_Option_Ooption_OSome @t191)) % 93.39/93.66 (define @t203 () (tptp.hAPP @t202 @t201)) % 93.39/93.66 (define @t204 () (tptp.hAPP @t131 @t26)) % 93.39/93.66 (define @t205 () (not (= @t204 @t203))) % 93.39/93.66 (define @t206 () (tptp.c_Option_Ooption_OSome tptp.tc_Value_Oval)) % 93.39/93.66 (define @t207 () (tptp.hAPP @t206 @t130)) % 93.39/93.66 (define @t208 () (tptp.c_Pair @t50 @t50)) % 93.39/93.66 (define @t209 () (tptp.hAPP (tptp.hAPP @t208 @t52) @t51)) % 93.39/93.66 (define @t210 () (tptp.c_COMBK @t115 @t81 @t1)) % 93.39/93.66 (define @t211 () (@var "V_zs" $$unsorted)) % 93.39/93.66 (define @t212 () (tptp.c_Map_Omap__of (tptp.c_List_Ozip @t103 @t211 @t10 @t1) @t10 @t1)) % 93.39/93.66 (define @t213 () (tptp.c_Map_Omap__of (tptp.c_List_Ozip @t103 @t107 @t10 @t1) @t10 @t1)) % 93.39/93.66 (define @t214 () (tptp.c_Nat_Osize__class_Osize @t103 @t106)) % 93.39/93.66 (define @t215 () (tptp.tc_Option_Ooption @t1)) % 93.39/93.66 (define @t216 () (@var "V_z" $$unsorted)) % 93.39/93.66 (define @t217 () (tptp.c_Option_Ooption_OSome @t1)) % 93.39/93.66 (define @t218 () (tptp.hAPP @t217 @t216)) % 93.39/93.66 (define @t219 () (tptp.hAPP @t217 @t42)) % 93.39/93.66 (define @t220 () (tptp.c_Fun_Ofun__upd @t85 @t3 @t115 @t1 @t81)) % 93.39/93.66 (define @t221 () (@list @t82 @t51 @t1 @t10 @t3)) % 93.39/93.66 (define @t222 () (tptp.c_List_Ofilter @t48 @t103 @t1)) % 93.39/93.66 (define @t223 () (tptp.c_List_Ofilter @t48 @t123 @t1)) % 93.39/93.66 (define @t224 () (@list @t48 @t3 @t103 @t1)) % 93.39/93.66 (define @t225 () (@var "V_E" $$unsorted)) % 93.39/93.66 (define @t226 () (tptp.c_Progress_OWTrt_H @t48 @t131 @t225 @t47 @t127)) % 93.39/93.66 (define @t227 () (tptp.c_WellTypeRT_OWTrt @t48 @t131 @t225 @t47 @t127)) % 93.39/93.66 (define @t228 () (@list @t48 @t131 @t225 @t47 @t127)) % 93.39/93.66 (define @t229 () (not @t227)) % 93.39/93.66 (define @t230 () (@var "V_e_092_060_094isub_0622" $$unsorted)) % 93.39/93.66 (define @t231 () (@list @t10)) % 93.39/93.66 (define @t232 () (= @t2 @t95)) % 93.39/93.66 (define @t233 () (tptp.c_Set_Oimage @t14 @t2 @t10 @t1)) % 93.39/93.66 (define @t234 () (tptp.c_Fun_Ofun__upd @t131 @t26 (tptp.hAPP @t202 @t3) tptp.tc_nat @t192)) % 93.39/93.66 (define @t235 () (not (= @t204 (tptp.c_Option_Ooption_ONone @t191)))) % 93.39/93.66 (define @t236 () (@list @t131 @t26 @t3)) % 93.39/93.66 (define @t237 () (= (tptp.c_Fun_Ocomp @t183 @t14 @t10 @t1 @t1) @t120)) % 93.39/93.66 (define @t238 () (@list @t3 @t1)) % 93.39/93.66 (define @t239 () (@var "V_l_H" $$unsorted)) % 93.39/93.66 (define @t240 () (= @t3 @t42)) % 93.39/93.66 (define @t241 () (tptp.hAPP @t14 @t42)) % 93.39/93.66 (define @t242 () (not (= @t56 @t241))) % 93.39/93.66 (define @t243 () (@list @t14 @t3 @t42 @t1 @t10)) % 93.39/93.66 (define @t244 () (tptp.c_COMBK @t115 @t81 tptp.t_a)) % 93.39/93.66 (define @t245 () (@var "T_aa" $$unsorted)) % 93.39/93.66 (define @t246 () (@var "V_g2" $$unsorted)) % 93.39/93.66 (define @t247 () (= (tptp.c_Option_Ooption_Ooption__case @t3 @t172 @t43 @t1 @t245) (tptp.c_Option_Ooption_Ooption__case @t3 @t246 @t43 @t1 @t245))) % 93.39/93.66 (define @t248 () (tptp.c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1 @t43 @t172 @t246 @t245 @t1)) % 93.39/93.66 (define @t249 () (not (tptp.c_Fun_Oinj__on @t14 @t11 @t1 @t10))) % 93.39/93.66 (define @t250 () (@list @t10 @t14 @t11 @t1)) % 93.39/93.66 (define @t251 () (tptp.v_sko__Option__Xoption__Xsplit__asm__1 @t48 @t172 @t3)) % 93.39/93.66 (define @t252 () (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP @t172 @t251))))) % 93.39/93.66 (define @t253 () (not (tptp.c_Conform_Ohconf @t48 @t131 @t1))) % 93.39/93.66 (define @t254 () (@var "V_xo" $$unsorted)) % 93.39/93.66 (define @t255 () (tptp.c_Option_Oset @t254 @t1)) % 93.39/93.66 (define @t256 () (tptp.c_Conform_Osko__Conform__Xconf__def__1__1 @t48 @t127 @t131 @t130 @t1)) % 93.39/93.66 (define @t257 () (not @t4)) % 93.39/93.66 (define @t258 () (tptp.hAPP @t82 @t3)) % 93.39/93.66 (define @t259 () (tptp.hAPP (tptp.c_Map_Orestrict__map @t82 @t2 @t1 @t10) @t3)) % 93.39/93.66 (define @t260 () (@list @t82 @t2 @t1 @t10 @t3)) % 93.39/93.66 (define @t261 () (= @t26 @t22)) % 93.39/93.66 (define @t262 () (@var "V_d" $$unsorted)) % 93.39/93.66 (define @t263 () (= @t26 @t262)) % 93.39/93.66 (define @t264 () (not (= (tptp.c_Set_Oinsert @t26 @t137 @t1) (tptp.c_Set_Oinsert @t22 (tptp.c_Set_Oinsert @t262 @t6 @t1) @t1)))) % 93.39/93.66 (define @t265 () (@list @t26 @t135 @t1 @t22 @t262)) % 93.39/93.66 (define @t266 () (= @t135 @t22)) % 93.39/93.66 (define @t267 () (= @t135 @t262)) % 93.39/93.66 (define @t268 () (tptp.c_Orderings_Obot__class_Obot (tptp.tc_fun tptp.t_a tptp.tc_bool))) % 93.39/93.66 (define @t269 () (tptp.hAPP @t217 @t3)) % 93.39/93.66 (define @t270 () (tptp.c_Option_Oset @t269 @t1)) % 93.39/93.66 (define @t271 () (tptp.hAPP @t110 @t42)) % 93.39/93.66 (define @t272 () (tptp.c_Orderings_Otop__class_Otop (tptp.tc_fun @t245 tptp.tc_bool))) % 93.39/93.66 (define @t273 () (tptp.c_TypeRel_Ohas__field @t48 @t198 @t52 @t127 @t51 @t1)) % 93.39/93.66 (define @t274 () (not @t273)) % 93.39/93.66 (define @t275 () (tptp.c_Option_Ooption_OSome tptp.tc_Type_Oty)) % 93.39/93.66 (define @t276 () (tptp.hAPP @t275 @t127)) % 93.39/93.66 (define @t277 () (tptp.c_TypeRel_Osko__TypeRel__Xhas__field__def__1__1 @t198 @t51 @t52 @t48 @t127 @t1)) % 93.39/93.66 (define @t278 () (tptp.c_List_Oset @t123 @t1)) % 93.39/93.66 (define @t279 () (= @t42 @t3)) % 93.39/93.66 (define @t280 () (tptp.c_Map_Oran @t82 @t10 @t1)) % 93.39/93.66 (define @t281 () (tptp.hAPP @t217 @t135)) % 93.39/93.66 (define @t282 () (tptp.hAPP @t82 @t26)) % 93.39/93.66 (define @t283 () (not (= @t282 @t281))) % 93.39/93.66 (define @t284 () (@list @t82 @t26 @t1 @t135 @t10)) % 93.39/93.66 (define @t285 () (tptp.c_Hilbert__Choice_Oinv__into @t2 @t14 @t10 @t1)) % 93.39/93.66 (define @t286 () (tptp.hBOOL (tptp.c_in @t42 @t19 @t10))) % 93.39/93.66 (define @t287 () (not @t286)) % 93.39/93.66 (define @t288 () (tptp.c_Hilbert__Choice_Oinv__into @t2 @t14 @t1 @t10)) % 93.39/93.66 (define @t289 () (@list @t2 @t14 @t1 @t10 @t3)) % 93.39/93.66 (define @t290 () (not (tptp.c_Fun_Oinj__on @t14 @t2 @t245 @t1))) % 93.39/93.66 (define @t291 () (not (tptp.hBOOL (tptp.c_in @t3 @t2 @t245)))) % 93.39/93.66 (define @t292 () (@list @t3 @t2 @t245 @t14 @t1)) % 93.39/93.66 (define @t293 () (tptp.c_Fun_Othe__inv__into @t2 @t14 @t1 @t10)) % 93.39/93.66 (define @t294 () (tptp.hBOOL (tptp.c_in @t26 (tptp.c_Map_Odom @t82 @t1 @t10) @t1))) % 93.39/93.66 (define @t295 () (= @t282 @t115)) % 93.39/93.66 (define @t296 () (@list @t2 @t14 @t1 @t10)) % 93.39/93.66 (define @t297 () (= @t2 @t11)) % 93.39/93.66 (define @t298 () (tptp.c_COMBK @t22 @t1 @t10)) % 93.39/93.66 (define @t299 () (@var "V_l2" $$unsorted)) % 93.39/93.66 (define @t300 () (tptp.hBOOL (tptp.c_in @t82 (tptp.c_Map_Odom @t299 @t1 @t10) @t1))) % 93.39/93.66 (define @t301 () (@var "V_l1" $$unsorted)) % 93.39/93.66 (define @t302 () (tptp.hAPP (tptp.c_Map_Omap__add @t301 @t299 @t1 @t10) @t82)) % 93.39/93.66 (define @t303 () (= @t302 (tptp.hAPP @t299 @t82))) % 93.39/93.66 (define @t304 () (@list @t301 @t299 @t1 @t10 @t82)) % 93.39/93.66 (define @t305 () (@var "V_m_092_060_094isub_0622" $$unsorted)) % 93.39/93.66 (define @t306 () (@var "V_m_092_060_094isub_0621" $$unsorted)) % 93.39/93.66 (define @t307 () (tptp.c_Option_Ooption_OSome @t245)) % 93.39/93.66 (define @t308 () (tptp.c_Option_Ooption_OSome tptp.t_b)) % 93.39/93.66 (define @t309 () (= @t3 (tptp.hAPP @t308 @t251))) % 93.39/93.66 (define @t310 () (= @t3 (tptp.hAPP @t308 @t173))) % 93.39/93.66 (define @t311 () (tptp.c_Option_Ooption_ONone tptp.t_b)) % 93.39/93.66 (define @t312 () (= @t3 @t311)) % 93.39/93.66 (define @t313 () (@var "V_g1" $$unsorted)) % 93.39/93.66 (define @t314 () (= (tptp.c_Option_Ooption_Ooption__case @t169 @t172 @t3 @t10 @t1) (tptp.c_Option_Ooption_Ooption__case @t313 @t246 @t3 @t10 @t1))) % 93.39/93.66 (define @t315 () (= @t3 @t55)) % 93.39/93.66 (define @t316 () (tptp.c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1 @t3 @t172 @t246 @t1 @t10)) % 93.39/93.66 (define @t317 () (@var "T_d" $$unsorted)) % 93.39/93.66 (define @t318 () (@var "V_k" $$unsorted)) % 93.39/93.66 (define @t319 () (@var "V_m2" $$unsorted)) % 93.39/93.66 (define @t320 () (tptp.hAPP @t319 @t318)) % 93.39/93.66 (define @t321 () (= @t320 @t115)) % 93.39/93.66 (define @t322 () (@var "V_m1" $$unsorted)) % 93.39/93.66 (define @t323 () (tptp.c_Map_Osko__Map__Xmap__comp__None__iff__1__1 @t318 @t322 @t319 @t164 @t10 @t1)) % 93.39/93.66 (define @t324 () (tptp.c_Map_Omap__comp @t322 @t319 @t318 @t10 @t1 @t164)) % 93.39/93.66 (define @t325 () (= @t324 @t55)) % 93.39/93.66 (define @t326 () (not @t325)) % 93.39/93.66 (define @t327 () (@list @t322 @t319 @t318 @t10 @t1 @t164)) % 93.39/93.66 (define @t328 () (tptp.c_split @t1 @t10 @t164)) % 93.39/93.66 (define @t329 () (@list @t1 @t10 @t164 @t14)) % 93.39/93.66 (define @t330 () (tptp.hBOOL (tptp.hAPP @t2 @t3))) % 93.39/93.66 (define @t331 () (tptp.c_Set_Oinsert @t42 @t2 @t1)) % 93.39/93.66 (define @t332 () (tptp.hBOOL (tptp.hAPP @t331 @t3))) % 93.39/93.66 (define @t333 () (@list @t14 @t3 @t2 @t1 @t10)) % 93.39/93.66 (define @t334 () (tptp.c_Set_Oinsert @t3 @t11 @t1)) % 93.39/93.66 (define @t335 () (@var "V_p" $$unsorted)) % 93.39/93.66 (define @t336 () (tptp.c_Product__Type_Oapfst @t143 @t317 @t1 @t164)) % 93.39/93.66 (define @t337 () (tptp.c_Product__Type_Oapsnd @t164 @t10 @t1)) % 93.39/93.66 (define @t338 () (tptp.hAPP @t337 @t14)) % 93.39/93.66 (define @t339 () (tptp.c_Fun_Ocomp @t14 @t143 @t164 @t10 @t317)) % 93.39/93.66 (define @t340 () (tptp.c_Pair @t1 @t10)) % 93.39/93.66 (define @t341 () (tptp.c_Product__Type_Oapfst @t14 @t164 @t1 @t10)) % 93.39/93.66 (define @t342 () (tptp.c_snd @t3 @t10 @t164)) % 93.39/93.66 (define @t343 () (tptp.hAPP @t328 @t14)) % 93.39/93.66 (define @t344 () (tptp.hAPP (tptp.hAPP @t22 @t26) @t135)) % 93.39/93.66 (define @t345 () (tptp.c_Pair @t10 @t164)) % 93.39/93.66 (define @t346 () (tptp.hAPP (tptp.hAPP @t345 @t26) @t135)) % 93.39/93.66 (define @t347 () (tptp.c_Option_Omap @t14 @t10 @t1)) % 93.39/93.66 (define @t348 () (not (tptp.hBOOL (tptp.c_in @t135 @t2 @t1)))) % 93.39/93.66 (define @t349 () (tptp.c_Fun_Oswap @t26 @t135 @t14 @t1 @t10)) % 93.39/93.66 (define @t350 () (tptp.c_Fun_Oinj__on @t349 @t2 @t1 @t10)) % 93.39/93.66 (define @t351 () (@list @t26 @t135 @t14 @t1 @t10 @t2)) % 93.39/93.66 (define @t352 () (tptp.c_snd @t335 @t1 @t10)) % 93.39/93.66 (define @t353 () (tptp.c_fst @t335 @t1 @t10)) % 93.39/93.66 (define @t354 () (@var "V_ps" $$unsorted)) % 93.39/93.66 (define @t355 () (tptp.tc_prod @t1 @t10)) % 93.39/93.66 (define @t356 () (@var "V_n" $$unsorted)) % 93.39/93.66 (define @t357 () (tptp.hAPP (tptp.c_Map_Omap__add @t82 @t356 @t10 @t1) @t318)) % 93.39/93.66 (define @t358 () (= @t357 @t55)) % 93.39/93.66 (define @t359 () (tptp.hAPP @t356 @t318)) % 93.39/93.66 (define @t360 () (= @t359 @t55)) % 93.39/93.66 (define @t361 () (not @t360)) % 93.39/93.66 (define @t362 () (tptp.hAPP @t82 @t318)) % 93.39/93.66 (define @t363 () (= @t362 @t55)) % 93.39/93.66 (define @t364 () (@var "V_t" $$unsorted)) % 93.39/93.66 (define @t365 () (tptp.c_Option_Ooption_ONone @t164)) % 93.39/93.66 (define @t366 () (tptp.c_Map_Omap__comp @t322 @t319 @t318 @t1 @t164 @t10)) % 93.39/93.66 (define @t367 () (tptp.c_Map_Omap__add @t143 @t14 @t1 @t10)) % 93.39/93.66 (define @t368 () (tptp.hBOOL (tptp.c_in @t56 @t233 @t1))) % 93.39/93.66 (define @t369 () (tptp.c_Fun_Ocomp @t14 @t143 @t164 @t10 @t1)) % 93.39/93.66 (define @t370 () (tptp.c_Map_Omap__le @t143 @t131 @t1 @t10)) % 93.39/93.66 (define @t371 () (tptp.c_Map_Omap__add @t14 @t143 @t1 @t10)) % 93.39/93.66 (define @t372 () (tptp.c_Map_Omap__le @t14 @t371 @t1 @t10)) % 93.39/93.66 (define @t373 () (not @t372)) % 93.39/93.66 (define @t374 () (tptp.c_Map_Omap__le @t371 @t131 @t1 @t10)) % 93.39/93.66 (define @t375 () (tptp.tc_prod (tptp.tc_List_Olist @t50) (tptp.tc_Expr_Oexp @t50))) % 93.39/93.66 (define @t376 () (tptp.c_TypeRel_Owiden tptp.v_P tptp.v_Tv____ tptp.v_TF____ @t375)) % 93.39/93.66 (define @t377 () (@var "V_obj" $$unsorted)) % 93.39/93.66 (define @t378 () (tptp.c_Conform_Ooconf @t48 @t131 @t377 @t1)) % 93.39/93.66 (define @t379 () (not @t378)) % 93.39/93.66 (define @t380 () (tptp.hAPP @t202 @t377)) % 93.39/93.66 (define @t381 () (tptp.tc_Option_Ooption @t164)) % 93.39/93.66 (define @t382 () (tptp.c_COMBK @t365 @t381 tptp.t_a)) % 93.39/93.66 (define @t383 () (tptp.c_Option_Omap @t14 @t164 @t10)) % 93.39/93.66 (define @t384 () (@var "V_as" $$unsorted)) % 93.39/93.66 (define @t385 () (tptp.hAPP @t110 @t135)) % 93.39/93.66 (define @t386 () (@var "V_bs" $$unsorted)) % 93.39/93.66 (define @t387 () (tptp.c_Map_Omap__upds (tptp.c_Fun_Ofun__upd @t82 @t26 @t385 @t1 @t81) @t384 @t386 @t1 @t10)) % 93.39/93.66 (define @t388 () (@var "V_e2" $$unsorted)) % 93.39/93.66 (define @t389 () (@var "V_u1" $$unsorted)) % 93.39/93.66 (define @t390 () (tptp.hAPP @t110 @t389)) % 93.39/93.66 (define @t391 () (@var "V_e1" $$unsorted)) % 93.39/93.66 (define @t392 () (tptp.c_Fun_Ofun__upd @t82 @t26 @t281 @t10 @t215)) % 93.39/93.66 (define @t393 () (tptp.c_ATP__Linkup_Osko__Option__Xospec__1__1 @t269 @t48 @t1)) % 93.39/93.66 (define @t394 () (tptp.c_Set_Oimage @t143 @t2 @t164 @t1)) % 93.39/93.66 (define @t395 () (not (tptp.c_Fun_Oinj__on @t14 @t394 @t1 @t10))) % 93.39/93.66 (define @t396 () (not (tptp.c_Fun_Oinj__on @t143 @t2 @t164 @t1))) % 93.39/93.66 (define @t397 () (not (tptp.hBOOL (tptp.c_in @t3 (tptp.c_Set_Oimage @t14 @t394 @t1 @t10) @t10)))) % 93.39/93.66 (define @t398 () (tptp.c_Fun_Ocomp @t14 @t143 @t1 @t10 @t164)) % 93.39/93.66 (define @t399 () (@list @t2 @t14 @t143 @t1 @t10 @t164 @t3)) % 93.39/93.66 (define @t400 () (tptp.c_Objects_Otypeof__h @t131 @t130)) % 93.39/93.66 (define @t401 () (tptp.hAPP @t200 (tptp.c_Fun_Ofun__upd @t197 @t209 @t207 @t189 @t188))) % 93.39/93.66 (define @t402 () (tptp.hAPP @t202 @t401)) % 93.39/93.66 (define @t403 () (tptp.c_Expr_Oexp_OVal tptp.c_Value_Oval_OUnit @t50)) % 93.39/93.66 (define @t404 () (@var "V_l_092_060_094isub_0622" $$unsorted)) % 93.39/93.66 (define @t405 () (@var "V_h_092_060_094isub_0622" $$unsorted)) % 93.39/93.66 (define @t406 () (@var "V_e_092_060_094isub_0621" $$unsorted)) % 93.39/93.66 (define @t407 () (@var "V_s_092_060_094isub_0621" $$unsorted)) % 93.39/93.66 (define @t408 () (@var "V_fs_H" $$unsorted)) % 93.39/93.66 (define @t409 () (tptp.hAPP @t200 @t408)) % 93.39/93.66 (define @t410 () (tptp.c_Fun_Ofun__upd @t131 @t26 (tptp.hAPP @t202 @t409) tptp.tc_nat @t192)) % 93.39/93.66 (define @t411 () (@list @t131 @t26 @t198 @t197 @t408)) % 93.39/93.66 (define @t412 () (tptp.hAPP @t159 @t26)) % 93.39/93.66 (define @t413 () (not (= @t400 @t276))) % 93.39/93.66 (define @t414 () (@list @t131 @t130 @t127 @t48 @t225)) % 93.39/93.66 (define @t415 () (tptp.tc_prod @t10 @t1)) % 93.39/93.66 (define @t416 () (tptp.hAPP @t340 @t3)) % 93.39/93.66 (define @t417 () (tptp.hAPP @t416 @t42)) % 93.39/93.66 (define @t418 () (tptp.c_split @t10 @t164 @t1)) % 93.39/93.66 (define @t419 () (tptp.c_Fun_Ocomp @t131 @t14 @t10 @t164 @t1)) % 93.39/93.66 (define @t420 () (not (tptp.class_OrderedGroup_Ocomm__monoid__mult @t164))) % 93.39/93.66 (define @t421 () (@list @t164 @t131 @t14 @t11 @t1 @t10)) % 93.39/93.66 (define @t422 () (tptp.hBOOL (tptp.c_in @t148 @t2 @t1))) % 93.39/93.66 (define @t423 () (tptp.hBOOL (tptp.c_in @t147 @t2 @t1))) % 93.39/93.66 (define @t424 () (tptp.hBOOL (tptp.c_in @t90 @t19 @t10))) % 93.39/93.66 (define @t425 () (@var "V_m_H" $$unsorted)) % 93.39/93.66 (define @t426 () (tptp.c_Map_Odom @t425 @t1 @t10)) % 93.39/93.66 (define @t427 () (tptp.c_Fun_Oinj__on @t425 @t426 @t1 @t81)) % 93.39/93.66 (define @t428 () (tptp.c_Fun_Oinj__on (tptp.c_Map_Omap__add @t82 @t425 @t1 @t10) @t426 @t1 @t81)) % 93.39/93.66 (define @t429 () (@list @t1 @t10 @t164)) % 93.39/93.66 (define @t430 () (@var "V_h_H_H" $$unsorted)) % 93.39/93.66 (define @t431 () (not @t358)) % 93.39/93.66 (define @t432 () (@list @t82 @t356 @t10 @t1 @t318)) % 93.39/93.66 (define @t433 () (= @t357 @t269)) % 93.39/93.66 (define @t434 () (= @t362 @t269)) % 93.39/93.66 (define @t435 () (not (tptp.hBOOL (tptp.c_in @t42 @t2 @t1)))) % 93.39/93.66 (define @t436 () (@list @t14 @t3 @t42 @t2 @t1 @t10)) % 93.39/93.66 (define @t437 () (@list @t169 @t172 @t10 @t1)) % 93.39/93.66 (define @t438 () (@var "V_Q" $$unsorted)) % 93.39/93.66 (define @t439 () (tptp.c_COMBI @t1)) % 93.39/93.66 (define @t440 () (tptp.c_Conform_Oconf @t48 @t410 @t3 @t127 @t1)) % 93.39/93.66 (define @t441 () (tptp.c_Conform_Oconf @t48 @t131 @t3 @t127 @t1)) % 93.39/93.66 (define @t442 () (tptp.c_snd @t364 @t1 @t10)) % 93.39/93.66 (define @t443 () (tptp.c_fst @t364 @t1 @t10)) % 93.39/93.66 (define @t444 () (tptp.hBOOL (tptp.c_in @t3 @t129 @t1))) % 93.39/93.66 (define @t445 () (tptp.hBOOL (tptp.hAPP @t129 @t3))) % 93.39/93.66 (define @t446 () (@list @t26 @t135 @t14 @t1 @t10)) % 93.39/93.66 (define @t447 () (not (tptp.c_Map_Omap__le @t14 @t143 @t1 @t10))) % 93.39/93.66 (define @t448 () (@var "V_q" $$unsorted)) % 93.39/93.66 (define @t449 () (tptp.hAPP (tptp.c_Fun_Ooverride__on @t14 @t143 @t2 @t1 @t10) @t26)) % 93.39/93.66 (define @t450 () (@list @t14 @t143 @t2 @t1 @t10 @t26)) % 93.39/93.66 (define @t451 () (not (tptp.c_Map_Omap__le @t322 @t319 @t1 @t10))) % 93.39/93.66 (define @t452 () (@var "V_m3" $$unsorted)) % 93.39/93.66 (define @t453 () (tptp.c_snd @t3 @t1 @t164)) % 93.39/93.66 (define @t454 () (= (tptp.hAPP @t14 @t453) (tptp.hAPP @t143 @t453))) % 93.39/93.66 (define @t455 () (tptp.hAPP @t338 @t3)) % 93.39/93.66 (define @t456 () (= @t455 (tptp.hAPP (tptp.hAPP @t337 @t143) @t3))) % 93.39/93.66 (define @t457 () (@var "V_exp2" $$unsorted)) % 93.39/93.66 (define @t458 () (@var "V_exp1" $$unsorted)) % 93.39/93.66 (define @t459 () (not (= (tptp.c_Expr_Oexp_OFAss @t458 @t65 @t63 @t457 @t1) @t75))) % 93.39/93.66 (define @t460 () (@list @t458 @t65 @t63 @t457 @t1 @t74 @t35 @t34 @t73)) % 93.39/93.66 (define @t461 () (tptp.hAPP @t14 (tptp.hAPP @t143 @t3))) % 93.39/93.66 (define @t462 () (tptp.c_Fun_Ocomp @t14 @t143 @t10 @t1 @t164)) % 93.39/93.66 (define @t463 () (tptp.hAPP @t462 @t3)) % 93.39/93.66 (define @t464 () (tptp.hAPP @t143 @t26)) % 93.39/93.66 (define @t465 () (tptp.c_Map_Omap__add @t322 @t319 @t1 @t10)) % 93.39/93.66 (define @t466 () (tptp.c_Pair @t10 @t1)) % 93.39/93.66 (define @t467 () (@var "V_opt" $$unsorted)) % 93.39/93.66 (define @t468 () (tptp.c_Product__Type_Oprod_Oprod__case @t10 @t164 @t1)) % 93.39/93.66 (define @t469 () (= @t371 @t367)) % 93.39/93.66 (define @t470 () (tptp.hBOOL (tptp.c_in @t26 (tptp.c_Set_Oinsert @t135 @t2 @t1) @t1))) % 93.39/93.66 (define @t471 () (@var "V_FDTs" $$unsorted)) % 93.39/93.66 (define @t472 () (not (tptp.c_TypeRel_OFields @t48 @t198 @t471 @t1))) % 93.39/93.66 (define @t473 () (@var "V_FDTs_H" $$unsorted)) % 93.39/93.66 (define @t474 () (@var "V_nat" $$unsorted)) % 93.39/93.66 (define @t475 () (tptp.c_fst @t3 @t164 @t10)) % 93.39/93.66 (define @t476 () (tptp.hAPP @t14 @t475)) % 93.39/93.66 (define @t477 () (tptp.hAPP @t341 @t3)) % 93.39/93.66 (define @t478 () (= @t476 (tptp.hAPP @t143 @t475))) % 93.39/93.66 (define @t479 () (= @t477 (tptp.hAPP (tptp.c_Product__Type_Oapfst @t143 @t164 @t1 @t10) @t3))) % 93.39/93.66 (define @t480 () (= @t359 @t269)) % 93.39/93.66 (define @t481 () (not @t433)) % 93.39/93.66 (define @t482 () (@list @t82 @t356 @t10 @t1 @t318 @t3)) % 93.39/93.66 (define @t483 () (tptp.c_Fun_Ofun__upd @t14 @t3 @t42 @t1 @t10)) % 93.39/93.66 (define @t484 () (@var "V_r" $$unsorted)) % 93.39/93.66 (define @t485 () (tptp.hAPP @t110 @t3)) % 93.39/93.66 (define @t486 () (not (= @t320 @t485))) % 93.39/93.66 (define @t487 () (tptp.hAPP @t322 @t3)) % 93.39/93.66 (define @t488 () (@var "V_a_H" $$unsorted)) % 93.39/93.66 (define @t489 () (= @t26 @t488)) % 93.39/93.66 (define @t490 () (@var "V_list_H" $$unsorted)) % 93.39/93.66 (define @t491 () (@var "V_list" $$unsorted)) % 93.39/93.66 (define @t492 () (not (= (tptp.c_List_Olist_OCons @t26 @t491 @t1) (tptp.c_List_Olist_OCons @t488 @t490 @t1)))) % 93.39/93.66 (define @t493 () (@list @t26 @t491 @t1 @t488 @t490)) % 93.39/93.66 (define @t494 () (@var "T_e" $$unsorted)) % 93.39/93.66 (define @t495 () (@var "V_g_H" $$unsorted)) % 93.39/93.66 (define @t496 () (@var "V_f_H" $$unsorted)) % 93.39/93.66 (define @t497 () (tptp.hAPP (tptp.hAPP @t466 @t3) @t42)) % 93.39/93.66 (define @t498 () (tptp.c_snd @t497 @t10 @t1)) % 93.39/93.66 (define @t499 () (@var "V_val_H" $$unsorted)) % 93.39/93.66 (define @t500 () (tptp.c_TypeRel_Ohas__field tptp.v_P tptp.v_C____ tptp.v_F____ tptp.v_TF____ tptp.v_D____ @t375)) % 93.39/93.66 (define @t501 () (tptp.hAPP @t199 tptp.v_C____)) % 93.39/93.66 (define @t502 () (tptp.hAPP @t501 tptp.v_fs____)) % 93.39/93.66 (define @t503 () (= (tptp.hAPP tptp.v_ha____ tptp.v_a____) (tptp.hAPP @t202 @t502))) % 93.39/93.66 (define @t504 () (tptp.hAPP @t172 @t26)) % 93.39/93.66 (define @t505 () (tptp.hAPP @t110 @t26)) % 93.39/93.66 (define @t506 () (@list @t169 @t172 @t10 @t26 @t1)) % 93.39/93.66 (define @t507 () (= @t216 @t3)) % 93.39/93.66 (define @t508 () (tptp.hAPP @t14 @t216)) % 93.39/93.66 (define @t509 () (@list @t14 @t3 @t42 @t1 @t10 @t216)) % 93.39/93.66 (define @t510 () (@var "V_b_H" $$unsorted)) % 93.39/93.66 (define @t511 () (tptp.hAPP (tptp.hAPP @t340 @t26) @t135)) % 93.39/93.66 (define @t512 () (not (= @t511 (tptp.hAPP (tptp.hAPP @t340 @t488) @t510)))) % 93.39/93.66 (define @t513 () (@list @t1 @t10 @t26 @t135 @t488 @t510)) % 93.39/93.66 (define @t514 () (tptp.hAPP @t217 @t130)) % 93.39/93.66 (define @t515 () (@var "V_xb" $$unsorted)) % 93.39/93.66 (define @t516 () (tptp.c_Pair tptp.t_b tptp.t_c)) % 93.39/93.66 (define @t517 () (tptp.hAPP (tptp.c_Product__Type_Oprod_Oprod__case tptp.t_b tptp.t_c tptp.t_a) @t169)) % 93.39/93.66 (define @t518 () (tptp.hAPP (tptp.hAPP @t169 @t26) @t135)) % 93.39/93.66 (define @t519 () (tptp.hAPP @t14 @t135)) % 93.39/93.66 (define @t520 () (= (tptp.c_Objects_Otypeof__h tptp.v_ha____ tptp.v_v____) (tptp.hAPP @t275 tptp.v_Tv____))) % 93.39/93.66 (define @t521 () (tptp.c_Conform_Ohconf tptp.v_P tptp.v_ha____ @t375)) % 93.39/93.66 (define @t522 () (tptp.hAPP @t217 @t488)) % 93.39/93.66 (define @t523 () (@list @t1 @t488)) % 93.39/93.66 (define @t524 () (@var "V_R" $$unsorted)) % 93.39/93.66 (define @t525 () (tptp.hAPP @t90 @t135)) % 93.39/93.66 (define @t526 () (tptp.hBOOL @t525)) % 93.39/93.66 (define @t527 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_split @t1 @t10 tptp.tc_bool) @t14) @t511))) % 93.39/93.66 (define @t528 () (= (tptp.hAPP @t392 @t3) @t219)) % 93.39/93.66 (define @t529 () (= @t3 @t26)) % 93.39/93.66 (define @t530 () (= @t258 @t219)) % 93.39/93.66 (define @t531 () (= @t135 @t42)) % 93.39/93.66 (define @t532 () (not @t528)) % 93.39/93.66 (define @t533 () (@list @t82 @t26 @t1 @t135 @t10 @t3 @t42)) % 93.39/93.66 (define @t534 () (tptp.hBOOL (tptp.hAPP @t14 @t511))) % 93.39/93.66 (define @t535 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_curry @t14 @t1 @t10 tptp.tc_bool) @t26) @t135))) % 93.39/93.66 (define @t536 () (@list @t14 @t1 @t10 @t26 @t135)) % 93.39/93.66 (define @t537 () (@var "V_k_H" $$unsorted)) % 93.39/93.66 (define @t538 () (not (tptp.hBOOL (tptp.hAPP @t48 @t335)))) % 93.39/93.66 (define @t539 () (not (tptp.hBOOL (tptp.hAPP @t438 @t448)))) % 93.39/93.66 (define @t540 () (tptp.hAPP (tptp.hAPP @t340 @t335) @t448)) % 93.39/93.66 (define @t541 () (@var "V_xx" $$unsorted)) % 93.39/93.66 (define @t542 () (tptp.hAPP @t217 @t541)) % 93.39/93.66 (define @t543 () (forall (@list @t48 @t131 @t198 @t197 @t52 @t51 @t130 @t1 @t127) (or (tptp.c_Conform_Ooconf @t48 @t131 @t401 @t1) (not (tptp.c_Conform_Ooconf @t48 @t131 @t201 @t1)) @t133 @t274))) % 93.39/93.66 (define @t544 () (tptp.c_Conform_Ooconf tptp.v_P tptp.v_ha____ (tptp.hAPP @t501 (tptp.c_Fun_Ofun__upd tptp.v_fs____ (tptp.hAPP (tptp.hAPP @t208 tptp.v_F____) tptp.v_D____) (tptp.hAPP @t206 tptp.v_v____) @t189 @t188)) @t375)) % 93.39/93.66 (define @t545 () (@var "T_1" $$unsorted)) % 93.39/93.66 (define @t546 () (@var "T_2" $$unsorted)) % 93.39/93.66 (define @t547 () (tptp.tc_fun @t546 @t545)) % 93.39/93.66 (define @t548 () (@list @t546 @t545)) % 93.39/93.66 (define @t549 () (not @t376)) % 93.39/93.66 (define @t550 () (tptp.c_Conform_Oconf tptp.v_P tptp.v_ha____ tptp.v_v____ tptp.v_TF____ @t375)) % 93.39/93.66 (define @t551 () (not @t520)) % 93.39/93.66 (define @t552 () (or @t551 @t550 @t549)) % 93.39/93.66 (define @t553 () (@list false false false)) % 93.39/93.66 (define @t554 () (tptp.c_Conform_Ooconf tptp.v_P tptp.v_ha____ @t502 @t375)) % 93.39/93.66 (define @t555 () (not @t521)) % 93.39/93.66 (define @t556 () (not @t503)) % 93.39/93.66 (define @t557 () (or @t556 @t555 @t554)) % 93.39/93.66 (define @t558 () (not @t500)) % 93.39/93.66 (define @t559 () (not @t550)) % 93.39/93.66 (define @t560 () (not @t554)) % 93.39/93.66 (define @t561 () (or @t544 @t560 @t559 @t558)) % 93.39/93.66 (define @t562 () (not @t561)) % 93.39/93.66 (assume @p1 (forall @t9 (or (= (tptp.c_HOL_Ominus__class_Ominus @t8 @t7 @t5) @t2) @t4))) % 93.39/93.66 (assume @p2 (forall (@list @t10 @t2 @t11) (or (not (tptp.class_HOL_Ominus @t10)) (= (tptp.hAPP (tptp.c_HOL_Ominus__class_Ominus @t2 @t11 @t12) tptp.v_x) (tptp.c_HOL_Ominus__class_Ominus (tptp.hAPP @t2 tptp.v_x) (tptp.hAPP @t11 tptp.v_x) @t10))))) % 93.39/93.66 (assume @p3 (forall @t21 (or (= (tptp.c_Set_Oimage @t14 @t20 @t1 @t10) (tptp.c_HOL_Ominus__class_Ominus @t19 @t18 @t17)) @t16))) % 93.39/93.66 (assume @p4 (forall (@list @t22 @t2 @t11 @t1) (or @t25 @t24 (not @t23)))) % 93.39/93.66 (assume @p5 (forall @t31 (= @t30 @t27))) % 93.39/93.66 (assume @p6 (forall (@list @t36 @t35 @t34 @t1 @t32) (not (= @t37 @t33)))) % 93.39/93.66 (assume @p7 (forall (@list @t1 @t3 @t39 @t38) (or @t41 (not (= @t40 (tptp.c_HOL_Ominus__class_Ominus @t39 @t38 @t1))) (= @t39 @t38)))) % 93.39/93.66 (assume @p8 (forall (@list @t1 @t43 @t42 @t3) (or @t41 (not (= (tptp.c_HOL_Ominus__class_Ominus @t43 @t42 @t1) @t40)) (= @t43 @t42)))) % 93.39/93.66 (assume @p9 (forall (@list @t2 @t11 @t1) (= (tptp.c_HOL_Ominus__class_Ominus @t20 @t11 @t5) @t20))) % 93.39/93.66 (assume @p10 (forall (@list @t48 @t47 @t52 @t51 @t46 @t45 @t44) (or (tptp.c_SmallStep_Oredp @t48 @t53 @t46 (tptp.c_Expr_Oexp_OFAcc @t45 @t52 @t51 @t50) @t44) @t49))) % 93.39/93.66 (assume @p11 (forall (@list @t14 @t3 @t1 @t10 @t2) (or (not (= @t56 @t55)) (= (tptp.c_HOL_Ominus__class_Ominus @t54 (tptp.c_Set_Oinsert @t3 @t2 @t10) @t17) (tptp.c_HOL_Ominus__class_Ominus @t54 @t2 @t17))))) % 93.39/93.66 (assume @p12 (forall @t21 (or (tptp.c_Fun_Oinj__on @t14 @t20 @t1 @t10) @t58))) % 93.39/93.66 (assume @p13 (forall @t61 (= @t60 (tptp.c_HOL_Ominus__class_Ominus @t20 @t28 @t5)))) % 93.39/93.66 (assume @p14 (forall @t61 (= @t60 (tptp.c_HOL_Ominus__class_Ominus @t29 @t11 @t5)))) % 93.39/93.66 (assume @p15 (forall (@list @t22 @t2 @t1 @t11) (or @t23 @t62))) % 93.39/93.66 (assume @p16 (forall (@list @t22 @t11 @t1 @t2) (or (not @t24) @t62))) % 93.39/93.66 (assume @p17 (forall @t69 (or @t68 @t64))) % 93.39/93.66 (assume @p18 (forall @t69 (or @t68 @t70))) % 93.39/93.66 (assume @p19 (forall @t69 (or @t68 (= @t66 @t36)))) % 93.39/93.66 (assume @p20 (forall @t71 (= (tptp.c_HOL_Ominus__class_Ominus @t2 @t6 @t5) @t2))) % 93.39/93.66 (assume @p21 (forall @t71 (= (tptp.c_HOL_Ominus__class_Ominus @t2 @t2 @t5) @t6))) % 93.39/93.66 (assume @p22 (forall @t72 (= (tptp.c_HOL_Ominus__class_Ominus @t6 @t2 @t5) @t6))) % 93.39/93.66 (assume @p23 (forall (@list @t74 @t35 @t34 @t73 @t1 @t66 @t65 @t63) (not (= @t75 @t67)))) % 93.39/93.66 (assume @p24 (forall @t71 (= (tptp.c_HOL_Ominus__class_Ominus @t2 @t13 @t5) @t6))) % 93.39/93.66 (assume @p25 (forall (@list @t66 @t65 @t63 @t1 @t74 @t35 @t34 @t73) (not (= @t67 @t75)))) % 93.39/93.66 (assume @p26 (forall @t31 (or (= @t30 @t2) @t77))) % 93.39/93.66 (assume @p27 (forall (@list @t32 @t1 @t36 @t35 @t34) (not (= @t33 @t37)))) % 93.39/93.66 (assume @p28 (forall @t80 (or (= @t79 (tptp.c_Set_Oinsert @t3 @t20 @t1)) @t78))) % 93.39/93.66 (assume @p29 (forall @t80 (or (= @t79 @t20) (not @t78)))) % 93.39/93.66 (assume @p30 (forall @t87 @t86)) % 93.39/93.66 (assume @p31 (forall @t92 (or (not @t91) @t89))) % 93.39/93.66 (assume @p32 (forall @t92 (or @t88 @t91 @t58))) % 93.39/93.66 (assume @p33 (forall @t98 (or (= @t97 (tptp.c_Set_Oinsert @t42 (tptp.c_Set_Oimage @t14 (tptp.c_HOL_Ominus__class_Ominus @t2 (tptp.c_Set_Oinsert @t3 @t95 @t10) @t17) @t10 @t1) @t1)) @t94))) % 93.39/93.66 (assume @p34 (forall @t87 (or @t86 @t100))) % 93.39/93.66 (assume @p35 (forall @t102 (or (= @t101 @t84) @t100))) % 93.39/93.66 (assume @p36 (forall (@list @t103 @t107 @t1 @t10 @t3 @t43) (or (not (= @t113 @t111)) @t109 @t105))) % 93.39/93.66 (assume @p37 (forall @t117 (= (tptp.c_Map_Odom @t116 @t1 @t10) (tptp.c_HOL_Ominus__class_Ominus @t114 @t7 @t5)))) % 93.39/93.66 (assume @p38 (forall (@list @t103 @t107 @t1 @t10 @t3) (or (not @t119) @t109 @t118))) % 93.39/93.66 (assume @p39 (forall (@list @t103 @t1 @t107 @t10 @t3) (or @t109 @t119 @t105))) % 93.39/93.66 (assume @p40 (forall @t72 (tptp.c_Fun_Oinj__on @t120 @t2 @t1 @t1))) % 93.39/93.66 (assume @p41 (forall (@list @t43 @t3 @t1) (= (tptp.c_Set_Oinsert @t43 @t7 @t1) (tptp.c_Set_Oinsert @t3 (tptp.c_Set_Oinsert @t43 @t6 @t1) @t1)))) % 93.39/93.66 (assume @p42 (forall (@list @t3 @t103 @t1 @t48 @t107) (or (not (= @t123 @t122)) @t121))) % 93.39/93.66 (assume @p43 (forall @t125 (= @t124 @t6))) % 93.39/93.66 (assume @p44 (forall @t126 (tptp.c_Fun_Oinj__on @t14 @t6 @t1 @t10))) % 93.39/93.66 (assume @p45 (forall (@list @t48 @t127 @t1) (tptp.c_TypeRel_Owiden @t48 @t127 @t127 @t1))) % 93.39/93.66 (assume @p46 (forall (@list @t48 @t129 @t127 @t1 @t128) (or (tptp.c_TypeRel_Owiden @t48 @t129 @t127 @t1) (not (tptp.c_TypeRel_Owiden @t48 @t128 @t127 @t1)) (not (tptp.c_TypeRel_Owiden @t48 @t129 @t128 @t1))))) % 93.39/93.66 (assume @p47 (forall (@list @t48 @t131 @t130 @t134 @t1 @t127) (or (tptp.c_Conform_Oconf @t48 @t131 @t130 @t134 @t1) (not (tptp.c_TypeRel_Owiden @t48 @t127 @t134 @t1)) @t133))) % 93.39/93.66 (assume @p48 (forall (@list @t26 @t1 @t135) (or (not (= @t28 @t137)) @t136))) % 93.39/93.66 (assume @p49 (forall @t140 (or @t139 @t138))) % 93.39/93.66 (assume @p50 (forall @t141 (= (tptp.c_Option_Oset @t55 @t1) @t6))) % 93.39/93.66 (assume @p51 (forall @t153 (or @t152 @t150 @t146 @t145 @t142))) % 93.39/93.66 (assume @p52 (forall @t153 (or @t152 @t150 @t144 @t154 @t142))) % 93.39/93.66 (assume @p53 (forall @t155 (or @t146 @t145 @t142 @t151 @t149))) % 93.39/93.66 (assume @p54 (forall @t156 (or @t144 @t154 @t142 @t151 @t149))) % 93.39/93.66 (assume @p55 (forall (@list @t159 @t131) (or (tptp.c_Exceptions_Opreallocated @t159) @t161 @t158))) % 93.39/93.66 (assume @p56 (forall (@list @t26 @t135 @t164 @t10 @t1 @t22 @t130) (or (not (= @t165 (tptp.c_Fun_Ocomp @t163 @t22 @t10 @t10 @t1))) (= @t162 (tptp.hAPP @t22 @t130))))) % 93.39/93.66 (assume @p57 (forall @t166 (or (= (tptp.hAPP (tptp.c_Fun_Othe__inv__into @t13 @t14 @t1 @t10) @t56) @t3) @t16))) % 93.39/93.66 (assume @p58 (forall (@list @t44 @t46 @t48 @t130 @t45) (or (= @t44 @t46) @t168))) % 93.39/93.66 (assume @p59 (forall @t176 (or @t175 @t174 @t171))) % 93.39/93.66 (assume @p60 (forall @t178 (= (tptp.c_Set_Oimage @t120 @t177 @t1 @t1) @t177))) % 93.39/93.66 (assume @p61 (forall @t181 (not (= tptp.c_Value_Oval_OUnit @t180)))) % 93.39/93.66 (assume @p62 (forall (@list @t1 @t14 @t10 @t182) (or (= (tptp.c_Set_Oimage @t183 (tptp.c_Set_Oimage @t14 @t182 @t1 @t10) @t10 @t1) @t182) @t16))) % 93.39/93.66 (assume @p63 (forall (@list @t1 @t14 @t10 @t2) (or (= (tptp.c_Set_Oimage @t183 @t19 @t10 @t1) @t2) @t16))) % 93.39/93.66 (assume @p64 (forall @t184 (= @t6 @t124))) % 93.39/93.66 (assume @p65 (forall @t185 (= (tptp.hAPP @t120 @t3) @t3))) % 93.39/93.66 (assume @p66 (forall @t186 (= (tptp.c_Fun_Ooverride__on @t14 @t143 @t6 @t1 @t10) @t14))) % 93.39/93.66 (assume @p67 (forall (@list @t197 @t52 @t51 @t130 @t131 @t26 @t198 @t48 @t47 @t195 @t187) (or (not (= (tptp.hAPP @t197 @t209) @t207)) @t205 (not (tptp.c_BigStep_Oeval @t48 @t47 @t195 @t196 @t194)) (tptp.c_BigStep_Oeval @t48 @t53 @t195 @t167 @t194)))) % 93.39/93.66 (assume @p68 (forall (@list @t14 @t1 @t10 @t3) (or (not (= @t114 @t7)) (= @t14 (tptp.c_Fun_Ofun__upd @t210 @t3 (tptp.hAPP @t110 (tptp.c_Map_Osko__Map__Xdom__eq__singleton__conv__1__1 @t14 @t3 @t1 @t10)) @t1 @t81))))) % 93.39/93.66 (assume @p69 (forall (@list @t103 @t107 @t10 @t1 @t3 @t42 @t211 @t216) (or (not (= (tptp.c_Fun_Ofun__upd @t213 @t3 @t219 @t10 @t215) (tptp.c_Fun_Ofun__upd @t212 @t3 @t218 @t10 @t215))) (tptp.hBOOL (tptp.c_in @t3 (tptp.c_List_Oset @t103 @t10) @t10)) (not (= (tptp.c_Nat_Osize__class_Osize @t211 @t108) @t214)) (not (= (tptp.c_Nat_Osize__class_Osize @t107 @t108) @t214)) (= @t213 @t212)))) % 93.39/93.66 (assume @p70 (forall @t221 (or (= @t220 @t83) @t100))) % 93.39/93.66 (assume @p71 (forall @t141 (= (tptp.c_Hilbert__Choice_Oinv__into @t13 @t120 @t1 @t1) @t120))) % 93.39/93.66 (assume @p72 (forall (@list @t10 @t143 @t1) (= (tptp.c_Fun_Ocomp @t163 @t143 @t10 @t10 @t1) @t143))) % 93.39/93.66 (assume @p73 (forall @t126 (= (tptp.c_Fun_Ocomp @t14 @t120 @t1 @t10 @t1) @t14))) % 93.39/93.66 (assume @p74 (forall @t224 (or (= @t223 (tptp.c_List_Olist_OCons @t3 @t222 @t1)) @t139))) % 93.39/93.66 (assume @p75 (forall (@list @t10 @t1) (= (tptp.c_Map_Odom @t210 @t1 @t10) @t6))) % 93.39/93.66 (assume @p76 (forall (@list @t48 @t103 @t1 @t3) (or (not (= @t222 @t103)) @t121 @t118))) % 93.39/93.66 (assume @p77 (forall @t228 (or @t227 (not @t226)))) % 93.39/93.66 (assume @p78 (forall @t228 (or @t226 @t229))) % 93.39/93.66 (assume @p79 (forall (@list @t48 @t47 @t52 @t51 @t230 @t46 @t45 @t44) (or (tptp.c_SmallStep_Oredp @t48 (tptp.c_Expr_Oexp_OFAss @t47 @t52 @t51 @t230 @t50) @t46 (tptp.c_Expr_Oexp_OFAss @t45 @t52 @t51 @t230 @t50) @t44) @t49))) % 93.39/93.66 (assume @p80 (forall @t231 (or (not (tptp.class_Orderings_Obot @t10)) (= (tptp.hAPP (tptp.c_Orderings_Obot__class_Obot @t12) tptp.v_x) (tptp.c_Orderings_Obot__class_Obot @t10))))) % 93.39/93.66 (assume @p81 (forall (@list @t1 @t14 @t2 @t10) (or (not (= @t6 @t233)) @t232))) % 93.39/93.66 (assume @p82 (forall (@list @t48 @t107 @t1 @t3 @t103) (or (not (= @t122 @t123)) @t121))) % 93.39/93.66 (assume @p83 (forall @t31 (not (= @t27 @t6)))) % 93.39/93.66 (assume @p84 (forall @t236 (or @t235 @t158 (tptp.c_Exceptions_Opreallocated @t234)))) % 93.39/93.66 (assume @p85 (forall @t184 (or @t237 @t16))) % 93.39/93.66 (assume @p86 (forall @t184 (or (not @t237) @t15))) % 93.39/93.66 (assume @p87 (forall @t238 (tptp.hBOOL (tptp.c_in @t3 @t13 @t1)))) % 93.39/93.66 (assume @p88 (forall (@list @t131 @t159 @t48 @t47 @t187 @t45 @t239) (or @t160 (not (tptp.c_BigStep_Oeval @t48 @t47 @t194 @t45 (tptp.hAPP (tptp.hAPP @t193 @t159) @t239)))))) % 93.39/93.66 (assume @p89 (forall @t243 (or @t242 @t16 @t240))) % 93.39/93.66 (assume @p90 (= (tptp.hAPP (tptp.c_Fun_Oid tptp.t_a) tptp.v_x) tptp.v_x)) % 93.39/93.66 (assume @p91 (forall (@list @t45 @t130 @t48 @t46 @t44) (or (= @t45 @t167) @t168))) % 93.39/93.66 (assume @p92 (forall (@list @t10 @t51) (= (tptp.hAPP (tptp.c_Map_Orestrict__map @t244 @t51 tptp.t_a @t10) tptp.v_x) @t115))) % 93.39/93.66 (assume @p93 (forall (@list @t172 @t43 @t246 @t245 @t1 @t3) (or (not (= (tptp.hAPP @t172 @t248) (tptp.hAPP @t246 @t248))) @t247))) % 93.39/93.66 (assume @p94 (forall @t181 (not (= @t180 tptp.c_Value_Oval_OUnit)))) % 93.39/93.66 (assume @p95 (forall @t185 (not (tptp.hBOOL (tptp.hAPP @t6 @t3))))) % 93.39/93.66 (assume @p96 (forall @t141 (not (= @t13 @t6)))) % 93.39/93.66 (assume @p97 (forall @t250 (or (not (tptp.class_OrderedGroup_Ocomm__monoid__add @t10)) (= (tptp.c_Finite__Set_Osetsum @t14 @t11 @t1 @t10) (tptp.c_Finite__Set_Osetsum @t163 @t18 @t10 @t10)) @t249))) % 93.39/93.66 (assume @p98 (forall @t176 (or @t175 @t252 @t171))) % 93.39/93.66 (assume @p99 (forall (@list @t131 @t48 @t1) (or @t157 @t253))) % 93.39/93.66 (assume @p100 (forall @t185 (tptp.hBOOL (tptp.hAPP @t13 @t3)))) % 93.39/93.66 (assume @p101 (forall (@list @t48 @t130 @t46) (tptp.c_BigStep_Oeval @t48 @t167 @t46 @t167 @t46))) % 93.39/93.66 (assume @p102 (forall @t231 (or (not (tptp.class_Orderings_Otop @t10)) (= (tptp.hAPP (tptp.c_Orderings_Otop__class_Otop @t12) tptp.v_x) (tptp.c_Orderings_Otop__class_Otop @t10))))) % 93.39/93.66 (assume @p103 (forall (@list @t254 @t1) (or (not (= @t255 @t6)) (= @t254 @t55)))) % 93.39/93.66 (assume @p104 (forall (@list @t48 @t127 @t131 @t130 @t1) (or (tptp.c_TypeRel_Owiden @t48 @t256 @t127 @t1) @t133))) % 93.39/93.66 (assume @p105 (forall @t260 (or (= @t259 @t258) @t257))) % 93.39/93.66 (assume @p106 (forall @t265 (or @t264 @t263 @t261))) % 93.39/93.66 (assume @p107 (forall @t265 (or @t264 @t266 @t261))) % 93.39/93.66 (assume @p108 (forall @t265 (or @t264 @t263 @t267))) % 93.39/93.66 (assume @p109 (forall @t265 (or @t264 @t266 @t267))) % 93.39/93.66 (assume @p110 (= (tptp.hAPP @t268 tptp.v_x) (tptp.c_in tptp.v_x @t268 tptp.t_a))) % 93.39/93.66 (assume @p111 (forall @t250 (or (not (tptp.class_OrderedGroup_Ocomm__monoid__mult @t10)) (= (tptp.c_Finite__Set_Osetprod @t14 @t11 @t1 @t10) (tptp.c_Finite__Set_Osetprod @t163 @t18 @t10 @t10)) @t249))) % 93.39/93.66 (assume @p112 (forall @t126 (or (not (= @t114 @t6)) (= @t14 @t210)))) % 93.39/93.66 (assume @p113 (forall (@list @t1 @t26 @t2) (not (= @t6 @t27)))) % 93.39/93.66 (assume @p114 (forall (@list @t1 @t10) (= (tptp.c_Map_Oran (tptp.c_COMBK @t55 @t215 @t10) @t10 @t1) @t6))) % 93.39/93.66 (assume @p115 (forall (@list @t26 @t1) (not (tptp.hBOOL (tptp.c_in @t26 @t6 @t1))))) % 93.39/93.66 (assume @p116 (forall (@list @t22 @t1) (not (tptp.hBOOL (tptp.c_in @t22 @t6 @t1))))) % 93.39/93.66 (assume @p117 (forall @t140 (or @t121 @t138))) % 93.39/93.66 (assume @p118 (forall @t238 @t138)) % 93.39/93.66 (assume @p119 (forall (@list @t14 @t143 @t164 @t10) (= (tptp.hAPP (tptp.c_Fun_Ocomp @t14 @t143 @t164 @t10 tptp.t_a) tptp.v_x) (tptp.hAPP @t14 (tptp.hAPP @t143 tptp.v_x))))) % 93.39/93.66 (assume @p120 (forall @t185 (= @t270 @t7))) % 93.39/93.66 (assume @p121 (forall (@list @t10 @t42 @t1) (= (tptp.c_Map_Odom (tptp.c_COMBK @t271 @t81 @t1) @t1 @t10) @t13))) % 93.39/93.66 (assume @p122 (forall @t166 (or (= (tptp.hAPP @t183 @t56) @t3) @t16))) % 93.39/93.66 (assume @p123 (forall (@list @t14 @t245 @t1 @t3) (or (not (tptp.c_Fun_Oinj__on @t14 @t272 @t245 @t1)) (= (tptp.hAPP (tptp.c_Hilbert__Choice_Oinv__into @t272 @t14 @t245 @t1) @t56) @t3)))) % 93.39/93.66 (assume @p124 (forall (@list @t14 @t2 @t10 @t1) (or (not (= @t233 @t6)) @t232))) % 93.39/93.66 (assume @p125 (forall @t224 (or (= @t223 @t222) @t121))) % 93.39/93.66 (assume @p126 (forall (@list @t82 @t10) (= (tptp.hAPP (tptp.c_Map_Orestrict__map @t82 @t268 tptp.t_a @t10) tptp.v_x) @t115))) % 93.39/93.66 (assume @p127 (forall (@list @t143 @t1 @t14 @t10 @t164) (or (= (tptp.c_Fun_Ocomp (tptp.c_Fun_Ocomp @t143 @t183 @t1 @t164 @t10) @t14 @t10 @t164 @t1) @t143) @t16))) % 93.39/93.66 (assume @p128 (forall (@list @t198 @t51 @t52 @t48 @t127 @t1) (or (= (tptp.hAPP (tptp.c_Map_Omap__of @t277 @t189 tptp.tc_Type_Oty) @t209) @t276) @t274))) % 93.39/93.66 (assume @p129 (forall (@list @t42 @t103 @t1 @t3) (or (tptp.hBOOL (tptp.c_in @t42 @t104 @t1)) @t279 (not (tptp.hBOOL (tptp.c_in @t42 @t278 @t1)))))) % 93.39/93.66 (assume @p130 (forall (@list @t3 @t43 @t1) (or (not (= (tptp.c_Set_Oinsert @t3 @t43 @t1) @t6)) (tptp.hBOOL (tptp.c_in @t3 @t43 @t1))))) % 93.39/93.66 (assume @p131 (forall (@list @t135 @t26 @t1) (or (= @t135 @t26) (not (tptp.hBOOL (tptp.c_in @t135 @t28 @t1)))))) % 93.39/93.66 (assume @p132 (forall @t238 (tptp.hBOOL (tptp.c_in @t3 @t7 @t1)))) % 93.39/93.66 (assume @p133 (forall @t284 (or @t283 (tptp.hBOOL (tptp.c_in @t135 @t280 @t1))))) % 93.39/93.66 (assume @p134 (forall (@list @t254 @t1 @t3) (or (= @t254 @t269) (not (tptp.hBOOL (tptp.c_in @t3 @t255 @t1)))))) % 93.39/93.66 (assume @p135 (forall @t284 (or @t283 (tptp.hBOOL (tptp.c_in @t26 (tptp.c_Map_Odom @t82 @t10 @t1) @t10))))) % 93.39/93.66 (assume @p136 (forall @t238 (tptp.hBOOL (tptp.c_in @t3 @t270 @t1)))) % 93.39/93.66 (assume @p137 (forall @t117 (tptp.hBOOL (tptp.c_in @t56 (tptp.c_Set_Oimage @t14 (tptp.c_Orderings_Otop__class_Otop @t17) @t10 @t1) @t1)))) % 93.39/93.66 (assume @p138 (forall (@list @t2 @t14 @t10 @t1 @t3) (or (tptp.hBOOL (tptp.c_in (tptp.hAPP @t285 @t3) @t2 @t10)) (not (tptp.hBOOL (tptp.c_in @t3 @t233 @t1)))))) % 93.39/93.66 (assume @p139 (forall (@list @t2 @t14 @t1 @t10 @t3 @t42) (or (not (= (tptp.hAPP @t288 @t3) (tptp.hAPP @t288 @t42))) @t240 @t287 (not (tptp.hBOOL (tptp.c_in @t3 @t19 @t10)))))) % 93.39/93.66 (assume @p140 (forall (@list @t14 @t2 @t10 @t1 @t42) (or (= (tptp.hAPP @t14 (tptp.hAPP @t285 @t42)) @t42) (not (tptp.hBOOL (tptp.c_in @t42 @t233 @t1)))))) % 93.39/93.66 (assume @p141 (forall (@list @t3 @t103 @t1) (= @t278 (tptp.c_Set_Oinsert @t3 @t104 @t1)))) % 93.39/93.66 (assume @p142 (forall @t289 (or (= (tptp.hAPP @t288 @t56) @t3) @t257 @t58))) % 93.39/93.66 (assume @p143 (forall @t292 (or @t291 @t290 (= (tptp.hAPP (tptp.c_Hilbert__Choice_Oinv__into @t2 @t14 @t245 @t1) @t56) @t3)))) % 93.39/93.66 (assume @p144 (forall @t289 (or (= (tptp.hAPP @t293 @t56) @t3) @t257 @t58))) % 93.39/93.66 (assume @p145 (forall (@list @t14 @t2 @t245 @t1 @t3) (or @t290 (= (tptp.hAPP (tptp.c_Fun_Othe__inv__into @t2 @t14 @t245 @t1) @t56) @t3) @t291))) % 93.39/93.66 (assume @p146 (forall @t260 (or (= @t259 @t115) @t4))) % 93.39/93.66 (assume @p147 (forall (@list @t82 @t26 @t10 @t1) (or (not @t295) (not @t294)))) % 93.39/93.66 (assume @p148 (forall (@list @t26 @t82 @t1 @t10) (or @t294 @t295))) % 93.39/93.66 (assume @p149 (forall @t102 (or (= @t101 @t85) @t99))) % 93.39/93.66 (assume @p150 (forall (@list @t14 @t3 @t1 @t42 @t10) (or (not (= @t56 @t219)) (= (tptp.c_Set_Oinsert @t3 @t54 @t10) @t54)))) % 93.39/93.66 (assume @p151 (forall @t296 (or (tptp.c_Fun_Oinj__on @t293 @t19 @t10 @t1) @t58))) % 93.39/93.66 (assume @p152 (forall (@list @t14 @t2 @t1 @t10 @t11) (or (not (= @t19 @t18)) @t16 @t297))) % 93.39/93.66 (assume @p153 (forall @t296 (or (= (tptp.c_Set_Oimage @t293 @t19 @t10 @t1) @t2) @t58))) % 93.39/93.66 (assume @p154 (forall (@list @t22 @t1 @t10) (= (tptp.c_Set_Oimage @t298 @t95 @t10 @t1) @t6))) % 93.39/93.66 (assume @p155 (forall @t92 (= (tptp.c_Map_Orestrict__map @t14 @t27 @t1 @t10) (tptp.c_Fun_Ofun__upd (tptp.c_Map_Orestrict__map @t14 @t2 @t1 @t10) @t26 @t90 @t1 @t81)))) % 93.39/93.66 (assume @p156 (forall @t304 (or @t303 (not @t300)))) % 93.39/93.66 (assume @p157 (forall @t304 (or @t303 (tptp.hBOOL (tptp.c_in @t82 (tptp.c_Map_Odom @t301 @t1 @t10) @t1))))) % 93.39/93.66 (assume @p158 (forall @t304 (or (= @t302 (tptp.hAPP @t301 @t82)) @t300))) % 93.39/93.66 (assume @p159 (forall (@list @t22 @t10 @t164 @t14) (= (tptp.hAPP (tptp.c_Fun_Ocomp (tptp.c_COMBK @t22 @t10 @t164) @t14 @t164 @t10 tptp.t_a) tptp.v_x) @t22))) % 93.39/93.66 (assume @p160 (forall (@list @t14 @t103 @t107 @t1 @t10 @t3) (or (= (tptp.hAPP (tptp.c_Map_Omap__upds @t14 @t103 @t107 @t1 @t10) @t3) @t56) @t105))) % 93.39/93.66 (assume @p161 (forall (@list @t306 @t3 @t305 @t1 @t10) (or (= (tptp.hAPP @t306 @t3) (tptp.hAPP @t305 @t3)) (not (tptp.hBOOL (tptp.c_in @t3 (tptp.c_Map_Odom @t306 @t1 @t10) @t1))) (not (tptp.c_Map_Omap__le @t306 @t305 @t1 @t10))))) % 93.39/93.66 (assume @p162 (forall (@list @t48 @t130 @t52 @t51 @t47 @t46 @t45 @t44) (or (tptp.c_SmallStep_Oredp @t48 (tptp.c_Expr_Oexp_OFAss @t167 @t52 @t51 @t47 @t50) @t46 (tptp.c_Expr_Oexp_OFAss @t167 @t52 @t51 @t45 @t50) @t44) @t49))) % 93.39/93.66 (assume @p163 (forall (@list @t3 @t172 @t43 @t1 @t245 @t246) (or @t247 (= @t43 (tptp.hAPP @t307 @t248))))) % 93.39/93.66 (assume @p164 (forall @t176 (or @t175 @t309 @t171))) % 93.39/93.66 (assume @p165 (forall @t176 (or @t175 @t310 @t171))) % 93.39/93.66 (assume @p166 (forall @t176 (or @t175 @t174 @t312))) % 93.39/93.66 (assume @p167 (forall (@list @t172 @t3 @t246 @t1 @t10 @t169 @t313) (or (not (= (tptp.hAPP @t172 @t316) (tptp.hAPP @t246 @t316))) @t315 @t314))) % 93.39/93.66 (assume @p168 (forall @t176 (or @t175 @t252 @t312))) % 93.39/93.66 (assume @p169 (forall (@list @t14 @t143 @t164 @t317 @t10) (= (tptp.hAPP (tptp.c_Product__Type_Oscomp @t14 @t143 tptp.t_a @t164 @t317 @t10) tptp.v_x) (tptp.hAPP (tptp.hAPP (tptp.c_split @t164 @t317 @t10) @t143) (tptp.hAPP @t14 tptp.v_x))))) % 93.39/93.66 (assume @p170 (forall @t327 (or @t326 (= (tptp.hAPP @t322 @t323) @t55) @t321))) % 93.39/93.66 (assume @p171 (forall (@list @t131) (tptp.c_Objects_Ohext @t131 @t131))) % 93.39/93.66 (assume @p172 (forall (@list @t48 @t159 @t130 @t127 @t1 @t131) (or (tptp.c_Conform_Oconf @t48 @t159 @t130 @t127 @t1) @t133 @t161))) % 93.39/93.66 (assume @p173 (forall @t329 (= (tptp.hAPP @t328 (tptp.c_curry @t14 @t1 @t10 @t164)) @t14))) % 93.39/93.66 (assume @p174 (forall (@list @t42 @t2 @t1 @t3) (or @t332 (not @t330)))) % 93.39/93.66 (assume @p175 (forall @t333 (or (= (tptp.c_Set_Oinsert @t56 @t19 @t10) @t19) @t257))) % 93.39/93.66 (assume @p176 (forall @t80 (or (not (= @t8 @t334)) @t78 @t4 @t297))) % 93.39/93.66 (assume @p177 (forall (@list @t164 @t10 @t1 @t14 @t143 @t317 @t335) (= (tptp.hAPP @t338 (tptp.hAPP @t336 @t335)) (tptp.hAPP (tptp.c_Product__Type_Oapfst @t143 @t317 @t1 @t10) (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oapsnd @t164 @t10 @t317) @t14) @t335))))) % 93.39/93.66 (assume @p178 (forall (@list @t14 @t143 @t10 @t164 @t317 @t1 @t3) (= (tptp.hAPP (tptp.c_Product__Type_Oscomp @t14 @t143 @t10 @t164 @t317 @t1) @t3) (tptp.hAPP (tptp.hAPP (tptp.c_split @t164 @t317 @t1) @t143) @t56)))) % 93.39/93.66 (assume @p179 (forall (@list @t164 @t10 @t1 @t14 @t317 @t143 @t3) (= (tptp.hAPP @t338 (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oapsnd @t317 @t164 @t1) @t143) @t3)) (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oapsnd @t317 @t10 @t1) @t339) @t3)))) % 93.39/93.66 (assume @p180 (forall (@list @t14 @t164 @t1 @t10 @t317 @t143 @t3) (= (tptp.hAPP @t341 (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oapsnd @t317 @t10 @t164) @t143) @t3)) (tptp.hAPP (tptp.hAPP @t340 (tptp.hAPP @t14 (tptp.c_fst @t3 @t164 @t317))) (tptp.hAPP @t143 (tptp.c_snd @t3 @t164 @t317)))))) % 93.39/93.66 (assume @p181 (forall (@list @t164 @t1 @t10 @t14 @t3) (= (tptp.c_snd (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oapsnd @t164 @t1 @t10) @t14) @t3) @t10 @t1) (tptp.hAPP @t14 @t342)))) % 93.39/93.66 (assume @p182 (forall @t329 (= (tptp.c_curry @t343 @t1 @t10 @t164) @t14))) % 93.39/93.66 (assume @p183 (forall (@list @t216 @t10 @t164 @t1 @t22 @t26 @t135) (or (tptp.hBOOL (tptp.c_in @t216 (tptp.hAPP (tptp.hAPP (tptp.c_split @t10 @t164 @t5) @t22) @t346) @t1)) (not (tptp.hBOOL (tptp.c_in @t216 @t344 @t1)))))) % 93.39/93.66 (assume @p184 (forall @t238 (or @t315 (not (tptp.hBOOL (tptp.c_Option_Ois__none @t3 @t1)))))) % 93.39/93.66 (assume @p185 (forall @t31 (or (= @t27 @t2) @t77))) % 93.39/93.66 (assume @p186 (forall @t125 (= (tptp.hAPP @t347 @t115) @t55))) % 93.39/93.66 (assume @p187 (forall (@list @t143 @t14 @t10 @t164 @t1 @t2) (or (tptp.c_Fun_Oinj__on (tptp.c_Fun_Ocomp @t143 @t14 @t10 @t164 @t1) @t2 @t1 @t164) (not (tptp.c_Fun_Oinj__on @t143 @t19 @t10 @t164)) @t58))) % 93.39/93.66 (assume @p188 (forall @t351 (or @t350 @t348 @t77 @t58))) % 93.39/93.66 (assume @p189 (forall @t351 (or @t350 @t58 @t348 @t77))) % 93.39/93.66 (assume @p190 (forall (@list @t14 @t2 @t1 @t10 @t26 @t135) (or @t57 (not @t350) @t348 @t77))) % 93.39/93.66 (assume @p191 (forall (@list @t335 @t354 @t1 @t10) (= (tptp.c_Map_Omap__of (tptp.c_List_Olist_OCons @t335 @t354 @t355) @t1 @t10) (tptp.c_Fun_Ofun__upd (tptp.c_Map_Omap__of @t354 @t1 @t10) @t353 (tptp.hAPP @t110 @t352) @t1 @t81)))) % 93.39/93.66 (assume @p192 (forall (@list @t82 @t318 @t1 @t356 @t10) (or (not @t363) @t361 @t358))) % 93.39/93.66 (assume @p193 (forall (@list @t3 @t364 @t1) (not (= (tptp.c_List_Olist_OCons @t3 @t364 @t1) @t364)))) % 93.39/93.66 (assume @p194 (forall (@list @t103 @t3 @t1) (not (= @t103 @t123)))) % 93.39/93.66 (assume @p195 (forall (@list @t319 @t318 @t10 @t322 @t1 @t164) (or (not @t321) @t325))) % 93.39/93.66 (assume @p196 (forall (@list @t319 @t318 @t1 @t322 @t164 @t10) (or (not (= @t320 @t55)) (= @t366 @t365)))) % 93.39/93.66 (assume @p197 (forall @t186 (tptp.c_Map_Omap__le @t14 @t367 @t1 @t10))) % 93.39/93.66 (assume @p198 (forall @t292 (or @t291 (tptp.hBOOL (tptp.c_in @t56 (tptp.c_Set_Oimage @t14 @t2 @t245 @t1) @t1))))) % 93.39/93.66 (assume @p199 (forall (@list @t3 @t2 @t10 @t14 @t1) (or @t94 @t368))) % 93.39/93.66 (assume @p200 (forall (@list @t14 @t3 @t2 @t10 @t1) (or @t368 @t94))) % 93.39/93.66 (assume @p201 (forall @t333 (or (tptp.hBOOL (tptp.c_in @t56 @t19 @t10)) @t257))) % 93.39/93.66 (assume @p202 (forall (@list @t14 @t26 @t135 @t143 @t1 @t164 @t10) (= (tptp.c_Fun_Ocomp @t14 (tptp.c_Fun_Oswap @t26 @t135 @t143 @t1 @t164) @t164 @t10 @t1) (tptp.c_Fun_Oswap @t26 @t135 @t369 @t1 @t10)))) % 93.39/93.66 (assume @p203 (forall (@list @t14 @t143 @t1 @t10 @t131) (or @t374 @t373 (not @t370) (not (tptp.c_Map_Omap__le @t14 @t131 @t1 @t10))))) % 93.39/93.66 (assume @p204 @t376) % 93.39/93.66 (assume @p205 (forall (@list @t131 @t26 @t48 @t1 @t377) (or @t235 @t253 (tptp.c_Conform_Ohconf @t48 (tptp.c_Fun_Ofun__upd @t131 @t26 @t380 tptp.tc_nat @t192) @t1) @t379))) % 93.39/93.66 (assume @p206 (forall (@list @t14 @t164 @t10) (= (tptp.hAPP (tptp.c_Fun_Ocomp @t383 @t382 @t381 @t81 tptp.t_a) tptp.v_x) @t115))) % 93.39/93.66 (assume @p207 (forall (@list @t3 @t52 @t51 @t127 @t48 @t198 @t1) (or (not (= (tptp.hAPP (tptp.c_Map_Omap__of @t3 @t189 tptp.tc_Type_Oty) @t209) @t276)) (not (tptp.c_TypeRel_OFields @t48 @t198 @t3 @t1)) @t273))) % 93.39/93.66 (assume @p208 (forall (@list @t82 @t26 @t10 @t135 @t1 @t384 @t386) (or (= @t387 (tptp.c_Fun_Ofun__upd (tptp.c_Map_Omap__upds @t82 @t384 @t386 @t1 @t10) @t26 @t385 @t1 @t81)) (tptp.hBOOL (tptp.c_in @t26 (tptp.c_List_Oset @t384 @t1) @t1))))) % 93.39/93.66 (assume @p209 (forall (@list @t391 @t82 @t10 @t389 @t1 @t388) (or (= (tptp.c_Map_Omap__add (tptp.c_Fun_Ofun__upd @t391 @t82 @t390 @t1 @t81) @t388 @t1 @t10) (tptp.c_Fun_Ofun__upd (tptp.c_Map_Omap__add @t391 @t388 @t1 @t10) @t82 @t390 @t1 @t81)) (tptp.hBOOL (tptp.c_in @t82 (tptp.c_Map_Odom @t388 @t1 @t10) @t1))))) % 93.39/93.66 (assume @p210 (forall @t284 (or (not (= @t282 @t55)) (= (tptp.c_Map_Oran @t392 @t10 @t1) (tptp.c_Set_Oinsert @t135 @t280 @t1))))) % 93.39/93.66 (assume @p211 (forall (@list @t1 @t3 @t48) (or (tptp.hBOOL (tptp.c_in @t393 @t270 @t1)) @t121))) % 93.39/93.66 (assume @p212 (forall @t399 (or (= (tptp.hAPP (tptp.c_Fun_Othe__inv__into @t2 @t398 @t164 @t10) @t3) (tptp.hAPP (tptp.c_Fun_Ocomp (tptp.c_Fun_Othe__inv__into @t2 @t143 @t164 @t1) (tptp.c_Fun_Othe__inv__into @t394 @t14 @t1 @t10) @t1 @t164 @t10) @t3)) @t397 @t396 @t395))) % 93.39/93.66 (assume @p213 (forall @t399 (or (= (tptp.hAPP (tptp.c_Hilbert__Choice_Oinv__into @t2 @t398 @t164 @t10) @t3) (tptp.hAPP (tptp.c_Fun_Ocomp (tptp.c_Hilbert__Choice_Oinv__into @t2 @t143 @t164 @t1) (tptp.c_Hilbert__Choice_Oinv__into @t394 @t14 @t1 @t10) @t1 @t164 @t10) @t3)) @t397 @t396 @t395))) % 93.39/93.66 (assume @p214 (forall (@list @t22 @t10 @t1 @t2 @t3) (or (= (tptp.c_Set_Oimage (tptp.c_COMBK @t22 @t10 @t1) @t2 @t1 @t10) (tptp.c_Set_Oinsert @t22 @t95 @t10)) @t257))) % 93.39/93.66 (assume @p215 (forall (@list @t131 @t26 @t48 @t377 @t1 @t3) (or @t235 @t379 (tptp.c_Conform_Ooconf @t48 @t234 @t377 @t1)))) % 93.39/93.66 (assume @p216 (forall (@list @t10 @t164 @t82) (= (tptp.c_Map_Omap__comp (tptp.c_COMBK @t115 @t81 @t164) @t82 tptp.v_x @t164 @t10 tptp.t_a) @t115))) % 93.39/93.66 (assume @p217 (forall (@list @t82 @t164 @t10) (= (tptp.c_Map_Omap__comp @t82 @t382 tptp.v_x @t164 @t10 tptp.t_a) @t115))) % 93.39/93.66 (assume @p218 (forall @t236 (or @t235 (tptp.c_Objects_Ohext @t131 @t234)))) % 93.39/93.66 (assume @p219 (forall (@list @t131 @t130 @t3 @t48 @t127 @t1) (or (not (= @t400 (tptp.hAPP @t275 @t3))) @t132 (not (tptp.c_TypeRel_Owiden @t48 @t3 @t127 @t1))))) % 93.39/93.66 (assume @p220 (forall (@list @t131 @t130 @t48 @t127 @t1) (or (= @t400 (tptp.hAPP @t275 @t256)) @t133))) % 93.39/93.66 (assume @p221 (forall (@list @t131 @t26 @t198 @t197 @t48 @t52 @t51 @t130 @t187) (or @t205 (tptp.c_SmallStep_Oredp @t48 (tptp.c_Expr_Oexp_OFAss @t196 @t52 @t51 @t167 @t50) @t194 @t403 (tptp.hAPP (tptp.hAPP @t193 (tptp.c_Fun_Ofun__upd @t131 @t26 @t402 tptp.tc_nat @t192)) @t187))))) % 93.39/93.66 (assume @p222 (forall (@list @t405 @t26 @t198 @t197 @t48 @t230 @t407 @t130 @t404 @t406 @t195 @t52 @t51) (or (not (= (tptp.hAPP @t405 @t26) @t203)) (not (tptp.c_BigStep_Oeval @t48 @t230 @t407 @t167 (tptp.hAPP (tptp.hAPP @t193 @t405) @t404))) (not (tptp.c_BigStep_Oeval @t48 @t406 @t195 @t196 @t407)) (tptp.c_BigStep_Oeval @t48 (tptp.c_Expr_Oexp_OFAss @t406 @t52 @t51 @t230 @t50) @t195 @t403 (tptp.hAPP (tptp.hAPP @t193 (tptp.c_Fun_Ofun__upd @t405 @t26 @t402 tptp.tc_nat @t192)) @t404))))) % 93.39/93.66 (assume @p223 (forall @t411 (or @t205 @t158 (tptp.c_Exceptions_Opreallocated @t410)))) % 93.39/93.66 (assume @p224 (forall (@list @t131 @t26 @t198 @t43 @t159) (or (not (= @t204 (tptp.hAPP @t202 (tptp.hAPP @t200 @t43)))) @t161 (= @t412 (tptp.hAPP @t202 (tptp.hAPP @t200 (tptp.c_Objects_Osko__Objects__Xhext__def__1__1 @t198 @t26 @t159))))))) % 93.39/93.66 (assume @p225 (forall (@list @t131 @t26 @t198 @t197 @t159) (or @t205 @t161 (= @t412 (tptp.hAPP @t202 (tptp.hAPP @t200 (tptp.c_Objects_Osko__Objects__Xhext__objD__1__1 @t198 @t26 @t159))))))) % 93.39/93.66 (assume @p226 (forall @t327 (or @t326 (= @t320 (tptp.hAPP @t110 @t323)) @t321))) % 93.39/93.66 (assume @p227 (forall @t414 (or @t413 (tptp.c_Progress_OWTrt_H @t48 @t131 @t225 @t167 @t127)))) % 93.39/93.66 (assume @p228 (forall (@list @t10 @t3) (= (tptp.hAPP (tptp.c_Fun_Ofun__upd @t244 @t3 @t115 tptp.t_a @t81) tptp.v_xa) @t115))) % 93.39/93.66 (assume @p229 (forall (@list @t103 @t10 @t1 @t318 @t216 @t48) (or (not (= (tptp.hAPP (tptp.c_Map_Omap__of @t103 @t10 @t1) @t318) @t218)) (= (tptp.hAPP (tptp.c_Map_Omap__of (tptp.c_List_Ofilter (tptp.hAPP (tptp.c_split @t10 @t1 tptp.tc_bool) @t48) @t103 @t415) @t10 @t1) @t318) @t218) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t48 @t318) @t216)))))) % 93.39/93.66 (assume @p230 (forall @t176 (or @t175 @t310 @t312))) % 93.39/93.66 (assume @p231 (forall (@list @t169 @t172 @t3 @t10 @t1 @t313 @t246) (or @t314 (= @t3 (tptp.hAPP @t217 @t316)) @t315))) % 93.39/93.66 (assume @p232 (forall @t176 (or @t175 @t309 @t312))) % 93.39/93.66 (assume @p233 (forall (@list @t3 @t103 @t1 @t42 @t107 @t10) (= (tptp.c_List_Ozip @t123 (tptp.c_List_Olist_OCons @t42 @t107 @t10) @t1 @t10) (tptp.c_List_Olist_OCons @t417 @t112 @t355)))) % 93.39/93.66 (assume @p234 (forall (@list @t10 @t164 @t1 @t14 @t143 @t317 @t3) (= (tptp.hAPP (tptp.hAPP @t418 (tptp.c_Fun_Ocomp @t14 @t143 @t317 (tptp.tc_fun @t164 @t1) @t10)) @t3) (tptp.hAPP (tptp.hAPP @t14 (tptp.hAPP @t143 (tptp.c_fst @t3 @t10 @t164))) @t342)))) % 93.39/93.66 (assume @p235 (forall @t243 (or (= (tptp.c_Map_Odom (tptp.c_Fun_Ofun__upd @t14 @t3 @t42 @t1 @t81) @t1 @t10) (tptp.c_Set_Oinsert @t3 @t114 @t1)) (= @t42 @t115)))) % 93.39/93.66 (assume @p236 (forall (@list @t164 @t14 @t2 @t1 @t10 @t131) (or @t420 @t58 (= (tptp.c_Finite__Set_Osetprod @t131 @t19 @t10 @t164) (tptp.c_Finite__Set_Osetprod @t419 @t2 @t1 @t164))))) % 93.39/93.66 (assume @p237 (forall @t421 (or @t420 (= (tptp.c_Finite__Set_Osetprod @t131 @t18 @t10 @t164) (tptp.c_Finite__Set_Osetprod @t419 @t11 @t1 @t164)) @t249))) % 93.39/93.66 (assume @p238 (forall @t421 (or (not (tptp.class_OrderedGroup_Ocomm__monoid__add @t164)) (= (tptp.c_Finite__Set_Osetsum @t131 @t18 @t10 @t164) (tptp.c_Finite__Set_Osetsum @t419 @t11 @t1 @t164)) @t249))) % 93.39/93.66 (assume @p239 (forall @t221 (or (= @t220 @t85) @t99))) % 93.39/93.66 (assume @p240 (forall (@list @t22 @t1 @t10 @t2) (or (= (tptp.c_Set_Oimage @t298 @t2 @t10 @t1) (tptp.c_Set_Oinsert @t22 @t6 @t1)) @t232))) % 93.39/93.66 (assume @p241 (forall @t155 (or @t146 @t145 @t142 @t422))) % 93.39/93.66 (assume @p242 (forall @t156 (or @t144 @t154 @t142 @t422))) % 93.39/93.66 (assume @p243 (forall @t155 (or @t146 @t145 @t142 @t423))) % 93.39/93.66 (assume @p244 (forall @t156 (or @t144 @t154 @t142 @t423))) % 93.39/93.66 (assume @p245 (forall (@list @t14 @t2 @t1 @t10 @t42) (or (= (tptp.hAPP @t14 (tptp.hAPP @t293 @t42)) @t42) @t287 @t58))) % 93.39/93.66 (assume @p246 (forall @t92 (or @t424 @t77 @t16))) % 93.39/93.66 (assume @p247 (forall (@list @t26 @t2 @t1 @t14 @t10) (or @t76 (not @t424) @t16))) % 93.39/93.66 (assume @p248 (= (tptp.c_Option_Ois__none tptp.v_x tptp.t_a) (tptp.c_fequal tptp.v_x (tptp.c_Option_Ooption_ONone tptp.t_a) (tptp.tc_Option_Ooption tptp.t_a)))) % 93.39/93.66 (assume @p249 (forall (@list @t82 @t425 @t1 @t10) (or @t428 (not @t427)))) % 93.39/93.66 (assume @p250 (forall (@list @t425 @t1 @t10 @t82) (or @t427 (not @t428)))) % 93.39/93.66 (assume @p251 (forall (@list @t10 @t1 @t3 @t43) (= (tptp.c_Map_Odom (tptp.c_Fun_Ofun__upd @t210 @t3 @t111 @t1 @t81) @t1 @t10) @t7))) % 93.39/93.66 (assume @p252 (forall @t429 (= (tptp.c_Product__Type_Oapsnd @t1 @t10 @t164) (tptp.c_Product__Type_Oprod__fun (tptp.c_Fun_Oid @t164) @t164 @t164 @t1 @t10)))) % 93.39/93.66 (assume @p253 (forall (@list @t10 @t164 @t1 @t14) (= (tptp.hAPP (tptp.c_Product__Type_Oapsnd @t10 @t164 @t1) @t14) (tptp.hAPP (tptp.c_Product__Type_Oprod__fun @t120 @t1 @t1 @t10 @t164) @t14)))) % 93.39/93.66 (assume @p254 (forall (@list @t48 @t198 @t51 @t52 @t127 @t1) (or (tptp.c_TypeRel_OFields @t48 @t198 @t277 @t1) @t274))) % 93.39/93.66 (assume @p255 (forall (@list @t14 @t1 @t164 @t10) (= (tptp.c_Product__Type_Oapfst @t14 @t1 @t164 @t10) (tptp.hAPP (tptp.c_Product__Type_Oprod__fun @t14 @t1 @t164 @t10 @t10) @t163)))) % 93.39/93.66 (assume @p256 (forall (@list @t131 @t430 @t159) (or (tptp.c_Objects_Ohext @t131 @t430) (not (tptp.c_Objects_Ohext @t159 @t430)) @t161))) % 93.39/93.66 (assume @p257 (forall (@list @t131 @t130 @t127 @t159) (or @t413 @t161 (= (tptp.c_Objects_Otypeof__h @t159 @t130) @t276)))) % 93.39/93.66 (assume @p258 (forall (@list @t48 @t159 @t225 @t47 @t127 @t131) (or (tptp.c_WellTypeRT_OWTrt @t48 @t159 @t225 @t47 @t127) @t161 @t229))) % 93.39/93.66 (assume @p259 (forall @t432 (or @t431 @t360))) % 93.39/93.66 (assume @p260 (forall @t432 (or @t431 @t363))) % 93.39/93.66 (assume @p261 (forall (@list @t82 @t318 @t1 @t3 @t356 @t10) (or (not @t434) @t361 @t433))) % 93.39/93.66 (assume @p262 (forall (@list @t26 @t135 @t22 @t14 @t1 @t10) (or (= (tptp.c_Fun_Oswap @t26 @t135 (tptp.c_Fun_Oswap @t135 @t22 @t349 @t1 @t10) @t1 @t10) (tptp.c_Fun_Oswap @t26 @t22 @t14 @t1 @t10)) @t266 @t261))) % 93.39/93.66 (assume @p263 (forall @t436 (or @t242 @t58 @t240 @t435 @t257))) % 93.39/93.66 (assume @p264 (forall (@list @t14 @t3 @t43 @t2 @t1 @t10) (or (not (= @t56 (tptp.hAPP @t14 @t43))) (not (tptp.hBOOL (tptp.c_in @t43 @t2 @t1))) @t257 @t58 (= @t3 @t43)))) % 93.39/93.66 (assume @p265 (forall @t436 (or @t242 @t435 @t257 @t58 @t240))) % 93.39/93.66 (assume @p266 (forall @t436 (or @t242 @t435 @t257 @t240 @t58))) % 93.39/93.66 (assume @p267 (forall @t437 (= (tptp.c_Option_Ooption_Ooption__rec @t169 @t172 @t115 @t1 @t10) @t169))) % 93.39/93.66 (assume @p268 (forall (@list @t10 @t1 @t82) (= (tptp.c_Map_Omap__add @t210 @t82 @t1 @t10) @t82))) % 93.39/93.66 (assume @p269 (forall (@list @t82 @t10 @t1) (= (tptp.c_Map_Omap__add @t82 @t210 @t1 @t10) @t82))) % 93.39/93.66 (assume @p270 (forall (@list @t48 @t169 @t172) (or (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_Option_Ooption_Ooption__case @t169 @t172 @t311 tptp.t_a tptp.t_b)))) @t170))) % 93.39/93.66 (assume @p271 (forall (@list @t48 @t1 @t10 @t438) (= (tptp.hAPP (tptp.c_COMBK @t48 @t1 @t10) @t438) @t48))) % 93.39/93.66 (assume @p272 (forall (@list @t1 @t48) (= (tptp.hAPP @t439 @t48) @t48))) % 93.39/93.66 (assume @p273 (forall (@list @t164 @t10 @t1 @t14 @t143 @t317 @t3) (= (tptp.hAPP @t338 (tptp.hAPP @t336 @t3)) (tptp.hAPP (tptp.hAPP @t340 (tptp.hAPP @t143 (tptp.c_fst @t3 @t317 @t164))) (tptp.hAPP @t14 (tptp.c_snd @t3 @t317 @t164)))))) % 93.39/93.66 (assume @p274 (forall (@list @t131 @t26 @t198 @t197 @t48 @t3 @t127 @t1 @t408) (or @t205 @t441 (not @t440)))) % 93.39/93.66 (assume @p275 (forall (@list @t131 @t26 @t198 @t197 @t48 @t408 @t3 @t127 @t1) (or @t205 @t440 (not @t441)))) % 93.39/93.66 (assume @p276 (forall (@list @t1 @t10 @t335) (= (tptp.hAPP (tptp.hAPP @t340 @t353) @t352) @t335))) % 93.39/93.66 (assume @p277 (forall (@list @t364 @t1 @t10) (= @t364 (tptp.hAPP (tptp.hAPP @t340 @t443) @t442)))) % 93.39/93.66 (assume @p278 (forall (@list @t14 @t164 @t10 @t1 @t3) (= (tptp.c_snd (tptp.hAPP (tptp.c_Product__Type_Oapfst @t14 @t164 @t10 @t1) @t3) @t10 @t1) (tptp.c_snd @t3 @t164 @t1)))) % 93.39/93.66 (assume @p279 (forall (@list @t129 @t3 @t1) (or @t445 (not @t444)))) % 93.39/93.66 (assume @p280 (forall (@list @t3 @t129 @t1) (or @t444 (not @t445)))) % 93.39/93.66 (assume @p281 (forall (@list @t3 @t42 @t2 @t1) (= (tptp.c_Set_Oinsert @t3 @t331 @t1) (tptp.c_Set_Oinsert @t42 @t8 @t1)))) % 93.39/93.66 (assume @p282 (forall (@list @t3 @t11 @t1) (tptp.hBOOL (tptp.c_in @t3 @t334 @t1)))) % 93.39/93.66 (assume @p283 (forall (@list @t26 @t11 @t1) (tptp.hBOOL (tptp.c_in @t26 @t59 @t1)))) % 93.39/93.66 (assume @p284 (forall @t9 (tptp.hBOOL (tptp.c_in @t3 @t8 @t1)))) % 93.39/93.66 (assume @p285 (forall (@list @t74 @t35 @t34 @t73 @t1 @t32) (not (= @t75 @t33)))) % 93.39/93.66 (assume @p286 (forall @t446 (= @t349 (tptp.c_Fun_Oswap @t135 @t26 @t14 @t1 @t10)))) % 93.39/93.66 (assume @p287 (forall @t446 (= (tptp.c_Fun_Oswap @t26 @t135 @t349 @t1 @t10) @t14))) % 93.39/93.66 (assume @p288 (forall @t429 (= (tptp.c_Product__Type_Oprod_Oprod__case @t1 @t10 @t164) @t328))) % 93.39/93.66 (assume @p289 (forall (@list @t143 @t14 @t2 @t1 @t164 @t10) (or (tptp.c_Fun_Oinj__on @t143 (tptp.c_Set_Oimage @t14 @t2 @t1 @t164) @t164 @t10) (not (tptp.c_Fun_Oinj__on (tptp.c_Fun_Ocomp @t143 @t14 @t164 @t10 @t1) @t2 @t1 @t10))))) % 93.39/93.66 (assume @p290 (forall (@list @t14 @t384 @t386 @t1 @t10 @t143) (or (tptp.c_Map_Omap__le (tptp.c_Map_Omap__upds @t14 @t384 @t386 @t1 @t10) (tptp.c_Map_Omap__upds @t143 @t384 @t386 @t1 @t10) @t1 @t10) @t447))) % 93.39/93.66 (assume @p291 (forall (@list @t14 @t2 @t1 @t10 @t26) (or @t57 @t89))) % 93.39/93.66 (assume @p292 (forall @t178 (= (tptp.c_Set_Oimage @t439 @t177 @t1 @t1) @t177))) % 93.39/93.66 (assume @p293 (forall (@list @t335 @t1 @t10 @t448) (or (not (= @t352 (tptp.c_snd @t448 @t1 @t10))) (not (= @t353 (tptp.c_fst @t448 @t1 @t10))) (= @t335 @t448)))) % 93.39/93.66 (assume @p294 (forall (@list @t46 @t1 @t10 @t364) (or (not (= (tptp.c_snd @t46 @t1 @t10) @t442)) (not (= (tptp.c_fst @t46 @t1 @t10) @t443)) (= @t46 @t364)))) % 93.39/93.66 (assume @p295 (forall @t450 (or (= @t449 @t90) @t76))) % 93.39/93.66 (assume @p296 (forall @t429 (= (tptp.c_Product__Type_Ointernal__split @t1 @t10 @t164) @t328))) % 93.39/93.66 (assume @p297 (forall @t72 (tptp.c_Fun_Oinj__on @t439 @t2 @t1 @t1))) % 93.39/93.66 (assume @p298 (forall (@list @t143 @t131 @t1 @t10 @t14) (or @t370 (not @t374)))) % 93.39/93.66 (assume @p299 (forall @t9 (= (tptp.c_Set_Oinsert @t3 @t8 @t1) @t8))) % 93.39/93.66 (assume @p300 (forall (@list @t26 @t14 @t1 @t10) (= (tptp.c_Fun_Oswap @t26 @t26 @t14 @t1 @t10) @t14))) % 93.39/93.66 (assume @p301 (forall @t126 (tptp.c_Map_Omap__le @t14 @t14 @t1 @t10))) % 93.39/93.66 (assume @p302 (forall (@list @t322 @t452 @t1 @t10 @t319) (or (tptp.c_Map_Omap__le @t322 @t452 @t1 @t10) (not (tptp.c_Map_Omap__le @t319 @t452 @t1 @t10)) @t451))) % 93.39/93.66 (assume @p303 (forall (@list @t2 @t3 @t42 @t1) (or @t330 @t279 (not @t332)))) % 93.39/93.66 (assume @p304 (forall (@list @t131 @t130 @t127 @t48 @t1) (or @t413 @t132))) % 93.39/93.66 (assume @p305 (forall (@list @t164 @t10 @t1 @t14 @t3 @t143) (or (not @t456) @t454))) % 93.39/93.66 (assume @p306 (forall (@list @t14 @t3 @t1 @t164 @t143 @t10) (or (not @t454) @t456))) % 93.39/93.66 (assume @p307 (forall @t460 (or @t459 (= @t457 @t73)))) % 93.39/93.66 (assume @p308 (forall @t460 (or @t459 @t64))) % 93.39/93.66 (assume @p309 (forall @t460 (or @t459 @t70))) % 93.39/93.66 (assume @p310 (forall @t460 (or @t459 (= @t458 @t74)))) % 93.39/93.66 (assume @p311 (forall @t414 (or @t413 (tptp.c_WellTypeRT_OWTrt @t48 @t131 @t225 @t167 @t127)))) % 93.39/93.66 (assume @p312 (forall (@list @t14 @t143 @t10 @t1 @t164 @t3) (= @t463 @t461))) % 93.39/93.66 (assume @p313 (forall (@list @t26 @t135 @t130 @t164 @t10 @t1) (= @t162 (tptp.hAPP @t165 @t130)))) % 93.39/93.66 (assume @p314 (forall @t450 (or (= @t449 @t464) @t77))) % 93.39/93.66 (assume @p315 (forall (@list @t164 @t10 @t1 @t14 @t3) (= (tptp.c_fst @t455 @t1 @t10) (tptp.c_fst @t3 @t1 @t164)))) % 93.39/93.66 (assume @p316 (forall (@list @t322 @t319 @t452 @t1 @t10) (= (tptp.c_Map_Omap__add @t322 (tptp.c_Map_Omap__add @t319 @t452 @t1 @t10) @t1 @t10) (tptp.c_Map_Omap__add @t465 @t452 @t1 @t10)))) % 93.39/93.66 (assume @p317 (forall (@list @t322 @t319 @t103 @t107 @t1 @t10) (= (tptp.c_Map_Omap__add @t322 (tptp.c_Map_Omap__upds @t319 @t103 @t107 @t1 @t10) @t1 @t10) (tptp.c_Map_Omap__upds @t465 @t103 @t107 @t1 @t10)))) % 93.39/93.66 (assume @p318 (forall (@list @t10 @t1 @t187 @t130 @t354 @t318) (or (= (tptp.hAPP (tptp.c_Map_Omap__of (tptp.c_List_Olist_OCons (tptp.hAPP (tptp.hAPP @t466 @t187) @t130) @t354 @t415) @t10 @t1) @t318) (tptp.hAPP (tptp.c_Map_Omap__of @t354 @t10 @t1) @t318)) (= @t187 @t318)))) % 93.39/93.66 (assume @p319 (forall @t411 (or @t205 (tptp.c_Objects_Ohext @t131 @t410)))) % 93.39/93.66 (assume @p320 (forall (@list @t14 @t10 @t1 @t467) (or (not (= (tptp.hAPP @t347 @t467) @t55)) (= @t467 @t115)))) % 93.39/93.66 (assume @p321 (forall (@list @t10 @t164 @t1 @t14 @t335) (= (tptp.hAPP (tptp.hAPP @t468 @t14) @t335) (tptp.hAPP (tptp.hAPP @t14 (tptp.c_fst @t335 @t10 @t164)) (tptp.c_snd @t335 @t10 @t164))))) % 93.39/93.66 (assume @p322 (forall @t186 (or @t469 @t373))) % 93.39/93.66 (assume @p323 (forall @t186 (or (not @t469) @t372))) % 93.39/93.66 (assume @p324 (forall (@list @t14 @t10 @t1 @t143 @t164 @t467) (= (tptp.hAPP @t347 (tptp.hAPP (tptp.c_Option_Omap @t143 @t164 @t10) @t467)) (tptp.hAPP (tptp.c_Option_Omap @t462 @t164 @t1) @t467)))) % 93.39/93.66 (assume @p325 (forall (@list @t26 @t2 @t1 @t135) (or @t76 @t136 (not @t470)))) % 93.39/93.66 (assume @p326 (forall @t117 (tptp.c_Map_Omap__le @t116 @t14 @t1 @t10))) % 93.39/93.66 (assume @p327 (forall @t186 (or (= @t14 @t143) (not (tptp.c_Map_Omap__le @t143 @t14 @t1 @t10)) @t447))) % 93.39/93.66 (assume @p328 (forall (@list @t473 @t471 @t48 @t198 @t1) (or (= @t473 @t471) (not (tptp.c_TypeRel_OFields @t48 @t198 @t473 @t1)) @t472))) % 93.39/93.66 (assume @p329 (forall (@list @t10 @t164 @t1 @t48 @t216) (= (tptp.hAPP (tptp.hAPP @t418 @t48) @t216) (tptp.hAPP (tptp.hAPP @t48 (tptp.c_fst @t216 @t10 @t164)) (tptp.c_snd @t216 @t10 @t164))))) % 93.39/93.66 (assume @p330 (forall (@list @t474 @t179) (or (not (= (tptp.c_Value_Oval_OAddr @t474) @t180)) (= @t474 @t179)))) % 93.39/93.66 (assume @p331 (forall (@list @t14 @t164 @t1 @t10 @t3) (= (tptp.c_fst @t477 @t1 @t10) @t476))) % 93.39/93.66 (assume @p332 (forall @t141 (tptp.hBOOL (tptp.c_Option_Ois__none @t55 @t1)))) % 93.39/93.66 (assume @p333 (forall @t437 (= (tptp.c_Option_Ooption_Ooption__case @t169 @t172 @t115 @t1 @t10) @t169))) % 93.39/93.66 (assume @p334 (forall (@list @t131 @t26 @t377 @t48 @t1) (or (not (= @t204 @t380)) @t253 @t378))) % 93.39/93.66 (assume @p335 (forall (@list @t14 @t164 @t1 @t10 @t3 @t143) (or (not @t479) @t478))) % 93.39/93.66 (assume @p336 (forall (@list @t14 @t3 @t164 @t10 @t143 @t1) (or (not @t478) @t479))) % 93.39/93.66 (assume @p337 (forall (@list @t10 @t1 @t143) (tptp.c_Map_Omap__le @t210 @t143 @t1 @t10))) % 93.39/93.66 (assume @p338 (forall (@list @t14 @t26 @t11 @t10 @t1) (= (tptp.c_Set_Oimage @t14 (tptp.c_Set_Oinsert @t26 @t11 @t10) @t10 @t1) (tptp.c_Set_Oinsert @t90 (tptp.c_Set_Oimage @t14 @t11 @t10 @t1) @t1)))) % 93.39/93.66 (assume @p339 (forall @t482 (or @t481 @t360 @t480))) % 93.39/93.66 (assume @p340 (forall (@list @t14 @t3 @t42 @t1 @t10 @t2) (or (tptp.c_Fun_Oinj__on @t483 @t2 @t1 @t10) @t286 @t58))) % 93.39/93.66 (assume @p341 (forall @t98 (or (= @t97 @t233) @t93))) % 93.39/93.66 (assume @p342 (forall (@list @t14 @t143 @t131 @t317 @t164 @t1 @t10) (= (tptp.c_Fun_Ocomp @t14 (tptp.c_Fun_Ocomp @t143 @t131 @t317 @t164 @t1) @t164 @t10 @t1) (tptp.c_Fun_Ocomp @t339 @t131 @t317 @t10 @t1)))) % 93.39/93.66 (assume @p343 (forall @t9 (tptp.hBOOL (tptp.hAPP @t8 @t3)))) % 93.39/93.66 (assume @p344 (forall (@list @t14 @t143 @t164 @t1 @t10 @t484) (= (tptp.c_Set_Oimage (tptp.c_Fun_Ocomp @t14 @t143 @t164 @t1 @t10) @t484 @t10 @t1) (tptp.c_Set_Oimage @t14 (tptp.c_Set_Oimage @t143 @t484 @t10 @t164) @t164 @t1)))) % 93.39/93.66 (assume @p345 (forall (@list @t322 @t3 @t1 @t319 @t318 @t10 @t164) (or (not (= @t487 @t55)) @t486 @t325))) % 93.39/93.66 (assume @p346 (forall @t493 (or @t492 @t489))) % 93.39/93.66 (assume @p347 (forall @t493 (or @t492 (= @t491 @t490)))) % 93.39/93.66 (assume @p348 (forall (@list @t26 @t135 @t11 @t1) (or (tptp.hBOOL (tptp.c_in @t26 (tptp.c_Set_Oinsert @t135 @t11 @t1) @t1)) (not (tptp.hBOOL (tptp.c_in @t26 @t11 @t1)))))) % 93.39/93.66 (assume @p349 (forall (@list @t26 @t135 @t2 @t1) (or @t470 @t77))) % 93.39/93.66 (assume @p350 (forall (@list @t26 @t135 @t164 @t10 @t1 @t22 @t262 @t317 @t130) (or (not (= @t165 (tptp.c_Fun_Ocomp @t22 @t262 @t317 @t10 @t1))) (= @t162 (tptp.hAPP @t22 (tptp.hAPP @t262 @t130)))))) % 93.39/93.66 (assume @p351 (forall (@list @t14 @t143 @t3 @t496 @t495 @t39 @t10 @t1 @t164 @t317 @t494) (or (not (= @t461 (tptp.hAPP @t496 (tptp.hAPP @t495 @t39)))) (= @t463 (tptp.hAPP (tptp.c_Fun_Ocomp @t496 @t495 @t317 @t1 @t494) @t39))))) % 93.39/93.66 (assume @p352 (forall (@list @t14 @t164 @t1 @t10 @t143 @t317 @t3) (= (tptp.hAPP @t341 (tptp.hAPP (tptp.c_Product__Type_Oapfst @t143 @t317 @t164 @t10) @t3)) (tptp.hAPP (tptp.c_Product__Type_Oapfst (tptp.c_Fun_Ocomp @t14 @t143 @t164 @t1 @t317) @t317 @t1 @t10) @t3)))) % 93.39/93.66 (assume @p353 (forall (@list @t32 @t1 @t74 @t35 @t34 @t73) (not (= @t33 @t75)))) % 93.39/93.66 (assume @p354 (forall (@list @t48 @t10 @t1 @t3 @t42) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t48 @t498) (tptp.c_fst @t497 @t10 @t1))) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t48 @t42) @t3)))))) % 93.39/93.66 (assume @p355 (forall (@list @t32 @t1 @t499) (or (not (= @t33 (tptp.c_Expr_Oexp_OVal @t499 @t1))) (= @t32 @t499)))) % 93.39/93.66 (assume @p356 @t500) % 93.39/93.66 (assume @p357 @t503) % 93.39/93.66 (assume @p358 (forall (@list @t82 @t26 @t10 @t3 @t1 @t356 @t42) (or (not (= (tptp.c_Fun_Ofun__upd @t82 @t26 @t485 @t1 @t81) (tptp.c_Fun_Ofun__upd @t356 @t26 @t271 @t1 @t81))) @t240))) % 93.39/93.66 (assume @p359 (forall @t185 (= (tptp.c_Option_Othe @t269 @t1) @t3))) % 93.39/93.66 (assume @p360 (forall @t506 (= (tptp.c_Option_Ooption_Ooption__rec @t169 @t172 @t505 @t1 @t10) @t504))) % 93.39/93.66 (assume @p361 (forall @t509 (or (= (tptp.hAPP @t483 @t216) @t508) @t507))) % 93.39/93.66 (assume @p362 (forall (@list @t14 @t3 @t42 @t10 @t1 @t216) (or (= (tptp.hAPP @t96 @t216) @t508) @t507))) % 93.39/93.66 (assume @p363 (forall (@list @t14 @t164 @t1 @t317 @t10 @t143 @t26 @t135) (= (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oprod__fun @t14 @t164 @t1 @t317 @t10) @t143) (tptp.hAPP (tptp.hAPP (tptp.c_Pair @t164 @t317) @t26) @t135)) (tptp.hAPP (tptp.hAPP @t340 @t90) (tptp.hAPP @t143 @t135))))) % 93.39/93.66 (assume @p364 (forall @t513 (or @t512 (= @t135 @t510)))) % 93.39/93.66 (assume @p365 (forall @t513 (or @t512 @t489))) % 93.39/93.66 (assume @p366 (forall (@list @t364 @t318 @t1 @t3 @t10) (or (not (= (tptp.hAPP @t364 @t318) @t269)) (= (tptp.c_Fun_Ofun__upd @t364 @t318 @t269 @t10 @t215) @t364)))) % 93.39/93.66 (assume @p367 (forall (@list @t82 @t43 @t1 @t3 @t245) (= (tptp.hAPP (tptp.c_Fun_Ofun__upd @t82 @t43 @t269 @t245 @t215) @t43) @t269))) % 93.39/93.66 (assume @p368 (forall (@list @t322 @t3 @t1 @t130 @t319 @t318 @t10 @t164) (or (not (= @t487 @t514)) @t486 (= @t324 @t514)))) % 93.39/93.66 (assume @p369 (forall (@list @t48 @t169 @t43 @t515) (or (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP @t517 (tptp.hAPP (tptp.hAPP @t516 @t43) @t515))))) (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP (tptp.hAPP @t169 @t43) @t515)))))) % 93.39/93.66 (assume @p370 (forall (@list @t1 @t10 @t169 @t26 @t135) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Oprod_Oprod__case @t1 @t10 tptp.tc_bool) @t169) @t511)) (not (tptp.hBOOL @t518))))) % 93.39/93.66 (assume @p371 (forall (@list @t48 @t169 @t26 @t135) (or (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP @t517 (tptp.hAPP (tptp.hAPP @t516 @t26) @t135))))) (tptp.hBOOL (tptp.hAPP @t48 @t518))))) % 93.39/93.66 (assume @p372 (forall (@list @t14 @t143 @t3 @t10 @t42 @t1) (= (tptp.c_Map_Omap__add @t14 (tptp.c_Fun_Ofun__upd @t143 @t3 @t271 @t1 @t81) @t1 @t10) (tptp.c_Fun_Ofun__upd @t371 @t3 @t271 @t1 @t81)))) % 93.39/93.66 (assume @p373 (forall (@list @t48 @t1 @t10 @t26 @t135) (or (tptp.hBOOL (tptp.hAPP @t48 @t511)) (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_ATP__Linkup_Osko__Product__Type__Xsplit__paired__All__1__1 @t48 @t1 @t10))))))) % 93.39/93.66 (assume @p374 (forall (@list @t48 @t1 @t10 @t3 @t43) (or (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_ATP__Linkup_Osko__Product__Type__Xsplit__paired__Ex__1__3 @t48 @t1 @t10))) (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP @t416 @t43))))))) % 93.39/93.66 (assume @p375 (forall (@list @t10 @t164 @t1 @t22 @t26 @t135) (= (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Ointernal__split @t10 @t164 @t1) @t22) @t346) @t344))) % 93.39/93.66 (assume @p376 (forall (@list @t14 @t3 @t245 @t1) (= (tptp.c_Fun_Ofun__upd @t14 @t3 @t56 @t245 @t1) @t14))) % 93.39/93.66 (assume @p377 (forall (@list @t14 @t3 @t42 @t1 @t245) (= (tptp.hAPP (tptp.c_Fun_Ofun__upd @t14 @t3 @t42 @t1 @t245) @t3) @t42))) % 93.39/93.66 (assume @p378 (forall (@list @t14 @t3 @t1 @t10) (= (tptp.c_Fun_Ofun__upd @t14 @t3 @t56 @t1 @t10) @t14))) % 93.39/93.66 (assume @p379 (forall (@list @t14 @t3 @t42 @t10 @t1) (= (tptp.hAPP @t96 @t3) @t42))) % 93.39/93.66 (assume @p380 (forall @t117 (= (tptp.c_Fun_Ofun__upd @t14 @t3 @t56 @t10 @t1) @t14))) % 93.39/93.66 (assume @p381 (forall @t446 (= @t349 (tptp.c_Fun_Ofun__upd (tptp.c_Fun_Ofun__upd @t14 @t26 @t519 @t1 @t10) @t135 @t90 @t1 @t10)))) % 93.39/93.66 (assume @p382 @t520) % 93.39/93.66 (assume @p383 (forall (@list @t3 @t10 @t164 @t1) (= (tptp.c_Product__Type_Oscomp @t3 @t345 @t1 @t10 @t164 (tptp.tc_prod @t10 @t164)) @t3))) % 93.39/93.66 (assume @p384 (forall (@list @t164 @t1 @t3 @t14 @t10) (= (tptp.c_Product__Type_Oscomp (tptp.hAPP (tptp.c_Pair @t164 @t1) @t3) @t14 @t1 @t164 @t1 @t10) @t56))) % 93.39/93.66 (assume @p385 (forall @t509 (= (tptp.c_Fun_Ofun__upd @t483 @t3 @t216 @t1 @t10) (tptp.c_Fun_Ofun__upd @t14 @t3 @t216 @t1 @t10)))) % 93.39/93.66 (assume @p386 (forall (@list @t131 @t26 @t198 @t197 @t48 @t1 @t408) (or @t205 @t253 (tptp.c_Conform_Ohconf @t48 @t410 @t1) (not (tptp.c_Conform_Ooconf @t48 @t131 @t409 @t1))))) % 93.39/93.66 (assume @p387 (forall (@list @t131 @t26 @t198 @t197 @t48 @t377 @t1 @t408) (or @t205 @t379 (tptp.c_Conform_Ooconf @t48 @t410 @t377 @t1)))) % 93.39/93.66 (assume @p388 (forall (@list @t14 @t10 @t164 @t1 @t26 @t135) (= (tptp.hAPP (tptp.hAPP (tptp.c_curry @t14 @t10 @t164 @t1) @t26) @t135) (tptp.hAPP @t14 @t346)))) % 93.39/93.66 (assume @p389 (forall (@list @t14 @t143 @t26 @t10 @t135 @t1 @t2) (= (tptp.c_Fun_Ofun__upd (tptp.c_Fun_Ooverride__on @t14 (tptp.c_Fun_Ofun__upd @t143 @t26 @t385 @t1 @t81) @t2 @t1 @t81) @t26 @t464 @t1 @t81) (tptp.c_Fun_Ooverride__on @t14 @t143 @t27 @t1 @t81)))) % 93.39/93.66 (assume @p390 @t521) % 93.39/93.66 (assume @p391 (forall (@list @t48 @t169 @t172 @t43) (or (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_Option_Ooption_Ooption__case @t169 @t172 (tptp.hAPP @t308 @t43) tptp.t_a tptp.t_b)))) (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP @t172 @t43)))))) % 93.39/93.66 (assume @p392 (forall (@list @t48 @t169 @t172 @t26) (or (not (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_Option_Ooption_Ooption__case @t169 @t172 (tptp.hAPP @t308 @t26) tptp.t_a tptp.t_b)))) (tptp.hBOOL (tptp.hAPP @t48 @t504))))) % 93.39/93.66 (assume @p393 (forall @t72 (tptp.c_Fun_Oinj__on @t217 @t2 @t1 @t215))) % 93.39/93.66 (assume @p394 (forall @t185 (not (tptp.hBOOL (tptp.c_Option_Ois__none @t269 @t1))))) % 93.39/93.66 (assume @p395 (forall (@list @t82 @t26 @t135 @t1 @t10 @t22 @t262) (or (= (tptp.c_Fun_Ofun__upd (tptp.c_Fun_Ofun__upd @t82 @t26 @t135 @t1 @t10) @t22 @t262 @t1 @t10) (tptp.c_Fun_Ofun__upd (tptp.c_Fun_Ofun__upd @t82 @t22 @t262 @t1 @t10) @t26 @t135 @t1 @t10)) @t261))) % 93.39/93.66 (assume @p396 (forall (@list @t10 @t164 @t1 @t169 @t26 @t135) (= (tptp.hAPP (tptp.hAPP @t468 @t169) @t346) @t518))) % 93.39/93.66 (assume @p397 (forall (@list @t1 @t26 @t488) (or (not (= (tptp.hAPP @t217 @t26) @t522)) @t489))) % 93.39/93.66 (assume @p398 (forall (@list @t1 @t43) (not (= (tptp.hAPP @t217 @t43) @t55)))) % 93.39/93.66 (assume @p399 (forall @t523 (not (= @t522 @t55)))) % 93.39/93.66 (assume @p400 (forall (@list @t14 @t26 @t135 @t1 @t10 @t143) (or (tptp.c_Map_Omap__le (tptp.c_Fun_Ofun__upd @t14 @t26 @t135 @t1 @t81) (tptp.c_Fun_Ofun__upd @t143 @t26 @t135 @t1 @t81) @t1 @t10) @t447))) % 93.39/93.66 (assume @p401 (forall (@list @t322 @t3 @t10 @t1 @t319 @t42) (or (tptp.c_Map_Omap__le (tptp.c_Fun_Ofun__upd @t322 @t3 @t115 @t1 @t81) (tptp.c_Fun_Ofun__upd @t319 @t3 @t271 @t1 @t81) @t1 @t10) @t451))) % 93.39/93.66 (assume @p402 (forall (@list @t524 @t26 @t135 @t22 @t1 @t10 @t164) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.hAPP @t524 @t26) @t135) @t22)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.c_split @t1 @t10 (tptp.tc_fun @t164 tptp.tc_bool)) @t524) @t511) @t22)))))) % 93.39/93.66 (assume @p403 (forall (@list @t1 @t10 @t14 @t26 @t135) (or @t527 (not @t526)))) % 93.39/93.66 (assume @p404 (forall (@list @t14 @t26 @t135 @t1 @t10) (or @t526 (not @t527)))) % 93.39/93.66 (assume @p405 (forall (@list @t82 @t3 @t1 @t42 @t26 @t135 @t10) (or (not @t530) @t529 @t528))) % 93.39/93.66 (assume @p406 (forall @t533 (or @t532 @t530 @t531))) % 93.39/93.66 (assume @p407 (forall @t533 (or @t532 @t530 @t529))) % 93.39/93.66 (assume @p408 (forall (@list @t364 @t318 @t10 @t3 @t1) (not (= (tptp.c_Fun_Ofun__upd @t364 @t318 @t485 @t1 @t81) @t210)))) % 93.39/93.66 (assume @p409 (forall (@list @t48 @t131 @t198 @t471 @t1) (or (tptp.c_Conform_Ooconf @t48 @t131 (tptp.hAPP @t200 (tptp.c_Objects_Oinit__fields @t471)) @t1) @t472))) % 93.39/93.66 (assume @p410 (forall (@list @t1 @t10 @t164 @t14 @t26 @t135) (= (tptp.hAPP @t343 @t511) @t525))) % 93.39/93.66 (assume @p411 (forall (@list @t10 @t164 @t1 @t14 @t26 @t135) (= (tptp.hAPP (tptp.hAPP @t418 @t14) @t346) @t525))) % 93.39/93.66 (assume @p412 (forall @t536 (or @t535 (not @t534)))) % 93.39/93.66 (assume @p413 (forall @t536 (or @t534 (not @t535)))) % 93.39/93.66 (assume @p414 (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_ha____ tptp.v_E____ (tptp.c_Expr_Oexp_OFAss (tptp.c_Expr_Oexp_OVal (tptp.c_Value_Oval_OAddr tptp.v_a____) @t50) tptp.v_F____ tptp.v_D____ (tptp.c_Expr_Oexp_OVal tptp.v_v____ @t50) @t50) tptp.v_T____)) % 93.39/93.66 (assume @p415 (forall @t506 (= (tptp.c_Option_Ooption_Ooption__case @t169 @t172 @t505 @t1 @t10) @t504))) % 93.39/93.66 (assume @p416 (forall (@list @t14 @t164 @t10 @t82 @t26 @t135 @t1) (= (tptp.c_Fun_Ocomp @t383 (tptp.c_Fun_Ofun__upd @t82 @t26 (tptp.hAPP (tptp.c_Option_Ooption_OSome @t164) @t135) @t1 @t381) @t381 @t81 @t1) (tptp.c_Fun_Ofun__upd (tptp.c_Fun_Ocomp @t383 @t82 @t381 @t81 @t1) @t26 (tptp.hAPP @t110 @t519) @t1 @t81)))) % 93.39/93.66 (assume @p417 (forall (@list @t82 @t26 @t384 @t1 @t135 @t386 @t10) (= (tptp.c_Map_Omap__upds @t82 (tptp.c_List_Olist_OCons @t26 @t384 @t1) (tptp.c_List_Olist_OCons @t135 @t386 @t10) @t1 @t10) @t387))) % 93.39/93.66 (assume @p418 (forall (@list @t169 @t10 @t164 @t26 @t135 @t1) (= (tptp.c_Product__Type_Oprod_Oprod__rec @t169 @t346 @t10 @t164 @t1) @t518))) % 93.39/93.66 (assume @p419 (forall (@list @t1 @t10 @t26 @t135) (= (tptp.c_fst @t511 @t1 @t10) @t26))) % 93.39/93.66 (assume @p420 (forall (@list @t3 @t1 @t10 @t42) (= @t3 (tptp.c_fst @t417 @t1 @t10)))) % 93.39/93.66 (assume @p421 (forall (@list @t135 @t42 @t82 @t3 @t245 @t1) (or @t531 (not (= (tptp.hAPP (tptp.c_Fun_Ofun__upd @t82 @t3 (tptp.hAPP @t307 @t135) @t1 (tptp.tc_Option_Ooption @t245)) @t3) (tptp.hAPP @t307 @t42)))))) % 93.39/93.66 (assume @p422 (forall (@list @t14 @t164 @t1 @t10 @t3 @t42) (= (tptp.hAPP @t341 (tptp.hAPP (tptp.hAPP (tptp.c_Pair @t164 @t10) @t3) @t42)) (tptp.hAPP (tptp.hAPP @t340 @t56) @t42)))) % 93.39/93.66 (assume @p423 (forall (@list @t14 @t143 @t3 @t42 @t1 @t164 @t10) (= (tptp.c_Fun_Ocomp @t14 (tptp.c_Fun_Ofun__upd @t143 @t3 @t42 @t1 @t164) @t164 @t10 @t1) (tptp.c_Fun_Ofun__upd @t369 @t3 @t241 @t1 @t10)))) % 93.39/93.66 (assume @p424 (forall (@list @t1 @t42) (not (= @t55 @t219)))) % 93.39/93.66 (assume @p425 (forall @t523 (not (= @t55 @t522)))) % 93.39/93.66 (assume @p426 (forall (@list @t82 @t3 @t10 @t42 @t1 @t2) (or (= (tptp.c_Set_Oimage (tptp.c_Fun_Ofun__upd @t82 @t3 @t271 @t1 @t81) @t2 @t1 @t81) (tptp.c_Set_Oimage @t82 @t2 @t1 @t81)) @t4))) % 93.39/93.66 (assume @p427 (forall (@list @t164 @t10 @t1 @t14 @t3 @t42) (= (tptp.hAPP @t338 (tptp.hAPP (tptp.hAPP (tptp.c_Pair @t1 @t164) @t3) @t42)) (tptp.hAPP @t416 @t241)))) % 93.39/93.66 (assume @p428 (forall (@list @t10 @t1 @t26 @t135) (= (tptp.c_snd (tptp.hAPP (tptp.hAPP @t466 @t26) @t135) @t10 @t1) @t135))) % 93.39/93.66 (assume @p429 (forall (@list @t42 @t10 @t1 @t3) (= @t42 @t498))) % 93.39/93.66 (assume @p430 (forall @t482 (or @t481 @t434 @t480))) % 93.39/93.66 (assume @p431 (forall (@list @t14 @t10 @t1 @t3) (= (tptp.hAPP @t347 @t485) (tptp.hAPP @t217 @t56)))) % 93.39/93.66 (assume @p432 (forall (@list @t48 @t159 @t377 @t1 @t131) (or (tptp.c_Conform_Ooconf @t48 @t159 @t377 @t1) @t161 @t379))) % 93.39/93.66 (assume @p433 (forall (@list @t319 @t318 @t1 @t537 @t322 @t164 @t10) (or (not (= @t320 (tptp.hAPP @t217 @t537))) (= @t366 (tptp.hAPP @t322 @t537))))) % 93.39/93.66 (assume @p434 (forall (@list @t48 @t1 @t3) (or (not (tptp.hBOOL (tptp.hAPP @t48 @t393))) @t121))) % 93.39/93.66 (assume @p435 (forall (@list @t48 @t1 @t10 @t335 @t448 @t438) (or (tptp.hBOOL (tptp.hAPP @t48 (tptp.c_fst @t540 @t1 @t10))) @t539 @t538))) % 93.39/93.66 (assume @p436 (= (tptp.hAPP (tptp.c_COMBI tptp.t_a) tptp.v_P) tptp.v_P)) % 93.39/93.66 (assume @p437 (forall (@list @t356 @t318 @t1 @t541 @t82 @t10) (or (not (= @t359 @t542)) (= @t357 @t542)))) % 93.39/93.66 (assume @p438 (forall (@list @t356 @t318 @t1 @t3 @t82 @t10) (or (not @t480) @t433))) % 93.39/93.66 (assume @p439 (forall (@list @t1 @t245 @t3 @t130 @t354) (= (tptp.hAPP (tptp.c_Map_Omap__of (tptp.c_List_Olist_OCons (tptp.hAPP (tptp.hAPP (tptp.c_Pair @t1 @t245) @t3) @t130) @t354 (tptp.tc_prod @t1 @t245)) @t1 @t245) @t3) (tptp.hAPP @t307 @t130)))) % 93.39/93.66 (assume @p440 (forall @t243 (or (not (= @t483 @t14)) (= @t56 @t42)))) % 93.39/93.66 (assume @p441 @t543) % 93.39/93.66 (assume @p442 (forall (@list @t438 @t1 @t10 @t335 @t448 @t48) (or (tptp.hBOOL (tptp.hAPP @t438 (tptp.c_snd @t540 @t1 @t10))) @t539 @t538))) % 93.39/93.66 (assume @p443 (not @t544)) % 93.39/93.66 (assume @p444 (forall @t548 (or (tptp.class_Orderings_Otop @t547) (not (tptp.class_Orderings_Otop @t545))))) % 93.39/93.66 (assume @p445 (forall @t548 (or (tptp.class_Orderings_Obot @t547) (not (tptp.class_Orderings_Obot @t545))))) % 93.39/93.66 (assume @p446 (forall @t548 (or (tptp.class_HOL_Ominus @t547) (not (tptp.class_HOL_Ominus @t545))))) % 93.39/93.66 (assume @p447 (tptp.class_OrderedGroup_Ocomm__monoid__mult tptp.tc_nat)) % 93.39/93.66 (assume @p448 (tptp.class_OrderedGroup_Ocomm__monoid__add tptp.tc_nat)) % 93.39/93.66 (assume @p449 (tptp.class_Orderings_Obot tptp.tc_nat)) % 93.39/93.66 (assume @p450 (tptp.class_HOL_Ominus tptp.tc_nat)) % 93.39/93.66 (assume @p451 (tptp.class_Orderings_Otop tptp.tc_bool)) % 93.39/93.66 (assume @p452 (tptp.class_Orderings_Obot tptp.tc_bool)) % 93.39/93.66 (assume @p453 (tptp.class_HOL_Ominus tptp.tc_bool)) % 93.39/93.66 (assume @p454 (forall @t238 (tptp.hBOOL (tptp.c_fequal @t3 @t3 @t1)))) % 93.39/93.66 (assume @p455 (forall (@list @t182 @t177 @t1) (or (= @t182 @t177) (not (tptp.hBOOL (tptp.c_fequal @t182 @t177 @t1)))))) % 93.39/93.66 (step @p456 :rule instantiate :premises (@p219) :args ((@list tptp.v_ha____ tptp.v_v____ tptp.v_Tv____ tptp.v_P tptp.v_TF____ @t375))) % 93.39/93.66 (step @p457 :rule cnf_or_pos :args (@t552)) % 93.39/93.66 (step @p458 :rule reordering :premises (@p457) :args ((or @t549 @t551 @t550 (not @t552)))) % 93.39/93.66 (step @p459 :rule chain_m_resolution :premises (@p458 @p204 @p382 @p456) :args (@t550 @t553 (@list @t376 @t520 @t552))) % 93.39/93.66 (step @p460 :rule instantiate :premises (@p334) :args ((@list tptp.v_ha____ tptp.v_a____ @t502 tptp.v_P @t375))) % 93.39/93.66 (step @p461 :rule cnf_or_pos :args (@t557)) % 93.39/93.66 (step @p462 :rule reordering :premises (@p461) :args ((or @t556 @t555 @t554 (not @t557)))) % 93.39/93.66 (step @p463 :rule chain_m_resolution :premises (@p462 @p357 @p390 @p460) :args (@t554 @t553 (@list @t503 @t521 @t557))) % 93.39/93.66 (step @p464 :rule cnf_or_pos :args (@t561)) % 93.39/93.66 (step @p465 :rule reordering :premises (@p464) :args ((or @t544 @t558 @t560 @t559 @t562))) % 93.39/93.66 (step @p466 :rule chain_m_resolution :premises (@p465 @p443 @p356 @p463 @p459) :args (@t562 (@list true false false false) (@list @t544 @t500 @t554 @t550))) % 93.39/93.66 (assume-push @p473 @t543) % 93.39/93.66 (step @p468 :rule instantiate :premises (@p441) :args ((@list tptp.v_P tptp.v_ha____ tptp.v_C____ tptp.v_fs____ tptp.v_F____ tptp.v_D____ tptp.v_v____ @t375 tptp.v_TF____))) % 93.39/93.66 (step-pop @p474 :rule scope :premises (@p468)) % 93.39/93.66 (step @p469 :rule process_scope :premises (@p474) :args (@t561)) % 93.39/93.66 (step @p471 :rule implies_elim :premises (@p469)) % 93.39/93.66 (step @p472 false :rule chain_m_resolution :premises (@p471 @p466 @p441) :args (false (@list true false) (@list @t561 @t543))) % 93.39/93.66 ) % 93.39/93.66 % SZS output end Proof % 93.39/93.66 % cvc5 exiting %------------------------------------------------------------------------------