%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV057^5 : TPTP v6.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n190.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:33:40 EDT 2014 % Result : Theorem 4.17s % Output : Proof 4.17s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV057^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n190.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 07:48:56 CDT 2014 % % CPUTime : 4.17 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x1aa6b00>, <kernel.Type object at 0x1aa6c20>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (forall (Xx:(a->Prop)), ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0)))))))))))) of role conjecture named cEQP1_1A_pme % Conjecture to prove = (forall (Xx:(a->Prop)), ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0)))))))))))):Prop % Parameter a_DUMMY:a. % We need to prove ['(forall (Xx:(a->Prop)), ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))))'] % Parameter a:Type. % Trying to prove (forall (Xx:(a->Prop)), ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0)))))))))))) % Found x0:(Xx Xx0) % Instantiate: x:=(fun (x1:a)=> x1):(a->a) % Found (fun (x0:(Xx Xx0))=> x0) as proof of (Xx (x Xx0)) % Found (fun (Xx0:a) (x0:(Xx Xx0))=> x0) as proof of ((Xx Xx0)->(Xx (x Xx0))) % Found (fun (Xx0:a) (x0:(Xx Xx0))=> x0) as proof of (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0)))) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))):(((eq ((a->a)->Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))))) % Found (eta_expansion_dep00 (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) as proof of (((eq ((a->a)->Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) b) % Found ((eta_expansion_dep0 (fun (x1:(a->a))=> Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) as proof of (((eq ((a->a)->Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) b) % Found (((eta_expansion_dep (a->a)) (fun (x1:(a->a))=> Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) as proof of (((eq ((a->a)->Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) b) % Found (((eta_expansion_dep (a->a)) (fun (x1:(a->a))=> Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) as proof of (((eq ((a->a)->Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) b) % Found (((eta_expansion_dep (a->a)) (fun (x1:(a->a))=> Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) as proof of (((eq ((a->a)->Prop)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) b) % Found eq_ref00:=(eq_ref0 Xz):(((eq a) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq a) Xz) x00) % Found ((eq_ref a) Xz) as proof of (((eq a) Xz) x00) % Found ((eq_ref a) Xz) as proof of (((eq a) Xz) x00) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> ((eq_ref a) Xz)) as proof of (((eq a) Xz) x00) % Found eq_ref00:=(eq_ref0 Xz):(((eq a) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq a) Xz) x00) % Found ((eq_ref a) Xz) as proof of (((eq a) Xz) x00) % Found ((eq_ref a) Xz) as proof of (((eq a) Xz) x00) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> ((eq_ref a) Xz)) as proof of (((eq a) Xz) x00) % Found eq_ref000:=(eq_ref00 P):((P Xz)->(P Xz)) % Found (eq_ref00 P) as proof of ((P Xz)->(P x00)) % Found ((eq_ref0 Xz) P) as proof of ((P Xz)->(P x00)) % Found (((eq_ref a) Xz) P) as proof of ((P Xz)->(P x00)) % Found (((eq_ref a) Xz) P) as proof of ((P Xz)->(P x00)) % Found (fun (P:(a->Prop))=> (((eq_ref a) Xz) P)) as proof of ((P Xz)->(P x00)) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz)))) (P:(a->Prop))=> (((eq_ref a) Xz) P)) as proof of (((eq a) Xz) x00) % Found x1:(P Xz) % Instantiate: x00:=Xz:a % Found (fun (x1:(P Xz))=> x1) as proof of (P x00) % Found (fun (P:(a->Prop)) (x1:(P Xz))=> x1) as proof of ((P Xz)->(P x00)) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz)))) (P:(a->Prop)) (x1:(P Xz))=> x1) as proof of (((eq a) Xz) x00) % Found x1:(P Xz) % Instantiate: x00:=Xz:a % Found (fun (x1:(P Xz))=> x1) as proof of (P x00) % Found (fun (P:(a->Prop)) (x1:(P Xz))=> x1) as proof of ((P Xz)->(P x00)) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz)))) (P:(a->Prop)) (x1:(P Xz))=> x1) as proof of (((eq a) Xz) x00) % Found eq_ref000:=(eq_ref00 P):((P Xz)->(P Xz)) % Found (eq_ref00 P) as proof of ((P Xz)->(P x00)) % Found ((eq_ref0 Xz) P) as proof of ((P Xz)->(P x00)) % Found (((eq_ref a) Xz) P) as proof of ((P Xz)->(P x00)) % Found (((eq_ref a) Xz) P) as proof of ((P Xz)->(P x00)) % Found (fun (P:(a->Prop))=> (((eq_ref a) Xz) P)) as proof of ((P Xz)->(P x00)) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz)))) (P:(a->Prop))=> (((eq_ref a) Xz) P)) as proof of (((eq a) Xz) x00) % Found x0:(Xx Xy) % Instantiate: x00:=Xy:a % Found x0 as proof of (Xx x00) % Found x0:(Xx Xy) % Instantiate: x00:=Xy:a % Found x0 as proof of (Xx x00) % Found eq_ref00:=(eq_ref0 Xy):(((eq a) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq a) Xy) (x x00)) % Found ((eq_ref a) Xy) as proof of (((eq a) Xy) (x x00)) % Found ((eq_ref a) Xy) as proof of (((eq a) Xy) (x x00)) % Found ((conj20 x0) ((eq_ref a) Xy)) as proof of ((and (Xx x00)) (((eq a) Xy) (x x00))) % Found (((conj2 (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy)) as proof of ((and (Xx x00)) (((eq a) Xy) (x x00))) % Found ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy)) as proof of ((and (Xx x00)) (((eq a) Xy) (x x00))) % Found ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy)) as proof of ((and (Xx x00)) (((eq a) Xy) (x x00))) % Found eq_sym000:=(eq_sym00 (x Xz)):((((eq a) Xy) (x Xz))->(((eq a) (x Xz)) Xy)) % Found (eq_sym00 (x Xz)) as proof of ((((eq a) Xy) (x Xz))->(((eq a) Xz) x00)) % Found ((eq_sym0 Xy) (x Xz)) as proof of ((((eq a) Xy) (x Xz))->(((eq a) Xz) x00)) % Found (((eq_sym a) Xy) (x Xz)) as proof of ((((eq a) Xy) (x Xz))->(((eq a) Xz) x00)) % Found (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))) as proof of ((((eq a) Xy) (x Xz))->(((eq a) Xz) x00)) % Found (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))) as proof of ((Xx Xz)->((((eq a) Xy) (x Xz))->(((eq a) Xz) x00))) % Found (and_rect00 (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))) as proof of (((eq a) Xz) x00) % Found ((and_rect0 (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))) as proof of (((eq a) Xz) x00) % Found (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))) as proof of (((eq a) Xz) x00) % Found (fun (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))) as proof of (((eq a) Xz) x00) % Found (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))) as proof of (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)) % Found (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))) as proof of (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00))) % Found ((conj10 ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))) as proof of ((and ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) % Found (((conj1 (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))) as proof of ((and ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) % Found ((((conj ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))) as proof of ((and ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) % Found ((((conj ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))) as proof of ((and ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) % Found (ex_intro100 ((((conj ((and (Xx x00)) (((eq a) Xy) (x x00)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) x00)))) ((((conj (Xx x00)) (((eq a) Xy) (x x00))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) x00)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))) as proof of ((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) % Found ((ex_intro10 Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))) as proof of ((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) % Found (((ex_intro1 (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))) as proof of ((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) % Found ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))) as proof of ((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) % Found (fun (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))))) as proof of ((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) % Found (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))))) as proof of ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))) % Found (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))))) as proof of (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))))) % Found ((conj00 (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))))) as proof of ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) % Found (((conj0 (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))))) as proof of ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) % Found ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))))) as proof of ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) % Found ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz))))))))) as proof of ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) % Found (ex_intro000 ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx (x Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (x Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) (x Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (x Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) (x Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) (x Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) (x Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) (x Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) (x Xz)))))))))) as proof of ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) % Found ((ex_intro00 (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz)))))))))) as proof of ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) % Found (((ex_intro0 (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz)))))))))) as proof of ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) % Found ((((ex_intro (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz)))))))))) as proof of ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) % Found (fun (Xx:(a->Prop))=> ((((ex_intro (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz))))))))))) as proof of ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) % Found (fun (Xx:(a->Prop))=> ((((ex_intro (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz))))))))))) as proof of (forall (Xx:(a->Prop)), ((ex (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0)))))))))))) % Got proof (fun (Xx:(a->Prop))=> ((((ex_intro (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz))))))))))) % Time elapsed = 3.832708s % node=469 cost=1356.000000 depth=31 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (Xx:(a->Prop))=> ((((ex_intro (a->a)) (fun (Xs:(a->a))=> ((and (forall (Xx0:a), ((Xx Xx0)->(Xx (Xs Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) (Xs Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) (Xs Xz)))->(((eq a) Xz) Xx0))))))))))) (fun (x1:a)=> x1)) ((((conj (forall (Xx0:a), ((Xx Xx0)->(Xx ((fun (x1:a)=> x1) Xx0))))) (forall (Xy:a), ((Xx Xy)->((ex a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0))))))))) (fun (Xx0:a) (x0:(Xx Xx0))=> x0)) (fun (Xy:a) (x0:(Xx Xy))=> ((((ex_intro a) (fun (Xx0:a)=> ((and ((and (Xx Xx0)) (((eq a) Xy) ((fun (x1:a)=> x1) Xx0)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xx0)))))) Xy) ((((conj ((and (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy)))) (forall (Xz:a), (((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz)))->(((eq a) Xz) Xy)))) ((((conj (Xx Xy)) (((eq a) Xy) ((fun (x1:a)=> x1) Xy))) x0) ((eq_ref a) Xy))) (fun (Xz:a) (x000:((and (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))))=> (((fun (P:Type) (x1:((Xx Xz)->((((eq a) Xy) ((fun (x1:a)=> x1) Xz))->P)))=> (((((and_rect (Xx Xz)) (((eq a) Xy) ((fun (x1:a)=> x1) Xz))) P) x1) x000)) (((eq a) Xz) Xy)) (fun (x01:(Xx Xz))=> (((eq_sym a) Xy) ((fun (x1:a)=> x1) Xz))))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------