%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO221^5 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Mar 29 00:50:56 EDT 2022 % Result : Theorem 6.00s 6.18s % Output : Proof 6.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYO221^5 : TPTP v7.5.0. Released v4.0.0. % 0.03/0.12 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.33 % Computer : n006.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Fri Mar 11 19:39:14 EST 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.12/0.34 Python 2.7.5 % 3.11/3.28 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 3.11/3.28 FOF formula (<kernel.Constant object at 0x27f1638>, <kernel.Constant object at 0x27f13f8>) of role type named b % 3.11/3.28 Using role type % 3.11/3.28 Declaring b:fofType % 3.11/3.28 FOF formula (<kernel.Constant object at 0x27f1518>, <kernel.DependentProduct object at 0x2b7410b47bd8>) of role type named cP % 3.11/3.28 Using role type % 3.11/3.28 Declaring cP:(fofType->Prop) % 3.11/3.28 FOF formula (<kernel.Constant object at 0x27f5ea8>, <kernel.Single object at 0x27f1098>) of role type named a % 3.11/3.28 Using role type % 3.11/3.28 Declaring a:fofType % 3.11/3.28 FOF formula ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) of role conjecture named cBLEDSOE6 % 3.11/3.28 Conjecture to prove = ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))):Prop % 3.11/3.28 We need to prove ['((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False)))))'] % 3.11/3.28 Parameter fofType:Type. % 3.11/3.28 Parameter b:fofType. % 3.11/3.28 Parameter cP:(fofType->Prop). % 3.11/3.28 Parameter a:fofType. % 3.11/3.28 Trying to prove ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) % 3.11/3.28 Found x01:(not (((eq fofType) a) b)) % 3.11/3.28 Instantiate: x:=((eq fofType) a):(fofType->Prop) % 3.11/3.28 Found x01 as proof of ((x b)->False) % 3.11/3.28 Found x000:=(x00 x0):False % 3.11/3.28 Found (x00 x0) as proof of False % 3.11/3.28 Found (x00 x0) as proof of False % 3.11/3.28 Found (fun (x00:(x b))=> (x00 x0)) as proof of False % 3.11/3.28 Found (fun (x00:(x b))=> (x00 x0)) as proof of ((x b)->False) % 3.11/3.28 Found x01:(not (((eq fofType) a) b)) % 3.11/3.28 Instantiate: x:=((eq fofType) a):(fofType->Prop) % 3.11/3.28 Found x01 as proof of (not (x b)) % 3.11/3.28 Found x000:=(x00 x0):False % 3.11/3.28 Found (x00 x0) as proof of False % 3.11/3.28 Found (x00 x0) as proof of False % 3.11/3.28 Found (fun (x00:(x b))=> (x00 x0)) as proof of False % 3.11/3.28 Found (fun (x00:(x b))=> (x00 x0)) as proof of (not (x b)) % 3.11/3.28 Found eq_ref000:=(eq_ref00 x):((x Xx)->(x Xx)) % 3.11/3.28 Found (eq_ref00 x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found ((eq_ref0 Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 3.11/3.28 Found eq_ref000:=(eq_ref00 x):((x Xx)->(x Xx)) % 3.11/3.28 Found (eq_ref00 x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found ((eq_ref0 Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 3.11/3.28 Found eq_ref000:=(eq_ref00 x):((x Xx)->(x Xx)) % 3.11/3.28 Found (eq_ref00 x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found ((eq_ref0 Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 3.11/3.28 Found eq_ref000:=(eq_ref00 x):((x Xx)->(x Xx)) % 3.11/3.28 Found (eq_ref00 x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found ((eq_ref0 Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of ((x Xx)->(cP Xx)) % 3.11/3.28 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 4.08/4.25 Found eq_ref000:=(eq_ref00 x):((x Xx)->(x Xx)) % 4.08/4.25 Found (eq_ref00 x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found ((eq_ref0 Xx) x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 4.08/4.25 Found eq_ref000:=(eq_ref00 x):((x Xx)->(x Xx)) % 4.08/4.25 Found (eq_ref00 x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found ((eq_ref0 Xx) x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (((eq_ref fofType) Xx) x) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of ((x Xx)->(cP Xx)) % 4.08/4.25 Found (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 4.08/4.25 Found eta_expansion000:=(eta_expansion00 (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))):(((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) (fun (x:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))))) % 4.08/4.25 Found (eta_expansion00 (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) b0) % 4.08/4.25 Found ((eta_expansion0 Prop) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) b0) % 4.08/4.25 Found (((eta_expansion (fofType->Prop)) Prop) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) b0) % 4.08/4.25 Found (((eta_expansion (fofType->Prop)) Prop) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) b0) % 4.08/4.25 Found (((eta_expansion (fofType->Prop)) Prop) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) b0) % 4.08/4.25 Found x0200:=(x020 x00):(cP Xx) % 4.08/4.25 Found (x020 x00) as proof of (cP Xx) % 4.08/4.25 Found ((x02 cP) x00) as proof of (cP Xx) % 4.08/4.25 Found (fun (x02:(x Xx))=> ((x02 cP) x00)) as proof of (cP Xx) % 4.52/4.71 Found (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00)) as proof of ((x Xx)->(cP Xx)) % 4.52/4.71 Found (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 4.52/4.71 Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))):(((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) (fun (x:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (not (x b)))))) % 4.52/4.71 Found (eta_expansion_dep00 (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) b0) % 4.52/4.71 Found ((eta_expansion_dep0 (fun (x1:(fofType->Prop))=> Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) b0) % 4.52/4.71 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) b0) % 4.52/4.71 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) b0) % 4.52/4.71 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) as proof of (((eq ((fofType->Prop)->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) (not (A b)))))) b0) % 4.52/4.71 Found x00000:=(x0000 x00):(cP Xx) % 4.52/4.71 Found (x0000 x00) as proof of (cP Xx) % 4.52/4.71 Found ((x000 cP) x00) as proof of (cP Xx) % 4.52/4.71 Found (fun (x000:(x Xx))=> ((x000 cP) x00)) as proof of (cP Xx) % 4.52/4.71 Found (fun (Xx:fofType) (x000:(x Xx))=> ((x000 cP) x00)) as proof of ((x Xx)->(cP Xx)) % 4.52/4.71 Found (fun (Xx:fofType) (x000:(x Xx))=> ((x000 cP) x00)) as proof of (forall (Xx:fofType), ((x Xx)->(cP Xx))) % 4.52/4.71 Found ex_intro1000:=(ex_intro100 x00):((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.52/4.71 Found (ex_intro100 x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.52/4.71 Found ((ex_intro10 a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.52/4.71 Found (((ex_intro1 (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.52/4.71 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found ((conj10 (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found (((conj1 ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found ex_intro1000:=(ex_intro100 x00):((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found (ex_intro100 x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found ((ex_intro10 a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found (((ex_intro1 (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.71/4.85 Found ((conj10 (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found (((conj1 ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found (fun (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.71/4.85 Found (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00))) as proof of ((not (((eq fofType) a) b))->((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) % 4.71/4.85 Found (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00))) as proof of ((cP a)->((not (((eq fofType) a) b))->((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))))) % 4.71/4.85 Found (and_rect00 (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found ((and_rect0 ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found ex_intro1000:=(ex_intro100 x00):((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found (ex_intro100 x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((ex_intro10 a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found (((ex_intro1 (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((conj10 (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found (((conj1 ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 4.93/5.09 Found ex_intro1000:=(ex_intro100 x00):((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found (ex_intro100 x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((ex_intro10 a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found (((ex_intro1 (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 4.93/5.09 Found ((conj10 (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found (((conj1 ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found (fun (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00))) as proof of ((not (((eq fofType) a) b))->((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) % 6.00/6.16 Found (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00))) as proof of ((cP a)->((not (((eq fofType) a) b))->((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))))) % 6.00/6.16 Found (and_rect00 (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found ((and_rect0 ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType)=> (((eq_ref fofType) Xx) x))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) x00)))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % 6.00/6.16 Found (eq_ref0 a) as proof of (x x02) % 6.00/6.16 Found ((eq_ref fofType) a) as proof of (x x02) % 6.00/6.16 Found ((eq_ref fofType) a) as proof of (x x02) % 6.00/6.16 Found ((eq_ref fofType) a) as proof of (x x02) % 6.00/6.16 Found (ex_intro100 ((eq_ref fofType) a)) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 6.00/6.16 Found ((ex_intro10 a) ((eq_ref fofType) a)) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 6.00/6.16 Found (((ex_intro1 (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 6.00/6.16 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 6.00/6.16 Found ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)) as proof of ((ex fofType) (fun (Xy:fofType)=> (x Xy))) % 6.00/6.16 Found ((conj10 (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found (((conj1 ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a))) as proof of ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) % 6.00/6.16 Found ((conj00 ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.16 Found (((conj0 ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.16 Found ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.16 Found (fun (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01)) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.16 Found (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01)) as proof of ((not (((eq fofType) a) b))->((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) % 6.00/6.17 Found (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01)) as proof of ((cP a)->((not (((eq fofType) a) b))->((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)))) % 6.00/6.17 Found (and_rect00 (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01))) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.17 Found ((and_rect0 ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01))) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.17 Found (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01))) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.17 Found (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01)))) as proof of ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) % 6.00/6.17 Found (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01)))) as proof of (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) % 6.00/6.18 Found (ex_intro000 (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy))))) ((x b)->False)) ((((conj (forall (Xx:fofType), ((x Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (x Xy)))) (fun (Xx:fofType) (x02:(x Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (x Xy))) a) ((eq_ref fofType) a)))) x01))))) as proof of ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) % 6.00/6.18 Found ((ex_intro00 ((eq fofType) a)) (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False)) ((((conj (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy)))) (fun (Xx:fofType) (x02:(((eq fofType) a) Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))) a) ((eq_ref fofType) a)))) x01))))) as proof of ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) % 6.00/6.18 Found (((ex_intro0 (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) ((eq fofType) a)) (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False)) ((((conj (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy)))) (fun (Xx:fofType) (x02:(((eq fofType) a) Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))) a) ((eq_ref fofType) a)))) x01))))) as proof of ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) % 6.00/6.18 Found ((((ex_intro (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) ((eq fofType) a)) (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False)) ((((conj (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy)))) (fun (Xx:fofType) (x02:(((eq fofType) a) Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))) a) ((eq_ref fofType) a)))) x01))))) as proof of ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) % 6.00/6.18 Found ((((ex_intro (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) ((eq fofType) a)) (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False)) ((((conj (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy)))) (fun (Xx:fofType) (x02:(((eq fofType) a) Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))) a) ((eq_ref fofType) a)))) x01))))) as proof of ((ex (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) % 6.00/6.18 Got proof ((((ex_intro (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) ((eq fofType) a)) (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False)) ((((conj (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy)))) (fun (Xx:fofType) (x02:(((eq fofType) a) Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))) a) ((eq_ref fofType) a)))) x01))))) % 6.00/6.18 Time elapsed = 5.574786s % 6.00/6.18 node=1507 cost=1346.000000 depth=28 % 6.00/6.18 :::::::::::::::::::::: % 6.00/6.18 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.00/6.18 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.00/6.18 ((((ex_intro (fofType->Prop)) (fun (A:(fofType->Prop))=> (((and (cP a)) (not (((eq fofType) a) b)))->((and ((and (forall (Xx:fofType), ((A Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (A Xy))))) ((A b)->False))))) ((eq fofType) a)) (fun (x0:((and (cP a)) (not (((eq fofType) a) b))))=> (((fun (P:Type) (x1:((cP a)->((not (((eq fofType) a) b))->P)))=> (((((and_rect (cP a)) (not (((eq fofType) a) b))) P) x1) x0)) ((and ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False))) (fun (x00:(cP a)) (x01:(not (((eq fofType) a) b)))=> ((((conj ((and (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))))) ((((eq fofType) a) b)->False)) ((((conj (forall (Xx:fofType), ((((eq fofType) a) Xx)->(cP Xx)))) ((ex fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy)))) (fun (Xx:fofType) (x02:(((eq fofType) a) Xx))=> ((x02 cP) x00))) ((((ex_intro fofType) (fun (Xy:fofType)=> (((eq fofType) a) Xy))) a) ((eq_ref fofType) a)))) x01))))) % 6.05/6.23 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------