%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : ITP001^5 : TPTP v7.5.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n024.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:28 EDT 2021 % Result : Theorem 0.58s % Output : Proof 0.58s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : ITP001^5 : TPTP v7.5.0. Bugfixed v7.5.0. % 0.03/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.32 % Computer : n024.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % DateTime : Thu Mar 18 19:11:30 EDT 2021 % 0.11/0.32 % CPUTime : % 0.11/0.33 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.11/0.34 Python 2.7.5 % 0.39/0.62 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.39/0.62 Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/ITP001/ITP001^2.ax, trying next directory % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcac68>, <kernel.Type object at 0xbcabd8>) of role type named del_tp % 0.39/0.62 Using role type % 0.39/0.62 Declaring del:Type % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbca200>, <kernel.Constant object at 0xbcafc8>) of role type named bool % 0.39/0.62 Using role type % 0.39/0.62 Declaring bool:del % 0.39/0.62 FOF formula (<kernel.Constant object at 0x2af8cb63d1b8>, <kernel.Constant object at 0xbcafc8>) of role type named ind % 0.39/0.62 Using role type % 0.39/0.62 Declaring ind:del % 0.39/0.62 FOF formula (<kernel.Constant object at 0x2af8cb63d1b8>, <kernel.DependentProduct object at 0xbca200>) of role type named arr % 0.39/0.62 Using role type % 0.39/0.62 Declaring arr:(del->(del->del)) % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcafc8>, <kernel.DependentProduct object at 0xbad908>) of role type named mem % 0.39/0.62 Using role type % 0.39/0.62 Declaring mem:(fofType->(del->Prop)) % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcabd8>, <kernel.DependentProduct object at 0xbad5f0>) of role type named ap % 0.39/0.62 Using role type % 0.39/0.62 Declaring ap:(fofType->(fofType->fofType)) % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcaef0>, <kernel.DependentProduct object at 0xbade18>) of role type named lam % 0.39/0.62 Using role type % 0.39/0.62 Declaring lam:(del->((fofType->fofType)->fofType)) % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcafc8>, <kernel.DependentProduct object at 0xbad908>) of role type named p % 0.39/0.62 Using role type % 0.39/0.62 Declaring p:(fofType->Prop) % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcaef0>, <kernel.DependentProduct object at 0xbad950>) of role type named stp_inj_o % 0.39/0.62 Using role type % 0.39/0.62 Declaring inj__o:(Prop->fofType) % 0.39/0.62 FOF formula (forall (X:Prop), (((eq Prop) (p (inj__o X))) X)) of role axiom named stp_inj_surj_o % 0.39/0.62 A new axiom: (forall (X:Prop), (((eq Prop) (p (inj__o X))) X)) % 0.39/0.62 FOF formula (forall (X:Prop), ((mem (inj__o X)) bool)) of role axiom named stp_inj_mem_o % 0.39/0.62 A new axiom: (forall (X:Prop), ((mem (inj__o X)) bool)) % 0.39/0.62 FOF formula (forall (X:fofType), (((mem X) bool)->(((eq fofType) X) (inj__o (p X))))) of role axiom named stp_iso_mem_o % 0.39/0.62 A new axiom: (forall (X:fofType), (((mem X) bool)->(((eq fofType) X) (inj__o (p X))))) % 0.39/0.62 FOF formula (forall (A:del) (B:del) (F:fofType), (((mem F) ((arr A) B))->(forall (X:fofType), (((mem X) A)->((mem ((ap F) X)) B))))) of role axiom named ap_tp % 0.39/0.62 A new axiom: (forall (A:del) (B:del) (F:fofType), (((mem F) ((arr A) B))->(forall (X:fofType), (((mem X) A)->((mem ((ap F) X)) B))))) % 0.39/0.62 FOF formula (forall (A:del) (B:del) (F:(fofType->fofType)), ((forall (X:fofType), (((mem X) A)->((mem (F X)) B)))->((mem ((lam A) F)) ((arr A) B)))) of role axiom named lam_tp % 0.39/0.62 A new axiom: (forall (A:del) (B:del) (F:(fofType->fofType)), ((forall (X:fofType), (((mem X) A)->((mem (F X)) B)))->((mem ((lam A) F)) ((arr A) B)))) % 0.39/0.62 FOF formula (forall (A:del) (B:del) (F:fofType), (((mem F) ((arr A) B))->(forall (G:fofType), (((mem G) ((arr A) B))->((forall (X:fofType), (((mem X) A)->(((eq fofType) ((ap F) X)) ((ap G) X))))->(((eq fofType) F) G)))))) of role axiom named funcext % 0.39/0.62 A new axiom: (forall (A:del) (B:del) (F:fofType), (((mem F) ((arr A) B))->(forall (G:fofType), (((mem G) ((arr A) B))->((forall (X:fofType), (((mem X) A)->(((eq fofType) ((ap F) X)) ((ap G) X))))->(((eq fofType) F) G)))))) % 0.39/0.62 FOF formula (forall (A:del) (F:(fofType->fofType)) (X:fofType), (((mem X) A)->(((eq fofType) ((ap ((lam A) F)) X)) (F X)))) of role axiom named beta % 0.39/0.62 A new axiom: (forall (A:del) (F:(fofType->fofType)) (X:fofType), (((mem X) A)->(((eq fofType) ((ap ((lam A) F)) X)) (F X)))) % 0.39/0.62 Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/ITP001/ITP002^5.ax, trying next directory % 0.39/0.62 FOF formula (<kernel.Constant object at 0xbcaf38>, <kernel.DependentProduct object at 0xbad950>) of role type named tp_c_2Emin_2E_3D % 0.39/0.62 Using role type % 0.39/0.62 Declaring c_2Emin_2E_3D:(del->fofType) % 0.39/0.62 FOF formula (forall (A_27a:del), ((mem (c_2Emin_2E_3D A_27a)) ((arr A_27a) ((arr A_27a) bool)))) of role axiom named mem_c_2Emin_2E_3D % 0.39/0.62 A new axiom: (forall (A_27a:del), ((mem (c_2Emin_2E_3D A_27a)) ((arr A_27a) ((arr A_27a) bool)))) % 0.47/0.63 FOF formula (forall (A:del) (X:fofType), (((mem X) A)->(forall (Y:fofType), (((mem Y) A)->((iff (p ((ap ((ap (c_2Emin_2E_3D A)) X)) Y))) (((eq fofType) X) Y)))))) of role axiom named ax_eq_p % 0.47/0.63 A new axiom: (forall (A:del) (X:fofType), (((mem X) A)->(forall (Y:fofType), (((mem Y) A)->((iff (p ((ap ((ap (c_2Emin_2E_3D A)) X)) Y))) (((eq fofType) X) Y)))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0xbcae18>, <kernel.Single object at 0xbcaf38>) of role type named tp_c_2Emin_2E_3D_3D_3E % 0.47/0.63 Using role type % 0.47/0.63 Declaring c_2Emin_2E_3D_3D_3E:fofType % 0.47/0.63 FOF formula ((mem c_2Emin_2E_3D_3D_3E) ((arr bool) ((arr bool) bool))) of role axiom named mem_c_2Emin_2E_3D_3D_3E % 0.47/0.63 A new axiom: ((mem c_2Emin_2E_3D_3D_3E) ((arr bool) ((arr bool) bool))) % 0.47/0.63 FOF formula (forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Emin_2E_3D_3D_3E) Q)) R))) ((p Q)->(p R))))))) of role axiom named ax_imp_p % 0.47/0.63 A new axiom: (forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Emin_2E_3D_3D_3E) Q)) R))) ((p Q)->(p R))))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0xbcabd8>, <kernel.DependentProduct object at 0xbadc68>) of role type named tp_c_2Emin_2E_40 % 0.47/0.63 Using role type % 0.47/0.63 Declaring c_2Emin_2E_40:(del->fofType) % 0.47/0.63 FOF formula (forall (A_27a:del), ((mem (c_2Emin_2E_40 A_27a)) ((arr ((arr A_27a) bool)) A_27a))) of role axiom named mem_c_2Emin_2E_40 % 0.47/0.63 A new axiom: (forall (A_27a:del), ((mem (c_2Emin_2E_40 A_27a)) ((arr ((arr A_27a) bool)) A_27a))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0xe72a70>, <kernel.DependentProduct object at 0x2af8cb63a0e0>) of role type named tp_ty_2Ebool_2Eitself % 0.47/0.63 Using role type % 0.47/0.63 Declaring ty_2Ebool_2Eitself:(del->del) % 0.47/0.63 FOF formula (<kernel.Constant object at 0xe72a70>, <kernel.DependentProduct object at 0x2af8cb63a560>) of role type named tp_c_2Ebool_2E_21 % 0.47/0.63 Using role type % 0.47/0.63 Declaring c_2Ebool_2E_21:(del->fofType) % 0.47/0.63 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2E_21 A_27a)) ((arr ((arr A_27a) bool)) bool))) of role axiom named mem_c_2Ebool_2E_21 % 0.47/0.63 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2E_21 A_27a)) ((arr ((arr A_27a) bool)) bool))) % 0.47/0.63 FOF formula (forall (A:del) (Q:fofType), (((mem Q) ((arr A) bool))->((iff (p ((ap (c_2Ebool_2E_21 A)) Q))) (forall (X:fofType), (((mem X) A)->(p ((ap Q) X))))))) of role axiom named ax_all_p % 0.47/0.63 A new axiom: (forall (A:del) (Q:fofType), (((mem Q) ((arr A) bool))->((iff (p ((ap (c_2Ebool_2E_21 A)) Q))) (forall (X:fofType), (((mem X) A)->(p ((ap Q) X))))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0xbd4ea8>, <kernel.Single object at 0x2af8cb63a878>) of role type named tp_c_2Ebool_2E_2F_5C % 0.47/0.63 Using role type % 0.47/0.63 Declaring c_2Ebool_2E_2F_5C:fofType % 0.47/0.63 FOF formula ((mem c_2Ebool_2E_2F_5C) ((arr bool) ((arr bool) bool))) of role axiom named mem_c_2Ebool_2E_2F_5C % 0.47/0.63 A new axiom: ((mem c_2Ebool_2E_2F_5C) ((arr bool) ((arr bool) bool))) % 0.47/0.63 FOF formula (forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Ebool_2E_2F_5C) Q)) R))) ((and (p Q)) (p R))))))) of role axiom named ax_and_p % 0.47/0.63 A new axiom: (forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Ebool_2E_2F_5C) Q)) R))) ((and (p Q)) (p R))))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x2af8cb63a488>, <kernel.DependentProduct object at 0x2af8cb63a560>) of role type named tp_c_2Ebool_2E_3F % 0.47/0.63 Using role type % 0.47/0.63 Declaring c_2Ebool_2E_3F:(del->fofType) % 0.47/0.63 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2E_3F A_27a)) ((arr ((arr A_27a) bool)) bool))) of role axiom named mem_c_2Ebool_2E_3F % 0.47/0.63 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2E_3F A_27a)) ((arr ((arr A_27a) bool)) bool))) % 0.47/0.63 FOF formula (forall (A:del) (Q:fofType), (((mem Q) ((arr A) bool))->((iff (p ((ap (c_2Ebool_2E_3F A)) Q))) ((ex fofType) (fun (X:fofType)=> ((and ((mem X) A)) (p ((ap Q) X)))))))) of role axiom named ax_ex_p % 0.47/0.63 A new axiom: (forall (A:del) (Q:fofType), (((mem Q) ((arr A) bool))->((iff (p ((ap (c_2Ebool_2E_3F A)) Q))) ((ex fofType) (fun (X:fofType)=> ((and ((mem X) A)) (p ((ap Q) X)))))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x2af8cb63a560>, <kernel.DependentProduct object at 0x2af8cb63a290>) of role type named tp_c_2Ebool_2E_3F_21 % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2E_3F_21:(del->fofType) % 0.47/0.64 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2E_3F_21 A_27a)) ((arr ((arr A_27a) bool)) bool))) of role axiom named mem_c_2Ebool_2E_3F_21 % 0.47/0.64 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2E_3F_21 A_27a)) ((arr ((arr A_27a) bool)) bool))) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63a560>, <kernel.DependentProduct object at 0x2af8cb63fef0>) of role type named tp_c_2Ebool_2EARB % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EARB:(del->fofType) % 0.47/0.64 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2EARB A_27a)) A_27a)) of role axiom named mem_c_2Ebool_2EARB % 0.47/0.64 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2EARB A_27a)) A_27a)) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63a560>, <kernel.Single object at 0x2af8cb63a998>) of role type named tp_c_2Ebool_2EBOUNDED % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EBOUNDED:fofType % 0.47/0.64 FOF formula ((mem c_2Ebool_2EBOUNDED) ((arr bool) bool)) of role axiom named mem_c_2Ebool_2EBOUNDED % 0.47/0.64 A new axiom: ((mem c_2Ebool_2EBOUNDED) ((arr bool) bool)) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63a560>, <kernel.DependentProduct object at 0x2af8cb63fb00>) of role type named tp_c_2Ebool_2ECOND % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2ECOND:(del->fofType) % 0.47/0.64 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2ECOND A_27a)) ((arr bool) ((arr A_27a) ((arr A_27a) A_27a))))) of role axiom named mem_c_2Ebool_2ECOND % 0.47/0.64 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2ECOND A_27a)) ((arr bool) ((arr A_27a) ((arr A_27a) A_27a))))) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63a560>, <kernel.DependentProduct object at 0xbca200>) of role type named tp_c_2Ebool_2EDATATYPE % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EDATATYPE:(del->fofType) % 0.47/0.64 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2EDATATYPE A_27a)) ((arr A_27a) bool))) of role axiom named mem_c_2Ebool_2EDATATYPE % 0.47/0.64 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2EDATATYPE A_27a)) ((arr A_27a) bool))) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63aea8>, <kernel.Single object at 0x2af8cb63fef0>) of role type named tp_c_2Ebool_2EF % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EF:fofType % 0.47/0.64 FOF formula ((mem c_2Ebool_2EF) bool) of role axiom named mem_c_2Ebool_2EF % 0.47/0.64 A new axiom: ((mem c_2Ebool_2EF) bool) % 0.47/0.64 FOF formula ((p c_2Ebool_2EF)->False) of role axiom named ax_false_p % 0.47/0.64 A new axiom: ((p c_2Ebool_2EF)->False) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63fdd0>, <kernel.DependentProduct object at 0xbca200>) of role type named tp_c_2Ebool_2EIN % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EIN:(del->fofType) % 0.47/0.64 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2EIN A_27a)) ((arr A_27a) ((arr ((arr A_27a) bool)) bool)))) of role axiom named mem_c_2Ebool_2EIN % 0.47/0.64 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2EIN A_27a)) ((arr A_27a) ((arr ((arr A_27a) bool)) bool)))) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63fdd0>, <kernel.DependentProduct object at 0xbcabd8>) of role type named tp_c_2Ebool_2ELET % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2ELET:(del->(del->fofType)) % 0.47/0.64 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ELET A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b)))) of role axiom named mem_c_2Ebool_2ELET % 0.47/0.64 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ELET A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b)))) % 0.47/0.64 FOF formula (<kernel.Constant object at 0x2af8cb63fd88>, <kernel.DependentProduct object at 0xbcac20>) of role type named tp_c_2Ebool_2EONE__ONE % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EONE__ONE:(del->(del->fofType)) % 0.47/0.64 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2EONE__ONE A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) bool))) of role axiom named mem_c_2Ebool_2EONE__ONE % 0.47/0.64 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2EONE__ONE A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) bool))) % 0.47/0.64 FOF formula (<kernel.Constant object at 0xbcac20>, <kernel.DependentProduct object at 0xbcaf38>) of role type named tp_c_2Ebool_2EONTO % 0.47/0.64 Using role type % 0.47/0.64 Declaring c_2Ebool_2EONTO:(del->(del->fofType)) % 0.47/0.64 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2EONTO A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) bool))) of role axiom named mem_c_2Ebool_2EONTO % 0.47/0.65 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2EONTO A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) bool))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbcaf38>, <kernel.DependentProduct object at 0xbcaf80>) of role type named tp_c_2Ebool_2ERES__ABSTRACT % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ERES__ABSTRACT:(del->(del->fofType)) % 0.47/0.65 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ERES__ABSTRACT A_27a) A_27b)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b))))) of role axiom named mem_c_2Ebool_2ERES__ABSTRACT % 0.47/0.65 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ERES__ABSTRACT A_27a) A_27b)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b))))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbcaf80>, <kernel.DependentProduct object at 0xbadab8>) of role type named tp_c_2Ebool_2ERES__EXISTS % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ERES__EXISTS:(del->fofType) % 0.47/0.65 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2ERES__EXISTS A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))) of role axiom named mem_c_2Ebool_2ERES__EXISTS % 0.47/0.65 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2ERES__EXISTS A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbad5a8>, <kernel.DependentProduct object at 0xbad638>) of role type named tp_c_2Ebool_2ERES__EXISTS__UNIQUE % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ERES__EXISTS__UNIQUE:(del->fofType) % 0.47/0.65 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2ERES__EXISTS__UNIQUE A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))) of role axiom named mem_c_2Ebool_2ERES__EXISTS__UNIQUE % 0.47/0.65 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2ERES__EXISTS__UNIQUE A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbcacf8>, <kernel.DependentProduct object at 0xbadb48>) of role type named tp_c_2Ebool_2ERES__FORALL % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ERES__FORALL:(del->fofType) % 0.47/0.65 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2ERES__FORALL A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))) of role axiom named mem_c_2Ebool_2ERES__FORALL % 0.47/0.65 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2ERES__FORALL A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbadab8>, <kernel.DependentProduct object at 0xbade18>) of role type named tp_c_2Ebool_2ERES__SELECT % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ERES__SELECT:(del->fofType) % 0.47/0.65 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2ERES__SELECT A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) A_27a)))) of role axiom named mem_c_2Ebool_2ERES__SELECT % 0.47/0.65 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2ERES__SELECT A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) A_27a)))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbada28>, <kernel.Single object at 0xbad950>) of role type named tp_c_2Ebool_2ET % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ET:fofType % 0.47/0.65 FOF formula ((mem c_2Ebool_2ET) bool) of role axiom named mem_c_2Ebool_2ET % 0.47/0.65 A new axiom: ((mem c_2Ebool_2ET) bool) % 0.47/0.65 FOF formula (p c_2Ebool_2ET) of role axiom named ax_true_p % 0.47/0.65 A new axiom: (p c_2Ebool_2ET) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbad5a8>, <kernel.DependentProduct object at 0xbadcb0>) of role type named tp_c_2Ebool_2ETYPE__DEFINITION % 0.47/0.65 Using role type % 0.47/0.65 Declaring c_2Ebool_2ETYPE__DEFINITION:(del->(del->fofType)) % 0.47/0.65 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ETYPE__DEFINITION A_27a) A_27b)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27b) A_27a)) bool)))) of role axiom named mem_c_2Ebool_2ETYPE__DEFINITION % 0.47/0.65 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ETYPE__DEFINITION A_27a) A_27b)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27b) A_27a)) bool)))) % 0.47/0.65 FOF formula (<kernel.Constant object at 0xbadcb0>, <kernel.Single object at 0xbada28>) of role type named tp_c_2Ebool_2E_5C_2F % 0.47/0.65 Using role type % 0.47/0.66 Declaring c_2Ebool_2E_5C_2F:fofType % 0.47/0.66 FOF formula ((mem c_2Ebool_2E_5C_2F) ((arr bool) ((arr bool) bool))) of role axiom named mem_c_2Ebool_2E_5C_2F % 0.47/0.66 A new axiom: ((mem c_2Ebool_2E_5C_2F) ((arr bool) ((arr bool) bool))) % 0.47/0.66 FOF formula (forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Ebool_2E_5C_2F) Q)) R))) ((or (p Q)) (p R))))))) of role axiom named ax_or_p % 0.47/0.66 A new axiom: (forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Ebool_2E_5C_2F) Q)) R))) ((or (p Q)) (p R))))))) % 0.47/0.66 FOF formula (<kernel.Constant object at 0xbadd88>, <kernel.DependentProduct object at 0xbadcf8>) of role type named tp_c_2Ebool_2Eitself__case % 0.47/0.66 Using role type % 0.47/0.66 Declaring c_2Ebool_2Eitself__case:(del->(del->fofType)) % 0.47/0.66 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2Eitself__case A_27a) A_27b)) ((arr (ty_2Ebool_2Eitself A_27a)) ((arr A_27b) A_27b)))) of role axiom named mem_c_2Ebool_2Eitself__case % 0.47/0.66 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2Eitself__case A_27a) A_27b)) ((arr (ty_2Ebool_2Eitself A_27a)) ((arr A_27b) A_27b)))) % 0.47/0.66 FOF formula (<kernel.Constant object at 0xbadd88>, <kernel.DependentProduct object at 0xbcfd40>) of role type named tp_c_2Ebool_2Eliteral__case % 0.47/0.66 Using role type % 0.47/0.66 Declaring c_2Ebool_2Eliteral__case:(del->(del->fofType)) % 0.47/0.66 FOF formula (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2Eliteral__case A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b)))) of role axiom named mem_c_2Ebool_2Eliteral__case % 0.47/0.66 A new axiom: (forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2Eliteral__case A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b)))) % 0.47/0.66 FOF formula (<kernel.Constant object at 0xbadcf8>, <kernel.DependentProduct object at 0xbcfa70>) of role type named tp_c_2Ebool_2Ethe__value % 0.47/0.66 Using role type % 0.47/0.66 Declaring c_2Ebool_2Ethe__value:(del->fofType) % 0.47/0.66 FOF formula (forall (A_27a:del), ((mem (c_2Ebool_2Ethe__value A_27a)) (ty_2Ebool_2Eitself A_27a))) of role axiom named mem_c_2Ebool_2Ethe__value % 0.47/0.66 A new axiom: (forall (A_27a:del), ((mem (c_2Ebool_2Ethe__value A_27a)) (ty_2Ebool_2Eitself A_27a))) % 0.47/0.66 FOF formula (<kernel.Constant object at 0xbadcf8>, <kernel.Single object at 0xbcf128>) of role type named tp_c_2Ebool_2E_7E % 0.47/0.66 Using role type % 0.47/0.66 Declaring c_2Ebool_2E_7E:fofType % 0.47/0.66 FOF formula ((mem c_2Ebool_2E_7E) ((arr bool) bool)) of role axiom named mem_c_2Ebool_2E_7E % 0.47/0.66 A new axiom: ((mem c_2Ebool_2E_7E) ((arr bool) bool)) % 0.47/0.66 FOF formula (forall (Q:fofType), (((mem Q) bool)->((iff (p ((ap c_2Ebool_2E_7E) Q))) ((p Q)->False)))) of role axiom named ax_neg_p % 0.47/0.66 A new axiom: (forall (Q:fofType), (((mem Q) bool)->((iff (p ((ap c_2Ebool_2E_7E) Q))) ((p Q)->False)))) % 0.47/0.66 FOF formula ((iff True) (((eq fofType) ((lam bool) (fun (V0x:fofType)=> V0x))) ((lam bool) (fun (V1x:fofType)=> V1x)))) of role axiom named ax_thm_2Ebool_2ET__DEF % 0.47/0.66 A new axiom: ((iff True) (((eq fofType) ((lam bool) (fun (V0x:fofType)=> V0x))) ((lam bool) (fun (V1x:fofType)=> V1x)))) % 0.47/0.66 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_21 A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap ((ap (c_2Emin_2E_3D ((arr A_27a) bool))) V0P)) ((lam A_27a) (fun (V1x:fofType)=> c_2Ebool_2ET))))))) of role axiom named ax_thm_2Ebool_2EFORALL__DEF % 0.47/0.66 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_21 A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap ((ap (c_2Emin_2E_3D ((arr A_27a) bool))) V0P)) ((lam A_27a) (fun (V1x:fofType)=> c_2Ebool_2ET))))))) % 0.47/0.66 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_3F A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap V0P) ((ap (c_2Emin_2E_40 A_27a)) V0P)))))) of role axiom named ax_thm_2Ebool_2EEXISTS__DEF % 0.47/0.66 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_3F A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap V0P) ((ap (c_2Emin_2E_40 A_27a)) V0P)))))) % 0.47/0.66 FOF formula (((eq fofType) c_2Ebool_2E_2F_5C) ((lam bool) (fun (V0t1:fofType)=> ((lam bool) (fun (V1t2:fofType)=> ((ap (c_2Ebool_2E_21 bool)) ((lam bool) (fun (V2t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t1)) ((ap ((ap c_2Emin_2E_3D_3D_3E) V1t2)) V2t)))) V2t))))))))) of role axiom named ax_thm_2Ebool_2EAND__DEF % 0.51/0.68 A new axiom: (((eq fofType) c_2Ebool_2E_2F_5C) ((lam bool) (fun (V0t1:fofType)=> ((lam bool) (fun (V1t2:fofType)=> ((ap (c_2Ebool_2E_21 bool)) ((lam bool) (fun (V2t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t1)) ((ap ((ap c_2Emin_2E_3D_3D_3E) V1t2)) V2t)))) V2t))))))))) % 0.51/0.68 FOF formula (((eq fofType) c_2Ebool_2E_5C_2F) ((lam bool) (fun (V0t1:fofType)=> ((lam bool) (fun (V1t2:fofType)=> ((ap (c_2Ebool_2E_21 bool)) ((lam bool) (fun (V2t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t1)) V2t))) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V1t2)) V2t))) V2t)))))))))) of role axiom named ax_thm_2Ebool_2EOR__DEF % 0.51/0.68 A new axiom: (((eq fofType) c_2Ebool_2E_5C_2F) ((lam bool) (fun (V0t1:fofType)=> ((lam bool) (fun (V1t2:fofType)=> ((ap (c_2Ebool_2E_21 bool)) ((lam bool) (fun (V2t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t1)) V2t))) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V1t2)) V2t))) V2t)))))))))) % 0.51/0.68 FOF formula ((iff False) (forall (V0t:fofType), (((mem V0t) bool)->(p V0t)))) of role axiom named ax_thm_2Ebool_2EF__DEF % 0.51/0.68 A new axiom: ((iff False) (forall (V0t:fofType), (((mem V0t) bool)->(p V0t)))) % 0.51/0.68 FOF formula (((eq fofType) c_2Ebool_2E_7E) ((lam bool) (fun (V0t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t)) c_2Ebool_2EF)))) of role axiom named ax_thm_2Ebool_2ENOT__DEF % 0.51/0.68 A new axiom: (((eq fofType) c_2Ebool_2E_7E) ((lam bool) (fun (V0t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t)) c_2Ebool_2EF)))) % 0.51/0.68 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_3F_21 A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap (c_2Ebool_2E_3F A_27a)) V0P))) ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V1x:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2y:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Ebool_2E_2F_5C) ((ap V0P) V1x))) ((ap V0P) V2y)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V1x)) V2y))))))))))))) of role axiom named ax_thm_2Ebool_2EEXISTS__UNIQUE__DEF % 0.51/0.68 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_3F_21 A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap (c_2Ebool_2E_3F A_27a)) V0P))) ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V1x:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2y:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Ebool_2E_2F_5C) ((ap V0P) V1x))) ((ap V0P) V2y)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V1x)) V2y))))))))))))) % 0.51/0.68 FOF formula (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2ELET A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((lam A_27a) (fun (V1x:fofType)=> ((ap V0f) V1x))))))) of role axiom named ax_thm_2Ebool_2ELET__DEF % 0.51/0.68 A new axiom: (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2ELET A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((lam A_27a) (fun (V1x:fofType)=> ((ap V0f) V1x))))))) % 0.51/0.68 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ECOND A_27a)) ((lam bool) (fun (V0t:fofType)=> ((lam A_27a) (fun (V1t1:fofType)=> ((lam A_27a) (fun (V2t2:fofType)=> ((ap (c_2Emin_2E_40 A_27a)) ((lam A_27a) (fun (V3x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D bool)) V0t)) c_2Ebool_2ET))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V1t1)))) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D bool)) V0t)) c_2Ebool_2EF))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V2t2)))))))))))))) of role axiom named ax_thm_2Ebool_2ECOND__DEF % 0.51/0.68 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ECOND A_27a)) ((lam bool) (fun (V0t:fofType)=> ((lam A_27a) (fun (V1t1:fofType)=> ((lam A_27a) (fun (V2t2:fofType)=> ((ap (c_2Emin_2E_40 A_27a)) ((lam A_27a) (fun (V3x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D bool)) V0t)) c_2Ebool_2ET))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V1t1)))) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D bool)) V0t)) c_2Ebool_2EF))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V2t2)))))))))))))) % 0.51/0.69 FOF formula (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2EONE__ONE A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V1x1:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2x2:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D A_27b)) ((ap V0f) V1x1))) ((ap V0f) V2x2)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V1x1)) V2x2)))))))))))) of role axiom named ax_thm_2Ebool_2EONE__ONE__DEF % 0.51/0.69 A new axiom: (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2EONE__ONE A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V1x1:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2x2:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D A_27b)) ((ap V0f) V1x1))) ((ap V0f) V2x2)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V1x1)) V2x2)))))))))))) % 0.51/0.69 FOF formula (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2EONTO A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V1y:fofType)=> ((ap (c_2Ebool_2E_3F A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap (c_2Emin_2E_3D A_27b)) V1y)) ((ap V0f) V2x)))))))))))) of role axiom named ax_thm_2Ebool_2EONTO__DEF % 0.51/0.69 A new axiom: (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2EONTO A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V1y:fofType)=> ((ap (c_2Ebool_2E_3F A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap (c_2Emin_2E_3D A_27b)) V1y)) ((ap V0f) V2x)))))))))))) % 0.51/0.69 FOF formula (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2ETYPE__DEFINITION A_27a) A_27b)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((lam ((arr A_27b) A_27a)) (fun (V1rep:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V2x_27:fofType)=> ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V3x_27_27:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D A_27a)) ((ap V1rep) V2x_27))) ((ap V1rep) V3x_27_27)))) ((ap ((ap (c_2Emin_2E_3D A_27b)) V2x_27)) V3x_27_27)))))))))) ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V4x:fofType)=> ((ap ((ap (c_2Emin_2E_3D bool)) ((ap V0P) V4x))) ((ap (c_2Ebool_2E_3F A_27b)) ((lam A_27b) (fun (V5x_27:fofType)=> ((ap ((ap (c_2Emin_2E_3D A_27a)) V4x)) ((ap V1rep) V5x_27)))))))))))))))) of role axiom named ax_thm_2Ebool_2ETYPE__DEFINITION % 0.51/0.69 A new axiom: (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2ETYPE__DEFINITION A_27a) A_27b)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((lam ((arr A_27b) A_27a)) (fun (V1rep:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V2x_27:fofType)=> ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V3x_27_27:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D A_27a)) ((ap V1rep) V2x_27))) ((ap V1rep) V3x_27_27)))) ((ap ((ap (c_2Emin_2E_3D A_27b)) V2x_27)) V3x_27_27)))))))))) ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V4x:fofType)=> ((ap ((ap (c_2Emin_2E_3D bool)) ((ap V0P) V4x))) ((ap (c_2Ebool_2E_3F A_27b)) ((lam A_27b) (fun (V5x_27:fofType)=> ((ap ((ap (c_2Emin_2E_3D A_27a)) V4x)) ((ap V1rep) V5x_27)))))))))))))))) % 0.51/0.69 FOF formula (forall (V0t:fofType), (((mem V0t) bool)->((or ((iff (p V0t)) True)) ((iff (p V0t)) False)))) of role axiom named ax_thm_2Ebool_2EBOOL__CASES__AX % 0.51/0.69 A new axiom: (forall (V0t:fofType), (((mem V0t) bool)->((or ((iff (p V0t)) True)) ((iff (p V0t)) False)))) % 0.51/0.69 FOF formula (forall (A_27a:del) (A_27b:del) (V0t:fofType), (((mem V0t) ((arr A_27a) A_27b))->(((eq fofType) ((lam A_27a) (fun (V1x:fofType)=> ((ap V0t) V1x)))) V0t))) of role axiom named ax_thm_2Ebool_2EETA__AX % 0.51/0.69 A new axiom: (forall (A_27a:del) (A_27b:del) (V0t:fofType), (((mem V0t) ((arr A_27a) A_27b))->(((eq fofType) ((lam A_27a) (fun (V1x:fofType)=> ((ap V0t) V1x)))) V0t))) % 0.51/0.69 FOF formula (forall (A_27a:del) (V0P:fofType), (((mem V0P) ((arr A_27a) bool))->(forall (V1x:fofType), (((mem V1x) A_27a)->((p ((ap V0P) V1x))->(p ((ap V0P) ((ap (c_2Emin_2E_40 A_27a)) V0P)))))))) of role axiom named ax_thm_2Ebool_2ESELECT__AX % 0.51/0.71 A new axiom: (forall (A_27a:del) (V0P:fofType), (((mem V0P) ((arr A_27a) bool))->(forall (V1x:fofType), (((mem V1x) A_27a)->((p ((ap V0P) V1x))->(p ((ap V0P) ((ap (c_2Emin_2E_40 A_27a)) V0P)))))))) % 0.51/0.71 FOF formula (<kernel.Constant object at 0xbd03b0>, <kernel.Type object at 0xbd08c0>) of role type named stp_i % 0.51/0.71 Using role type % 0.51/0.71 Declaring tp__i:Type % 0.51/0.71 FOF formula (<kernel.Constant object at 0xbd0e60>, <kernel.DependentProduct object at 0x2af8c3b6a3b0>) of role type named stp_inj_i % 0.51/0.71 Using role type % 0.51/0.71 Declaring inj__i:(tp__i->fofType) % 0.51/0.71 FOF formula (<kernel.Constant object at 0xbd0b00>, <kernel.DependentProduct object at 0x2af8c3b6a710>) of role type named stp_surj_i % 0.51/0.71 Using role type % 0.51/0.71 Declaring surj__i:(fofType->tp__i) % 0.51/0.71 FOF formula (forall (X:tp__i), (((eq tp__i) (surj__i (inj__i X))) X)) of role axiom named stp_inj_surj_i % 0.51/0.71 A new axiom: (forall (X:tp__i), (((eq tp__i) (surj__i (inj__i X))) X)) % 0.51/0.71 FOF formula (forall (X:tp__i), ((mem (inj__i X)) ind)) of role axiom named stp_inj_mem_i % 0.51/0.71 A new axiom: (forall (X:tp__i), ((mem (inj__i X)) ind)) % 0.51/0.71 FOF formula (forall (X:fofType), (((mem X) ind)->(((eq fofType) X) (inj__i (surj__i X))))) of role axiom named stp_iso_mem_i % 0.51/0.71 A new axiom: (forall (X:fofType), (((mem X) ind)->(((eq fofType) X) (inj__i (surj__i X))))) % 0.51/0.71 FOF formula ((ex fofType) (fun (V0f:fofType)=> ((and ((and ((mem V0f) ((arr ind) ind))) (p ((ap ((c_2Ebool_2EONE__ONE ind) ind)) V0f)))) ((p ((ap ((c_2Ebool_2EONTO ind) ind)) V0f))->False)))) of role axiom named ax_thm_2Ebool_2EINFINITY__AX % 0.51/0.71 A new axiom: ((ex fofType) (fun (V0f:fofType)=> ((and ((and ((mem V0f) ((arr ind) ind))) (p ((ap ((c_2Ebool_2EONE__ONE ind) ind)) V0f)))) ((p ((ap ((c_2Ebool_2EONTO ind) ind)) V0f))->False)))) % 0.51/0.71 FOF formula (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2Eliteral__case A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((lam A_27a) (fun (V1x:fofType)=> ((ap V0f) V1x))))))) of role axiom named ax_thm_2Ebool_2Eliteral__case__DEF % 0.51/0.71 A new axiom: (forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2Eliteral__case A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((lam A_27a) (fun (V1x:fofType)=> ((ap V0f) V1x))))))) % 0.51/0.71 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2EIN A_27a)) ((lam A_27a) (fun (V0x:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1f:fofType)=> ((ap V1f) V0x))))))) of role axiom named ax_thm_2Ebool_2EIN__DEF % 0.51/0.71 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2EIN A_27a)) ((lam A_27a) (fun (V0x:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1f:fofType)=> ((ap V1f) V0x))))))) % 0.51/0.71 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__FORALL A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))) of role axiom named ax_thm_2Ebool_2ERES__FORALL__DEF % 0.51/0.71 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__FORALL A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))) % 0.51/0.71 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__EXISTS A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Ebool_2E_3F A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))) of role axiom named ax_thm_2Ebool_2ERES__EXISTS__DEF % 0.51/0.71 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__EXISTS A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Ebool_2E_3F A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))) % 0.51/0.72 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__EXISTS__UNIQUE A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2ERES__EXISTS A_27a)) V0p)) ((lam A_27a) (fun (V2x:fofType)=> ((ap V1m) V2x)))))) ((ap ((ap (c_2Ebool_2ERES__FORALL A_27a)) V0p)) ((lam A_27a) (fun (V3x:fofType)=> ((ap ((ap (c_2Ebool_2ERES__FORALL A_27a)) V0p)) ((lam A_27a) (fun (V4y:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Ebool_2E_2F_5C) ((ap V1m) V3x))) ((ap V1m) V4y)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V4y))))))))))))))) of role axiom named ax_thm_2Ebool_2ERES__EXISTS__UNIQUE__DEF % 0.51/0.72 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__EXISTS__UNIQUE A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2ERES__EXISTS A_27a)) V0p)) ((lam A_27a) (fun (V2x:fofType)=> ((ap V1m) V2x)))))) ((ap ((ap (c_2Ebool_2ERES__FORALL A_27a)) V0p)) ((lam A_27a) (fun (V3x:fofType)=> ((ap ((ap (c_2Ebool_2ERES__FORALL A_27a)) V0p)) ((lam A_27a) (fun (V4y:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Ebool_2E_2F_5C) ((ap V1m) V3x))) ((ap V1m) V4y)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V4y))))))))))))))) % 0.51/0.72 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__SELECT A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Emin_2E_40 A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))) of role axiom named ax_thm_2Ebool_2ERES__SELECT__DEF % 0.51/0.72 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__SELECT A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Emin_2E_40 A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))) % 0.51/0.72 FOF formula (((eq fofType) c_2Ebool_2EBOUNDED) ((lam bool) (fun (V0v:fofType)=> c_2Ebool_2ET))) of role axiom named ax_thm_2Ebool_2EBOUNDED__DEF % 0.51/0.72 A new axiom: (((eq fofType) c_2Ebool_2EBOUNDED) ((lam bool) (fun (V0v:fofType)=> c_2Ebool_2ET))) % 0.51/0.72 FOF formula (forall (A_27a:del), (((eq fofType) (c_2Ebool_2EDATATYPE A_27a)) ((lam A_27a) (fun (V0x:fofType)=> c_2Ebool_2ET)))) of role axiom named ax_thm_2Ebool_2EDATATYPE__TAG__DEF % 0.51/0.72 A new axiom: (forall (A_27a:del), (((eq fofType) (c_2Ebool_2EDATATYPE A_27a)) ((lam A_27a) (fun (V0x:fofType)=> c_2Ebool_2ET)))) % 0.51/0.72 FOF formula True of role conjecture named conj_thm_2Ebool_2ETRUTH % 0.51/0.72 Conjecture to prove = True:Prop % 0.51/0.72 Parameter tp__i_DUMMY:tp__i. % 0.51/0.72 We need to prove ['True'] % 0.51/0.72 Parameter del:Type. % 0.51/0.72 Parameter bool:del. % 0.51/0.72 Parameter ind:del. % 0.51/0.72 Parameter arr:(del->(del->del)). % 0.51/0.72 Parameter fofType:Type. % 0.51/0.72 Parameter mem:(fofType->(del->Prop)). % 0.51/0.72 Parameter ap:(fofType->(fofType->fofType)). % 0.51/0.72 Parameter lam:(del->((fofType->fofType)->fofType)). % 0.51/0.72 Parameter p:(fofType->Prop). % 0.51/0.72 Parameter inj__o:(Prop->fofType). % 0.51/0.72 Axiom stp_inj_surj_o:(forall (X:Prop), (((eq Prop) (p (inj__o X))) X)). % 0.51/0.72 Axiom stp_inj_mem_o:(forall (X:Prop), ((mem (inj__o X)) bool)). % 0.51/0.72 Axiom stp_iso_mem_o:(forall (X:fofType), (((mem X) bool)->(((eq fofType) X) (inj__o (p X))))). % 0.51/0.72 Axiom ap_tp:(forall (A:del) (B:del) (F:fofType), (((mem F) ((arr A) B))->(forall (X:fofType), (((mem X) A)->((mem ((ap F) X)) B))))). % 0.51/0.72 Axiom lam_tp:(forall (A:del) (B:del) (F:(fofType->fofType)), ((forall (X:fofType), (((mem X) A)->((mem (F X)) B)))->((mem ((lam A) F)) ((arr A) B)))). % 0.51/0.72 Axiom funcext:(forall (A:del) (B:del) (F:fofType), (((mem F) ((arr A) B))->(forall (G:fofType), (((mem G) ((arr A) B))->((forall (X:fofType), (((mem X) A)->(((eq fofType) ((ap F) X)) ((ap G) X))))->(((eq fofType) F) G)))))). % 0.51/0.72 Axiom beta:(forall (A:del) (F:(fofType->fofType)) (X:fofType), (((mem X) A)->(((eq fofType) ((ap ((lam A) F)) X)) (F X)))). % 0.51/0.72 Parameter c_2Emin_2E_3D:(del->fofType). % 0.51/0.72 Axiom mem_c_2Emin_2E_3D:(forall (A_27a:del), ((mem (c_2Emin_2E_3D A_27a)) ((arr A_27a) ((arr A_27a) bool)))). % 0.51/0.72 Axiom ax_eq_p:(forall (A:del) (X:fofType), (((mem X) A)->(forall (Y:fofType), (((mem Y) A)->((iff (p ((ap ((ap (c_2Emin_2E_3D A)) X)) Y))) (((eq fofType) X) Y)))))). % 0.51/0.72 Parameter c_2Emin_2E_3D_3D_3E:fofType. % 0.51/0.72 Axiom mem_c_2Emin_2E_3D_3D_3E:((mem c_2Emin_2E_3D_3D_3E) ((arr bool) ((arr bool) bool))). % 0.51/0.72 Axiom ax_imp_p:(forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Emin_2E_3D_3D_3E) Q)) R))) ((p Q)->(p R))))))). % 0.51/0.72 Parameter c_2Emin_2E_40:(del->fofType). % 0.51/0.72 Axiom mem_c_2Emin_2E_40:(forall (A_27a:del), ((mem (c_2Emin_2E_40 A_27a)) ((arr ((arr A_27a) bool)) A_27a))). % 0.51/0.72 Parameter ty_2Ebool_2Eitself:(del->del). % 0.51/0.72 Parameter c_2Ebool_2E_21:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2E_21:(forall (A_27a:del), ((mem (c_2Ebool_2E_21 A_27a)) ((arr ((arr A_27a) bool)) bool))). % 0.51/0.72 Axiom ax_all_p:(forall (A:del) (Q:fofType), (((mem Q) ((arr A) bool))->((iff (p ((ap (c_2Ebool_2E_21 A)) Q))) (forall (X:fofType), (((mem X) A)->(p ((ap Q) X))))))). % 0.51/0.72 Parameter c_2Ebool_2E_2F_5C:fofType. % 0.51/0.72 Axiom mem_c_2Ebool_2E_2F_5C:((mem c_2Ebool_2E_2F_5C) ((arr bool) ((arr bool) bool))). % 0.51/0.72 Axiom ax_and_p:(forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Ebool_2E_2F_5C) Q)) R))) ((and (p Q)) (p R))))))). % 0.51/0.72 Parameter c_2Ebool_2E_3F:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2E_3F:(forall (A_27a:del), ((mem (c_2Ebool_2E_3F A_27a)) ((arr ((arr A_27a) bool)) bool))). % 0.51/0.72 Axiom ax_ex_p:(forall (A:del) (Q:fofType), (((mem Q) ((arr A) bool))->((iff (p ((ap (c_2Ebool_2E_3F A)) Q))) ((ex fofType) (fun (X:fofType)=> ((and ((mem X) A)) (p ((ap Q) X)))))))). % 0.51/0.72 Parameter c_2Ebool_2E_3F_21:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2E_3F_21:(forall (A_27a:del), ((mem (c_2Ebool_2E_3F_21 A_27a)) ((arr ((arr A_27a) bool)) bool))). % 0.51/0.72 Parameter c_2Ebool_2EARB:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2EARB:(forall (A_27a:del), ((mem (c_2Ebool_2EARB A_27a)) A_27a)). % 0.51/0.72 Parameter c_2Ebool_2EBOUNDED:fofType. % 0.51/0.72 Axiom mem_c_2Ebool_2EBOUNDED:((mem c_2Ebool_2EBOUNDED) ((arr bool) bool)). % 0.51/0.72 Parameter c_2Ebool_2ECOND:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2ECOND:(forall (A_27a:del), ((mem (c_2Ebool_2ECOND A_27a)) ((arr bool) ((arr A_27a) ((arr A_27a) A_27a))))). % 0.51/0.72 Parameter c_2Ebool_2EDATATYPE:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2EDATATYPE:(forall (A_27a:del), ((mem (c_2Ebool_2EDATATYPE A_27a)) ((arr A_27a) bool))). % 0.51/0.72 Parameter c_2Ebool_2EF:fofType. % 0.51/0.72 Axiom mem_c_2Ebool_2EF:((mem c_2Ebool_2EF) bool). % 0.51/0.72 Axiom ax_false_p:((p c_2Ebool_2EF)->False). % 0.51/0.72 Parameter c_2Ebool_2EIN:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2EIN:(forall (A_27a:del), ((mem (c_2Ebool_2EIN A_27a)) ((arr A_27a) ((arr ((arr A_27a) bool)) bool)))). % 0.51/0.72 Parameter c_2Ebool_2ELET:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2ELET:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ELET A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b)))). % 0.51/0.72 Parameter c_2Ebool_2EONE__ONE:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2EONE__ONE:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2EONE__ONE A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) bool))). % 0.51/0.72 Parameter c_2Ebool_2EONTO:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2EONTO:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2EONTO A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) bool))). % 0.51/0.72 Parameter c_2Ebool_2ERES__ABSTRACT:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2ERES__ABSTRACT:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ERES__ABSTRACT A_27a) A_27b)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b))))). % 0.51/0.72 Parameter c_2Ebool_2ERES__EXISTS:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2ERES__EXISTS:(forall (A_27a:del), ((mem (c_2Ebool_2ERES__EXISTS A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))). % 0.51/0.72 Parameter c_2Ebool_2ERES__EXISTS__UNIQUE:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2ERES__EXISTS__UNIQUE:(forall (A_27a:del), ((mem (c_2Ebool_2ERES__EXISTS__UNIQUE A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))). % 0.51/0.72 Parameter c_2Ebool_2ERES__FORALL:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2ERES__FORALL:(forall (A_27a:del), ((mem (c_2Ebool_2ERES__FORALL A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) bool)))). % 0.51/0.72 Parameter c_2Ebool_2ERES__SELECT:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2ERES__SELECT:(forall (A_27a:del), ((mem (c_2Ebool_2ERES__SELECT A_27a)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27a) bool)) A_27a)))). % 0.51/0.72 Parameter c_2Ebool_2ET:fofType. % 0.51/0.72 Axiom mem_c_2Ebool_2ET:((mem c_2Ebool_2ET) bool). % 0.51/0.72 Axiom ax_true_p:(p c_2Ebool_2ET). % 0.51/0.72 Parameter c_2Ebool_2ETYPE__DEFINITION:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2ETYPE__DEFINITION:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2ETYPE__DEFINITION A_27a) A_27b)) ((arr ((arr A_27a) bool)) ((arr ((arr A_27b) A_27a)) bool)))). % 0.51/0.72 Parameter c_2Ebool_2E_5C_2F:fofType. % 0.51/0.72 Axiom mem_c_2Ebool_2E_5C_2F:((mem c_2Ebool_2E_5C_2F) ((arr bool) ((arr bool) bool))). % 0.51/0.72 Axiom ax_or_p:(forall (Q:fofType), (((mem Q) bool)->(forall (R:fofType), (((mem R) bool)->((iff (p ((ap ((ap c_2Ebool_2E_5C_2F) Q)) R))) ((or (p Q)) (p R))))))). % 0.51/0.72 Parameter c_2Ebool_2Eitself__case:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2Eitself__case:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2Eitself__case A_27a) A_27b)) ((arr (ty_2Ebool_2Eitself A_27a)) ((arr A_27b) A_27b)))). % 0.51/0.72 Parameter c_2Ebool_2Eliteral__case:(del->(del->fofType)). % 0.51/0.72 Axiom mem_c_2Ebool_2Eliteral__case:(forall (A_27a:del) (A_27b:del), ((mem ((c_2Ebool_2Eliteral__case A_27a) A_27b)) ((arr ((arr A_27a) A_27b)) ((arr A_27a) A_27b)))). % 0.51/0.72 Parameter c_2Ebool_2Ethe__value:(del->fofType). % 0.51/0.72 Axiom mem_c_2Ebool_2Ethe__value:(forall (A_27a:del), ((mem (c_2Ebool_2Ethe__value A_27a)) (ty_2Ebool_2Eitself A_27a))). % 0.51/0.72 Parameter c_2Ebool_2E_7E:fofType. % 0.51/0.72 Axiom mem_c_2Ebool_2E_7E:((mem c_2Ebool_2E_7E) ((arr bool) bool)). % 0.51/0.72 Axiom ax_neg_p:(forall (Q:fofType), (((mem Q) bool)->((iff (p ((ap c_2Ebool_2E_7E) Q))) ((p Q)->False)))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ET__DEF:((iff True) (((eq fofType) ((lam bool) (fun (V0x:fofType)=> V0x))) ((lam bool) (fun (V1x:fofType)=> V1x)))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EFORALL__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_21 A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap ((ap (c_2Emin_2E_3D ((arr A_27a) bool))) V0P)) ((lam A_27a) (fun (V1x:fofType)=> c_2Ebool_2ET))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EEXISTS__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_3F A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap V0P) ((ap (c_2Emin_2E_40 A_27a)) V0P)))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EAND__DEF:(((eq fofType) c_2Ebool_2E_2F_5C) ((lam bool) (fun (V0t1:fofType)=> ((lam bool) (fun (V1t2:fofType)=> ((ap (c_2Ebool_2E_21 bool)) ((lam bool) (fun (V2t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t1)) ((ap ((ap c_2Emin_2E_3D_3D_3E) V1t2)) V2t)))) V2t))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EOR__DEF:(((eq fofType) c_2Ebool_2E_5C_2F) ((lam bool) (fun (V0t1:fofType)=> ((lam bool) (fun (V1t2:fofType)=> ((ap (c_2Ebool_2E_21 bool)) ((lam bool) (fun (V2t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t1)) V2t))) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Emin_2E_3D_3D_3E) V1t2)) V2t))) V2t)))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EF__DEF:((iff False) (forall (V0t:fofType), (((mem V0t) bool)->(p V0t)))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ENOT__DEF:(((eq fofType) c_2Ebool_2E_7E) ((lam bool) (fun (V0t:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) V0t)) c_2Ebool_2EF)))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EEXISTS__UNIQUE__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2E_3F_21 A_27a)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap (c_2Ebool_2E_3F A_27a)) V0P))) ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V1x:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2y:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Ebool_2E_2F_5C) ((ap V0P) V1x))) ((ap V0P) V2y)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V1x)) V2y))))))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ELET__DEF:(forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2ELET A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((lam A_27a) (fun (V1x:fofType)=> ((ap V0f) V1x))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ECOND__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2ECOND A_27a)) ((lam bool) (fun (V0t:fofType)=> ((lam A_27a) (fun (V1t1:fofType)=> ((lam A_27a) (fun (V2t2:fofType)=> ((ap (c_2Emin_2E_40 A_27a)) ((lam A_27a) (fun (V3x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D bool)) V0t)) c_2Ebool_2ET))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V1t1)))) ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D bool)) V0t)) c_2Ebool_2EF))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V2t2)))))))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EONE__ONE__DEF:(forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2EONE__ONE A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V1x1:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2x2:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D A_27b)) ((ap V0f) V1x1))) ((ap V0f) V2x2)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V1x1)) V2x2)))))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EONTO__DEF:(forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2EONTO A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V1y:fofType)=> ((ap (c_2Ebool_2E_3F A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap (c_2Emin_2E_3D A_27b)) V1y)) ((ap V0f) V2x)))))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ETYPE__DEFINITION:(forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2ETYPE__DEFINITION A_27a) A_27b)) ((lam ((arr A_27a) bool)) (fun (V0P:fofType)=> ((lam ((arr A_27b) A_27a)) (fun (V1rep:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V2x_27:fofType)=> ((ap (c_2Ebool_2E_21 A_27b)) ((lam A_27b) (fun (V3x_27_27:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Emin_2E_3D A_27a)) ((ap V1rep) V2x_27))) ((ap V1rep) V3x_27_27)))) ((ap ((ap (c_2Emin_2E_3D A_27b)) V2x_27)) V3x_27_27)))))))))) ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V4x:fofType)=> ((ap ((ap (c_2Emin_2E_3D bool)) ((ap V0P) V4x))) ((ap (c_2Ebool_2E_3F A_27b)) ((lam A_27b) (fun (V5x_27:fofType)=> ((ap ((ap (c_2Emin_2E_3D A_27a)) V4x)) ((ap V1rep) V5x_27)))))))))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EBOOL__CASES__AX:(forall (V0t:fofType), (((mem V0t) bool)->((or ((iff (p V0t)) True)) ((iff (p V0t)) False)))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EETA__AX:(forall (A_27a:del) (A_27b:del) (V0t:fofType), (((mem V0t) ((arr A_27a) A_27b))->(((eq fofType) ((lam A_27a) (fun (V1x:fofType)=> ((ap V0t) V1x)))) V0t))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ESELECT__AX:(forall (A_27a:del) (V0P:fofType), (((mem V0P) ((arr A_27a) bool))->(forall (V1x:fofType), (((mem V1x) A_27a)->((p ((ap V0P) V1x))->(p ((ap V0P) ((ap (c_2Emin_2E_40 A_27a)) V0P)))))))). % 0.51/0.72 Parameter tp__i:Type. % 0.51/0.72 Parameter inj__i:(tp__i->fofType). % 0.51/0.72 Parameter surj__i:(fofType->tp__i). % 0.51/0.72 Axiom stp_inj_surj_i:(forall (X:tp__i), (((eq tp__i) (surj__i (inj__i X))) X)). % 0.51/0.72 Axiom stp_inj_mem_i:(forall (X:tp__i), ((mem (inj__i X)) ind)). % 0.51/0.72 Axiom stp_iso_mem_i:(forall (X:fofType), (((mem X) ind)->(((eq fofType) X) (inj__i (surj__i X))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EINFINITY__AX:((ex fofType) (fun (V0f:fofType)=> ((and ((and ((mem V0f) ((arr ind) ind))) (p ((ap ((c_2Ebool_2EONE__ONE ind) ind)) V0f)))) ((p ((ap ((c_2Ebool_2EONTO ind) ind)) V0f))->False)))). % 0.51/0.72 Axiom ax_thm_2Ebool_2Eliteral__case__DEF:(forall (A_27a:del) (A_27b:del), (((eq fofType) ((c_2Ebool_2Eliteral__case A_27a) A_27b)) ((lam ((arr A_27a) A_27b)) (fun (V0f:fofType)=> ((lam A_27a) (fun (V1x:fofType)=> ((ap V0f) V1x))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2EIN__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2EIN A_27a)) ((lam A_27a) (fun (V0x:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1f:fofType)=> ((ap V1f) V0x))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ERES__FORALL__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__FORALL A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Ebool_2E_21 A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))). % 0.51/0.72 Axiom ax_thm_2Ebool_2ERES__EXISTS__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__EXISTS A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Ebool_2E_3F A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))). % 0.58/0.74 Axiom ax_thm_2Ebool_2ERES__EXISTS__UNIQUE__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__EXISTS__UNIQUE A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2ERES__EXISTS A_27a)) V0p)) ((lam A_27a) (fun (V2x:fofType)=> ((ap V1m) V2x)))))) ((ap ((ap (c_2Ebool_2ERES__FORALL A_27a)) V0p)) ((lam A_27a) (fun (V3x:fofType)=> ((ap ((ap (c_2Ebool_2ERES__FORALL A_27a)) V0p)) ((lam A_27a) (fun (V4y:fofType)=> ((ap ((ap c_2Emin_2E_3D_3D_3E) ((ap ((ap c_2Ebool_2E_2F_5C) ((ap V1m) V3x))) ((ap V1m) V4y)))) ((ap ((ap (c_2Emin_2E_3D A_27a)) V3x)) V4y))))))))))))))). % 0.58/0.74 Axiom ax_thm_2Ebool_2ERES__SELECT__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2ERES__SELECT A_27a)) ((lam ((arr A_27a) bool)) (fun (V0p:fofType)=> ((lam ((arr A_27a) bool)) (fun (V1m:fofType)=> ((ap (c_2Emin_2E_40 A_27a)) ((lam A_27a) (fun (V2x:fofType)=> ((ap ((ap c_2Ebool_2E_2F_5C) ((ap ((ap (c_2Ebool_2EIN A_27a)) V2x)) V0p))) ((ap V1m) V2x))))))))))). % 0.58/0.74 Axiom ax_thm_2Ebool_2EBOUNDED__DEF:(((eq fofType) c_2Ebool_2EBOUNDED) ((lam bool) (fun (V0v:fofType)=> c_2Ebool_2ET))). % 0.58/0.74 Axiom ax_thm_2Ebool_2EDATATYPE__TAG__DEF:(forall (A_27a:del), (((eq fofType) (c_2Ebool_2EDATATYPE A_27a)) ((lam A_27a) (fun (V0x:fofType)=> c_2Ebool_2ET)))). % 0.58/0.74 Trying to prove True % 0.58/0.74 Found I:True % 0.58/0.74 Found I as proof of True % 0.58/0.74 Got proof I % 0.58/0.74 Time elapsed = 0.000764s % 0.58/0.74 node=0 cost=0.000000 depth=0 % 0.58/0.74:::::::::::::::::::::: % 0.58/0.74 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.74 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.74 I % 0.58/0.74 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------