%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : ITP001^1 : TPTP v7.5.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % DateTime : Sun Mar 21 13:23:27 EDT 2021 % Result : Theorem 0.78s % Output : Proof 0.78s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : ITP001^1 : TPTP v7.5.0. Bugfixed v7.5.0. % 0.04/0.13 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % DateTime : Thu Mar 18 19:03:15 EDT 2021 % 0.13/0.34 % CPUTime : % 0.20/0.35 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.20/0.35 Python 2.7.5 % 0.46/0.83 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7af80>, <kernel.Type object at 0xf7a290>) of role type named u % 0.46/0.83 Using role type % 0.46/0.83 Declaring u:Type % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7b2d8>, <kernel.Type object at 0xf7a320>) of role type named d % 0.46/0.83 Using role type % 0.46/0.83 Declaring d:Type % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a9e0>, <kernel.Type object at 0xf7aa70>) of role type named du % 0.46/0.83 Using role type % 0.46/0.83 Declaring du:Type % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a290>, <kernel.Constant object at 0xf7ad40>) of role type named tyop_2Emin_2Ebool % 0.46/0.83 Using role type % 0.46/0.83 Declaring tyop_2Emin_2Ebool:d % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a1b8>, <kernel.DependentProduct object at 0xf7a320>) of role type named tyop_2Emin_2Efun % 0.46/0.83 Using role type % 0.46/0.83 Declaring tyop_2Emin_2Efun:(d->(d->d)) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a050>, <kernel.DependentProduct object at 0xf7a290>) of role type named s % 0.46/0.83 Using role type % 0.46/0.83 Declaring s:(d->(u->du)) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a170>, <kernel.DependentProduct object at 0xf7a1b8>) of role type named app_2E2 % 0.46/0.83 Using role type % 0.46/0.83 Declaring app_2E2:(du->(du->u)) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a9e0>, <kernel.Constant object at 0xf7a1b8>) of role type named combin_i_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring combin_i_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a050>, <kernel.Constant object at 0xf7a170>) of role type named combin_k_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring combin_k_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a9e0>, <kernel.Constant object at 0xf75ab8>) of role type named combin_s_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring combin_s_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a170>, <kernel.Constant object at 0xf754d0>) of role type named c_2Ebool_2E_21_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_21_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a9e0>, <kernel.DependentProduct object at 0xf75098>) of role type named c_2Ebool_2E_21_2E1 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_21_2E1:(du->u) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a1b8>, <kernel.Constant object at 0xf75098>) of role type named c_2Ebool_2E_2F_5C_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_2F_5C_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf7a1b8>, <kernel.DependentProduct object at 0xf75b48>) of role type named c_2Ebool_2E_2F_5C_2E2 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_2F_5C_2E2:(du->(du->u)) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75b00>, <kernel.Constant object at 0xf75b48>) of role type named c_2Emin_2E_3D_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Emin_2E_3D_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75518>, <kernel.DependentProduct object at 0xf75098>) of role type named c_2Emin_2E_3D_2E2 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Emin_2E_3D_2E2:(du->(du->u)) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.Constant object at 0xf75098>) of role type named c_2Emin_2E_3D_3D_3E_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Emin_2E_3D_3D_3E_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75b00>, <kernel.DependentProduct object at 0xf75b48>) of role type named c_2Emin_2E_3D_3D_3E_2E2 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Emin_2E_3D_3D_3E_2E2:(du->(du->u)) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75f38>, <kernel.Constant object at 0xf75b48>) of role type named c_2Ebool_2E_3F_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_3F_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.DependentProduct object at 0xf75518>) of role type named c_2Ebool_2E_3F_2E1 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_3F_2E1:(du->u) % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf753f8>, <kernel.Constant object at 0xf75518>) of role type named c_2Ebool_2EF_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2EF_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75f38>, <kernel.Constant object at 0xf75518>) of role type named c_2Ebool_2ET_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2ET_2E0:u % 0.46/0.83 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.Constant object at 0xf75518>) of role type named c_2Ebool_2E_5C_2F_2E0 % 0.46/0.83 Using role type % 0.46/0.83 Declaring c_2Ebool_2E_5C_2F_2E0:u % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf753f8>, <kernel.DependentProduct object at 0xf75098>) of role type named c_2Ebool_2E_5C_2F_2E2 % 0.46/0.84 Using role type % 0.46/0.84 Declaring c_2Ebool_2E_5C_2F_2E2:(du->(du->u)) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75dd0>, <kernel.Constant object at 0xf75098>) of role type named c_2Ebool_2E_7E_2E0 % 0.46/0.84 Using role type % 0.46/0.84 Declaring c_2Ebool_2E_7E_2E0:u % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.DependentProduct object at 0xf75f38>) of role type named c_2Ebool_2E_7E_2E1 % 0.46/0.84 Using role type % 0.46/0.84 Declaring c_2Ebool_2E_7E_2E1:(du->u) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75878>, <kernel.DependentProduct object at 0xf75518>) of role type named mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool:((Prop->Prop)->(Prop->Prop)) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75dd0>, <kernel.DependentProduct object at 0xf753f8>) of role type named mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:((Prop->(Prop->Prop))->(Prop->(Prop->Prop))) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.DependentProduct object at 0xf75d40>) of role type named mono_2Ec_2Ebool_2E_2F_5C % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Ec_2Ebool_2E_2F_5C:(Prop->(Prop->Prop)) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75878>, <kernel.DependentProduct object at 0xf75488>) of role type named mono_2Ec_2Emin_2E_3D_3D_3E % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Ec_2Emin_2E_3D_3D_3E:(Prop->(Prop->Prop)) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75dd0>, <kernel.Sort object at 0x2af8fb0be638>) of role type named mono_2Ec_2Ebool_2EF % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Ec_2Ebool_2EF:Prop % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75e60>, <kernel.Sort object at 0x2af8fb0be638>) of role type named mono_2Ec_2Ebool_2ET % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Ec_2Ebool_2ET:Prop % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.DependentProduct object at 0xf75710>) of role type named mono_2Ec_2Ebool_2E_5C_2F % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Ec_2Ebool_2E_5C_2F:(Prop->(Prop->Prop)) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75440>, <kernel.DependentProduct object at 0xf75bd8>) of role type named mono_2Ec_2Ebool_2E_7E % 0.46/0.84 Using role type % 0.46/0.84 Declaring mono_2Ec_2Ebool_2E_7E:(Prop->Prop) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75e60>, <kernel.DependentProduct object at 0xf75fc8>) of role type named i_mono_2Etyop_2Emin_2Ebool % 0.46/0.84 Using role type % 0.46/0.84 Declaring i_mono_2Etyop_2Emin_2Ebool:(Prop->u) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75c20>, <kernel.DependentProduct object at 0xf75248>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.46/0.84 Using role type % 0.46/0.84 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:((Prop->Prop)->u) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75440>, <kernel.DependentProduct object at 0xf75200>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 % 0.46/0.84 Using role type % 0.46/0.84 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29:((Prop->(Prop->Prop))->u) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75e60>, <kernel.DependentProduct object at 0xf75710>) of role type named j_mono_2Etyop_2Emin_2Ebool % 0.46/0.84 Using role type % 0.46/0.84 Declaring j_mono_2Etyop_2Emin_2Ebool:(du->Prop) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75f80>, <kernel.DependentProduct object at 0xf75638>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.46/0.84 Using role type % 0.46/0.84 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(du->(Prop->Prop)) % 0.46/0.84 FOF formula (<kernel.Constant object at 0xf75200>, <kernel.DependentProduct object at 0xf75440>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 % 0.55/0.85 Using role type % 0.55/0.85 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29:(du->(Prop->(Prop->Prop))) % 0.55/0.85 FOF formula (forall (A_27a:d) (A_27b:d) (V0f_2E0:u) (V1g_2E0:u), ((forall (V2x_2E0:u), (((eq du) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V0f_2E0)) ((s A_27a) V2x_2E0)))) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)) ((s A_27a) V2x_2E0)))))->(((eq du) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V0f_2E0)) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)))) of role axiom named reserved_2Eho_2Eeq__ext % 0.55/0.85 A new axiom: (forall (A_27a:d) (A_27b:d) (V0f_2E0:u) (V1g_2E0:u), ((forall (V2x_2E0:u), (((eq du) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V0f_2E0)) ((s A_27a) V2x_2E0)))) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)) ((s A_27a) V2x_2E0)))))->(((eq du) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V0f_2E0)) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)))) % 0.55/0.85 FOF formula (forall (A_27a:d) (V0x_2E0:u), (((eq du) ((s A_27a) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27a)) combin_i_2E0)) ((s A_27a) V0x_2E0)))) ((s A_27a) V0x_2E0))) of role axiom named reserved_2Eho_2Ei__thm % 0.55/0.85 A new axiom: (forall (A_27a:d) (V0x_2E0:u), (((eq du) ((s A_27a) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27a)) combin_i_2E0)) ((s A_27a) V0x_2E0)))) ((s A_27a) V0x_2E0))) % 0.55/0.85 FOF formula (forall (A_27a:d) (A_27b:d) (V0x_2E0:u) (V1y_2E0:u), (((eq du) ((s A_27a) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27b) A_27a)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27a))) combin_k_2E0)) ((s A_27a) V0x_2E0)))) ((s A_27b) V1y_2E0)))) ((s A_27a) V0x_2E0))) of role axiom named reserved_2Eho_2Ek__thm % 0.55/0.85 A new axiom: (forall (A_27a:d) (A_27b:d) (V0x_2E0:u) (V1y_2E0:u), (((eq du) ((s A_27a) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27b) A_27a)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27a))) combin_k_2E0)) ((s A_27a) V0x_2E0)))) ((s A_27b) V1y_2E0)))) ((s A_27a) V0x_2E0))) % 0.55/0.85 FOF formula (forall (A_27a:d) (A_27b:d) (A_27c:d) (V0f_2E0:u) (V1g_2E0:u) (V2x_2E0:u), (((eq du) ((s A_27c) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27c)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) A_27b)) ((tyop_2Emin_2Efun A_27a) A_27c))) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) A_27b)) ((tyop_2Emin_2Efun A_27a) A_27c)))) combin_s_2E0)) ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) V0f_2E0)))) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)))) ((s A_27a) V2x_2E0)))) ((s A_27c) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27b) A_27c)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) V0f_2E0)) ((s A_27a) V2x_2E0)))) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)) ((s A_27a) V2x_2E0))))))) of role axiom named reserved_2Eho_2Es__thm % 0.55/0.85 A new axiom: (forall (A_27a:d) (A_27b:d) (A_27c:d) (V0f_2E0:u) (V1g_2E0:u) (V2x_2E0:u), (((eq du) ((s A_27c) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27c)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) A_27b)) ((tyop_2Emin_2Efun A_27a) A_27c))) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) A_27b)) ((tyop_2Emin_2Efun A_27a) A_27c)))) combin_s_2E0)) ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) V0f_2E0)))) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)))) ((s A_27a) V2x_2E0)))) ((s A_27c) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27b) A_27c)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) V0f_2E0)) ((s A_27a) V2x_2E0)))) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)) ((s A_27a) V2x_2E0))))))) % 0.55/0.85 FOF formula (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_2F_5C V0) V1)) ((and V0) V1))) of role axiom named reserved_2Elogic_2E_2F_5C % 0.55/0.85 A new axiom: (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_2F_5C V0) V1)) ((and V0) V1))) % 0.55/0.85 FOF formula (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_5C_2F V0) V1)) ((or V0) V1))) of role axiom named reserved_2Elogic_2E_5C_2F % 0.55/0.87 A new axiom: (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_5C_2F V0) V1)) ((or V0) V1))) % 0.55/0.87 FOF formula (forall (V0:Prop), ((iff (mono_2Ec_2Ebool_2E_7E V0)) (not V0))) of role axiom named reserved_2Elogic_2E_7E % 0.55/0.87 A new axiom: (forall (V0:Prop), ((iff (mono_2Ec_2Ebool_2E_7E V0)) (not V0))) % 0.55/0.87 FOF formula (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Emin_2E_3D_3D_3E V0) V1)) (V0->V1))) of role axiom named reserved_2Elogic_2E_3D_3D_3E % 0.55/0.87 A new axiom: (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Emin_2E_3D_3D_3E V0) V1)) (V0->V1))) % 0.55/0.87 FOF formula (forall (A_27a:d) (V0_2E0:u) (V1_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((c_2Emin_2E_3D_2E2 ((s A_27a) V0_2E0)) ((s A_27a) V1_2E0))))) (((eq du) ((s A_27a) V0_2E0)) ((s A_27a) V1_2E0)))) of role axiom named reserved_2Elogic_2E_3D % 0.55/0.87 A new axiom: (forall (A_27a:d) (V0_2E0:u) (V1_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((c_2Emin_2E_3D_2E2 ((s A_27a) V0_2E0)) ((s A_27a) V1_2E0))))) (((eq du) ((s A_27a) V0_2E0)) ((s A_27a) V1_2E0)))) % 0.55/0.87 FOF formula (forall (A_27a:d) (V0f_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_21_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0))))) (forall (V1x_2E0:u), (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0)) ((s A_27a) V1x_2E0))))))) of role axiom named reserved_2Equant_2E_21 % 0.55/0.87 A new axiom: (forall (A_27a:d) (V0f_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_21_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0))))) (forall (V1x_2E0:u), (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0)) ((s A_27a) V1x_2E0))))))) % 0.55/0.87 FOF formula (forall (A_27a:d) (V0f_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_3F_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0))))) ((ex u) (fun (V1x_2E0:u)=> (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0)) ((s A_27a) V1x_2E0)))))))) of role axiom named reserved_2Equant_2E_3F % 0.55/0.87 A new axiom: (forall (A_27a:d) (V0f_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_3F_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0))))) ((ex u) (fun (V1x_2E0:u)=> (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0)) ((s A_27a) V1x_2E0)))))))) % 0.55/0.87 FOF formula (forall (V0_2E0:u), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) V0_2E0))))) ((s tyop_2Emin_2Ebool) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Ebool % 0.55/0.87 A new axiom: (forall (V0_2E0:u), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) V0_2E0))))) ((s tyop_2Emin_2Ebool) V0_2E0))) % 0.55/0.87 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.55/0.87 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) V0_2E0))) % 0.55/0.87 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 % 0.55/0.87 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) V0_2E0))) % 0.55/0.87 FOF formula (forall (V0:Prop), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Ebool % 0.55/0.87 A new axiom: (forall (V0:Prop), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V0)))) V0)) % 0.55/0.87 FOF formula (forall (V0:(Prop->Prop)), (((eq (Prop->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.55/0.87 A new axiom: (forall (V0:(Prop->Prop)), (((eq (Prop->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 V0)))) V0)) % 0.55/0.87 FOF formula (forall (V0:(Prop->(Prop->Prop))), (((eq (Prop->(Prop->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 % 0.55/0.87 A new axiom: (forall (V0:(Prop->(Prop->Prop))), (((eq (Prop->(Prop->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)) % 0.55/0.87 FOF formula (forall (A_27a:d) (X0_2E0:u), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_21_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0))))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) c_2Ebool_2E_21_2E0)) ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0)))))) of role axiom named arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a % 0.55/0.87 A new axiom: (forall (A_27a:d) (X0_2E0:u), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_21_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0))))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) c_2Ebool_2E_21_2E0)) ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0)))))) % 0.55/0.87 FOF formula (forall (A_27a:d) (X0_2E0:u) (X1_2E0:u), ((iff (((eq du) ((s A_27a) X0_2E0)) ((s A_27a) X1_2E0))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool))) c_2Emin_2E_3D_2E0)) ((s A_27a) X0_2E0)))) ((s A_27a) X1_2E0)))))) of role axiom named arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a % 0.58/0.88 A new axiom: (forall (A_27a:d) (X0_2E0:u) (X1_2E0:u), ((iff (((eq du) ((s A_27a) X0_2E0)) ((s A_27a) X1_2E0))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool))) c_2Emin_2E_3D_2E0)) ((s A_27a) X0_2E0)))) ((s A_27a) X1_2E0)))))) % 0.58/0.88 FOF formula (forall (A_27a:d) (X0_2E0:u), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_3F_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0))))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) c_2Ebool_2E_3F_2E0)) ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0)))))) of role axiom named arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a % 0.58/0.88 A new axiom: (forall (A_27a:d) (X0_2E0:u), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_3F_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0))))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) c_2Ebool_2E_3F_2E0)) ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0)))))) % 0.58/0.88 FOF formula (forall (V0:(Prop->Prop)) (V1:Prop), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool (V0 V1)))) ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 V0))) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool % 0.58/0.88 A new axiom: (forall (V0:(Prop->Prop)) (V1:Prop), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool (V0 V1)))) ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 V0))) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V1)))))) % 0.58/0.88 FOF formula (forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.58/0.88 A new axiom: (forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V1)))))) % 0.58/0.88 FOF formula (forall (V0:(Prop->Prop)) (V1:Prop), (((eq Prop) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool % 0.58/0.88 A new axiom: (forall (V0:(Prop->Prop)) (V1:Prop), (((eq Prop) (V0 V1)) (V0 V1))) % 0.58/0.88 FOF formula (forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq (Prop->Prop)) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.58/0.88 A new axiom: (forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq (Prop->Prop)) (V0 V1)) (V0 V1))) % 0.58/0.88 FOF formula ((iff mono_2Ec_2Ebool_2ET) (forall (V0x:Prop), (((eq Prop) V0x) V0x))) of role axiom named thm_2Ebool_2ET__DEF % 0.58/0.88 A new axiom: ((iff mono_2Ec_2Ebool_2ET) (forall (V0x:Prop), (((eq Prop) V0x) V0x))) % 0.58/0.88 FOF formula mono_2Ec_2Ebool_2ET of role conjecture named thm_2Ebool_2ETRUTH % 0.58/0.88 Conjecture to prove = mono_2Ec_2Ebool_2ET:Prop % 0.58/0.88 Parameter du_DUMMY:du. % 0.58/0.88 We need to prove ['mono_2Ec_2Ebool_2ET'] % 0.58/0.88 Parameter u:Type. % 0.58/0.88 Parameter d:Type. % 0.58/0.88 Parameter du:Type. % 0.58/0.88 Parameter tyop_2Emin_2Ebool:d. % 0.58/0.88 Parameter tyop_2Emin_2Efun:(d->(d->d)). % 0.58/0.88 Parameter s:(d->(u->du)). % 0.58/0.88 Parameter app_2E2:(du->(du->u)). % 0.58/0.88 Parameter combin_i_2E0:u. % 0.58/0.88 Parameter combin_k_2E0:u. % 0.58/0.88 Parameter combin_s_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_21_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_21_2E1:(du->u). % 0.58/0.88 Parameter c_2Ebool_2E_2F_5C_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_2F_5C_2E2:(du->(du->u)). % 0.58/0.88 Parameter c_2Emin_2E_3D_2E0:u. % 0.58/0.88 Parameter c_2Emin_2E_3D_2E2:(du->(du->u)). % 0.58/0.88 Parameter c_2Emin_2E_3D_3D_3E_2E0:u. % 0.58/0.88 Parameter c_2Emin_2E_3D_3D_3E_2E2:(du->(du->u)). % 0.58/0.88 Parameter c_2Ebool_2E_3F_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_3F_2E1:(du->u). % 0.58/0.88 Parameter c_2Ebool_2EF_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2ET_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_5C_2F_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_5C_2F_2E2:(du->(du->u)). % 0.58/0.88 Parameter c_2Ebool_2E_7E_2E0:u. % 0.58/0.88 Parameter c_2Ebool_2E_7E_2E1:(du->u). % 0.58/0.88 Parameter mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool:((Prop->Prop)->(Prop->Prop)). % 0.58/0.88 Parameter mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:((Prop->(Prop->Prop))->(Prop->(Prop->Prop))). % 0.58/0.88 Parameter mono_2Ec_2Ebool_2E_2F_5C:(Prop->(Prop->Prop)). % 0.58/0.88 Parameter mono_2Ec_2Emin_2E_3D_3D_3E:(Prop->(Prop->Prop)). % 0.58/0.88 Parameter mono_2Ec_2Ebool_2EF:Prop. % 0.58/0.88 Parameter mono_2Ec_2Ebool_2ET:Prop. % 0.58/0.88 Parameter mono_2Ec_2Ebool_2E_5C_2F:(Prop->(Prop->Prop)). % 0.58/0.88 Parameter mono_2Ec_2Ebool_2E_7E:(Prop->Prop). % 0.58/0.88 Parameter i_mono_2Etyop_2Emin_2Ebool:(Prop->u). % 0.58/0.88 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:((Prop->Prop)->u). % 0.58/0.88 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29:((Prop->(Prop->Prop))->u). % 0.58/0.88 Parameter j_mono_2Etyop_2Emin_2Ebool:(du->Prop). % 0.58/0.88 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(du->(Prop->Prop)). % 0.58/0.88 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29:(du->(Prop->(Prop->Prop))). % 0.58/0.88 Axiom reserved_2Eho_2Eeq__ext:(forall (A_27a:d) (A_27b:d) (V0f_2E0:u) (V1g_2E0:u), ((forall (V2x_2E0:u), (((eq du) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V0f_2E0)) ((s A_27a) V2x_2E0)))) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)) ((s A_27a) V2x_2E0)))))->(((eq du) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V0f_2E0)) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)))). % 0.58/0.88 Axiom reserved_2Eho_2Ei__thm:(forall (A_27a:d) (V0x_2E0:u), (((eq du) ((s A_27a) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27a)) combin_i_2E0)) ((s A_27a) V0x_2E0)))) ((s A_27a) V0x_2E0))). % 0.58/0.88 Axiom reserved_2Eho_2Ek__thm:(forall (A_27a:d) (A_27b:d) (V0x_2E0:u) (V1y_2E0:u), (((eq du) ((s A_27a) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27b) A_27a)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27a))) combin_k_2E0)) ((s A_27a) V0x_2E0)))) ((s A_27b) V1y_2E0)))) ((s A_27a) V0x_2E0))). % 0.58/0.88 Axiom reserved_2Eho_2Es__thm:(forall (A_27a:d) (A_27b:d) (A_27c:d) (V0f_2E0:u) (V1g_2E0:u) (V2x_2E0:u), (((eq du) ((s A_27c) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27c)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) A_27b)) ((tyop_2Emin_2Efun A_27a) A_27c))) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) A_27b)) ((tyop_2Emin_2Efun A_27a) A_27c)))) combin_s_2E0)) ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) V0f_2E0)))) ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)))) ((s A_27a) V2x_2E0)))) ((s A_27c) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27b) A_27c)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27b) A_27c))) V0f_2E0)) ((s A_27a) V2x_2E0)))) ((s A_27b) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) A_27b)) V1g_2E0)) ((s A_27a) V2x_2E0))))))). % 0.58/0.89 Axiom reserved_2Elogic_2E_2F_5C:(forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_2F_5C V0) V1)) ((and V0) V1))). % 0.58/0.89 Axiom reserved_2Elogic_2E_5C_2F:(forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_5C_2F V0) V1)) ((or V0) V1))). % 0.58/0.89 Axiom reserved_2Elogic_2E_7E:(forall (V0:Prop), ((iff (mono_2Ec_2Ebool_2E_7E V0)) (not V0))). % 0.58/0.89 Axiom reserved_2Elogic_2E_3D_3D_3E:(forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Emin_2E_3D_3D_3E V0) V1)) (V0->V1))). % 0.58/0.89 Axiom reserved_2Elogic_2E_3D:(forall (A_27a:d) (V0_2E0:u) (V1_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((c_2Emin_2E_3D_2E2 ((s A_27a) V0_2E0)) ((s A_27a) V1_2E0))))) (((eq du) ((s A_27a) V0_2E0)) ((s A_27a) V1_2E0)))). % 0.58/0.89 Axiom reserved_2Equant_2E_21:(forall (A_27a:d) (V0f_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_21_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0))))) (forall (V1x_2E0:u), (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0)) ((s A_27a) V1x_2E0))))))). % 0.58/0.89 Axiom reserved_2Equant_2E_3F:(forall (A_27a:d) (V0f_2E0:u), ((iff (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_3F_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0))))) ((ex u) (fun (V1x_2E0:u)=> (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0f_2E0)) ((s A_27a) V1x_2E0)))))))). % 0.58/0.89 Axiom ij_2Emono_2Etyop_2Emin_2Ebool:(forall (V0_2E0:u), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) V0_2E0))))) ((s tyop_2Emin_2Ebool) V0_2E0))). % 0.58/0.89 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) V0_2E0))). % 0.58/0.89 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) V0_2E0))). % 0.58/0.89 Axiom ji_2Emono_2Etyop_2Emin_2Ebool:(forall (V0:Prop), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V0)))) V0)). % 0.58/0.89 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(forall (V0:(Prop->Prop)), (((eq (Prop->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 V0)))) V0)). % 0.58/0.89 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29:(forall (V0:(Prop->(Prop->Prop))), (((eq (Prop->(Prop->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)). % 0.58/0.89 Axiom arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a:(forall (A_27a:d) (X0_2E0:u), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_21_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0))))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) c_2Ebool_2E_21_2E0)) ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0)))))). % 0.78/1.10 Axiom arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a:(forall (A_27a:d) (X0_2E0:u) (X1_2E0:u), ((iff (((eq du) ((s A_27a) X0_2E0)) ((s A_27a) X1_2E0))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool))) c_2Emin_2E_3D_2E0)) ((s A_27a) X0_2E0)))) ((s A_27a) X1_2E0)))))). % 0.78/1.10 Axiom arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a:(forall (A_27a:d) (X0_2E0:u), (((eq Prop) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) (c_2Ebool_2E_3F_2E1 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0))))) (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) c_2Ebool_2E_3F_2E0)) ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) X0_2E0)))))). % 0.78/1.10 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool:(forall (V0:(Prop->Prop)) (V1:Prop), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool (V0 V1)))) ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 V0))) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V1)))))). % 0.78/1.10 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) ((tyop_2Emin_2Efun tyop_2Emin_2Ebool) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool V1)))))). % 0.78/1.10 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool:(forall (V0:(Prop->Prop)) (V1:Prop), (((eq Prop) (V0 V1)) (V0 V1))). % 0.78/1.10 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq (Prop->Prop)) (V0 V1)) (V0 V1))). % 0.78/1.10 Axiom thm_2Ebool_2ET__DEF:((iff mono_2Ec_2Ebool_2ET) (forall (V0x:Prop), (((eq Prop) V0x) V0x))). % 0.78/1.10 Trying to prove mono_2Ec_2Ebool_2ET % 0.78/1.10 Found monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool0:=(monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3)):(forall (V1:Prop), (((eq Prop) V1) V1)) % 0.78/1.10 Found (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3)) as proof of (forall (V0x:Prop), (((eq Prop) V0x) V0x)) % 0.78/1.10 Found (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3)) as proof of (forall (V0x:Prop), (((eq Prop) V0x) V0x)) % 0.78/1.10 Found (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))) as proof of mono_2Ec_2Ebool_2ET % 0.78/1.10 Found (fun (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3)))) as proof of mono_2Ec_2Ebool_2ET % 0.78/1.10 Found (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3)))) as proof of (((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)->mono_2Ec_2Ebool_2ET) % 0.78/1.10 Found (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3)))) as proof of ((mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))->(((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)->mono_2Ec_2Ebool_2ET)) % 0.78/1.10 Found (and_rect00 (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))))) as proof of mono_2Ec_2Ebool_2ET % 0.78/1.10 Found ((and_rect0 mono_2Ec_2Ebool_2ET) (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))))) as proof of mono_2Ec_2Ebool_2ET % 0.78/1.10 Found (((fun (P:Type) (x:((mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))->(((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)->P)))=> (((((and_rect (mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) ((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)) P) x) thm_2Ebool_2ET__DEF)) mono_2Ec_2Ebool_2ET) (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))))) as proof of mono_2Ec_2Ebool_2ET % 0.78/1.10 Found (((fun (P:Type) (x:((mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))->(((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)->P)))=> (((((and_rect (mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) ((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)) P) x) thm_2Ebool_2ET__DEF)) mono_2Ec_2Ebool_2ET) (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))))) as proof of mono_2Ec_2Ebool_2ET % 0.78/1.10 Got proof (((fun (P:Type) (x:((mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))->(((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)->P)))=> (((((and_rect (mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) ((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)) P) x) thm_2Ebool_2ET__DEF)) mono_2Ec_2Ebool_2ET) (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))))) % 0.78/1.10 Time elapsed = 0.204862s % 0.78/1.10 node=21 cost=683.000000 depth=9 % 0.78/1.10:::::::::::::::::::::: % 0.78/1.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.78/1.10 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.78/1.10 (((fun (P:Type) (x:((mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))->(((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)->P)))=> (((((and_rect (mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) ((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET)) P) x) thm_2Ebool_2ET__DEF)) mono_2Ec_2Ebool_2ET) (fun (x:(mono_2Ec_2Ebool_2ET->(forall (V0x:Prop), (((eq Prop) V0x) V0x)))) (x0:((forall (V0x:Prop), (((eq Prop) V0x) V0x))->mono_2Ec_2Ebool_2ET))=> (x0 (monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (fun (x3:Prop)=> x3))))) % 0.78/1.10 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------