%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : ITP023^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 : n002.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:54 EDT 2021 % Result : Theorem 0.85s % Output : Proof 0.85s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : ITP023^1 : TPTP v7.5.0. Bugfixed v7.5.0. % 0.12/0.12 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.33 % Computer : n002.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % DateTime : Fri Mar 19 03:23:01 EDT 2021 % 0.13/0.34 % CPUTime : % 0.19/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.19/0.35 Python 2.7.5 % 0.43/0.62 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152fa28>, <kernel.Type object at 0x152f758>) of role type named u % 0.43/0.62 Using role type % 0.43/0.62 Declaring u:Type % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152f5f0>, <kernel.Type object at 0x152ad40>) of role type named d % 0.43/0.62 Using role type % 0.43/0.62 Declaring d:Type % 0.43/0.62 FOF formula (<kernel.Constant object at 0x1533d88>, <kernel.Type object at 0x152f758>) of role type named du % 0.43/0.62 Using role type % 0.43/0.62 Declaring du:Type % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152ad40>, <kernel.Type object at 0x2ad55202b998>) of role type named mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.43/0.62 Using role type % 0.43/0.62 Declaring mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:Type % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152f2d8>, <kernel.Type object at 0x2ad55202b998>) of role type named mono_2Etyop_2Erealax_2Ereal % 0.43/0.62 Using role type % 0.43/0.62 Declaring mono_2Etyop_2Erealax_2Ereal:Type % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152f128>, <kernel.Constant object at 0x152f758>) of role type named tyop_2Emin_2Ebool % 0.43/0.62 Using role type % 0.43/0.62 Declaring tyop_2Emin_2Ebool:d % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152fb48>, <kernel.DependentProduct object at 0x2ad55202b368>) of role type named tyop_2Emin_2Efun % 0.43/0.62 Using role type % 0.43/0.62 Declaring tyop_2Emin_2Efun:(d->(d->d)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152f758>, <kernel.DependentProduct object at 0x2ad55202b368>) of role type named tyop_2Epair_2Eprod % 0.43/0.62 Using role type % 0.43/0.62 Declaring tyop_2Epair_2Eprod:(d->(d->d)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152fb48>, <kernel.Constant object at 0x2ad55202b3b0>) of role type named tyop_2Erealax_2Ereal % 0.43/0.62 Using role type % 0.43/0.62 Declaring tyop_2Erealax_2Ereal:d % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152f2d8>, <kernel.DependentProduct object at 0x2ad55202bf80>) of role type named s % 0.43/0.62 Using role type % 0.43/0.62 Declaring s:(d->(u->du)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x152f2d8>, <kernel.DependentProduct object at 0x16a2ea8>) of role type named app_2E2 % 0.43/0.62 Using role type % 0.43/0.62 Declaring app_2E2:(du->(du->u)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2ad55202b440>, <kernel.Constant object at 0x16a2f80>) of role type named combin_i_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring combin_i_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2ad55202b368>, <kernel.Constant object at 0x16a2ef0>) of role type named combin_k_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring combin_k_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2ad55202b440>, <kernel.Constant object at 0x16a2f38>) of role type named combin_s_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring combin_s_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2ad55202bf80>, <kernel.Constant object at 0x16a2f38>) of role type named c_2Ebool_2E_21_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Ebool_2E_21_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2ad55202bf80>, <kernel.DependentProduct object at 0x16a2d88>) of role type named c_2Ebool_2E_21_2E1 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Ebool_2E_21_2E1:(du->u) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x16a2fc8>, <kernel.Constant object at 0x16a2d88>) of role type named c_2Epair_2E_2C_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Epair_2E_2C_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x16a2e60>, <kernel.DependentProduct object at 0x16a2f38>) of role type named c_2Epair_2E_2C_2E2 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Epair_2E_2C_2E2:(du->(du->u)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x16a2d40>, <kernel.Constant object at 0x16a2f38>) of role type named c_2Ebool_2E_2F_5C_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Ebool_2E_2F_5C_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x16a2fc8>, <kernel.DependentProduct object at 0x16a2d88>) of role type named c_2Ebool_2E_2F_5C_2E2 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Ebool_2E_2F_5C_2E2:(du->(du->u)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x16a2ea8>, <kernel.Constant object at 0x16a2d88>) of role type named c_2Emin_2E_3D_2E0 % 0.43/0.62 Using role type % 0.43/0.62 Declaring c_2Emin_2E_3D_2E0:u % 0.43/0.62 FOF formula (<kernel.Constant object at 0x16a2d40>, <kernel.DependentProduct object at 0x16a2f38>) of role type named c_2Emin_2E_3D_2E2 % 0.43/0.62 Using role type % 0.43/0.63 Declaring c_2Emin_2E_3D_2E2:(du->(du->u)) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2bd8>, <kernel.Constant object at 0x16a2f38>) of role type named c_2Emin_2E_3D_3D_3E_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Emin_2E_3D_3D_3E_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2ea8>, <kernel.DependentProduct object at 0x16a2d88>) of role type named c_2Emin_2E_3D_3D_3E_2E2 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Emin_2E_3D_3D_3E_2E2:(du->(du->u)) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2b48>, <kernel.Constant object at 0x16a2d88>) of role type named c_2Ebool_2E_3F_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2E_3F_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2bd8>, <kernel.DependentProduct object at 0x16a2d40>) of role type named c_2Ebool_2E_3F_2E1 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2E_3F_2E1:(du->u) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2ab8>, <kernel.Constant object at 0x16a2d40>) of role type named c_2Ebool_2EF_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2EF_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2b48>, <kernel.Constant object at 0x16a2d40>) of role type named c_2Epred__set_2ESUBSET_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Epred__set_2ESUBSET_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2bd8>, <kernel.DependentProduct object at 0x16a29e0>) of role type named c_2Epred__set_2ESUBSET_2E2 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Epred__set_2ESUBSET_2E2:(du->(du->u)) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2f38>, <kernel.Constant object at 0x16a29e0>) of role type named c_2Ebool_2ET_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2ET_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2b48>, <kernel.Constant object at 0x16a29e0>) of role type named c_2Ebool_2E_5C_2F_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2E_5C_2F_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2bd8>, <kernel.DependentProduct object at 0x16a2950>) of role type named c_2Ebool_2E_5C_2F_2E2 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2E_5C_2F_2E2:(du->(du->u)) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2bd8>, <kernel.Constant object at 0x16a29e0>) of role type named c_2Ereal__topology_2Eball_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ereal__topology_2Eball_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2908>, <kernel.DependentProduct object at 0x16a26c8>) of role type named c_2Ereal__topology_2Eball_2E1 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ereal__topology_2Eball_2E1:(du->u) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2710>, <kernel.Constant object at 0x16a2908>) of role type named c_2Ereal__topology_2Ebounded__def_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ereal__topology_2Ebounded__def_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a26c8>, <kernel.DependentProduct object at 0x16a2638>) of role type named c_2Ereal__topology_2Ebounded__def_2E1 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ereal__topology_2Ebounded__def_2E1:(du->u) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a26c8>, <kernel.Constant object at 0x16a2908>) of role type named c_2Ereal__topology_2Ecball_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ereal__topology_2Ecball_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a25f0>, <kernel.DependentProduct object at 0x16a2518>) of role type named c_2Ereal__topology_2Ecball_2E1 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ereal__topology_2Ecball_2E1:(du->u) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2560>, <kernel.Constant object at 0x16a25f0>) of role type named c_2Ebool_2E_7E_2E0 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2E_7E_2E0:u % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2518>, <kernel.DependentProduct object at 0x16a2488>) of role type named c_2Ebool_2E_7E_2E1 % 0.43/0.63 Using role type % 0.43/0.63 Declaring c_2Ebool_2E_7E_2E1:(du->u) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a24d0>, <kernel.DependentProduct object at 0x16a2908>) of role type named mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool % 0.43/0.63 Using role type % 0.43/0.63 Declaring mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool:((Prop->Prop)->(Prop->Prop)) % 0.43/0.63 FOF formula (<kernel.Constant object at 0x16a2560>, <kernel.DependentProduct object at 0x16a2680>) of role type named mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.48/0.63 Using role type % 0.48/0.63 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.48/0.63 FOF formula (<kernel.Constant object at 0x16a2518>, <kernel.DependentProduct object at 0x16a2368>) of role type named mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool:(((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a2488>, <kernel.DependentProduct object at 0x16a23f8>) of role type named mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))->((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a2440>, <kernel.DependentProduct object at 0x16a2290>) of role type named mono_2Eapp_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Eapp_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:((mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))->(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a2200>, <kernel.DependentProduct object at 0x16a23f8>) of role type named mono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:((mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))->(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a23b0>, <kernel.DependentProduct object at 0x16a2440>) of role type named mono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:((mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a2320>, <kernel.DependentProduct object at 0x16a2248>) of role type named mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a24d0>, <kernel.DependentProduct object at 0x16a23f8>) of role type named mono_2Ec_2Ebool_2E_2F_5C % 0.48/0.63 Using role type % 0.48/0.63 Declaring mono_2Ec_2Ebool_2E_2F_5C:(Prop->(Prop->Prop)) % 0.48/0.63 FOF formula (<kernel.Constant object at 0x16a23b0>, <kernel.DependentProduct object at 0x16a2290>) of role type named mono_2Ec_2Emin_2E_3D_3D_3E % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Emin_2E_3D_3D_3E:(Prop->(Prop->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2320>, <kernel.Sort object at 0x2ad552024638>) of role type named mono_2Ec_2Ebool_2EF % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ebool_2EF:Prop % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a21b8>, <kernel.DependentProduct object at 0x16a20e0>) of role type named mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2488>, <kernel.Sort object at 0x2ad552024638>) of role type named mono_2Ec_2Ebool_2ET % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ebool_2ET:Prop % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a23b0>, <kernel.DependentProduct object at 0x16a2098>) of role type named mono_2Ec_2Ebool_2E_5C_2F % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ebool_2E_5C_2F:(Prop->(Prop->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a23b0>, <kernel.DependentProduct object at 0x2ad55202c200>) of role type named mono_2Ec_2Ereal__topology_2Eball % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ereal__topology_2Eball:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a24d0>, <kernel.DependentProduct object at 0x2ad552024cf8>) of role type named mono_2Ec_2Ereal__topology_2Ebounded__def % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ereal__topology_2Ebounded__def:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2320>, <kernel.DependentProduct object at 0x16a24d0>) of role type named mono_2Ec_2Ereal__topology_2Ecball % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ereal__topology_2Ecball:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x2ad55202c200>, <kernel.DependentProduct object at 0x16a2098>) of role type named mono_2Ec_2Ebool_2E_7E % 0.48/0.64 Using role type % 0.48/0.64 Declaring mono_2Ec_2Ebool_2E_7E:(Prop->Prop) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x2ad55202c200>, <kernel.DependentProduct object at 0x2ad54a54f5f0>) of role type named i_mono_2Etyop_2Emin_2Ebool % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Ebool:(Prop->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2ef0>, <kernel.DependentProduct object at 0x2ad54a54edd0>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:((Prop->Prop)->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x2ad54a54f3b0>, <kernel.DependentProduct object at 0x17cee60>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.64 Using role type % 0.48/0.64 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.48/0.64 FOF formula (<kernel.Constant object at 0x2ad54a54f5f0>, <kernel.DependentProduct object at 0x17ceb90>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x2ad54a54f5f0>, <kernel.DependentProduct object at 0x17cecb0>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29:(((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2128>, <kernel.DependentProduct object at 0x17cebd8>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29:((mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2098>, <kernel.DependentProduct object at 0x17ceb90>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:((mono_2Etyop_2Erealax_2Ereal->Prop)->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a23b0>, <kernel.DependentProduct object at 0x17ce9e0>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29:((mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a23f8>, <kernel.DependentProduct object at 0x17cedd0>) of role type named i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:((mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2128>, <kernel.DependentProduct object at 0x17ceb90>) of role type named i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x17cebd8>, <kernel.DependentProduct object at 0x17cefc8>) of role type named i_mono_2Etyop_2Erealax_2Ereal % 0.48/0.64 Using role type % 0.48/0.64 Declaring i_mono_2Etyop_2Erealax_2Ereal:(mono_2Etyop_2Erealax_2Ereal->u) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x16a2128>, <kernel.DependentProduct object at 0x17cee18>) of role type named j_mono_2Etyop_2Emin_2Ebool % 0.48/0.64 Using role type % 0.48/0.64 Declaring j_mono_2Etyop_2Emin_2Ebool:(du->Prop) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x17cecb0>, <kernel.DependentProduct object at 0x17ceb00>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(du->(Prop->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x17cebd8>, <kernel.DependentProduct object at 0x17ceb90>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.64 Using role type % 0.48/0.64 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.48/0.64 FOF formula (<kernel.Constant object at 0x17cee18>, <kernel.DependentProduct object at 0x1532998>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.48/0.64 Using role type % 0.48/0.64 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(du->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) % 0.48/0.64 FOF formula (<kernel.Constant object at 0x17ceb00>, <kernel.DependentProduct object at 0x15325f0>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29:(du->((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) % 0.48/0.65 FOF formula (<kernel.Constant object at 0x17ceb90>, <kernel.DependentProduct object at 0x15328c0>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29:(du->(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) % 0.48/0.65 FOF formula (<kernel.Constant object at 0x17cee18>, <kernel.DependentProduct object at 0x15325a8>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:(du->(mono_2Etyop_2Erealax_2Ereal->Prop)) % 0.48/0.65 FOF formula (<kernel.Constant object at 0x17ceb00>, <kernel.DependentProduct object at 0x1532b00>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29:(du->(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) % 0.48/0.65 FOF formula (<kernel.Constant object at 0x17cee18>, <kernel.DependentProduct object at 0x15325a8>) of role type named j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:(du->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) % 0.48/0.65 FOF formula (<kernel.Constant object at 0x17ceb00>, <kernel.DependentProduct object at 0x1532b00>) of role type named j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(du->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) % 0.48/0.65 FOF formula (<kernel.Constant object at 0x15325a8>, <kernel.DependentProduct object at 0x16a3290>) of role type named j_mono_2Etyop_2Erealax_2Ereal % 0.48/0.65 Using role type % 0.48/0.65 Declaring j_mono_2Etyop_2Erealax_2Ereal:(du->mono_2Etyop_2Erealax_2Ereal) % 0.48/0.65 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.48/0.65 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.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 A new axiom: (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_2F_5C V0) V1)) ((and V0) V1))) % 0.48/0.66 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.48/0.66 A new axiom: (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_5C_2F V0) V1)) ((or V0) V1))) % 0.48/0.66 FOF formula (forall (V0:Prop), ((iff (mono_2Ec_2Ebool_2E_7E V0)) (not V0))) of role axiom named reserved_2Elogic_2E_7E % 0.48/0.66 A new axiom: (forall (V0:Prop), ((iff (mono_2Ec_2Ebool_2E_7E V0)) (not V0))) % 0.48/0.66 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.48/0.66 A new axiom: (forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Emin_2E_3D_3D_3E V0) V1)) (V0->V1))) % 0.48/0.66 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.48/0.66 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 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.48/0.67 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.48/0.67 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) V0_2E0))) % 0.48/0.67 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.67 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) V0_2E0))) % 0.48/0.67 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.68 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) V0_2E0))) % 0.48/0.68 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.48/0.68 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) V0_2E0))) % 0.48/0.68 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 % 0.48/0.68 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) V0_2E0))) % 0.48/0.68 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.48/0.68 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) V0_2E0))) % 0.48/0.68 FOF formula (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 (j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) V0_2E0))))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.48/0.68 A new axiom: (forall (V0_2E0:u), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 (j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) V0_2E0))))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) V0_2E0))) % 0.48/0.68 FOF formula (forall (V0_2E0:u), (((eq du) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal (j_mono_2Etyop_2Erealax_2Ereal ((s tyop_2Erealax_2Ereal) V0_2E0))))) ((s tyop_2Erealax_2Ereal) V0_2E0))) of role axiom named ij_2Emono_2Etyop_2Erealax_2Ereal % 0.48/0.68 A new axiom: (forall (V0_2E0:u), (((eq du) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal (j_mono_2Etyop_2Erealax_2Ereal ((s tyop_2Erealax_2Ereal) V0_2E0))))) ((s tyop_2Erealax_2Ereal) V0_2E0))) % 0.48/0.68 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.48/0.68 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.48/0.68 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.48/0.68 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.48/0.69 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.48/0.69 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.48/0.69 FOF formula (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.48/0.69 A new axiom: (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 V0)))) V0)) % 0.48/0.69 FOF formula (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.69 A new axiom: (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)) % 0.48/0.69 FOF formula (forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))), (((eq (mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 % 0.48/0.69 A new axiom: (forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))), (((eq (mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)) % 0.48/0.69 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq (mono_2Etyop_2Erealax_2Ereal->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.48/0.69 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq (mono_2Etyop_2Erealax_2Ereal->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V0)))) V0)) % 0.48/0.69 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))), (((eq (mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 % 0.48/0.69 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))), (((eq (mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 V0)))) V0)) % 0.48/0.69 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)), (((eq (mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.48/0.70 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)), (((eq (mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 V0)))) V0)) % 0.48/0.70 FOF formula (forall (V0:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) (j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.48/0.70 A new axiom: (forall (V0:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) (j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 V0)))) V0)) % 0.48/0.70 FOF formula (forall (V0:mono_2Etyop_2Erealax_2Ereal), (((eq mono_2Etyop_2Erealax_2Ereal) (j_mono_2Etyop_2Erealax_2Ereal ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V0)))) V0)) of role axiom named ji_2Emono_2Etyop_2Erealax_2Ereal % 0.48/0.70 A new axiom: (forall (V0:mono_2Etyop_2Erealax_2Ereal), (((eq mono_2Etyop_2Erealax_2Ereal) (j_mono_2Etyop_2Erealax_2Ereal ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V0)))) V0)) % 0.48/0.70 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.48/0.70 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.48/0.70 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.48/0.70 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.55/0.71 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.55/0.71 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.55/0.71 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.55/0.71 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.55/0.71 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.55/0.71 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.55/0.71 FOF formula (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->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_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool % 0.55/0.71 A new axiom: (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->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_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))) % 0.55/0.71 FOF formula (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.55/0.71 A new axiom: (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))) % 0.55/0.71 FOF formula (forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (V1:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.55/0.71 A new axiom: (forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (V1:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 V1)))))) % 0.55/0.72 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.55/0.72 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))) % 0.55/0.72 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 (V0 V1)))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))) of role axiom named monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.55/0.72 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 (V0 V1)))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))) % 0.55/0.72 FOF formula (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) c_2Epair_2E_2C_2E0)) of role axiom named monoeq_2Emono_2Ec_2Epair_2E_2C_2E0_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal % 0.55/0.72 A new axiom: (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) c_2Epair_2E_2C_2E0)) % 0.55/0.72 FOF formula (forall (V0:mono_2Etyop_2Erealax_2Ereal) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0) V1)))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((c_2Epair_2E_2C_2E2 ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))) of role axiom named monoeq_2Emono_2Ec_2Epair_2E_2C_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal % 0.55/0.72 A new axiom: (forall (V0:mono_2Etyop_2Erealax_2Ereal) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0) V1)))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((c_2Epair_2E_2C_2E2 ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))) % 0.55/0.72 FOF formula (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) c_2Epred__set_2ESUBSET_2E0)) of role axiom named monoeq_2Emono_2Ec_2Epred__set_2ESUBSET_2E0_2Emono_2Etyop_2Erealax_2Ereal % 0.55/0.72 A new axiom: (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) c_2Epred__set_2ESUBSET_2E0)) % 0.55/0.73 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal V0) V1)))) ((s tyop_2Emin_2Ebool) ((c_2Epred__set_2ESUBSET_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))) of role axiom named monoeq_2Emono_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2Etyop_2Erealax_2Ereal % 0.55/0.73 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal V0) V1)))) ((s tyop_2Emin_2Ebool) ((c_2Epred__set_2ESUBSET_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))) % 0.55/0.73 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.55/0.73 A new axiom: (forall (V0:(Prop->Prop)) (V1:Prop), (((eq Prop) (V0 V1)) (V0 V1))) % 0.55/0.73 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.55/0.73 A new axiom: (forall (V0:(Prop->(Prop->Prop))) (V1:Prop), (((eq (Prop->Prop)) (V0 V1)) (V0 V1))) % 0.55/0.73 FOF formula (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq Prop) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool % 0.55/0.73 A new axiom: (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq Prop) (V0 V1)) (V0 V1))) % 0.55/0.73 FOF formula (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 % 0.55/0.73 A new axiom: (forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V0 V1)) (V0 V1))) % 0.55/0.73 FOF formula (forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (V1:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq (mono_2Etyop_2Erealax_2Ereal->Prop)) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 % 0.55/0.73 A new axiom: (forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (V1:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq (mono_2Etyop_2Erealax_2Ereal->Prop)) (V0 V1)) (V0 V1))) % 0.55/0.73 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq (mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 % 0.55/0.74 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq (mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V0 V1)) (V0 V1))) % 0.55/0.74 FOF formula (forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) (V0 V1)) (V0 V1))) of role axiom named monoapp_2Emono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 % 0.55/0.74 A new axiom: (forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) (V0 V1)) (V0 V1))) % 0.55/0.74 FOF formula mono_2Ec_2Ebool_2ET of role axiom named thm_2Ebool_2ETRUTH % 0.55/0.74 A new axiom: mono_2Ec_2Ebool_2ET % 0.55/0.74 FOF formula (forall (V0t1:Prop) (V1t2:Prop), ((V0t1->V1t2)->((V1t2->V0t1)->(((eq Prop) V0t1) V1t2)))) of role axiom named thm_2Ebool_2EIMP__ANTISYM__AX % 0.55/0.74 A new axiom: (forall (V0t1:Prop) (V1t2:Prop), ((V0t1->V1t2)->((V1t2->V0t1)->(((eq Prop) V0t1) V1t2)))) % 0.55/0.74 FOF formula (forall (V0t:Prop), ((V0t->mono_2Ec_2Ebool_2EF)->(not V0t))) of role axiom named thm_2Ebool_2EIMP__F % 0.55/0.74 A new axiom: (forall (V0t:Prop), ((V0t->mono_2Ec_2Ebool_2EF)->(not V0t))) % 0.55/0.74 FOF formula (forall (V0t:Prop), ((not V0t)->(V0t->mono_2Ec_2Ebool_2EF))) of role axiom named thm_2Ebool_2EF__IMP % 0.55/0.74 A new axiom: (forall (V0t:Prop), ((not V0t)->(V0t->mono_2Ec_2Ebool_2EF))) % 0.55/0.74 FOF formula (forall (V0t:Prop), ((and ((and ((and ((and ((iff (mono_2Ec_2Ebool_2ET->V0t)) V0t)) ((iff (V0t->mono_2Ec_2Ebool_2ET)) mono_2Ec_2Ebool_2ET))) ((iff (mono_2Ec_2Ebool_2EF->V0t)) mono_2Ec_2Ebool_2ET))) ((iff (V0t->V0t)) mono_2Ec_2Ebool_2ET))) ((iff (V0t->mono_2Ec_2Ebool_2EF)) (not V0t)))) of role axiom named thm_2Ebool_2EIMP__CLAUSES % 0.55/0.74 A new axiom: (forall (V0t:Prop), ((and ((and ((and ((and ((iff (mono_2Ec_2Ebool_2ET->V0t)) V0t)) ((iff (V0t->mono_2Ec_2Ebool_2ET)) mono_2Ec_2Ebool_2ET))) ((iff (mono_2Ec_2Ebool_2EF->V0t)) mono_2Ec_2Ebool_2ET))) ((iff (V0t->V0t)) mono_2Ec_2Ebool_2ET))) ((iff (V0t->mono_2Ec_2Ebool_2EF)) (not V0t)))) % 0.55/0.74 FOF formula ((and ((and (forall (V0t:Prop), ((iff (not (not V0t))) V0t))) ((iff (not mono_2Ec_2Ebool_2ET)) mono_2Ec_2Ebool_2EF))) ((iff (not mono_2Ec_2Ebool_2EF)) mono_2Ec_2Ebool_2ET)) of role axiom named thm_2Ebool_2ENOT__CLAUSES % 0.55/0.74 A new axiom: ((and ((and (forall (V0t:Prop), ((iff (not (not V0t))) V0t))) ((iff (not mono_2Ec_2Ebool_2ET)) mono_2Ec_2Ebool_2EF))) ((iff (not mono_2Ec_2Ebool_2EF)) mono_2Ec_2Ebool_2ET)) % 0.55/0.74 FOF formula (forall (A_27a:d) (V0x_2E0:u) (V1y_2E0:u), ((iff (((eq du) ((s A_27a) V0x_2E0)) ((s A_27a) V1y_2E0))) (((eq du) ((s A_27a) V1y_2E0)) ((s A_27a) V0x_2E0)))) of role axiom named thm_2Ebool_2EEQ__SYM__EQ % 0.55/0.74 A new axiom: (forall (A_27a:d) (V0x_2E0:u) (V1y_2E0:u), ((iff (((eq du) ((s A_27a) V0x_2E0)) ((s A_27a) V1y_2E0))) (((eq du) ((s A_27a) V1y_2E0)) ((s A_27a) V0x_2E0)))) % 0.55/0.74 FOF formula (forall (V0t:Prop), ((and ((and ((and ((iff (((eq Prop) mono_2Ec_2Ebool_2ET) V0t)) V0t)) ((iff (((eq Prop) V0t) mono_2Ec_2Ebool_2ET)) V0t))) ((iff (((eq Prop) mono_2Ec_2Ebool_2EF) V0t)) (not V0t)))) ((iff (((eq Prop) V0t) mono_2Ec_2Ebool_2EF)) (not V0t)))) of role axiom named thm_2Ebool_2EEQ__CLAUSES % 0.55/0.74 A new axiom: (forall (V0t:Prop), ((and ((and ((and ((iff (((eq Prop) mono_2Ec_2Ebool_2ET) V0t)) V0t)) ((iff (((eq Prop) V0t) mono_2Ec_2Ebool_2ET)) V0t))) ((iff (((eq Prop) mono_2Ec_2Ebool_2EF) V0t)) (not V0t)))) ((iff (((eq Prop) V0t) mono_2Ec_2Ebool_2EF)) (not V0t)))) % 0.55/0.75 FOF formula (forall (A_27a:d) (V0P_2E0:u), ((iff (not (forall (V1x_2E0:u), (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0P_2E0)) ((s A_27a) V1x_2E0))))))) ((ex u) (fun (V2x_2E0:u)=> (not (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0P_2E0)) ((s A_27a) V2x_2E0))))))))) of role axiom named thm_2Ebool_2ENOT__FORALL__THM % 0.55/0.75 A new axiom: (forall (A_27a:d) (V0P_2E0:u), ((iff (not (forall (V1x_2E0:u), (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0P_2E0)) ((s A_27a) V1x_2E0))))))) ((ex u) (fun (V2x_2E0:u)=> (not (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0P_2E0)) ((s A_27a) V2x_2E0))))))))) % 0.55/0.75 FOF formula (forall (V0A:Prop) (V1B:Prop) (V2C:Prop), ((iff ((or ((or V0A) V1B)) V2C)) ((or ((or V0A) V1B)) V2C))) of role axiom named thm_2Ebool_2EDISJ__ASSOC % 0.55/0.75 A new axiom: (forall (V0A:Prop) (V1B:Prop) (V2C:Prop), ((iff ((or ((or V0A) V1B)) V2C)) ((or ((or V0A) V1B)) V2C))) % 0.55/0.75 FOF formula (forall (V0A:Prop) (V1B:Prop), ((iff ((or V0A) V1B)) ((or V1B) V0A))) of role axiom named thm_2Ebool_2EDISJ__SYM % 0.55/0.75 A new axiom: (forall (V0A:Prop) (V1B:Prop), ((iff ((or V0A) V1B)) ((or V1B) V0A))) % 0.55/0.75 FOF formula (forall (V0A:Prop) (V1B:Prop), ((and ((iff (not ((and V0A) V1B))) ((or (not V0A)) (not V1B)))) ((iff (not ((or V0A) V1B))) ((and (not V0A)) (not V1B))))) of role axiom named thm_2Ebool_2EDE__MORGAN__THM % 0.55/0.75 A new axiom: (forall (V0A:Prop) (V1B:Prop), ((and ((iff (not ((and V0A) V1B))) ((or (not V0A)) (not V1B)))) ((iff (not ((or V0A) V1B))) ((and (not V0A)) (not V1B))))) % 0.55/0.75 FOF formula (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) of role axiom named thm_2Ereal__topology_2EBALL__SUBSET__CBALL % 0.55/0.75 A new axiom: (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) % 0.55/0.75 FOF formula (forall (V0s:(mono_2Etyop_2Erealax_2Ereal->Prop)) (V1t:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal V0s) V1t))->(mono_2Ec_2Ereal__topology_2Ebounded__def V0s))) of role axiom named thm_2Ereal__topology_2EBOUNDED__SUBSET % 0.55/0.75 A new axiom: (forall (V0s:(mono_2Etyop_2Erealax_2Ereal->Prop)) (V1t:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal V0s) V1t))->(mono_2Ec_2Ereal__topology_2Ebounded__def V0s))) % 0.55/0.75 FOF formula (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) of role axiom named thm_2Ereal__topology_2EBOUNDED__CBALL % 0.55/0.75 A new axiom: (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) % 0.55/0.75 FOF formula (forall (V0t:Prop), ((iff (not (not V0t))) V0t)) of role axiom named thm_2Esat_2ENOT__NOT % 0.55/0.75 A new axiom: (forall (V0t:Prop), ((iff (not (not V0t))) V0t)) % 0.61/0.76 FOF formula (forall (V0A:Prop), (V0A->((not V0A)->mono_2Ec_2Ebool_2EF))) of role axiom named thm_2Esat_2EAND__INV__IMP % 0.61/0.76 A new axiom: (forall (V0A:Prop), (V0A->((not V0A)->mono_2Ec_2Ebool_2EF))) % 0.61/0.76 FOF formula (forall (V0B:Prop) (V1A:Prop), ((iff ((not ((or V1A) V0B))->mono_2Ec_2Ebool_2EF)) ((V1A->mono_2Ec_2Ebool_2EF)->((not V0B)->mono_2Ec_2Ebool_2EF)))) of role axiom named thm_2Esat_2EOR__DUAL2 % 0.61/0.76 A new axiom: (forall (V0B:Prop) (V1A:Prop), ((iff ((not ((or V1A) V0B))->mono_2Ec_2Ebool_2EF)) ((V1A->mono_2Ec_2Ebool_2EF)->((not V0B)->mono_2Ec_2Ebool_2EF)))) % 0.61/0.76 FOF formula (forall (V0B:Prop) (V1A:Prop), ((iff ((not ((or (not V1A)) V0B))->mono_2Ec_2Ebool_2EF)) (V1A->((not V0B)->mono_2Ec_2Ebool_2EF)))) of role axiom named thm_2Esat_2EOR__DUAL3 % 0.61/0.76 A new axiom: (forall (V0B:Prop) (V1A:Prop), ((iff ((not ((or (not V1A)) V0B))->mono_2Ec_2Ebool_2EF)) (V1A->((not V0B)->mono_2Ec_2Ebool_2EF)))) % 0.61/0.76 FOF formula (forall (V0A:Prop), (((not V0A)->mono_2Ec_2Ebool_2EF)->((V0A->mono_2Ec_2Ebool_2EF)->mono_2Ec_2Ebool_2EF))) of role axiom named thm_2Esat_2EAND__INV2 % 0.61/0.76 A new axiom: (forall (V0A:Prop), (((not V0A)->mono_2Ec_2Ebool_2EF)->((V0A->mono_2Ec_2Ebool_2EF)->mono_2Ec_2Ebool_2EF))) % 0.61/0.76 FOF formula (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) (((eq Prop) V1q) V0r))) ((and ((and ((and ((or ((or V2p) V1q)) V0r)) ((or ((or V2p) (not V0r))) (not V1q)))) ((or ((or V1q) (not V0r))) (not V2p)))) ((or ((or V0r) (not V1q))) (not V2p))))) of role axiom named thm_2Esat_2Edc__eq % 0.61/0.76 A new axiom: (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) (((eq Prop) V1q) V0r))) ((and ((and ((and ((or ((or V2p) V1q)) V0r)) ((or ((or V2p) (not V0r))) (not V1q)))) ((or ((or V1q) (not V0r))) (not V2p)))) ((or ((or V0r) (not V1q))) (not V2p))))) % 0.61/0.76 FOF formula (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) ((and V1q) V0r))) ((and ((and ((or ((or V2p) (not V1q))) (not V0r))) ((or V1q) (not V2p)))) ((or V0r) (not V2p))))) of role axiom named thm_2Esat_2Edc__conj % 0.61/0.76 A new axiom: (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) ((and V1q) V0r))) ((and ((and ((or ((or V2p) (not V1q))) (not V0r))) ((or V1q) (not V2p)))) ((or V0r) (not V2p))))) % 0.61/0.76 FOF formula (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) ((or V1q) V0r))) ((and ((and ((or V2p) (not V1q))) ((or V2p) (not V0r)))) ((or ((or V1q) V0r)) (not V2p))))) of role axiom named thm_2Esat_2Edc__disj % 0.61/0.76 A new axiom: (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) ((or V1q) V0r))) ((and ((and ((or V2p) (not V1q))) ((or V2p) (not V0r)))) ((or ((or V1q) V0r)) (not V2p))))) % 0.61/0.76 FOF formula (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) (V1q->V0r))) ((and ((and ((or V2p) V1q)) ((or V2p) (not V0r)))) ((or ((or (not V1q)) V0r)) (not V2p))))) of role axiom named thm_2Esat_2Edc__imp % 0.61/0.76 A new axiom: (forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) (V1q->V0r))) ((and ((and ((or V2p) V1q)) ((or V2p) (not V0r)))) ((or ((or (not V1q)) V0r)) (not V2p))))) % 0.61/0.76 FOF formula (forall (V0q:Prop) (V1p:Prop), ((iff ((iff V1p) (not V0q))) ((and ((or V1p) V0q)) ((or (not V0q)) (not V1p))))) of role axiom named thm_2Esat_2Edc__neg % 0.61/0.76 A new axiom: (forall (V0q:Prop) (V1p:Prop), ((iff ((iff V1p) (not V0q))) ((and ((or V1p) V0q)) ((or (not V0q)) (not V1p))))) % 0.61/0.76 FOF formula (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) of role conjecture named thm_2Ereal__topology_2EBOUNDED__BALL % 0.61/0.76 Conjecture to prove = (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))):Prop % 0.61/0.76 Parameter du_DUMMY:du. % 0.61/0.76 Parameter mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_DUMMY:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29. % 0.61/0.76 Parameter mono_2Etyop_2Erealax_2Ereal_DUMMY:mono_2Etyop_2Erealax_2Ereal. % 0.61/0.76 We need to prove ['(forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))))'] % 0.61/0.76 Parameter u:Type. % 0.61/0.76 Parameter d:Type. % 0.61/0.76 Parameter du:Type. % 0.61/0.76 Parameter mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:Type. % 0.61/0.76 Parameter mono_2Etyop_2Erealax_2Ereal:Type. % 0.61/0.76 Parameter tyop_2Emin_2Ebool:d. % 0.61/0.76 Parameter tyop_2Emin_2Efun:(d->(d->d)). % 0.61/0.76 Parameter tyop_2Epair_2Eprod:(d->(d->d)). % 0.61/0.76 Parameter tyop_2Erealax_2Ereal:d. % 0.61/0.76 Parameter s:(d->(u->du)). % 0.61/0.76 Parameter app_2E2:(du->(du->u)). % 0.61/0.76 Parameter combin_i_2E0:u. % 0.61/0.76 Parameter combin_k_2E0:u. % 0.61/0.76 Parameter combin_s_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_21_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_21_2E1:(du->u). % 0.61/0.76 Parameter c_2Epair_2E_2C_2E0:u. % 0.61/0.76 Parameter c_2Epair_2E_2C_2E2:(du->(du->u)). % 0.61/0.76 Parameter c_2Ebool_2E_2F_5C_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_2F_5C_2E2:(du->(du->u)). % 0.61/0.76 Parameter c_2Emin_2E_3D_2E0:u. % 0.61/0.76 Parameter c_2Emin_2E_3D_2E2:(du->(du->u)). % 0.61/0.76 Parameter c_2Emin_2E_3D_3D_3E_2E0:u. % 0.61/0.76 Parameter c_2Emin_2E_3D_3D_3E_2E2:(du->(du->u)). % 0.61/0.76 Parameter c_2Ebool_2E_3F_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_3F_2E1:(du->u). % 0.61/0.76 Parameter c_2Ebool_2EF_2E0:u. % 0.61/0.76 Parameter c_2Epred__set_2ESUBSET_2E0:u. % 0.61/0.76 Parameter c_2Epred__set_2ESUBSET_2E2:(du->(du->u)). % 0.61/0.76 Parameter c_2Ebool_2ET_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_5C_2F_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_5C_2F_2E2:(du->(du->u)). % 0.61/0.76 Parameter c_2Ereal__topology_2Eball_2E0:u. % 0.61/0.76 Parameter c_2Ereal__topology_2Eball_2E1:(du->u). % 0.61/0.76 Parameter c_2Ereal__topology_2Ebounded__def_2E0:u. % 0.61/0.76 Parameter c_2Ereal__topology_2Ebounded__def_2E1:(du->u). % 0.61/0.76 Parameter c_2Ereal__topology_2Ecball_2E0:u. % 0.61/0.76 Parameter c_2Ereal__topology_2Ecball_2E1:(du->u). % 0.61/0.76 Parameter c_2Ebool_2E_7E_2E0:u. % 0.61/0.76 Parameter c_2Ebool_2E_7E_2E1:(du->u). % 0.61/0.76 Parameter mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool:((Prop->Prop)->(Prop->Prop)). % 0.61/0.76 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.61/0.76 Parameter mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool:(((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)). % 0.61/0.76 Parameter mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))->((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))). % 0.61/0.76 Parameter mono_2Eapp_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:((mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))->(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))). % 0.61/0.76 Parameter mono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:((mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))->(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))). % 0.61/0.76 Parameter mono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:((mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)). % 0.61/0.76 Parameter mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)). % 0.61/0.76 Parameter mono_2Ec_2Ebool_2E_2F_5C:(Prop->(Prop->Prop)). % 0.61/0.76 Parameter mono_2Ec_2Emin_2E_3D_3D_3E:(Prop->(Prop->Prop)). % 0.61/0.76 Parameter mono_2Ec_2Ebool_2EF:Prop. % 0.61/0.76 Parameter mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)). % 0.61/0.76 Parameter mono_2Ec_2Ebool_2ET:Prop. % 0.61/0.76 Parameter mono_2Ec_2Ebool_2E_5C_2F:(Prop->(Prop->Prop)). % 0.61/0.76 Parameter mono_2Ec_2Ereal__topology_2Eball:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop)). % 0.61/0.76 Parameter mono_2Ec_2Ereal__topology_2Ebounded__def:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop). % 0.61/0.76 Parameter mono_2Ec_2Ereal__topology_2Ecball:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop)). % 0.61/0.76 Parameter mono_2Ec_2Ebool_2E_7E:(Prop->Prop). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Ebool:(Prop->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:((Prop->Prop)->u). % 0.61/0.76 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.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29:(((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29:((mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:((mono_2Etyop_2Erealax_2Ereal->Prop)->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29:((mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:((mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->u). % 0.61/0.76 Parameter i_mono_2Etyop_2Erealax_2Ereal:(mono_2Etyop_2Erealax_2Ereal->u). % 0.61/0.76 Parameter j_mono_2Etyop_2Emin_2Ebool:(du->Prop). % 0.61/0.76 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29:(du->(Prop->Prop)). % 0.61/0.76 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.61/0.76 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(du->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)). % 0.61/0.76 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29:(du->((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))). % 0.61/0.76 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29:(du->(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))). % 0.61/0.76 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:(du->(mono_2Etyop_2Erealax_2Ereal->Prop)). % 0.61/0.76 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29:(du->(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))). % 0.61/0.77 Parameter j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:(du->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)). % 0.61/0.77 Parameter j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(du->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29). % 0.61/0.77 Parameter j_mono_2Etyop_2Erealax_2Ereal:(du->mono_2Etyop_2Erealax_2Ereal). % 0.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 Axiom reserved_2Elogic_2E_2F_5C:(forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_2F_5C V0) V1)) ((and V0) V1))). % 0.61/0.77 Axiom reserved_2Elogic_2E_5C_2F:(forall (V0:Prop) (V1:Prop), ((iff ((mono_2Ec_2Ebool_2E_5C_2F V0) V1)) ((or V0) V1))). % 0.61/0.77 Axiom reserved_2Elogic_2E_7E:(forall (V0:Prop), ((iff (mono_2Ec_2Ebool_2E_7E V0)) (not V0))). % 0.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) V0_2E0))))) ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) V0_2E0))))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(forall (V0_2E0:u), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 (j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) V0_2E0))))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) V0_2E0))). % 0.61/0.77 Axiom ij_2Emono_2Etyop_2Erealax_2Ereal:(forall (V0_2E0:u), (((eq du) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal (j_mono_2Etyop_2Erealax_2Ereal ((s tyop_2Erealax_2Ereal) V0_2E0))))) ((s tyop_2Erealax_2Ereal) V0_2E0))). % 0.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29:(forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29:(forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))), (((eq (mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq (mono_2Etyop_2Erealax_2Ereal->Prop)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))), (((eq (mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)), (((eq (mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (j_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(forall (V0:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) (j_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 V0)))) V0)). % 0.61/0.77 Axiom ji_2Emono_2Etyop_2Erealax_2Ereal:(forall (V0:mono_2Etyop_2Erealax_2Ereal), (((eq mono_2Etyop_2Erealax_2Ereal) (j_mono_2Etyop_2Erealax_2Ereal ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V0)))) V0)). % 0.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 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.61/0.77 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool:(forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->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_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))). % 0.61/0.77 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))). % 0.61/0.77 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:(forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (V1:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((app_2E2 ((s ((tyop_2Emin_2Efun ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_29 V0))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 V1)))))). % 0.61/0.77 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 (V0 V1)))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))). % 0.61/0.77 Axiom monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 (V0 V1)))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((app_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29 V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))). % 0.61/0.77 Axiom monoeq_2Emono_2Ec_2Epair_2E_2C_2E0_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal:(((eq du) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29_29 mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)))) c_2Epair_2E_2C_2E0)). % 0.61/0.77 Axiom monoeq_2Emono_2Ec_2Epair_2E_2C_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal:(forall (V0:mono_2Etyop_2Erealax_2Ereal) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq du) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) (i_mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29 ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0) V1)))) ((s ((tyop_2Epair_2Eprod tyop_2Erealax_2Ereal) tyop_2Erealax_2Ereal)) ((c_2Epair_2E_2C_2E2 ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V0))) ((s tyop_2Erealax_2Ereal) (i_mono_2Etyop_2Erealax_2Ereal V1)))))). % 0.61/0.77 Axiom monoeq_2Emono_2Ec_2Epred__set_2ESUBSET_2E0_2Emono_2Etyop_2Erealax_2Ereal:(((eq du) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal))) ((s ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) ((tyop_2Emin_2Efun ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) tyop_2Emin_2Ebool))) c_2Epred__set_2ESUBSET_2E0)). % 0.61/0.77 Axiom monoeq_2Emono_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2Etyop_2Erealax_2Ereal:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq du) ((s tyop_2Emin_2Ebool) (i_mono_2Etyop_2Emin_2Ebool ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal V0) V1)))) ((s tyop_2Emin_2Ebool) ((c_2Epred__set_2ESUBSET_2E2 ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V0))) ((s ((tyop_2Emin_2Efun tyop_2Erealax_2Ereal) tyop_2Emin_2Ebool)) (i_mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29 V1)))))). % 0.61/0.77 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.61/0.77 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.61/0.77 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool:(forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq Prop) (V0 V1)) (V0 V1))). % 0.61/0.77 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29:(forall (V0:((mono_2Etyop_2Erealax_2Ereal->Prop)->((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop))) (V1:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((eq ((mono_2Etyop_2Erealax_2Ereal->Prop)->Prop)) (V0 V1)) (V0 V1))). % 0.61/0.77 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Emin_2Ebool_29:(forall (V0:(mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29->(mono_2Etyop_2Erealax_2Ereal->Prop))) (V1:mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29), (((eq (mono_2Etyop_2Erealax_2Ereal->Prop)) (V0 V1)) (V0 V1))). % 0.61/0.77 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Emin_2Efun_28tyop_2Erealax_2Ereal_2Ctyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29))) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq (mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V0 V1)) (V0 V1))). % 0.61/0.77 Axiom monoapp_2Emono_2Eapp_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29:(forall (V0:(mono_2Etyop_2Erealax_2Ereal->mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29)) (V1:mono_2Etyop_2Erealax_2Ereal), (((eq mono_2Etyop_2Epair_2Eprod_28tyop_2Erealax_2Ereal_2Ctyop_2Erealax_2Ereal_29) (V0 V1)) (V0 V1))). % 0.61/0.77 Axiom thm_2Ebool_2ETRUTH:mono_2Ec_2Ebool_2ET. % 0.61/0.77 Axiom thm_2Ebool_2EIMP__ANTISYM__AX:(forall (V0t1:Prop) (V1t2:Prop), ((V0t1->V1t2)->((V1t2->V0t1)->(((eq Prop) V0t1) V1t2)))). % 0.61/0.77 Axiom thm_2Ebool_2EIMP__F:(forall (V0t:Prop), ((V0t->mono_2Ec_2Ebool_2EF)->(not V0t))). % 0.61/0.77 Axiom thm_2Ebool_2EF__IMP:(forall (V0t:Prop), ((not V0t)->(V0t->mono_2Ec_2Ebool_2EF))). % 0.61/0.77 Axiom thm_2Ebool_2EIMP__CLAUSES:(forall (V0t:Prop), ((and ((and ((and ((and ((iff (mono_2Ec_2Ebool_2ET->V0t)) V0t)) ((iff (V0t->mono_2Ec_2Ebool_2ET)) mono_2Ec_2Ebool_2ET))) ((iff (mono_2Ec_2Ebool_2EF->V0t)) mono_2Ec_2Ebool_2ET))) ((iff (V0t->V0t)) mono_2Ec_2Ebool_2ET))) ((iff (V0t->mono_2Ec_2Ebool_2EF)) (not V0t)))). % 0.61/0.77 Axiom thm_2Ebool_2ENOT__CLAUSES:((and ((and (forall (V0t:Prop), ((iff (not (not V0t))) V0t))) ((iff (not mono_2Ec_2Ebool_2ET)) mono_2Ec_2Ebool_2EF))) ((iff (not mono_2Ec_2Ebool_2EF)) mono_2Ec_2Ebool_2ET)). % 0.61/0.77 Axiom thm_2Ebool_2EEQ__SYM__EQ:(forall (A_27a:d) (V0x_2E0:u) (V1y_2E0:u), ((iff (((eq du) ((s A_27a) V0x_2E0)) ((s A_27a) V1y_2E0))) (((eq du) ((s A_27a) V1y_2E0)) ((s A_27a) V0x_2E0)))). % 0.61/0.77 Axiom thm_2Ebool_2EEQ__CLAUSES:(forall (V0t:Prop), ((and ((and ((and ((iff (((eq Prop) mono_2Ec_2Ebool_2ET) V0t)) V0t)) ((iff (((eq Prop) V0t) mono_2Ec_2Ebool_2ET)) V0t))) ((iff (((eq Prop) mono_2Ec_2Ebool_2EF) V0t)) (not V0t)))) ((iff (((eq Prop) V0t) mono_2Ec_2Ebool_2EF)) (not V0t)))). % 0.61/0.77 Axiom thm_2Ebool_2ENOT__FORALL__THM:(forall (A_27a:d) (V0P_2E0:u), ((iff (not (forall (V1x_2E0:u), (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0P_2E0)) ((s A_27a) V1x_2E0))))))) ((ex u) (fun (V2x_2E0:u)=> (not (j_mono_2Etyop_2Emin_2Ebool ((s tyop_2Emin_2Ebool) ((app_2E2 ((s ((tyop_2Emin_2Efun A_27a) tyop_2Emin_2Ebool)) V0P_2E0)) ((s A_27a) V2x_2E0))))))))). % 0.61/0.77 Axiom thm_2Ebool_2EDISJ__ASSOC:(forall (V0A:Prop) (V1B:Prop) (V2C:Prop), ((iff ((or ((or V0A) V1B)) V2C)) ((or ((or V0A) V1B)) V2C))). % 0.61/0.77 Axiom thm_2Ebool_2EDISJ__SYM:(forall (V0A:Prop) (V1B:Prop), ((iff ((or V0A) V1B)) ((or V1B) V0A))). % 0.61/0.77 Axiom thm_2Ebool_2EDE__MORGAN__THM:(forall (V0A:Prop) (V1B:Prop), ((and ((iff (not ((and V0A) V1B))) ((or (not V0A)) (not V1B)))) ((iff (not ((or V0A) V1B))) ((and (not V0A)) (not V1B))))). % 0.61/0.77 Axiom thm_2Ereal__topology_2EBALL__SUBSET__CBALL:(forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))). % 0.85/1.02 Axiom thm_2Ereal__topology_2EBOUNDED__SUBSET:(forall (V0s:(mono_2Etyop_2Erealax_2Ereal->Prop)) (V1t:(mono_2Etyop_2Erealax_2Ereal->Prop)), (((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal V0s) V1t))->(mono_2Ec_2Ereal__topology_2Ebounded__def V0s))). % 0.85/1.02 Axiom thm_2Ereal__topology_2EBOUNDED__CBALL:(forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))). % 0.85/1.02 Axiom thm_2Esat_2ENOT__NOT:(forall (V0t:Prop), ((iff (not (not V0t))) V0t)). % 0.85/1.02 Axiom thm_2Esat_2EAND__INV__IMP:(forall (V0A:Prop), (V0A->((not V0A)->mono_2Ec_2Ebool_2EF))). % 0.85/1.02 Axiom thm_2Esat_2EOR__DUAL2:(forall (V0B:Prop) (V1A:Prop), ((iff ((not ((or V1A) V0B))->mono_2Ec_2Ebool_2EF)) ((V1A->mono_2Ec_2Ebool_2EF)->((not V0B)->mono_2Ec_2Ebool_2EF)))). % 0.85/1.02 Axiom thm_2Esat_2EOR__DUAL3:(forall (V0B:Prop) (V1A:Prop), ((iff ((not ((or (not V1A)) V0B))->mono_2Ec_2Ebool_2EF)) (V1A->((not V0B)->mono_2Ec_2Ebool_2EF)))). % 0.85/1.02 Axiom thm_2Esat_2EAND__INV2:(forall (V0A:Prop), (((not V0A)->mono_2Ec_2Ebool_2EF)->((V0A->mono_2Ec_2Ebool_2EF)->mono_2Ec_2Ebool_2EF))). % 0.85/1.02 Axiom thm_2Esat_2Edc__eq:(forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) (((eq Prop) V1q) V0r))) ((and ((and ((and ((or ((or V2p) V1q)) V0r)) ((or ((or V2p) (not V0r))) (not V1q)))) ((or ((or V1q) (not V0r))) (not V2p)))) ((or ((or V0r) (not V1q))) (not V2p))))). % 0.85/1.02 Axiom thm_2Esat_2Edc__conj:(forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) ((and V1q) V0r))) ((and ((and ((or ((or V2p) (not V1q))) (not V0r))) ((or V1q) (not V2p)))) ((or V0r) (not V2p))))). % 0.85/1.02 Axiom thm_2Esat_2Edc__disj:(forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) ((or V1q) V0r))) ((and ((and ((or V2p) (not V1q))) ((or V2p) (not V0r)))) ((or ((or V1q) V0r)) (not V2p))))). % 0.85/1.02 Axiom thm_2Esat_2Edc__imp:(forall (V0r:Prop) (V1q:Prop) (V2p:Prop), ((iff ((iff V2p) (V1q->V0r))) ((and ((and ((or V2p) V1q)) ((or V2p) (not V0r)))) ((or ((or (not V1q)) V0r)) (not V2p))))). % 0.85/1.02 Axiom thm_2Esat_2Edc__neg:(forall (V0q:Prop) (V1p:Prop), ((iff ((iff V1p) (not V0q))) ((and ((or V1p) V0q)) ((or (not V0q)) (not V1p))))). % 0.85/1.02 Trying to prove (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) % 0.85/1.02 Found thm_2Ereal__topology_2EBALL__SUBSET__CBALL00:=(thm_2Ereal__topology_2EBALL__SUBSET__CBALL0 V1e):((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) % 0.85/1.02 Found (thm_2Ereal__topology_2EBALL__SUBSET__CBALL0 V1e) as proof of ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t) % 0.85/1.02 Found ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e) as proof of ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t) % 0.85/1.02 Found ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e) as proof of ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t) % 0.85/1.02 Found ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e) as proof of ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t) % 0.85/1.06 Found thm_2Ereal__topology_2EBOUNDED__CBALL00:=(thm_2Ereal__topology_2EBOUNDED__CBALL0 V1e):(mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) % 0.85/1.06 Found (thm_2Ereal__topology_2EBOUNDED__CBALL0 V1e) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def V1t) % 0.85/1.06 Found ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def V1t) % 0.85/1.06 Found ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def V1t) % 0.85/1.06 Found ((conj00 ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)) as proof of ((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) % 0.85/1.06 Found (((conj0 ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)) as proof of ((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) % 0.85/1.06 Found ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)) as proof of ((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) % 0.85/1.06 Found ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)) as proof of ((and (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) % 0.85/1.06 Found (thm_2Ereal__topology_2EBOUNDED__SUBSET00 ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def V1t)) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) V1t)) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e))) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) % 0.85/1.06 Found ((thm_2Ereal__topology_2EBOUNDED__SUBSET0 (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e))) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) % 0.85/1.06 Found (((thm_2Ereal__topology_2EBOUNDED__SUBSET (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e))) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) % 0.85/1.06 Found (fun (V1e:mono_2Etyop_2Erealax_2Ereal)=> (((thm_2Ereal__topology_2EBOUNDED__SUBSET (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)))) as proof of (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) % 0.85/1.06 Found (fun (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal)=> (((thm_2Ereal__topology_2EBOUNDED__SUBSET (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)))) as proof of (forall (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) % 0.85/1.06 Found (fun (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal)=> (((thm_2Ereal__topology_2EBOUNDED__SUBSET (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)))) as proof of (forall (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal), (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) % 0.85/1.06 Got proof (fun (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal)=> (((thm_2Ereal__topology_2EBOUNDED__SUBSET (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)))) % 0.85/1.06 Time elapsed = 0.271368s % 0.85/1.06 node=72 cost=444.000000 depth=12 % 0.85/1.06:::::::::::::::::::::: % 0.85/1.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.85/1.06 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.85/1.06 (fun (V0x:mono_2Etyop_2Erealax_2Ereal) (V1e:mono_2Etyop_2Erealax_2Ereal)=> (((thm_2Ereal__topology_2EBOUNDED__SUBSET (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) ((((conj (mono_2Ec_2Ereal__topology_2Ebounded__def (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((mono_2Ec_2Epred__set_2ESUBSET_2Emono_2Etyop_2Erealax_2Ereal (mono_2Ec_2Ereal__topology_2Eball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e))) (mono_2Ec_2Ereal__topology_2Ecball ((mono_2Ec_2Epair_2E_2C_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal V0x) V1e)))) ((thm_2Ereal__topology_2EBOUNDED__CBALL V0x) V1e)) ((thm_2Ereal__topology_2EBALL__SUBSET__CBALL V0x) V1e)))) % 0.85/1.06 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------