%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SWW472^1 : TPTP v6.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n189.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:37:22 EDT 2014 % Result : Timeout 300.03s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SWW472^1 : TPTP v6.1.0. Released v5.3.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n189.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 09:16:16 CDT 2014 % % CPUTime : 300.03 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x1f1c878>, <kernel.Type object at 0x1ec73f8>) of role type named ty_ty_tc__Com__Ocom % Using role type % Declaring com:Type % FOF formula (<kernel.Constant object at 0x1f1ce18>, <kernel.Type object at 0x1ec71b8>) of role type named ty_ty_tc__Com__Ostate % Using role type % Declaring state:Type % FOF formula (<kernel.Constant object at 0x1f1c878>, <kernel.Type object at 0x1ec7758>) of role type named ty_ty_tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostate_J % Using role type % Declaring hoare_1262092251_state:Type % FOF formula (<kernel.Constant object at 0x1f1c878>, <kernel.DependentProduct object at 0x1ec71b8>) of role type named sy_c_Big__Operators_Osemilattice__big_000tc__Hoare____Mirabelle____ghhkfsbqqq__O % Using role type % Declaring big_se1697321605_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(((hoare_1262092251_state->Prop)->hoare_1262092251_state)->Prop)) % FOF formula (<kernel.Constant object at 0x1f1c878>, <kernel.Constant object at 0x1ec71b8>) of role type named sy_c_Com_Ocom_OSKIP % Using role type % Declaring skip:com % FOF formula (<kernel.Constant object at 0x1ec79e0>, <kernel.DependentProduct object at 0x1ec7bd8>) of role type named sy_c_Com_Ocom_OSemi % Using role type % Declaring semi:(com->(com->com)) % FOF formula (<kernel.Constant object at 0x1ec7050>, <kernel.DependentProduct object at 0x1ec7950>) of role type named sy_c_Ex % Using role type % Declaring _TPTP_ex:((hoare_1262092251_state->Prop)->Prop) % FOF formula (<kernel.Constant object at 0x1ec71b8>, <kernel.DependentProduct object at 0x1ec7bd8>) of role type named sy_c_Finite__Set_Ofinite_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__C % Using role type % Declaring finite1178804552_state:((hoare_1262092251_state->Prop)->Prop) % FOF formula (<kernel.Constant object at 0x1ec70e0>, <kernel.DependentProduct object at 0x1ec7950>) of role type named sy_c_Finite__Set_Ofold1Set_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc_ % Using role type % Declaring finite403475723_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop))) % FOF formula (<kernel.Constant object at 0x1ec7290>, <kernel.DependentProduct object at 0x1ec7830>) of role type named sy_c_Finite__Set_Ofold1_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Co % Using role type % Declaring finite1740352635_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->((hoare_1262092251_state->Prop)->hoare_1262092251_state)) % FOF formula (<kernel.Constant object at 0x1ec7050>, <kernel.DependentProduct object at 0x1aeb758>) of role type named sy_c_Finite__Set_Ofold__graph_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_I % Using role type % Declaring finite975744042_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(hoare_1262092251_state->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop)))) % FOF formula (<kernel.Constant object at 0x1ec7830>, <kernel.DependentProduct object at 0x1aeb758>) of role type named sy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_ % Using role type % Declaring finite1168661790_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(((hoare_1262092251_state->Prop)->hoare_1262092251_state)->Prop)) % FOF formula (<kernel.Constant object at 0x1ec7290>, <kernel.DependentProduct object at 0x1aeb758>) of role type named sy_c_Finite__Set_Ofolding__one__idem_000tc__Hoare____Mirabelle____ghhkfsbqqq__Ot % Using role type % Declaring finite900773345_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(((hoare_1262092251_state->Prop)->hoare_1262092251_state)->Prop)) % FOF formula (<kernel.Constant object at 0x1ec7830>, <kernel.DependentProduct object at 0x1aebea8>) of role type named sy_c_Groups_Ominus__class_Ominus_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__ % Using role type % Declaring minus_2758725tate_o:((hoare_1262092251_state->Prop)->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop))) % FOF formula (<kernel.Constant object at 0x1ec7290>, <kernel.DependentProduct object at 0x1aeb758>) of role type named sy_c_Hoare__Mirabelle__ghhkfsbqqq_OMGT % Using role type % Declaring hoare_Mirabelle_MGT:(com->hoare_1262092251_state) % FOF formula (<kernel.Constant object at 0x1ec7050>, <kernel.DependentProduct object at 0x1aeb440>) of role type named sy_c_Hoare__Mirabelle__ghhkfsbqqq_Ohoare__derivs_000tc__Com__Ostate % Using role type % Declaring hoare_930741239_state:((hoare_1262092251_state->Prop)->((hoare_1262092251_state->Prop)->Prop)) % FOF formula (<kernel.Constant object at 0x1ec7050>, <kernel.DependentProduct object at 0x1aeb7e8>) of role type named sy_c_Hoare__Mirabelle__ghhkfsbqqq_Ohoare__valids_000tc__Com__Ostate % Using role type % Declaring hoare_1337152501_state:((hoare_1262092251_state->Prop)->((hoare_1262092251_state->Prop)->Prop)) % FOF formula (<kernel.Constant object at 0x1aeb518>, <kernel.DependentProduct object at 0x1aebea8>) of role type named sy_c_Hoare__Mirabelle__ghhkfsbqqq_Otriple_Otriple_000tc__Com__Ostate % Using role type % Declaring hoare_951399329_state:((state->(state->Prop))->(com->((state->(state->Prop))->hoare_1262092251_state))) % FOF formula (<kernel.Constant object at 0x1aeb4d0>, <kernel.DependentProduct object at 0x1aeb7e8>) of role type named sy_c_Orderings_Obot__class_Obot_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__O % Using role type % Declaring bot_bo113204042tate_o:(hoare_1262092251_state->Prop) % FOF formula (<kernel.Constant object at 0x1aeb7a0>, <kernel.Sort object at 0x19b5098>) of role type named sy_c_Orderings_Obot__class_Obot_000_Eo % Using role type % Declaring bot_bot_o:Prop % FOF formula (<kernel.Constant object at 0x1aeb3f8>, <kernel.DependentProduct object at 0x1aeb518>) of role type named sy_c_Set_OCollect_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ost % Using role type % Declaring collec1121927558_state:((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop)) % FOF formula (<kernel.Constant object at 0x1aebf80>, <kernel.DependentProduct object at 0x1aebab8>) of role type named sy_c_Set_Oinsert_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Osta % Using role type % Declaring insert81609953_state:(hoare_1262092251_state->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop))) % FOF formula (<kernel.Constant object at 0x1aeb830>, <kernel.DependentProduct object at 0x1aebc20>) of role type named sy_c_Set_Othe__elem_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__O % Using role type % Declaring the_el417915516_state:((hoare_1262092251_state->Prop)->hoare_1262092251_state) % FOF formula (<kernel.Constant object at 0x1aeb7a0>, <kernel.DependentProduct object at 0x1aebfc8>) of role type named sy_c_member_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostate_J % Using role type % Declaring member5164104_state:(hoare_1262092251_state->((hoare_1262092251_state->Prop)->Prop)) % FOF formula (<kernel.Constant object at 0x1aeb4d0>, <kernel.DependentProduct object at 0x1aeb518>) of role type named sy_v_P % Using role type % Declaring p:(state->(state->Prop)) % FOF formula (<kernel.Constant object at 0x1aebc20>, <kernel.DependentProduct object at 0x1aebf80>) of role type named sy_v_Q % Using role type % Declaring q:(state->(state->Prop)) % FOF formula (<kernel.Constant object at 0x1aebfc8>, <kernel.Constant object at 0x1aebf80>) of role type named sy_v_c % Using role type % Declaring c:com % FOF formula (forall (G_12:(hoare_1262092251_state->Prop)), ((hoare_930741239_state G_12) bot_bo113204042tate_o)) of role axiom named fact_0_empty % A new axiom: (forall (G_12:(hoare_1262092251_state->Prop)), ((hoare_930741239_state G_12) bot_bo113204042tate_o)) % FOF formula (forall (Fun1_2:(state->(state->Prop))) (Com_2:com) (Fun2_2:(state->(state->Prop))) (Fun1_1:(state->(state->Prop))) (Com_1:com) (Fun2_1:(state->(state->Prop))), ((iff (((eq hoare_1262092251_state) (((hoare_951399329_state Fun1_2) Com_2) Fun2_2)) (((hoare_951399329_state Fun1_1) Com_1) Fun2_1))) ((and ((and (((eq (state->(state->Prop))) Fun1_2) Fun1_1)) (((eq com) Com_2) Com_1))) (((eq (state->(state->Prop))) Fun2_2) Fun2_1)))) of role axiom named fact_1_triple_Oinject % A new axiom: (forall (Fun1_2:(state->(state->Prop))) (Com_2:com) (Fun2_2:(state->(state->Prop))) (Fun1_1:(state->(state->Prop))) (Com_1:com) (Fun2_1:(state->(state->Prop))), ((iff (((eq hoare_1262092251_state) (((hoare_951399329_state Fun1_2) Com_2) Fun2_2)) (((hoare_951399329_state Fun1_1) Com_1) Fun2_1))) ((and ((and (((eq (state->(state->Prop))) Fun1_2) Fun1_1)) (((eq com) Com_2) Com_1))) (((eq (state->(state->Prop))) Fun2_2) Fun2_1)))) % FOF formula (forall (G_11:(hoare_1262092251_state->Prop)) (Ts_3:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_11) Ts_3)->((hoare_1337152501_state G_11) Ts_3))) of role axiom named fact_2_hoare__sound % A new axiom: (forall (G_11:(hoare_1262092251_state->Prop)) (Ts_3:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_11) Ts_3)->((hoare_1337152501_state G_11) Ts_3))) % FOF formula (forall (G_10:(hoare_1262092251_state->Prop)) (G_9:(hoare_1262092251_state->Prop)) (Ts_2:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_9) Ts_2)->(((hoare_930741239_state G_10) G_9)->((hoare_930741239_state G_10) Ts_2)))) of role axiom named fact_3_cut % A new axiom: (forall (G_10:(hoare_1262092251_state->Prop)) (G_9:(hoare_1262092251_state->Prop)) (Ts_2:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_9) Ts_2)->(((hoare_930741239_state G_10) G_9)->((hoare_930741239_state G_10) Ts_2)))) % FOF formula (forall (Ts_1:(hoare_1262092251_state->Prop)) (G_8:(hoare_1262092251_state->Prop)) (T_1:hoare_1262092251_state), (((hoare_930741239_state G_8) ((insert81609953_state T_1) bot_bo113204042tate_o))->(((hoare_930741239_state G_8) Ts_1)->((hoare_930741239_state G_8) ((insert81609953_state T_1) Ts_1))))) of role axiom named fact_4_hoare__derivs_Oinsert % A new axiom: (forall (Ts_1:(hoare_1262092251_state->Prop)) (G_8:(hoare_1262092251_state->Prop)) (T_1:hoare_1262092251_state), (((hoare_930741239_state G_8) ((insert81609953_state T_1) bot_bo113204042tate_o))->(((hoare_930741239_state G_8) Ts_1)->((hoare_930741239_state G_8) ((insert81609953_state T_1) Ts_1))))) % FOF formula (forall (G_7:(hoare_1262092251_state->Prop)) (T:hoare_1262092251_state) (Ts:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_7) ((insert81609953_state T) Ts))->((and ((hoare_930741239_state G_7) ((insert81609953_state T) bot_bo113204042tate_o))) ((hoare_930741239_state G_7) Ts)))) of role axiom named fact_5_derivs__insertD % A new axiom: (forall (G_7:(hoare_1262092251_state->Prop)) (T:hoare_1262092251_state) (Ts:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_7) ((insert81609953_state T) Ts))->((and ((hoare_930741239_state G_7) ((insert81609953_state T) bot_bo113204042tate_o))) ((hoare_930741239_state G_7) Ts)))) % FOF formula (forall (Q_7:(state->(state->Prop))) (G_6:(hoare_1262092251_state->Prop)) (P_14:(state->(state->Prop))) (C_8:com) (Q_6:(state->(state->Prop))), (((hoare_930741239_state G_6) ((insert81609953_state (((hoare_951399329_state P_14) C_8) Q_6)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((Q_6 Z_5) S)->((Q_7 Z_5) S)))->((hoare_930741239_state G_6) ((insert81609953_state (((hoare_951399329_state P_14) C_8) Q_7)) bot_bo113204042tate_o))))) of role axiom named fact_6_conseq2 % A new axiom: (forall (Q_7:(state->(state->Prop))) (G_6:(hoare_1262092251_state->Prop)) (P_14:(state->(state->Prop))) (C_8:com) (Q_6:(state->(state->Prop))), (((hoare_930741239_state G_6) ((insert81609953_state (((hoare_951399329_state P_14) C_8) Q_6)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((Q_6 Z_5) S)->((Q_7 Z_5) S)))->((hoare_930741239_state G_6) ((insert81609953_state (((hoare_951399329_state P_14) C_8) Q_7)) bot_bo113204042tate_o))))) % FOF formula (forall (P_13:(state->(state->Prop))) (G_5:(hoare_1262092251_state->Prop)) (P_12:(state->(state->Prop))) (C_7:com) (Q_5:(state->(state->Prop))), (((hoare_930741239_state G_5) ((insert81609953_state (((hoare_951399329_state P_12) C_7) Q_5)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((P_13 Z_5) S)->((P_12 Z_5) S)))->((hoare_930741239_state G_5) ((insert81609953_state (((hoare_951399329_state P_13) C_7) Q_5)) bot_bo113204042tate_o))))) of role axiom named fact_7_conseq1 % A new axiom: (forall (P_13:(state->(state->Prop))) (G_5:(hoare_1262092251_state->Prop)) (P_12:(state->(state->Prop))) (C_7:com) (Q_5:(state->(state->Prop))), (((hoare_930741239_state G_5) ((insert81609953_state (((hoare_951399329_state P_12) C_7) Q_5)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((P_13 Z_5) S)->((P_12 Z_5) S)))->((hoare_930741239_state G_5) ((insert81609953_state (((hoare_951399329_state P_13) C_7) Q_5)) bot_bo113204042tate_o))))) % FOF formula (forall (A_71:hoare_1262092251_state) (B_20:hoare_1262092251_state) (A_70:(hoare_1262092251_state->Prop)), (((member5164104_state A_71) ((insert81609953_state B_20) A_70))->((not (((eq hoare_1262092251_state) A_71) B_20))->((member5164104_state A_71) A_70)))) of role axiom named fact_8_insertE % A new axiom: (forall (A_71:hoare_1262092251_state) (B_20:hoare_1262092251_state) (A_70:(hoare_1262092251_state->Prop)), (((member5164104_state A_71) ((insert81609953_state B_20) A_70))->((not (((eq hoare_1262092251_state) A_71) B_20))->((member5164104_state A_71) A_70)))) % FOF formula (forall (B_19:hoare_1262092251_state) (A_69:hoare_1262092251_state) (B_18:(hoare_1262092251_state->Prop)), (((((member5164104_state A_69) B_18)->False)->(((eq hoare_1262092251_state) A_69) B_19))->((member5164104_state A_69) ((insert81609953_state B_19) B_18)))) of role axiom named fact_9_insertCI % A new axiom: (forall (B_19:hoare_1262092251_state) (A_69:hoare_1262092251_state) (B_18:(hoare_1262092251_state->Prop)), (((((member5164104_state A_69) B_18)->False)->(((eq hoare_1262092251_state) A_69) B_19))->((member5164104_state A_69) ((insert81609953_state B_19) B_18)))) % FOF formula (forall (Q_4:(state->(state->Prop))) (P_11:(state->(state->Prop))) (G_4:(hoare_1262092251_state->Prop)) (P_10:(state->(state->Prop))) (C_6:com) (Q_3:(state->(state->Prop))), (((hoare_930741239_state G_4) ((insert81609953_state (((hoare_951399329_state P_10) C_6) Q_3)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((P_11 Z_5) S)->(forall (S_1:state), ((forall (Z_6:state), (((P_10 Z_6) S)->((Q_3 Z_6) S_1)))->((Q_4 Z_5) S_1)))))->((hoare_930741239_state G_4) ((insert81609953_state (((hoare_951399329_state P_11) C_6) Q_4)) bot_bo113204042tate_o))))) of role axiom named fact_10_conseq12 % A new axiom: (forall (Q_4:(state->(state->Prop))) (P_11:(state->(state->Prop))) (G_4:(hoare_1262092251_state->Prop)) (P_10:(state->(state->Prop))) (C_6:com) (Q_3:(state->(state->Prop))), (((hoare_930741239_state G_4) ((insert81609953_state (((hoare_951399329_state P_10) C_6) Q_3)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((P_11 Z_5) S)->(forall (S_1:state), ((forall (Z_6:state), (((P_10 Z_6) S)->((Q_3 Z_6) S_1)))->((Q_4 Z_5) S_1)))))->((hoare_930741239_state G_4) ((insert81609953_state (((hoare_951399329_state P_11) C_6) Q_4)) bot_bo113204042tate_o))))) % FOF formula (forall (A_68:hoare_1262092251_state), (((member5164104_state A_68) bot_bo113204042tate_o)->False)) of role axiom named fact_11_emptyE % A new axiom: (forall (A_68:hoare_1262092251_state), (((member5164104_state A_68) bot_bo113204042tate_o)->False)) % FOF formula (forall (A_67:hoare_1262092251_state) (A_66:(hoare_1262092251_state->Prop)), (not (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) ((insert81609953_state A_67) A_66)))) of role axiom named fact_12_empty__not__insert % A new axiom: (forall (A_67:hoare_1262092251_state) (A_66:(hoare_1262092251_state->Prop)), (not (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) ((insert81609953_state A_67) A_66)))) % FOF formula (forall (A_65:hoare_1262092251_state) (A_64:(hoare_1262092251_state->Prop)), (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_65) A_64)) bot_bo113204042tate_o))) of role axiom named fact_13_insert__not__empty % A new axiom: (forall (A_65:hoare_1262092251_state) (A_64:(hoare_1262092251_state->Prop)), (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_65) A_64)) bot_bo113204042tate_o))) % FOF formula (forall (B_17:hoare_1262092251_state) (A_63:hoare_1262092251_state), ((iff ((member5164104_state B_17) ((insert81609953_state A_63) bot_bo113204042tate_o))) (((eq hoare_1262092251_state) B_17) A_63))) of role axiom named fact_14_singleton__iff % A new axiom: (forall (B_17:hoare_1262092251_state) (A_63:hoare_1262092251_state), ((iff ((member5164104_state B_17) ((insert81609953_state A_63) bot_bo113204042tate_o))) (((eq hoare_1262092251_state) B_17) A_63))) % FOF formula (forall (A_62:hoare_1262092251_state) (B_16:hoare_1262092251_state) (C_5:hoare_1262092251_state) (D_1:hoare_1262092251_state), ((iff (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_62) ((insert81609953_state B_16) bot_bo113204042tate_o))) ((insert81609953_state C_5) ((insert81609953_state D_1) bot_bo113204042tate_o)))) ((or ((and (((eq hoare_1262092251_state) A_62) C_5)) (((eq hoare_1262092251_state) B_16) D_1))) ((and (((eq hoare_1262092251_state) A_62) D_1)) (((eq hoare_1262092251_state) B_16) C_5))))) of role axiom named fact_15_doubleton__eq__iff % A new axiom: (forall (A_62:hoare_1262092251_state) (B_16:hoare_1262092251_state) (C_5:hoare_1262092251_state) (D_1:hoare_1262092251_state), ((iff (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_62) ((insert81609953_state B_16) bot_bo113204042tate_o))) ((insert81609953_state C_5) ((insert81609953_state D_1) bot_bo113204042tate_o)))) ((or ((and (((eq hoare_1262092251_state) A_62) C_5)) (((eq hoare_1262092251_state) B_16) D_1))) ((and (((eq hoare_1262092251_state) A_62) D_1)) (((eq hoare_1262092251_state) B_16) C_5))))) % FOF formula (forall (A_61:hoare_1262092251_state) (A_60:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) A_60) bot_bo113204042tate_o)->(((member5164104_state A_61) A_60)->False))) of role axiom named fact_16_equals0D % A new axiom: (forall (A_61:hoare_1262092251_state) (A_60:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) A_60) bot_bo113204042tate_o)->(((member5164104_state A_61) A_60)->False))) % FOF formula (forall (P_9:(hoare_1262092251_state->Prop)), ((iff (((eq (hoare_1262092251_state->Prop)) (collec1121927558_state P_9)) bot_bo113204042tate_o)) (forall (X_2:hoare_1262092251_state), ((P_9 X_2)->False)))) of role axiom named fact_17_Collect__empty__eq % A new axiom: (forall (P_9:(hoare_1262092251_state->Prop)), ((iff (((eq (hoare_1262092251_state->Prop)) (collec1121927558_state P_9)) bot_bo113204042tate_o)) (forall (X_2:hoare_1262092251_state), ((P_9 X_2)->False)))) % FOF formula (forall (C_4:hoare_1262092251_state), (((member5164104_state C_4) bot_bo113204042tate_o)->False)) of role axiom named fact_18_empty__iff % A new axiom: (forall (C_4:hoare_1262092251_state), (((member5164104_state C_4) bot_bo113204042tate_o)->False)) % FOF formula (forall (P_8:(hoare_1262092251_state->Prop)), ((iff (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) (collec1121927558_state P_8))) (forall (X_2:hoare_1262092251_state), ((P_8 X_2)->False)))) of role axiom named fact_19_empty__Collect__eq % A new axiom: (forall (P_8:(hoare_1262092251_state->Prop)), ((iff (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) (collec1121927558_state P_8))) (forall (X_2:hoare_1262092251_state), ((P_8 X_2)->False)))) % FOF formula (forall (A_59:(hoare_1262092251_state->Prop)), ((iff ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((member5164104_state X_2) A_59)))) (not (((eq (hoare_1262092251_state->Prop)) A_59) bot_bo113204042tate_o)))) of role axiom named fact_20_ex__in__conv % A new axiom: (forall (A_59:(hoare_1262092251_state->Prop)), ((iff ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((member5164104_state X_2) A_59)))) (not (((eq (hoare_1262092251_state->Prop)) A_59) bot_bo113204042tate_o)))) % FOF formula (forall (A_58:(hoare_1262092251_state->Prop)), ((iff (forall (X_2:hoare_1262092251_state), (((member5164104_state X_2) A_58)->False))) (((eq (hoare_1262092251_state->Prop)) A_58) bot_bo113204042tate_o))) of role axiom named fact_21_all__not__in__conv % A new axiom: (forall (A_58:(hoare_1262092251_state->Prop)), ((iff (forall (X_2:hoare_1262092251_state), (((member5164104_state X_2) A_58)->False))) (((eq (hoare_1262092251_state->Prop)) A_58) bot_bo113204042tate_o))) % FOF formula (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) (collec1121927558_state (fun (X_2:hoare_1262092251_state)=> False))) of role axiom named fact_22_empty__def % A new axiom: (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) (collec1121927558_state (fun (X_2:hoare_1262092251_state)=> False))) % FOF formula (forall (A_57:hoare_1262092251_state) (A_56:(hoare_1262092251_state->Prop)), (((member5164104_state A_57) A_56)->(((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_57) A_56)) A_56))) of role axiom named fact_23_insert__absorb % A new axiom: (forall (A_57:hoare_1262092251_state) (A_56:(hoare_1262092251_state->Prop)), (((member5164104_state A_57) A_56)->(((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_57) A_56)) A_56))) % FOF formula (forall (B_15:hoare_1262092251_state) (A_55:hoare_1262092251_state) (B_14:(hoare_1262092251_state->Prop)), (((member5164104_state A_55) B_14)->((member5164104_state A_55) ((insert81609953_state B_15) B_14)))) of role axiom named fact_24_insertI2 % A new axiom: (forall (B_15:hoare_1262092251_state) (A_55:hoare_1262092251_state) (B_14:(hoare_1262092251_state->Prop)), (((member5164104_state A_55) B_14)->((member5164104_state A_55) ((insert81609953_state B_15) B_14)))) % FOF formula (forall (B_13:(hoare_1262092251_state->Prop)) (X_22:hoare_1262092251_state) (A_54:(hoare_1262092251_state->Prop)), ((((member5164104_state X_22) A_54)->False)->((((member5164104_state X_22) B_13)->False)->((iff (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_22) A_54)) ((insert81609953_state X_22) B_13))) (((eq (hoare_1262092251_state->Prop)) A_54) B_13))))) of role axiom named fact_25_insert__ident % A new axiom: (forall (B_13:(hoare_1262092251_state->Prop)) (X_22:hoare_1262092251_state) (A_54:(hoare_1262092251_state->Prop)), ((((member5164104_state X_22) A_54)->False)->((((member5164104_state X_22) B_13)->False)->((iff (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_22) A_54)) ((insert81609953_state X_22) B_13))) (((eq (hoare_1262092251_state->Prop)) A_54) B_13))))) % FOF formula (forall (Y_4:hoare_1262092251_state) (A_53:(hoare_1262092251_state->Prop)) (X_21:hoare_1262092251_state), ((iff (((insert81609953_state Y_4) A_53) X_21)) ((or (((eq hoare_1262092251_state) Y_4) X_21)) (A_53 X_21)))) of role axiom named fact_26_insert__code % A new axiom: (forall (Y_4:hoare_1262092251_state) (A_53:(hoare_1262092251_state->Prop)) (X_21:hoare_1262092251_state), ((iff (((insert81609953_state Y_4) A_53) X_21)) ((or (((eq hoare_1262092251_state) Y_4) X_21)) (A_53 X_21)))) % FOF formula (forall (A_52:hoare_1262092251_state) (B_12:hoare_1262092251_state) (A_51:(hoare_1262092251_state->Prop)), ((iff ((member5164104_state A_52) ((insert81609953_state B_12) A_51))) ((or (((eq hoare_1262092251_state) A_52) B_12)) ((member5164104_state A_52) A_51)))) of role axiom named fact_27_insert__iff % A new axiom: (forall (A_52:hoare_1262092251_state) (B_12:hoare_1262092251_state) (A_51:(hoare_1262092251_state->Prop)), ((iff ((member5164104_state A_52) ((insert81609953_state B_12) A_51))) ((or (((eq hoare_1262092251_state) A_52) B_12)) ((member5164104_state A_52) A_51)))) % FOF formula (forall (X_20:hoare_1262092251_state) (Y_3:hoare_1262092251_state) (A_50:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_20) ((insert81609953_state Y_3) A_50))) ((insert81609953_state Y_3) ((insert81609953_state X_20) A_50)))) of role axiom named fact_28_insert__commute % A new axiom: (forall (X_20:hoare_1262092251_state) (Y_3:hoare_1262092251_state) (A_50:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_20) ((insert81609953_state Y_3) A_50))) ((insert81609953_state Y_3) ((insert81609953_state X_20) A_50)))) % FOF formula (forall (X_19:hoare_1262092251_state) (A_49:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_19) ((insert81609953_state X_19) A_49))) ((insert81609953_state X_19) A_49))) of role axiom named fact_29_insert__absorb2 % A new axiom: (forall (X_19:hoare_1262092251_state) (A_49:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_19) ((insert81609953_state X_19) A_49))) ((insert81609953_state X_19) A_49))) % FOF formula (forall (A_48:hoare_1262092251_state) (P_7:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_48) (collec1121927558_state P_7))) (collec1121927558_state (fun (U:hoare_1262092251_state)=> (((fun (X:Prop) (Y:Prop)=> (X->Y)) (not (((eq hoare_1262092251_state) U) A_48))) (P_7 U)))))) of role axiom named fact_30_insert__Collect % A new axiom: (forall (A_48:hoare_1262092251_state) (P_7:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_48) (collec1121927558_state P_7))) (collec1121927558_state (fun (U:hoare_1262092251_state)=> (((fun (X:Prop) (Y:Prop)=> (X->Y)) (not (((eq hoare_1262092251_state) U) A_48))) (P_7 U)))))) % FOF formula (forall (A_47:hoare_1262092251_state) (B_11:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_47) B_11)) (collec1121927558_state (fun (X_2:hoare_1262092251_state)=> ((or (((eq hoare_1262092251_state) X_2) A_47)) ((member5164104_state X_2) B_11)))))) of role axiom named fact_31_insert__compr % A new axiom: (forall (A_47:hoare_1262092251_state) (B_11:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_47) B_11)) (collec1121927558_state (fun (X_2:hoare_1262092251_state)=> ((or (((eq hoare_1262092251_state) X_2) A_47)) ((member5164104_state X_2) B_11)))))) % FOF formula (forall (A_46:hoare_1262092251_state) (B_10:(hoare_1262092251_state->Prop)), ((member5164104_state A_46) ((insert81609953_state A_46) B_10))) of role axiom named fact_32_insertI1 % A new axiom: (forall (A_46:hoare_1262092251_state) (B_10:(hoare_1262092251_state->Prop)), ((member5164104_state A_46) ((insert81609953_state A_46) B_10))) % FOF formula (forall (A_45:hoare_1262092251_state) (B_9:hoare_1262092251_state), ((((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_45) bot_bo113204042tate_o)) ((insert81609953_state B_9) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) A_45) B_9))) of role axiom named fact_33_singleton__inject % A new axiom: (forall (A_45:hoare_1262092251_state) (B_9:hoare_1262092251_state), ((((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_45) bot_bo113204042tate_o)) ((insert81609953_state B_9) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) A_45) B_9))) % FOF formula (forall (B_8:hoare_1262092251_state) (A_44:hoare_1262092251_state), (((member5164104_state B_8) ((insert81609953_state A_44) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) B_8) A_44))) of role axiom named fact_34_singletonE % A new axiom: (forall (B_8:hoare_1262092251_state) (A_44:hoare_1262092251_state), (((member5164104_state B_8) ((insert81609953_state A_44) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) B_8) A_44))) % FOF formula (forall (X_18:hoare_1262092251_state), (((eq hoare_1262092251_state) (the_el417915516_state ((insert81609953_state X_18) bot_bo113204042tate_o))) X_18)) of role axiom named fact_35_the__elem__eq % A new axiom: (forall (X_18:hoare_1262092251_state), (((eq hoare_1262092251_state) (the_el417915516_state ((insert81609953_state X_18) bot_bo113204042tate_o))) X_18)) % FOF formula (forall (X_17:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_17)) bot_bot_o)) of role axiom named fact_36_bot__apply % A new axiom: (forall (X_17:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_17)) bot_bot_o)) % FOF formula (forall (X_2:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_2)) bot_bot_o)) of role axiom named fact_37_bot__fun__def % A new axiom: (forall (X_2:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_2)) bot_bot_o)) % FOF formula (forall (G_3:(hoare_1262092251_state->Prop)) (P_6:(state->(state->Prop))), ((hoare_930741239_state G_3) ((insert81609953_state (((hoare_951399329_state P_6) skip) P_6)) bot_bo113204042tate_o))) of role axiom named fact_38_hoare__derivs_OSkip % A new axiom: (forall (G_3:(hoare_1262092251_state->Prop)) (P_6:(state->(state->Prop))), ((hoare_930741239_state G_3) ((insert81609953_state (((hoare_951399329_state P_6) skip) P_6)) bot_bo113204042tate_o))) % FOF formula (forall (D:com) (R:(state->(state->Prop))) (G_2:(hoare_1262092251_state->Prop)) (P_5:(state->(state->Prop))) (C_3:com) (Q_2:(state->(state->Prop))), (((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state P_5) C_3) Q_2)) bot_bo113204042tate_o))->(((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state Q_2) D) R)) bot_bo113204042tate_o))->((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state P_5) ((semi C_3) D)) R)) bot_bo113204042tate_o))))) of role axiom named fact_39_Comp % A new axiom: (forall (D:com) (R:(state->(state->Prop))) (G_2:(hoare_1262092251_state->Prop)) (P_5:(state->(state->Prop))) (C_3:com) (Q_2:(state->(state->Prop))), (((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state P_5) C_3) Q_2)) bot_bo113204042tate_o))->(((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state Q_2) D) R)) bot_bo113204042tate_o))->((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state P_5) ((semi C_3) D)) R)) bot_bo113204042tate_o))))) % FOF formula (forall (Y_2:hoare_1262092251_state), ((forall (Fun1:(state->(state->Prop))) (Com:com) (Fun2:(state->(state->Prop))), (not (((eq hoare_1262092251_state) Y_2) (((hoare_951399329_state Fun1) Com) Fun2))))->False)) of role axiom named fact_40_triple_Oexhaust % A new axiom: (forall (Y_2:hoare_1262092251_state), ((forall (Fun1:(state->(state->Prop))) (Com:com) (Fun2:(state->(state->Prop))), (not (((eq hoare_1262092251_state) Y_2) (((hoare_951399329_state Fun1) Com) Fun2))))->False)) % FOF formula (forall (X_16:hoare_1262092251_state) (A_43:(hoare_1262092251_state->Prop)), (((member5164104_state X_16) A_43)->((forall (B_7:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) A_43) ((insert81609953_state X_16) B_7))->((member5164104_state X_16) B_7)))->False))) of role axiom named fact_41_Set_Oset__insert % A new axiom: (forall (X_16:hoare_1262092251_state) (A_43:(hoare_1262092251_state->Prop)), (((member5164104_state X_16) A_43)->((forall (B_7:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) A_43) ((insert81609953_state X_16) B_7))->((member5164104_state X_16) B_7)))->False))) % FOF formula (forall (A_42:hoare_1262092251_state) (A_41:(hoare_1262092251_state->Prop)), (((member5164104_state A_42) A_41)->((ex (hoare_1262092251_state->Prop)) (fun (B_7:(hoare_1262092251_state->Prop))=> ((and (((eq (hoare_1262092251_state->Prop)) A_41) ((insert81609953_state A_42) B_7))) (((member5164104_state A_42) B_7)->False)))))) of role axiom named fact_42_mk__disjoint__insert % A new axiom: (forall (A_42:hoare_1262092251_state) (A_41:(hoare_1262092251_state->Prop)), (((member5164104_state A_42) A_41)->((ex (hoare_1262092251_state->Prop)) (fun (B_7:(hoare_1262092251_state->Prop))=> ((and (((eq (hoare_1262092251_state->Prop)) A_41) ((insert81609953_state A_42) B_7))) (((member5164104_state A_42) B_7)->False)))))) % FOF formula (forall (Com1:com) (Com2:com), (not (((eq com) ((semi Com1) Com2)) skip))) of role axiom named fact_43_com_Osimps_I13_J % A new axiom: (forall (Com1:com) (Com2:com), (not (((eq com) ((semi Com1) Com2)) skip))) % FOF formula (forall (Com1:com) (Com2:com), (not (((eq com) skip) ((semi Com1) Com2)))) of role axiom named fact_44_com_Osimps_I12_J % A new axiom: (forall (Com1:com) (Com2:com), (not (((eq com) skip) ((semi Com1) Com2)))) % FOF formula (forall (A_40:(hoare_1262092251_state->Prop)), ((forall (Y:hoare_1262092251_state), (((member5164104_state Y) A_40)->False))->(((eq (hoare_1262092251_state->Prop)) A_40) bot_bo113204042tate_o))) of role axiom named fact_45_equals0I % A new axiom: (forall (A_40:(hoare_1262092251_state->Prop)), ((forall (Y:hoare_1262092251_state), (((member5164104_state Y) A_40)->False))->(((eq (hoare_1262092251_state->Prop)) A_40) bot_bo113204042tate_o))) % FOF formula (forall (Q:(state->(state->Prop))) (G_1:(hoare_1262092251_state->Prop)) (C_2:com) (P_3:(state->(state->Prop))), ((forall (Z_5:state) (S:state), (((P_3 Z_5) S)->((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state G_1) ((insert81609953_state (((hoare_951399329_state P_4) C_2) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((Q Z_5) S_1))))))))))->((hoare_930741239_state G_1) ((insert81609953_state (((hoare_951399329_state P_3) C_2) Q)) bot_bo113204042tate_o)))) of role axiom named fact_46_conseq % A new axiom: (forall (Q:(state->(state->Prop))) (G_1:(hoare_1262092251_state->Prop)) (C_2:com) (P_3:(state->(state->Prop))), ((forall (Z_5:state) (S:state), (((P_3 Z_5) S)->((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state G_1) ((insert81609953_state (((hoare_951399329_state P_4) C_2) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((Q Z_5) S_1))))))))))->((hoare_930741239_state G_1) ((insert81609953_state (((hoare_951399329_state P_3) C_2) Q)) bot_bo113204042tate_o)))) % FOF formula (forall (Com1_1:com) (Com2_1:com) (Com1:com) (Com2:com), ((iff (((eq com) ((semi Com1_1) Com2_1)) ((semi Com1) Com2))) ((and (((eq com) Com1_1) Com1)) (((eq com) Com2_1) Com2)))) of role axiom named fact_47_com_Osimps_I3_J % A new axiom: (forall (Com1_1:com) (Com2_1:com) (Com1:com) (Com2:com), ((iff (((eq com) ((semi Com1_1) Com2_1)) ((semi Com1) Com2))) ((and (((eq com) Com1_1) Com1)) (((eq com) Com2_1) Com2)))) % FOF formula (forall (A_39:(hoare_1262092251_state->Prop)), ((iff (not (((eq (hoare_1262092251_state->Prop)) A_39) bot_bo113204042tate_o))) ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (B_7:(hoare_1262092251_state->Prop))=> ((and (((eq (hoare_1262092251_state->Prop)) A_39) ((insert81609953_state X_2) B_7))) (((member5164104_state X_2) B_7)->False)))))))) of role axiom named fact_48_nonempty__iff % A new axiom: (forall (A_39:(hoare_1262092251_state->Prop)), ((iff (not (((eq (hoare_1262092251_state->Prop)) A_39) bot_bo113204042tate_o))) ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (B_7:(hoare_1262092251_state->Prop))=> ((and (((eq (hoare_1262092251_state->Prop)) A_39) ((insert81609953_state X_2) B_7))) (((member5164104_state X_2) B_7)->False)))))))) % FOF formula (forall (X_2:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_2)) ((member5164104_state X_2) bot_bo113204042tate_o))) of role axiom named fact_49_bot__empty__eq % A new axiom: (forall (X_2:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_2)) ((member5164104_state X_2) bot_bo113204042tate_o))) % FOF formula (forall (F_34:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_38:hoare_1262092251_state) (B_6:hoare_1262092251_state), ((iff (((finite403475723_state F_34) ((insert81609953_state A_38) bot_bo113204042tate_o)) B_6)) (((eq hoare_1262092251_state) A_38) B_6))) of role axiom named fact_50_fold1Set__sing % A new axiom: (forall (F_34:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_38:hoare_1262092251_state) (B_6:hoare_1262092251_state), ((iff (((finite403475723_state F_34) ((insert81609953_state A_38) bot_bo113204042tate_o)) B_6)) (((eq hoare_1262092251_state) A_38) B_6))) % FOF formula (forall (X_15:hoare_1262092251_state) (F_33:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_32:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_33) F_32)->(((eq hoare_1262092251_state) (F_32 ((insert81609953_state X_15) bot_bo113204042tate_o))) X_15))) of role axiom named fact_51_folding__one_Osingleton % A new axiom: (forall (X_15:hoare_1262092251_state) (F_33:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_32:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_33) F_32)->(((eq hoare_1262092251_state) (F_32 ((insert81609953_state X_15) bot_bo113204042tate_o))) X_15))) % FOF formula (forall (F_31:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_37:hoare_1262092251_state), (((eq hoare_1262092251_state) ((finite1740352635_state F_31) ((insert81609953_state A_37) bot_bo113204042tate_o))) A_37)) of role axiom named fact_52_fold1__singleton % A new axiom: (forall (F_31:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_37:hoare_1262092251_state), (((eq hoare_1262092251_state) ((finite1740352635_state F_31) ((insert81609953_state A_37) bot_bo113204042tate_o))) A_37)) % FOF formula (forall (A_36:hoare_1262092251_state) (G:((hoare_1262092251_state->Prop)->hoare_1262092251_state)) (F_30:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))), ((((eq ((hoare_1262092251_state->Prop)->hoare_1262092251_state)) G) (finite1740352635_state F_30))->(((eq hoare_1262092251_state) (G ((insert81609953_state A_36) bot_bo113204042tate_o))) A_36))) of role axiom named fact_53_fold1__singleton__def % A new axiom: (forall (A_36:hoare_1262092251_state) (G:((hoare_1262092251_state->Prop)->hoare_1262092251_state)) (F_30:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))), ((((eq ((hoare_1262092251_state->Prop)->hoare_1262092251_state)) G) (finite1740352635_state F_30))->(((eq hoare_1262092251_state) (G ((insert81609953_state A_36) bot_bo113204042tate_o))) A_36))) % FOF formula (forall (F_29:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (X_14:hoare_1262092251_state), ((((finite403475723_state F_29) bot_bo113204042tate_o) X_14)->False)) of role axiom named fact_54_empty__fold1SetE % A new axiom: (forall (F_29:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (X_14:hoare_1262092251_state), ((((finite403475723_state F_29) bot_bo113204042tate_o) X_14)->False)) % FOF formula (forall (F_28:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_35:(hoare_1262092251_state->Prop)) (X_13:hoare_1262092251_state), ((((finite403475723_state F_28) A_35) X_13)->(not (((eq (hoare_1262092251_state->Prop)) A_35) bot_bo113204042tate_o)))) of role axiom named fact_55_fold1Set__nonempty % A new axiom: (forall (F_28:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_35:(hoare_1262092251_state->Prop)) (X_13:hoare_1262092251_state), ((((finite403475723_state F_28) A_35) X_13)->(not (((eq (hoare_1262092251_state->Prop)) A_35) bot_bo113204042tate_o)))) % FOF formula (forall (F_27:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_34:hoare_1262092251_state) (A_33:(hoare_1262092251_state->Prop)) (X_12:hoare_1262092251_state), (((((finite975744042_state F_27) A_34) A_33) X_12)->((((member5164104_state A_34) A_33)->False)->(((finite403475723_state F_27) ((insert81609953_state A_34) A_33)) X_12)))) of role axiom named fact_56_fold1Set_Ointros % A new axiom: (forall (F_27:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_34:hoare_1262092251_state) (A_33:(hoare_1262092251_state->Prop)) (X_12:hoare_1262092251_state), (((((finite975744042_state F_27) A_34) A_33) X_12)->((((member5164104_state A_34) A_33)->False)->(((finite403475723_state F_27) ((insert81609953_state A_34) A_33)) X_12)))) % FOF formula (forall (X_11:hoare_1262092251_state) (A_32:(hoare_1262092251_state->Prop)) (F_26:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_25:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_26) F_25)->((finite1178804552_state A_32)->((((member5164104_state X_11) A_32)->False)->((not (((eq (hoare_1262092251_state->Prop)) A_32) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F_25 ((insert81609953_state X_11) A_32))) ((F_26 X_11) (F_25 A_32)))))))) of role axiom named fact_57_folding__one_Oinsert % A new axiom: (forall (X_11:hoare_1262092251_state) (A_32:(hoare_1262092251_state->Prop)) (F_26:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_25:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_26) F_25)->((finite1178804552_state A_32)->((((member5164104_state X_11) A_32)->False)->((not (((eq (hoare_1262092251_state->Prop)) A_32) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F_25 ((insert81609953_state X_11) A_32))) ((F_26 X_11) (F_25 A_32)))))))) % FOF formula (forall (A_31:(hoare_1262092251_state->Prop)) (F_24:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_23:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_24) F_23)->((finite1178804552_state A_31)->(((eq hoare_1262092251_state) (F_23 A_31)) ((finite1740352635_state F_24) A_31))))) of role axiom named fact_58_folding__one_Oeq__fold % A new axiom: (forall (A_31:(hoare_1262092251_state->Prop)) (F_24:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_23:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_24) F_23)->((finite1178804552_state A_31)->(((eq hoare_1262092251_state) (F_23 A_31)) ((finite1740352635_state F_24) A_31))))) % FOF formula (finite1178804552_state bot_bo113204042tate_o) of role axiom named fact_59_finite_OemptyI % A new axiom: (finite1178804552_state bot_bo113204042tate_o) % FOF formula (forall (A_30:hoare_1262092251_state) (A_29:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_29)->(finite1178804552_state ((insert81609953_state A_30) A_29)))) of role axiom named fact_60_finite_OinsertI % A new axiom: (forall (A_30:hoare_1262092251_state) (A_29:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_29)->(finite1178804552_state ((insert81609953_state A_30) A_29)))) % FOF formula (forall (F_22:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_4:hoare_1262092251_state), ((((finite975744042_state F_22) Z_4) bot_bo113204042tate_o) Z_4)) of role axiom named fact_61_fold__graph_OemptyI % A new axiom: (forall (F_22:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_4:hoare_1262092251_state), ((((finite975744042_state F_22) Z_4) bot_bo113204042tate_o) Z_4)) % FOF formula (forall (F_21:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_3:hoare_1262092251_state) (X_10:hoare_1262092251_state), (((((finite975744042_state F_21) Z_3) bot_bo113204042tate_o) X_10)->(((eq hoare_1262092251_state) X_10) Z_3))) of role axiom named fact_62_empty__fold__graphE % A new axiom: (forall (F_21:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_3:hoare_1262092251_state) (X_10:hoare_1262092251_state), (((((finite975744042_state F_21) Z_3) bot_bo113204042tate_o) X_10)->(((eq hoare_1262092251_state) X_10) Z_3))) % FOF formula (forall (F_20:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_2:hoare_1262092251_state) (Y_1:hoare_1262092251_state) (X_9:hoare_1262092251_state) (A_28:(hoare_1262092251_state->Prop)), ((((member5164104_state X_9) A_28)->False)->(((((finite975744042_state F_20) Z_2) A_28) Y_1)->((((finite975744042_state F_20) Z_2) ((insert81609953_state X_9) A_28)) ((F_20 X_9) Y_1))))) of role axiom named fact_63_fold__graph_OinsertI % A new axiom: (forall (F_20:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_2:hoare_1262092251_state) (Y_1:hoare_1262092251_state) (X_9:hoare_1262092251_state) (A_28:(hoare_1262092251_state->Prop)), ((((member5164104_state X_9) A_28)->False)->(((((finite975744042_state F_20) Z_2) A_28) Y_1)->((((finite975744042_state F_20) Z_2) ((insert81609953_state X_9) A_28)) ((F_20 X_9) Y_1))))) % FOF formula (forall (A_27:hoare_1262092251_state) (A_26:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state ((insert81609953_state A_27) A_26))) (finite1178804552_state A_26))) of role axiom named fact_64_finite__insert % A new axiom: (forall (A_27:hoare_1262092251_state) (A_26:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state ((insert81609953_state A_27) A_26))) (finite1178804552_state A_26))) % FOF formula (forall (A_25:(hoare_1262092251_state->Prop)) (F_19:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_18:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_19) F_18)->((finite1178804552_state A_25)->((not (((eq (hoare_1262092251_state->Prop)) A_25) bot_bo113204042tate_o))->((forall (X_2:hoare_1262092251_state) (Y:hoare_1262092251_state), ((member5164104_state ((F_19 X_2) Y)) ((insert81609953_state X_2) ((insert81609953_state Y) bot_bo113204042tate_o))))->((member5164104_state (F_18 A_25)) A_25)))))) of role axiom named fact_65_folding__one_Oclosed % A new axiom: (forall (A_25:(hoare_1262092251_state->Prop)) (F_19:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_18:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_19) F_18)->((finite1178804552_state A_25)->((not (((eq (hoare_1262092251_state->Prop)) A_25) bot_bo113204042tate_o))->((forall (X_2:hoare_1262092251_state) (Y:hoare_1262092251_state), ((member5164104_state ((F_19 X_2) Y)) ((insert81609953_state X_2) ((insert81609953_state Y) bot_bo113204042tate_o))))->((member5164104_state (F_18 A_25)) A_25)))))) % FOF formula (forall (F_17:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_24:hoare_1262092251_state) (X_8:(hoare_1262092251_state->Prop)) (X_7:hoare_1262092251_state), ((((finite403475723_state F_17) ((insert81609953_state A_24) X_8)) X_7)->((forall (A_19:hoare_1262092251_state) (A_18:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_24) X_8)) ((insert81609953_state A_19) A_18))->(((((finite975744042_state F_17) A_19) A_18) X_7)->((member5164104_state A_19) A_18))))->False))) of role axiom named fact_66_insert__fold1SetE % A new axiom: (forall (F_17:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_24:hoare_1262092251_state) (X_8:(hoare_1262092251_state->Prop)) (X_7:hoare_1262092251_state), ((((finite403475723_state F_17) ((insert81609953_state A_24) X_8)) X_7)->((forall (A_19:hoare_1262092251_state) (A_18:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_24) X_8)) ((insert81609953_state A_19) A_18))->(((((finite975744042_state F_17) A_19) A_18) X_7)->((member5164104_state A_19) A_18))))->False))) % FOF formula (forall (F_16:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_23:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_23)->((not (((eq (hoare_1262092251_state->Prop)) A_23) bot_bo113204042tate_o))->(_TPTP_ex ((finite403475723_state F_16) A_23))))) of role axiom named fact_67_finite__nonempty__imp__fold1Set % A new axiom: (forall (F_16:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_23:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_23)->((not (((eq (hoare_1262092251_state->Prop)) A_23) bot_bo113204042tate_o))->(_TPTP_ex ((finite403475723_state F_16) A_23))))) % FOF formula (forall (P_2:((hoare_1262092251_state->Prop)->Prop)) (F_15:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_15)->((P_2 bot_bo113204042tate_o)->((forall (X_2:hoare_1262092251_state) (F_5:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_5)->((((member5164104_state X_2) F_5)->False)->((P_2 F_5)->(P_2 ((insert81609953_state X_2) F_5))))))->(P_2 F_15))))) of role axiom named fact_68_finite__induct % A new axiom: (forall (P_2:((hoare_1262092251_state->Prop)->Prop)) (F_15:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_15)->((P_2 bot_bo113204042tate_o)->((forall (X_2:hoare_1262092251_state) (F_5:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_5)->((((member5164104_state X_2) F_5)->False)->((P_2 F_5)->(P_2 ((insert81609953_state X_2) F_5))))))->(P_2 F_15))))) % FOF formula (forall (X_6:hoare_1262092251_state) (A_22:(hoare_1262092251_state->Prop)), ((iff ((member5164104_state X_6) A_22)) (A_22 X_6))) of role axiom named fact_69_mem__def % A new axiom: (forall (X_6:hoare_1262092251_state) (A_22:(hoare_1262092251_state->Prop)), ((iff ((member5164104_state X_6) A_22)) (A_22 X_6))) % FOF formula (forall (P_1:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) (collec1121927558_state P_1)) P_1)) of role axiom named fact_70_Collect__def % A new axiom: (forall (P_1:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) (collec1121927558_state P_1)) P_1)) % FOF formula (forall (A_21:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state A_21)) ((or (((eq (hoare_1262092251_state->Prop)) A_21) bot_bo113204042tate_o)) ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (A_19:hoare_1262092251_state)=> ((and (((eq (hoare_1262092251_state->Prop)) A_21) ((insert81609953_state A_19) A_18))) (finite1178804552_state A_18))))))))) of role axiom named fact_71_finite_Osimps % A new axiom: (forall (A_21:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state A_21)) ((or (((eq (hoare_1262092251_state->Prop)) A_21) bot_bo113204042tate_o)) ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (A_19:hoare_1262092251_state)=> ((and (((eq (hoare_1262092251_state->Prop)) A_21) ((insert81609953_state A_19) A_18))) (finite1178804552_state A_18))))))))) % FOF formula (forall (F_14:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_1:hoare_1262092251_state) (A_20:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_20)->(_TPTP_ex (((finite975744042_state F_14) Z_1) A_20)))) of role axiom named fact_72_finite__imp__fold__graph % A new axiom: (forall (F_14:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_1:hoare_1262092251_state) (A_20:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_20)->(_TPTP_ex (((finite975744042_state F_14) Z_1) A_20)))) % FOF formula (forall (F_13:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A1_1:(hoare_1262092251_state->Prop)) (A2_1:hoare_1262092251_state), ((iff (((finite403475723_state F_13) A1_1) A2_1)) ((ex hoare_1262092251_state) (fun (A_19:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((and ((and ((and (((eq (hoare_1262092251_state->Prop)) A1_1) ((insert81609953_state A_19) A_18))) (((eq hoare_1262092251_state) A2_1) X_2))) ((((finite975744042_state F_13) A_19) A_18) X_2))) (((member5164104_state A_19) A_18)->False)))))))))) of role axiom named fact_73_fold1Set_Osimps % A new axiom: (forall (F_13:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A1_1:(hoare_1262092251_state->Prop)) (A2_1:hoare_1262092251_state), ((iff (((finite403475723_state F_13) A1_1) A2_1)) ((ex hoare_1262092251_state) (fun (A_19:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((and ((and ((and (((eq (hoare_1262092251_state->Prop)) A1_1) ((insert81609953_state A_19) A_18))) (((eq hoare_1262092251_state) A2_1) X_2))) ((((finite975744042_state F_13) A_19) A_18) X_2))) (((member5164104_state A_19) A_18)->False)))))))))) % FOF formula (forall (F_12:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z:hoare_1262092251_state) (A1:(hoare_1262092251_state->Prop)) (A2:hoare_1262092251_state), ((iff ((((finite975744042_state F_12) Z) A1) A2)) ((or ((and (((eq (hoare_1262092251_state->Prop)) A1) bot_bo113204042tate_o)) (((eq hoare_1262092251_state) A2) Z))) ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (Y:hoare_1262092251_state)=> ((and ((and ((and (((eq (hoare_1262092251_state->Prop)) A1) ((insert81609953_state X_2) A_18))) (((eq hoare_1262092251_state) A2) ((F_12 X_2) Y)))) (((member5164104_state X_2) A_18)->False))) ((((finite975744042_state F_12) Z) A_18) Y))))))))))) of role axiom named fact_74_fold__graph_Osimps % A new axiom: (forall (F_12:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z:hoare_1262092251_state) (A1:(hoare_1262092251_state->Prop)) (A2:hoare_1262092251_state), ((iff ((((finite975744042_state F_12) Z) A1) A2)) ((or ((and (((eq (hoare_1262092251_state->Prop)) A1) bot_bo113204042tate_o)) (((eq hoare_1262092251_state) A2) Z))) ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (Y:hoare_1262092251_state)=> ((and ((and ((and (((eq (hoare_1262092251_state->Prop)) A1) ((insert81609953_state X_2) A_18))) (((eq hoare_1262092251_state) A2) ((F_12 X_2) Y)))) (((member5164104_state X_2) A_18)->False))) ((((finite975744042_state F_12) Z) A_18) Y))))))))))) % FOF formula (forall (X_5:hoare_1262092251_state) (A_17:(hoare_1262092251_state->Prop)) (F_11:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_10:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_11) F_10)->((finite1178804552_state A_17)->((not (((eq (hoare_1262092251_state->Prop)) A_17) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F_10 ((insert81609953_state X_5) A_17))) ((F_11 X_5) (F_10 A_17))))))) of role axiom named fact_75_folding__one__idem_Oinsert__idem % A new axiom: (forall (X_5:hoare_1262092251_state) (A_17:(hoare_1262092251_state->Prop)) (F_11:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_10:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_11) F_10)->((finite1178804552_state A_17)->((not (((eq (hoare_1262092251_state->Prop)) A_17) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F_10 ((insert81609953_state X_5) A_17))) ((F_11 X_5) (F_10 A_17))))))) % FOF formula (forall (X_4:hoare_1262092251_state) (F_9:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_8:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_9) F_8)->(((eq hoare_1262092251_state) ((F_9 X_4) X_4)) X_4))) of role axiom named fact_76_folding__one__idem_Oidem % A new axiom: (forall (X_4:hoare_1262092251_state) (F_9:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_8:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_9) F_8)->(((eq hoare_1262092251_state) ((F_9 X_4) X_4)) X_4))) % FOF formula (forall (X_3:hoare_1262092251_state) (A_16:(hoare_1262092251_state->Prop)) (F_7:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_6:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_7) F_6)->((finite1178804552_state A_16)->(((member5164104_state X_3) A_16)->(((eq hoare_1262092251_state) ((F_7 X_3) (F_6 A_16))) (F_6 A_16)))))) of role axiom named fact_77_folding__one__idem_Oin__idem % A new axiom: (forall (X_3:hoare_1262092251_state) (A_16:(hoare_1262092251_state->Prop)) (F_7:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_6:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_7) F_6)->((finite1178804552_state A_16)->(((member5164104_state X_3) A_16)->(((eq hoare_1262092251_state) ((F_7 X_3) (F_6 A_16))) (F_6 A_16)))))) % FOF formula (forall (P:((hoare_1262092251_state->Prop)->Prop)) (F_4:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_4)->((not (((eq (hoare_1262092251_state->Prop)) F_4) bot_bo113204042tate_o))->((forall (X_2:hoare_1262092251_state), (P ((insert81609953_state X_2) bot_bo113204042tate_o)))->((forall (X_2:hoare_1262092251_state) (F_5:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_5)->((not (((eq (hoare_1262092251_state->Prop)) F_5) bot_bo113204042tate_o))->((((member5164104_state X_2) F_5)->False)->((P F_5)->(P ((insert81609953_state X_2) F_5)))))))->(P F_4)))))) of role axiom named fact_78_finite__ne__induct % A new axiom: (forall (P:((hoare_1262092251_state->Prop)->Prop)) (F_4:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_4)->((not (((eq (hoare_1262092251_state->Prop)) F_4) bot_bo113204042tate_o))->((forall (X_2:hoare_1262092251_state), (P ((insert81609953_state X_2) bot_bo113204042tate_o)))->((forall (X_2:hoare_1262092251_state) (F_5:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_5)->((not (((eq (hoare_1262092251_state->Prop)) F_5) bot_bo113204042tate_o))->((((member5164104_state X_2) F_5)->False)->((P F_5)->(P ((insert81609953_state X_2) F_5)))))))->(P F_4)))))) % FOF formula (forall (A_15:(hoare_1262092251_state->Prop)) (F_3:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_2:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((big_se1697321605_state F_3) F_2)->((finite1178804552_state A_15)->(((eq hoare_1262092251_state) (F_2 A_15)) ((finite1740352635_state F_3) A_15))))) of role axiom named fact_79_semilattice__big_OF__eq % A new axiom: (forall (A_15:(hoare_1262092251_state->Prop)) (F_3:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_2:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((big_se1697321605_state F_3) F_2)->((finite1178804552_state A_15)->(((eq hoare_1262092251_state) (F_2 A_15)) ((finite1740352635_state F_3) A_15))))) % FOF formula (forall (X_1:hoare_1262092251_state) (A_14:(hoare_1262092251_state->Prop)) (F_1:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_1) F)->((finite1178804552_state A_14)->(((member5164104_state X_1) A_14)->((and ((((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))) bot_bo113204042tate_o)->(((eq hoare_1262092251_state) (F A_14)) X_1))) ((not (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F A_14)) ((F_1 X_1) (F ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))))))))))) of role axiom named fact_80_folding__one_Oremove % A new axiom: (forall (X_1:hoare_1262092251_state) (A_14:(hoare_1262092251_state->Prop)) (F_1:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_1) F)->((finite1178804552_state A_14)->(((member5164104_state X_1) A_14)->((and ((((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))) bot_bo113204042tate_o)->(((eq hoare_1262092251_state) (F A_14)) X_1))) ((not (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F A_14)) ((F_1 X_1) (F ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))))))))))) % FOF formula (forall (B_5:(hoare_1262092251_state->Prop)) (C_1:hoare_1262092251_state) (A_13:(hoare_1262092251_state->Prop)), (((member5164104_state C_1) A_13)->((((member5164104_state C_1) B_5)->False)->((member5164104_state C_1) ((minus_2758725tate_o A_13) B_5))))) of role axiom named fact_81_DiffI % A new axiom: (forall (B_5:(hoare_1262092251_state->Prop)) (C_1:hoare_1262092251_state) (A_13:(hoare_1262092251_state->Prop)), (((member5164104_state C_1) A_13)->((((member5164104_state C_1) B_5)->False)->((member5164104_state C_1) ((minus_2758725tate_o A_13) B_5))))) % FOF formula (forall (C:hoare_1262092251_state) (A_12:(hoare_1262092251_state->Prop)) (B_4:(hoare_1262092251_state->Prop)), (((member5164104_state C) ((minus_2758725tate_o A_12) B_4))->((((member5164104_state C) A_12)->((member5164104_state C) B_4))->False))) of role axiom named fact_82_DiffE % A new axiom: (forall (C:hoare_1262092251_state) (A_12:(hoare_1262092251_state->Prop)) (B_4:(hoare_1262092251_state->Prop)), (((member5164104_state C) ((minus_2758725tate_o A_12) B_4))->((((member5164104_state C) A_12)->((member5164104_state C) B_4))->False))) % FOF formula (forall (B_3:(hoare_1262092251_state->Prop)) (A_11:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_11)->(finite1178804552_state ((minus_2758725tate_o A_11) B_3)))) of role axiom named fact_83_finite__Diff % A new axiom: (forall (B_3:(hoare_1262092251_state->Prop)) (A_11:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_11)->(finite1178804552_state ((minus_2758725tate_o A_11) B_3)))) % FOF formula (forall (A_10:hoare_1262092251_state) (A_9:(hoare_1262092251_state->Prop)), (((member5164104_state A_10) A_9)->(((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_10) ((minus_2758725tate_o A_9) ((insert81609953_state A_10) bot_bo113204042tate_o)))) A_9))) of role axiom named fact_84_insert__Diff % A new axiom: (forall (A_10:hoare_1262092251_state) (A_9:(hoare_1262092251_state->Prop)), (((member5164104_state A_10) A_9)->(((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_10) ((minus_2758725tate_o A_9) ((insert81609953_state A_10) bot_bo113204042tate_o)))) A_9))) % FOF formula (forall (X:hoare_1262092251_state) (A_8:(hoare_1262092251_state->Prop)), ((((member5164104_state X) A_8)->False)->(((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o ((insert81609953_state X) A_8)) ((insert81609953_state X) bot_bo113204042tate_o))) A_8))) of role axiom named fact_85_Diff__insert__absorb % A new axiom: (forall (X:hoare_1262092251_state) (A_8:(hoare_1262092251_state->Prop)), ((((member5164104_state X) A_8)->False)->(((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o ((insert81609953_state X) A_8)) ((insert81609953_state X) bot_bo113204042tate_o))) A_8))) % FOF formula (forall (A_7:hoare_1262092251_state) (A_6:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_7) ((minus_2758725tate_o A_6) ((insert81609953_state A_7) bot_bo113204042tate_o)))) ((insert81609953_state A_7) A_6))) of role axiom named fact_86_insert__Diff__single % A new axiom: (forall (A_7:hoare_1262092251_state) (A_6:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_7) ((minus_2758725tate_o A_6) ((insert81609953_state A_7) bot_bo113204042tate_o)))) ((insert81609953_state A_7) A_6))) % FOF formula (forall (A_5:(hoare_1262092251_state->Prop)) (A_4:hoare_1262092251_state) (B_2:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_5) ((insert81609953_state A_4) B_2))) ((minus_2758725tate_o ((minus_2758725tate_o A_5) ((insert81609953_state A_4) bot_bo113204042tate_o))) B_2))) of role axiom named fact_87_Diff__insert2 % A new axiom: (forall (A_5:(hoare_1262092251_state->Prop)) (A_4:hoare_1262092251_state) (B_2:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_5) ((insert81609953_state A_4) B_2))) ((minus_2758725tate_o ((minus_2758725tate_o A_5) ((insert81609953_state A_4) bot_bo113204042tate_o))) B_2))) % FOF formula (forall (A_3:(hoare_1262092251_state->Prop)) (A_2:hoare_1262092251_state) (B_1:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_3) ((insert81609953_state A_2) B_1))) ((minus_2758725tate_o ((minus_2758725tate_o A_3) B_1)) ((insert81609953_state A_2) bot_bo113204042tate_o)))) of role axiom named fact_88_Diff__insert % A new axiom: (forall (A_3:(hoare_1262092251_state->Prop)) (A_2:hoare_1262092251_state) (B_1:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_3) ((insert81609953_state A_2) B_1))) ((minus_2758725tate_o ((minus_2758725tate_o A_3) B_1)) ((insert81609953_state A_2) bot_bo113204042tate_o)))) % FOF formula (forall (A_1:(hoare_1262092251_state->Prop)) (A:hoare_1262092251_state) (B:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state ((minus_2758725tate_o A_1) ((insert81609953_state A) B)))) (finite1178804552_state ((minus_2758725tate_o A_1) B)))) of role axiom named fact_89_finite__Diff__insert % A new axiom: (forall (A_1:(hoare_1262092251_state->Prop)) (A:hoare_1262092251_state) (B:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state ((minus_2758725tate_o A_1) ((insert81609953_state A) B)))) (finite1178804552_state ((minus_2758725tate_o A_1) B)))) % FOF formula ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) of role hypothesis named conj_0 % A new axiom: ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % FOF formula ((hoare_1337152501_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) of role hypothesis named conj_1 % A new axiom: ((hoare_1337152501_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % FOF formula ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) of role conjecture named conj_2 % Conjecture to prove = ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)):Prop % Parameter state_DUMMY:state. % Parameter hoare_1262092251_state_DUMMY:hoare_1262092251_state. % We need to prove ['((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o))'] % Parameter com:Type. % Parameter state:Type. % Parameter hoare_1262092251_state:Type. % Parameter big_se1697321605_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(((hoare_1262092251_state->Prop)->hoare_1262092251_state)->Prop)). % Parameter skip:com. % Parameter semi:(com->(com->com)). % Parameter _TPTP_ex:((hoare_1262092251_state->Prop)->Prop). % Parameter finite1178804552_state:((hoare_1262092251_state->Prop)->Prop). % Parameter finite403475723_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop))). % Parameter finite1740352635_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->((hoare_1262092251_state->Prop)->hoare_1262092251_state)). % Parameter finite975744042_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(hoare_1262092251_state->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop)))). % Parameter finite1168661790_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(((hoare_1262092251_state->Prop)->hoare_1262092251_state)->Prop)). % Parameter finite900773345_state:((hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))->(((hoare_1262092251_state->Prop)->hoare_1262092251_state)->Prop)). % Parameter minus_2758725tate_o:((hoare_1262092251_state->Prop)->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop))). % Parameter hoare_Mirabelle_MGT:(com->hoare_1262092251_state). % Parameter hoare_930741239_state:((hoare_1262092251_state->Prop)->((hoare_1262092251_state->Prop)->Prop)). % Parameter hoare_1337152501_state:((hoare_1262092251_state->Prop)->((hoare_1262092251_state->Prop)->Prop)). % Parameter hoare_951399329_state:((state->(state->Prop))->(com->((state->(state->Prop))->hoare_1262092251_state))). % Parameter bot_bo113204042tate_o:(hoare_1262092251_state->Prop). % Parameter bot_bot_o:Prop. % Parameter collec1121927558_state:((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop)). % Parameter insert81609953_state:(hoare_1262092251_state->((hoare_1262092251_state->Prop)->(hoare_1262092251_state->Prop))). % Parameter the_el417915516_state:((hoare_1262092251_state->Prop)->hoare_1262092251_state). % Parameter member5164104_state:(hoare_1262092251_state->((hoare_1262092251_state->Prop)->Prop)). % Parameter p:(state->(state->Prop)). % Parameter q:(state->(state->Prop)). % Parameter c:com. % Axiom fact_0_empty:(forall (G_12:(hoare_1262092251_state->Prop)), ((hoare_930741239_state G_12) bot_bo113204042tate_o)). % Axiom fact_1_triple_Oinject:(forall (Fun1_2:(state->(state->Prop))) (Com_2:com) (Fun2_2:(state->(state->Prop))) (Fun1_1:(state->(state->Prop))) (Com_1:com) (Fun2_1:(state->(state->Prop))), ((iff (((eq hoare_1262092251_state) (((hoare_951399329_state Fun1_2) Com_2) Fun2_2)) (((hoare_951399329_state Fun1_1) Com_1) Fun2_1))) ((and ((and (((eq (state->(state->Prop))) Fun1_2) Fun1_1)) (((eq com) Com_2) Com_1))) (((eq (state->(state->Prop))) Fun2_2) Fun2_1)))). % Axiom fact_2_hoare__sound:(forall (G_11:(hoare_1262092251_state->Prop)) (Ts_3:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_11) Ts_3)->((hoare_1337152501_state G_11) Ts_3))). % Axiom fact_3_cut:(forall (G_10:(hoare_1262092251_state->Prop)) (G_9:(hoare_1262092251_state->Prop)) (Ts_2:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_9) Ts_2)->(((hoare_930741239_state G_10) G_9)->((hoare_930741239_state G_10) Ts_2)))). % Axiom fact_4_hoare__derivs_Oinsert:(forall (Ts_1:(hoare_1262092251_state->Prop)) (G_8:(hoare_1262092251_state->Prop)) (T_1:hoare_1262092251_state), (((hoare_930741239_state G_8) ((insert81609953_state T_1) bot_bo113204042tate_o))->(((hoare_930741239_state G_8) Ts_1)->((hoare_930741239_state G_8) ((insert81609953_state T_1) Ts_1))))). % Axiom fact_5_derivs__insertD:(forall (G_7:(hoare_1262092251_state->Prop)) (T:hoare_1262092251_state) (Ts:(hoare_1262092251_state->Prop)), (((hoare_930741239_state G_7) ((insert81609953_state T) Ts))->((and ((hoare_930741239_state G_7) ((insert81609953_state T) bot_bo113204042tate_o))) ((hoare_930741239_state G_7) Ts)))). % Axiom fact_6_conseq2:(forall (Q_7:(state->(state->Prop))) (G_6:(hoare_1262092251_state->Prop)) (P_14:(state->(state->Prop))) (C_8:com) (Q_6:(state->(state->Prop))), (((hoare_930741239_state G_6) ((insert81609953_state (((hoare_951399329_state P_14) C_8) Q_6)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((Q_6 Z_5) S)->((Q_7 Z_5) S)))->((hoare_930741239_state G_6) ((insert81609953_state (((hoare_951399329_state P_14) C_8) Q_7)) bot_bo113204042tate_o))))). % Axiom fact_7_conseq1:(forall (P_13:(state->(state->Prop))) (G_5:(hoare_1262092251_state->Prop)) (P_12:(state->(state->Prop))) (C_7:com) (Q_5:(state->(state->Prop))), (((hoare_930741239_state G_5) ((insert81609953_state (((hoare_951399329_state P_12) C_7) Q_5)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((P_13 Z_5) S)->((P_12 Z_5) S)))->((hoare_930741239_state G_5) ((insert81609953_state (((hoare_951399329_state P_13) C_7) Q_5)) bot_bo113204042tate_o))))). % Axiom fact_8_insertE:(forall (A_71:hoare_1262092251_state) (B_20:hoare_1262092251_state) (A_70:(hoare_1262092251_state->Prop)), (((member5164104_state A_71) ((insert81609953_state B_20) A_70))->((not (((eq hoare_1262092251_state) A_71) B_20))->((member5164104_state A_71) A_70)))). % Axiom fact_9_insertCI:(forall (B_19:hoare_1262092251_state) (A_69:hoare_1262092251_state) (B_18:(hoare_1262092251_state->Prop)), (((((member5164104_state A_69) B_18)->False)->(((eq hoare_1262092251_state) A_69) B_19))->((member5164104_state A_69) ((insert81609953_state B_19) B_18)))). % Axiom fact_10_conseq12:(forall (Q_4:(state->(state->Prop))) (P_11:(state->(state->Prop))) (G_4:(hoare_1262092251_state->Prop)) (P_10:(state->(state->Prop))) (C_6:com) (Q_3:(state->(state->Prop))), (((hoare_930741239_state G_4) ((insert81609953_state (((hoare_951399329_state P_10) C_6) Q_3)) bot_bo113204042tate_o))->((forall (Z_5:state) (S:state), (((P_11 Z_5) S)->(forall (S_1:state), ((forall (Z_6:state), (((P_10 Z_6) S)->((Q_3 Z_6) S_1)))->((Q_4 Z_5) S_1)))))->((hoare_930741239_state G_4) ((insert81609953_state (((hoare_951399329_state P_11) C_6) Q_4)) bot_bo113204042tate_o))))). % Axiom fact_11_emptyE:(forall (A_68:hoare_1262092251_state), (((member5164104_state A_68) bot_bo113204042tate_o)->False)). % Axiom fact_12_empty__not__insert:(forall (A_67:hoare_1262092251_state) (A_66:(hoare_1262092251_state->Prop)), (not (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) ((insert81609953_state A_67) A_66)))). % Axiom fact_13_insert__not__empty:(forall (A_65:hoare_1262092251_state) (A_64:(hoare_1262092251_state->Prop)), (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_65) A_64)) bot_bo113204042tate_o))). % Axiom fact_14_singleton__iff:(forall (B_17:hoare_1262092251_state) (A_63:hoare_1262092251_state), ((iff ((member5164104_state B_17) ((insert81609953_state A_63) bot_bo113204042tate_o))) (((eq hoare_1262092251_state) B_17) A_63))). % Axiom fact_15_doubleton__eq__iff:(forall (A_62:hoare_1262092251_state) (B_16:hoare_1262092251_state) (C_5:hoare_1262092251_state) (D_1:hoare_1262092251_state), ((iff (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_62) ((insert81609953_state B_16) bot_bo113204042tate_o))) ((insert81609953_state C_5) ((insert81609953_state D_1) bot_bo113204042tate_o)))) ((or ((and (((eq hoare_1262092251_state) A_62) C_5)) (((eq hoare_1262092251_state) B_16) D_1))) ((and (((eq hoare_1262092251_state) A_62) D_1)) (((eq hoare_1262092251_state) B_16) C_5))))). % Axiom fact_16_equals0D:(forall (A_61:hoare_1262092251_state) (A_60:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) A_60) bot_bo113204042tate_o)->(((member5164104_state A_61) A_60)->False))). % Axiom fact_17_Collect__empty__eq:(forall (P_9:(hoare_1262092251_state->Prop)), ((iff (((eq (hoare_1262092251_state->Prop)) (collec1121927558_state P_9)) bot_bo113204042tate_o)) (forall (X_2:hoare_1262092251_state), ((P_9 X_2)->False)))). % Axiom fact_18_empty__iff:(forall (C_4:hoare_1262092251_state), (((member5164104_state C_4) bot_bo113204042tate_o)->False)). % Axiom fact_19_empty__Collect__eq:(forall (P_8:(hoare_1262092251_state->Prop)), ((iff (((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) (collec1121927558_state P_8))) (forall (X_2:hoare_1262092251_state), ((P_8 X_2)->False)))). % Axiom fact_20_ex__in__conv:(forall (A_59:(hoare_1262092251_state->Prop)), ((iff ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((member5164104_state X_2) A_59)))) (not (((eq (hoare_1262092251_state->Prop)) A_59) bot_bo113204042tate_o)))). % Axiom fact_21_all__not__in__conv:(forall (A_58:(hoare_1262092251_state->Prop)), ((iff (forall (X_2:hoare_1262092251_state), (((member5164104_state X_2) A_58)->False))) (((eq (hoare_1262092251_state->Prop)) A_58) bot_bo113204042tate_o))). % Axiom fact_22_empty__def:(((eq (hoare_1262092251_state->Prop)) bot_bo113204042tate_o) (collec1121927558_state (fun (X_2:hoare_1262092251_state)=> False))). % Axiom fact_23_insert__absorb:(forall (A_57:hoare_1262092251_state) (A_56:(hoare_1262092251_state->Prop)), (((member5164104_state A_57) A_56)->(((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_57) A_56)) A_56))). % Axiom fact_24_insertI2:(forall (B_15:hoare_1262092251_state) (A_55:hoare_1262092251_state) (B_14:(hoare_1262092251_state->Prop)), (((member5164104_state A_55) B_14)->((member5164104_state A_55) ((insert81609953_state B_15) B_14)))). % Axiom fact_25_insert__ident:(forall (B_13:(hoare_1262092251_state->Prop)) (X_22:hoare_1262092251_state) (A_54:(hoare_1262092251_state->Prop)), ((((member5164104_state X_22) A_54)->False)->((((member5164104_state X_22) B_13)->False)->((iff (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_22) A_54)) ((insert81609953_state X_22) B_13))) (((eq (hoare_1262092251_state->Prop)) A_54) B_13))))). % Axiom fact_26_insert__code:(forall (Y_4:hoare_1262092251_state) (A_53:(hoare_1262092251_state->Prop)) (X_21:hoare_1262092251_state), ((iff (((insert81609953_state Y_4) A_53) X_21)) ((or (((eq hoare_1262092251_state) Y_4) X_21)) (A_53 X_21)))). % Axiom fact_27_insert__iff:(forall (A_52:hoare_1262092251_state) (B_12:hoare_1262092251_state) (A_51:(hoare_1262092251_state->Prop)), ((iff ((member5164104_state A_52) ((insert81609953_state B_12) A_51))) ((or (((eq hoare_1262092251_state) A_52) B_12)) ((member5164104_state A_52) A_51)))). % Axiom fact_28_insert__commute:(forall (X_20:hoare_1262092251_state) (Y_3:hoare_1262092251_state) (A_50:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_20) ((insert81609953_state Y_3) A_50))) ((insert81609953_state Y_3) ((insert81609953_state X_20) A_50)))). % Axiom fact_29_insert__absorb2:(forall (X_19:hoare_1262092251_state) (A_49:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_19) ((insert81609953_state X_19) A_49))) ((insert81609953_state X_19) A_49))). % Axiom fact_30_insert__Collect:(forall (A_48:hoare_1262092251_state) (P_7:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_48) (collec1121927558_state P_7))) (collec1121927558_state (fun (U:hoare_1262092251_state)=> (((fun (X:Prop) (Y:Prop)=> (X->Y)) (not (((eq hoare_1262092251_state) U) A_48))) (P_7 U)))))). % Axiom fact_31_insert__compr:(forall (A_47:hoare_1262092251_state) (B_11:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_47) B_11)) (collec1121927558_state (fun (X_2:hoare_1262092251_state)=> ((or (((eq hoare_1262092251_state) X_2) A_47)) ((member5164104_state X_2) B_11)))))). % Axiom fact_32_insertI1:(forall (A_46:hoare_1262092251_state) (B_10:(hoare_1262092251_state->Prop)), ((member5164104_state A_46) ((insert81609953_state A_46) B_10))). % Axiom fact_33_singleton__inject:(forall (A_45:hoare_1262092251_state) (B_9:hoare_1262092251_state), ((((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_45) bot_bo113204042tate_o)) ((insert81609953_state B_9) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) A_45) B_9))). % Axiom fact_34_singletonE:(forall (B_8:hoare_1262092251_state) (A_44:hoare_1262092251_state), (((member5164104_state B_8) ((insert81609953_state A_44) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) B_8) A_44))). % Axiom fact_35_the__elem__eq:(forall (X_18:hoare_1262092251_state), (((eq hoare_1262092251_state) (the_el417915516_state ((insert81609953_state X_18) bot_bo113204042tate_o))) X_18)). % Axiom fact_36_bot__apply:(forall (X_17:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_17)) bot_bot_o)). % Axiom fact_37_bot__fun__def:(forall (X_2:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_2)) bot_bot_o)). % Axiom fact_38_hoare__derivs_OSkip:(forall (G_3:(hoare_1262092251_state->Prop)) (P_6:(state->(state->Prop))), ((hoare_930741239_state G_3) ((insert81609953_state (((hoare_951399329_state P_6) skip) P_6)) bot_bo113204042tate_o))). % Axiom fact_39_Comp:(forall (D:com) (R:(state->(state->Prop))) (G_2:(hoare_1262092251_state->Prop)) (P_5:(state->(state->Prop))) (C_3:com) (Q_2:(state->(state->Prop))), (((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state P_5) C_3) Q_2)) bot_bo113204042tate_o))->(((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state Q_2) D) R)) bot_bo113204042tate_o))->((hoare_930741239_state G_2) ((insert81609953_state (((hoare_951399329_state P_5) ((semi C_3) D)) R)) bot_bo113204042tate_o))))). % Axiom fact_40_triple_Oexhaust:(forall (Y_2:hoare_1262092251_state), ((forall (Fun1:(state->(state->Prop))) (Com:com) (Fun2:(state->(state->Prop))), (not (((eq hoare_1262092251_state) Y_2) (((hoare_951399329_state Fun1) Com) Fun2))))->False)). % Axiom fact_41_Set_Oset__insert:(forall (X_16:hoare_1262092251_state) (A_43:(hoare_1262092251_state->Prop)), (((member5164104_state X_16) A_43)->((forall (B_7:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) A_43) ((insert81609953_state X_16) B_7))->((member5164104_state X_16) B_7)))->False))). % Axiom fact_42_mk__disjoint__insert:(forall (A_42:hoare_1262092251_state) (A_41:(hoare_1262092251_state->Prop)), (((member5164104_state A_42) A_41)->((ex (hoare_1262092251_state->Prop)) (fun (B_7:(hoare_1262092251_state->Prop))=> ((and (((eq (hoare_1262092251_state->Prop)) A_41) ((insert81609953_state A_42) B_7))) (((member5164104_state A_42) B_7)->False)))))). % Axiom fact_43_com_Osimps_I13_J:(forall (Com1:com) (Com2:com), (not (((eq com) ((semi Com1) Com2)) skip))). % Axiom fact_44_com_Osimps_I12_J:(forall (Com1:com) (Com2:com), (not (((eq com) skip) ((semi Com1) Com2)))). % Axiom fact_45_equals0I:(forall (A_40:(hoare_1262092251_state->Prop)), ((forall (Y:hoare_1262092251_state), (((member5164104_state Y) A_40)->False))->(((eq (hoare_1262092251_state->Prop)) A_40) bot_bo113204042tate_o))). % Axiom fact_46_conseq:(forall (Q:(state->(state->Prop))) (G_1:(hoare_1262092251_state->Prop)) (C_2:com) (P_3:(state->(state->Prop))), ((forall (Z_5:state) (S:state), (((P_3 Z_5) S)->((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state G_1) ((insert81609953_state (((hoare_951399329_state P_4) C_2) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((Q Z_5) S_1))))))))))->((hoare_930741239_state G_1) ((insert81609953_state (((hoare_951399329_state P_3) C_2) Q)) bot_bo113204042tate_o)))). % Axiom fact_47_com_Osimps_I3_J:(forall (Com1_1:com) (Com2_1:com) (Com1:com) (Com2:com), ((iff (((eq com) ((semi Com1_1) Com2_1)) ((semi Com1) Com2))) ((and (((eq com) Com1_1) Com1)) (((eq com) Com2_1) Com2)))). % Axiom fact_48_nonempty__iff:(forall (A_39:(hoare_1262092251_state->Prop)), ((iff (not (((eq (hoare_1262092251_state->Prop)) A_39) bot_bo113204042tate_o))) ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (B_7:(hoare_1262092251_state->Prop))=> ((and (((eq (hoare_1262092251_state->Prop)) A_39) ((insert81609953_state X_2) B_7))) (((member5164104_state X_2) B_7)->False)))))))). % Axiom fact_49_bot__empty__eq:(forall (X_2:hoare_1262092251_state), ((iff (bot_bo113204042tate_o X_2)) ((member5164104_state X_2) bot_bo113204042tate_o))). % Axiom fact_50_fold1Set__sing:(forall (F_34:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_38:hoare_1262092251_state) (B_6:hoare_1262092251_state), ((iff (((finite403475723_state F_34) ((insert81609953_state A_38) bot_bo113204042tate_o)) B_6)) (((eq hoare_1262092251_state) A_38) B_6))). % Axiom fact_51_folding__one_Osingleton:(forall (X_15:hoare_1262092251_state) (F_33:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_32:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_33) F_32)->(((eq hoare_1262092251_state) (F_32 ((insert81609953_state X_15) bot_bo113204042tate_o))) X_15))). % Axiom fact_52_fold1__singleton:(forall (F_31:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_37:hoare_1262092251_state), (((eq hoare_1262092251_state) ((finite1740352635_state F_31) ((insert81609953_state A_37) bot_bo113204042tate_o))) A_37)). % Axiom fact_53_fold1__singleton__def:(forall (A_36:hoare_1262092251_state) (G:((hoare_1262092251_state->Prop)->hoare_1262092251_state)) (F_30:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))), ((((eq ((hoare_1262092251_state->Prop)->hoare_1262092251_state)) G) (finite1740352635_state F_30))->(((eq hoare_1262092251_state) (G ((insert81609953_state A_36) bot_bo113204042tate_o))) A_36))). % Axiom fact_54_empty__fold1SetE:(forall (F_29:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (X_14:hoare_1262092251_state), ((((finite403475723_state F_29) bot_bo113204042tate_o) X_14)->False)). % Axiom fact_55_fold1Set__nonempty:(forall (F_28:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_35:(hoare_1262092251_state->Prop)) (X_13:hoare_1262092251_state), ((((finite403475723_state F_28) A_35) X_13)->(not (((eq (hoare_1262092251_state->Prop)) A_35) bot_bo113204042tate_o)))). % Axiom fact_56_fold1Set_Ointros:(forall (F_27:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_34:hoare_1262092251_state) (A_33:(hoare_1262092251_state->Prop)) (X_12:hoare_1262092251_state), (((((finite975744042_state F_27) A_34) A_33) X_12)->((((member5164104_state A_34) A_33)->False)->(((finite403475723_state F_27) ((insert81609953_state A_34) A_33)) X_12)))). % Axiom fact_57_folding__one_Oinsert:(forall (X_11:hoare_1262092251_state) (A_32:(hoare_1262092251_state->Prop)) (F_26:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_25:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_26) F_25)->((finite1178804552_state A_32)->((((member5164104_state X_11) A_32)->False)->((not (((eq (hoare_1262092251_state->Prop)) A_32) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F_25 ((insert81609953_state X_11) A_32))) ((F_26 X_11) (F_25 A_32)))))))). % Axiom fact_58_folding__one_Oeq__fold:(forall (A_31:(hoare_1262092251_state->Prop)) (F_24:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_23:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_24) F_23)->((finite1178804552_state A_31)->(((eq hoare_1262092251_state) (F_23 A_31)) ((finite1740352635_state F_24) A_31))))). % Axiom fact_59_finite_OemptyI:(finite1178804552_state bot_bo113204042tate_o). % Axiom fact_60_finite_OinsertI:(forall (A_30:hoare_1262092251_state) (A_29:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_29)->(finite1178804552_state ((insert81609953_state A_30) A_29)))). % Axiom fact_61_fold__graph_OemptyI:(forall (F_22:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_4:hoare_1262092251_state), ((((finite975744042_state F_22) Z_4) bot_bo113204042tate_o) Z_4)). % Axiom fact_62_empty__fold__graphE:(forall (F_21:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_3:hoare_1262092251_state) (X_10:hoare_1262092251_state), (((((finite975744042_state F_21) Z_3) bot_bo113204042tate_o) X_10)->(((eq hoare_1262092251_state) X_10) Z_3))). % Axiom fact_63_fold__graph_OinsertI:(forall (F_20:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_2:hoare_1262092251_state) (Y_1:hoare_1262092251_state) (X_9:hoare_1262092251_state) (A_28:(hoare_1262092251_state->Prop)), ((((member5164104_state X_9) A_28)->False)->(((((finite975744042_state F_20) Z_2) A_28) Y_1)->((((finite975744042_state F_20) Z_2) ((insert81609953_state X_9) A_28)) ((F_20 X_9) Y_1))))). % Axiom fact_64_finite__insert:(forall (A_27:hoare_1262092251_state) (A_26:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state ((insert81609953_state A_27) A_26))) (finite1178804552_state A_26))). % Axiom fact_65_folding__one_Oclosed:(forall (A_25:(hoare_1262092251_state->Prop)) (F_19:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_18:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_19) F_18)->((finite1178804552_state A_25)->((not (((eq (hoare_1262092251_state->Prop)) A_25) bot_bo113204042tate_o))->((forall (X_2:hoare_1262092251_state) (Y:hoare_1262092251_state), ((member5164104_state ((F_19 X_2) Y)) ((insert81609953_state X_2) ((insert81609953_state Y) bot_bo113204042tate_o))))->((member5164104_state (F_18 A_25)) A_25)))))). % Axiom fact_66_insert__fold1SetE:(forall (F_17:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_24:hoare_1262092251_state) (X_8:(hoare_1262092251_state->Prop)) (X_7:hoare_1262092251_state), ((((finite403475723_state F_17) ((insert81609953_state A_24) X_8)) X_7)->((forall (A_19:hoare_1262092251_state) (A_18:(hoare_1262092251_state->Prop)), ((((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_24) X_8)) ((insert81609953_state A_19) A_18))->(((((finite975744042_state F_17) A_19) A_18) X_7)->((member5164104_state A_19) A_18))))->False))). % Axiom fact_67_finite__nonempty__imp__fold1Set:(forall (F_16:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A_23:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_23)->((not (((eq (hoare_1262092251_state->Prop)) A_23) bot_bo113204042tate_o))->(_TPTP_ex ((finite403475723_state F_16) A_23))))). % Axiom fact_68_finite__induct:(forall (P_2:((hoare_1262092251_state->Prop)->Prop)) (F_15:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_15)->((P_2 bot_bo113204042tate_o)->((forall (X_2:hoare_1262092251_state) (F_5:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_5)->((((member5164104_state X_2) F_5)->False)->((P_2 F_5)->(P_2 ((insert81609953_state X_2) F_5))))))->(P_2 F_15))))). % Axiom fact_69_mem__def:(forall (X_6:hoare_1262092251_state) (A_22:(hoare_1262092251_state->Prop)), ((iff ((member5164104_state X_6) A_22)) (A_22 X_6))). % Axiom fact_70_Collect__def:(forall (P_1:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) (collec1121927558_state P_1)) P_1)). % Axiom fact_71_finite_Osimps:(forall (A_21:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state A_21)) ((or (((eq (hoare_1262092251_state->Prop)) A_21) bot_bo113204042tate_o)) ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (A_19:hoare_1262092251_state)=> ((and (((eq (hoare_1262092251_state->Prop)) A_21) ((insert81609953_state A_19) A_18))) (finite1178804552_state A_18))))))))). % Axiom fact_72_finite__imp__fold__graph:(forall (F_14:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z_1:hoare_1262092251_state) (A_20:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_20)->(_TPTP_ex (((finite975744042_state F_14) Z_1) A_20)))). % Axiom fact_73_fold1Set_Osimps:(forall (F_13:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (A1_1:(hoare_1262092251_state->Prop)) (A2_1:hoare_1262092251_state), ((iff (((finite403475723_state F_13) A1_1) A2_1)) ((ex hoare_1262092251_state) (fun (A_19:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((and ((and ((and (((eq (hoare_1262092251_state->Prop)) A1_1) ((insert81609953_state A_19) A_18))) (((eq hoare_1262092251_state) A2_1) X_2))) ((((finite975744042_state F_13) A_19) A_18) X_2))) (((member5164104_state A_19) A_18)->False)))))))))). % Axiom fact_74_fold__graph_Osimps:(forall (F_12:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (Z:hoare_1262092251_state) (A1:(hoare_1262092251_state->Prop)) (A2:hoare_1262092251_state), ((iff ((((finite975744042_state F_12) Z) A1) A2)) ((or ((and (((eq (hoare_1262092251_state->Prop)) A1) bot_bo113204042tate_o)) (((eq hoare_1262092251_state) A2) Z))) ((ex hoare_1262092251_state) (fun (X_2:hoare_1262092251_state)=> ((ex (hoare_1262092251_state->Prop)) (fun (A_18:(hoare_1262092251_state->Prop))=> ((ex hoare_1262092251_state) (fun (Y:hoare_1262092251_state)=> ((and ((and ((and (((eq (hoare_1262092251_state->Prop)) A1) ((insert81609953_state X_2) A_18))) (((eq hoare_1262092251_state) A2) ((F_12 X_2) Y)))) (((member5164104_state X_2) A_18)->False))) ((((finite975744042_state F_12) Z) A_18) Y))))))))))). % Axiom fact_75_folding__one__idem_Oinsert__idem:(forall (X_5:hoare_1262092251_state) (A_17:(hoare_1262092251_state->Prop)) (F_11:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_10:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_11) F_10)->((finite1178804552_state A_17)->((not (((eq (hoare_1262092251_state->Prop)) A_17) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F_10 ((insert81609953_state X_5) A_17))) ((F_11 X_5) (F_10 A_17))))))). % Axiom fact_76_folding__one__idem_Oidem:(forall (X_4:hoare_1262092251_state) (F_9:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_8:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_9) F_8)->(((eq hoare_1262092251_state) ((F_9 X_4) X_4)) X_4))). % Axiom fact_77_folding__one__idem_Oin__idem:(forall (X_3:hoare_1262092251_state) (A_16:(hoare_1262092251_state->Prop)) (F_7:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_6:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite900773345_state F_7) F_6)->((finite1178804552_state A_16)->(((member5164104_state X_3) A_16)->(((eq hoare_1262092251_state) ((F_7 X_3) (F_6 A_16))) (F_6 A_16)))))). % Axiom fact_78_finite__ne__induct:(forall (P:((hoare_1262092251_state->Prop)->Prop)) (F_4:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_4)->((not (((eq (hoare_1262092251_state->Prop)) F_4) bot_bo113204042tate_o))->((forall (X_2:hoare_1262092251_state), (P ((insert81609953_state X_2) bot_bo113204042tate_o)))->((forall (X_2:hoare_1262092251_state) (F_5:(hoare_1262092251_state->Prop)), ((finite1178804552_state F_5)->((not (((eq (hoare_1262092251_state->Prop)) F_5) bot_bo113204042tate_o))->((((member5164104_state X_2) F_5)->False)->((P F_5)->(P ((insert81609953_state X_2) F_5)))))))->(P F_4)))))). % Axiom fact_79_semilattice__big_OF__eq:(forall (A_15:(hoare_1262092251_state->Prop)) (F_3:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F_2:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((big_se1697321605_state F_3) F_2)->((finite1178804552_state A_15)->(((eq hoare_1262092251_state) (F_2 A_15)) ((finite1740352635_state F_3) A_15))))). % Axiom fact_80_folding__one_Oremove:(forall (X_1:hoare_1262092251_state) (A_14:(hoare_1262092251_state->Prop)) (F_1:(hoare_1262092251_state->(hoare_1262092251_state->hoare_1262092251_state))) (F:((hoare_1262092251_state->Prop)->hoare_1262092251_state)), (((finite1168661790_state F_1) F)->((finite1178804552_state A_14)->(((member5164104_state X_1) A_14)->((and ((((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))) bot_bo113204042tate_o)->(((eq hoare_1262092251_state) (F A_14)) X_1))) ((not (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))) bot_bo113204042tate_o))->(((eq hoare_1262092251_state) (F A_14)) ((F_1 X_1) (F ((minus_2758725tate_o A_14) ((insert81609953_state X_1) bot_bo113204042tate_o))))))))))). % Axiom fact_81_DiffI:(forall (B_5:(hoare_1262092251_state->Prop)) (C_1:hoare_1262092251_state) (A_13:(hoare_1262092251_state->Prop)), (((member5164104_state C_1) A_13)->((((member5164104_state C_1) B_5)->False)->((member5164104_state C_1) ((minus_2758725tate_o A_13) B_5))))). % Axiom fact_82_DiffE:(forall (C:hoare_1262092251_state) (A_12:(hoare_1262092251_state->Prop)) (B_4:(hoare_1262092251_state->Prop)), (((member5164104_state C) ((minus_2758725tate_o A_12) B_4))->((((member5164104_state C) A_12)->((member5164104_state C) B_4))->False))). % Axiom fact_83_finite__Diff:(forall (B_3:(hoare_1262092251_state->Prop)) (A_11:(hoare_1262092251_state->Prop)), ((finite1178804552_state A_11)->(finite1178804552_state ((minus_2758725tate_o A_11) B_3)))). % Axiom fact_84_insert__Diff:(forall (A_10:hoare_1262092251_state) (A_9:(hoare_1262092251_state->Prop)), (((member5164104_state A_10) A_9)->(((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_10) ((minus_2758725tate_o A_9) ((insert81609953_state A_10) bot_bo113204042tate_o)))) A_9))). % Axiom fact_85_Diff__insert__absorb:(forall (X:hoare_1262092251_state) (A_8:(hoare_1262092251_state->Prop)), ((((member5164104_state X) A_8)->False)->(((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o ((insert81609953_state X) A_8)) ((insert81609953_state X) bot_bo113204042tate_o))) A_8))). % Axiom fact_86_insert__Diff__single:(forall (A_7:hoare_1262092251_state) (A_6:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state A_7) ((minus_2758725tate_o A_6) ((insert81609953_state A_7) bot_bo113204042tate_o)))) ((insert81609953_state A_7) A_6))). % Axiom fact_87_Diff__insert2:(forall (A_5:(hoare_1262092251_state->Prop)) (A_4:hoare_1262092251_state) (B_2:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_5) ((insert81609953_state A_4) B_2))) ((minus_2758725tate_o ((minus_2758725tate_o A_5) ((insert81609953_state A_4) bot_bo113204042tate_o))) B_2))). % Axiom fact_88_Diff__insert:(forall (A_3:(hoare_1262092251_state->Prop)) (A_2:hoare_1262092251_state) (B_1:(hoare_1262092251_state->Prop)), (((eq (hoare_1262092251_state->Prop)) ((minus_2758725tate_o A_3) ((insert81609953_state A_2) B_1))) ((minus_2758725tate_o ((minus_2758725tate_o A_3) B_1)) ((insert81609953_state A_2) bot_bo113204042tate_o)))). % Axiom fact_89_finite__Diff__insert:(forall (A_1:(hoare_1262092251_state->Prop)) (A:hoare_1262092251_state) (B:(hoare_1262092251_state->Prop)), ((iff (finite1178804552_state ((minus_2758725tate_o A_1) ((insert81609953_state A) B)))) (finite1178804552_state ((minus_2758725tate_o A_1) B)))). % Axiom conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)). % Axiom conj_1:((hoare_1337152501_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)). % Trying to prove ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found x:((Q_6 Z_5) S) % Found x as proof of ((q Z_5) S) % Found (fun (x:((Q_6 Z_5) S))=> x) as proof of ((q Z_5) S) % Found (fun (S:state) (x:((Q_6 Z_5) S))=> x) as proof of (((Q_6 Z_5) S)->((q Z_5) S)) % Found (fun (Z_5:state) (S:state) (x:((Q_6 Z_5) S))=> x) as proof of (forall (S:state), (((Q_6 Z_5) S)->((q Z_5) S))) % Found (fun (Z_5:state) (S:state) (x:((Q_6 Z_5) S))=> x) as proof of (forall (Z_5:state) (S:state), (((Q_6 Z_5) S)->((q Z_5) S))) % Found x:((p Z_5) S) % Instantiate: P_12:=p:(state->(state->Prop)) % Found (fun (x:((p Z_5) S))=> x) as proof of ((P_12 Z_5) S) % Found (fun (S:state) (x:((p Z_5) S))=> x) as proof of (((p Z_5) S)->((P_12 Z_5) S)) % Found (fun (Z_5:state) (S:state) (x:((p Z_5) S))=> x) as proof of (forall (S:state), (((p Z_5) S)->((P_12 Z_5) S))) % Found (fun (Z_5:state) (S:state) (x:((p Z_5) S))=> x) as proof of (forall (Z_5:state) (S:state), (((p Z_5) S)->((P_12 Z_5) S))) % Found fact_0_empty0:=(fact_0_empty bot_bo113204042tate_o):((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found x:((P_12 Z_5) S) % Found x as proof of ((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_4) c) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((q Z_5) S_1)))))))) % Found (fun (x:((P_12 Z_5) S))=> x) as proof of ((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_4) c) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((q Z_5) S_1)))))))) % Found (fun (S:state) (x:((P_12 Z_5) S))=> x) as proof of (((P_12 Z_5) S)->((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_4) c) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((q Z_5) S_1))))))))) % Found (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x) as proof of (forall (S:state), (((P_12 Z_5) S)->((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_4) c) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((q Z_5) S_1)))))))))) % Found (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x) as proof of (forall (Z_5:state) (S:state), (((P_12 Z_5) S)->((ex (state->(state->Prop))) (fun (P_4:(state->(state->Prop)))=> ((ex (state->(state->Prop))) (fun (Q_1:(state->(state->Prop)))=> ((and ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_4) c) Q_1)) bot_bo113204042tate_o))) (forall (S_1:state), ((forall (Z_6:state), (((P_4 Z_6) S)->((Q_1 Z_6) S_1)))->((q Z_5) S_1)))))))))) % Found (fact_46_conseq0000 (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x)) as proof of ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_12) c) q)) bot_bo113204042tate_o)) % Found ((fact_46_conseq000 P_12) (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x)) as proof of ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_12) c) q)) bot_bo113204042tate_o)) % Found (((fact_46_conseq00 c) P_12) (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x)) as proof of ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_12) c) q)) bot_bo113204042tate_o)) % Found ((((fact_46_conseq0 bot_bo113204042tate_o) c) P_12) (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x)) as proof of ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_12) c) q)) bot_bo113204042tate_o)) % Found (((((fact_46_conseq q) bot_bo113204042tate_o) c) P_12) (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x)) as proof of ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_12) c) q)) bot_bo113204042tate_o)) % Found (((((fact_46_conseq q) bot_bo113204042tate_o) c) P_12) (fun (Z_5:state) (S:state) (x:((P_12 Z_5) S))=> x)) as proof of ((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (((hoare_951399329_state P_12) c) q)) bot_bo113204042tate_o)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_60_finite_OinsertI000:=(fact_60_finite_OinsertI00 fact_59_finite_OemptyI):(finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found (fact_60_finite_OinsertI00 fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found ((fact_60_finite_OinsertI0 bot_bo113204042tate_o) fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found (((fact_60_finite_OinsertI (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o) fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found (((fact_60_finite_OinsertI (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o) fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found x1:((hoare_930741239_state bot_bo113204042tate_o) F_5) % Found x1 as proof of ((hoare_930741239_state bot_bo113204042tate_o) F_5) % Found x1:((hoare_930741239_state bot_bo113204042tate_o) F_5) % Instantiate: G_9:=F_5:(hoare_1262092251_state->Prop) % Found x1 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_13_insert__not__empty00:=(fact_13_insert__not__empty0 F_5):(not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) F_5)) bot_bo113204042tate_o)) % Found (fact_13_insert__not__empty0 F_5) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) F_5)) bot_bo113204042tate_o)) % Found ((fact_13_insert__not__empty X_2) F_5) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) F_5)) bot_bo113204042tate_o)) % Found ((fact_13_insert__not__empty X_2) F_5) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) F_5)) bot_bo113204042tate_o)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_0_empty0:=(fact_0_empty bot_bo113204042tate_o):((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_0_empty0:=(fact_0_empty bot_bo113204042tate_o):((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_90:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_90) % Found fact_0_empty0:=(fact_0_empty G_9):((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found fact_0_empty0:=(fact_0_empty G_9):((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found fact_0_empty0:=(fact_0_empty bot_bo113204042tate_o):((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found x:((Q_60 Z_5) S) % Found x as proof of ((q Z_5) S) % Found (fun (x:((Q_60 Z_5) S))=> x) as proof of ((q Z_5) S) % Found (fun (S:state) (x:((Q_60 Z_5) S))=> x) as proof of (((Q_60 Z_5) S)->((q Z_5) S)) % Found (fun (Z_5:state) (S:state) (x:((Q_60 Z_5) S))=> x) as proof of (forall (S:state), (((Q_60 Z_5) S)->((q Z_5) S))) % Found (fun (Z_5:state) (S:state) (x:((Q_60 Z_5) S))=> x) as proof of (forall (Z_5:state) (S:state), (((Q_60 Z_5) S)->((q Z_5) S))) % Found fact_0_empty0:=(fact_0_empty bot_bo113204042tate_o):((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_0_empty0:=(fact_0_empty bot_bo113204042tate_o):((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found (fact_0_empty bot_bo113204042tate_o) as proof of ((hoare_930741239_state bot_bo113204042tate_o) bot_bo113204042tate_o) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_13_insert__not__empty00:=(fact_13_insert__not__empty0 bot_bo113204042tate_o):(not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) bot_bo113204042tate_o)) % Found (fact_13_insert__not__empty0 bot_bo113204042tate_o) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) bot_bo113204042tate_o)) % Found ((fact_13_insert__not__empty (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) bot_bo113204042tate_o)) % Found ((fact_13_insert__not__empty (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) bot_bo113204042tate_o)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_90:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop);G_9:=bot_bo113204042tate_o:(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state G_9) G_90) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found x:((p Z_5) S) % Instantiate: P_120:=p:(state->(state->Prop)) % Found (fun (x:((p Z_5) S))=> x) as proof of ((P_120 Z_5) S) % Found (fun (S:state) (x:((p Z_5) S))=> x) as proof of (((p Z_5) S)->((P_120 Z_5) S)) % Found (fun (Z_5:state) (S:state) (x:((p Z_5) S))=> x) as proof of (forall (S:state), (((p Z_5) S)->((P_120 Z_5) S))) % Found (fun (Z_5:state) (S:state) (x:((p Z_5) S))=> x) as proof of (forall (Z_5:state) (S:state), (((p Z_5) S)->((P_120 Z_5) S))) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_32_insertI100:=(fact_32_insertI10 bot_bo113204042tate_o):((member5164104_state A_10) ((insert81609953_state A_10) bot_bo113204042tate_o)) % Found (fact_32_insertI10 bot_bo113204042tate_o) as proof of ((member5164104_state A_10) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found ((fact_32_insertI1 A_10) bot_bo113204042tate_o) as proof of ((member5164104_state A_10) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found ((fact_32_insertI1 A_10) bot_bo113204042tate_o) as proof of ((member5164104_state A_10) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found ((fact_32_insertI1 A_10) bot_bo113204042tate_o) as proof of ((member5164104_state A_10) ((insert81609953_state (((hoare_951399329_state p) c) q)) bot_bo113204042tate_o)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_0_empty0:=(fact_0_empty G_9):((hoare_930741239_state G_9) bot_bo113204042tate_o) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) G_90) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) G_90) % Found (fact_0_empty G_9) as proof of ((hoare_930741239_state G_9) G_90) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found x1:((hoare_930741239_state bot_bo113204042tate_o) F_5) % Instantiate: G_9:=bot_bo113204042tate_o:(hoare_1262092251_state->Prop) % Found x1 as proof of ((hoare_930741239_state G_9) F_5) % Found fact_60_finite_OinsertI000:=(fact_60_finite_OinsertI00 x):(finite1178804552_state ((insert81609953_state X_2) F_5)) % Found (fact_60_finite_OinsertI00 x) as proof of (finite1178804552_state ((insert81609953_state X_2) F_5)) % Found ((fact_60_finite_OinsertI0 F_5) x) as proof of (finite1178804552_state ((insert81609953_state X_2) F_5)) % Found (((fact_60_finite_OinsertI X_2) F_5) x) as proof of (finite1178804552_state ((insert81609953_state X_2) F_5)) % Found (((fact_60_finite_OinsertI X_2) F_5) x) as proof of (finite1178804552_state ((insert81609953_state X_2) F_5)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_13_insert__not__empty00:=(fact_13_insert__not__empty0 ((insert81609953_state X_2) F_5)):(not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) ((insert81609953_state X_2) F_5))) bot_bo113204042tate_o)) % Found (fact_13_insert__not__empty0 ((insert81609953_state X_2) F_5)) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) ((insert81609953_state X_2) F_5))) bot_bo113204042tate_o)) % Found ((fact_13_insert__not__empty X_2) ((insert81609953_state X_2) F_5)) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) ((insert81609953_state X_2) F_5))) bot_bo113204042tate_o)) % Found ((fact_13_insert__not__empty X_2) ((insert81609953_state X_2) F_5)) as proof of (not (((eq (hoare_1262092251_state->Prop)) ((insert81609953_state X_2) ((insert81609953_state X_2) F_5))) bot_bo113204042tate_o)) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_0_empty0:=(fact_0_empty F_5):((hoare_930741239_state F_5) bot_bo113204042tate_o) % Found (fact_0_empty F_5) as proof of ((hoare_930741239_state F_5) G_9) % Found (fact_0_empty F_5) as proof of ((hoare_930741239_state F_5) G_9) % Found (fact_0_empty F_5) as proof of ((hoare_930741239_state F_5) G_9) % Found conj_0:((hoare_930741239_state bot_bo113204042tate_o) ((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o)) % Instantiate: G_9:=((insert81609953_state (hoare_Mirabelle_MGT c)) bot_bo113204042tate_o):(hoare_1262092251_state->Prop) % Found conj_0 as proof of ((hoare_930741239_state bot_bo113204042tate_o) G_9) % Found fact_60_finite_OinsertI000:=(fact_60_finite_OinsertI00 fact_59_finite_OemptyI):(finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o)) % Found (fact_60_finite_OinsertI00 fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o)) % Found ((fact_60_finite_OinsertI0 bot_bo113204042tate_o) fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o)) % Found (((fact_60_finite_OinsertI (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o) fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o)) % Found (((fact_60_finite_OinsertI (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o) fact_59_finite_OemptyI) as proof of (finite1178804552_state ((insert81609953_state (((hoare_951399329_state p) c) Q_6)) bot_bo113204042tate_o)) % Found x1:((hoare_930741239_state bot_bo113204042tate_o) F_5) % Found x1 as proof of ((hoare_930741239_state bot_bo113204042tate_o) F_5) % Found conj_0:((hoare_9 % EOF %------------------------------------------------------------------------------