%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV097^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 : n095.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:44 EDT 2014 % Result : Theorem 86.51s % Output : Proof 86.51s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV097^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n095.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 08:02:56 CDT 2014 % % CPUTime : 86.51 % 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 0x113eb00>, <kernel.Type object at 0x113ebd8>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (<kernel.Constant object at 0x11ee878>, <kernel.Type object at 0x113e3f8>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (<kernel.Constant object at 0x113e1b8>, <kernel.Constant object at 0x113eb00>) of role type named z % Using role type % Declaring z:a % FOF formula (<kernel.Constant object at 0x113e320>, <kernel.DependentProduct object at 0x113d680>) of role type named cR % Using role type % Declaring cR:(a->(a->Prop)) % FOF formula (<kernel.Constant object at 0x113eb00>, <kernel.DependentProduct object at 0x113dcb0>) of role type named f % Using role type % Declaring f:(a->(b->Prop)) % FOF formula (<kernel.Constant object at 0x113e1b8>, <kernel.DependentProduct object at 0x113d5a8>) of role type named cS % Using role type % Declaring cS:(b->(b->Prop)) % FOF formula (((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))->(((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))->(forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))))) of role conjecture named cTHM552C_pme % Conjecture to prove = (((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))->(((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))->(forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))))):Prop % Parameter b_DUMMY:b. % We need to prove ['(((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))->(((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))->(forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))))))'] % Parameter a:Type. % Parameter b:Type. % Parameter z:a. % Parameter cR:(a->(a->Prop)). % Parameter f:(a->(b->Prop)). % Parameter cS:(b->(b->Prop)). % Trying to prove (((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))->(((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))->(forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))))) % Found or_introl00:=(or_introl0 ((and (((f Xw) x5)->False)) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found (or_introl0 ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (((f Xw) x5)->False)) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found (or_introl0 ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (((f Xw) x3)->False)) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found (or_introl0 ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (((f Xw) x3)->False)) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found (or_introl0 ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x3)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x3)) ((and (((f Xw) x3)->False)) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (((f Xw) x1)->False)) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found (or_introl0 ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (((f Xw) x1)->False)) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found (or_introl0 ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (((f Xw) x1)->False)) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x1)) ((and (((f Xw) x1)->False)) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (not ((f Xw) x5))) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found (or_introl0 ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found or_introl00:=(or_introl0 ((and (not ((f Xw) x5))) ((cR Xx) z))):(((f Xx0) x6)->((or ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found (or_introl0 ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found ((or_introl ((f Xx0) x6)) ((and (not ((f Xw) x5))) ((cR Xx) z))) as proof of (((f Xx0) x6)->((or ((f Xx) x5)) ((and (not ((f Xw) x5))) ((cR Xx) z)))) % Found x6:((f Xx0) x5) % Instantiate: Xx0:=Xx:a;x7:=x5:b % Found x6 as proof of ((f Xx) x7) % Found (or_introl00 x6) as proof of ((or ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) % Found ((or_introl0 ((and (((f Xw) x7)->False)) ((cR Xx) z))) x6) as proof of ((or ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) % Found (((or_introl ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) x6) as proof of ((or ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) % Found (fun (Xw:a)=> (((or_introl ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) x6)) as proof of ((or ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) % Found (fun (Xw:a)=> (((or_introl ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) x6)) as proof of (forall (Xw:a), ((or ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z)))) % Found (ex_intro000 (fun (Xw:a)=> (((or_introl ((f Xx) x7)) ((and (((f Xw) x7)->False)) ((cR Xx) z))) x6))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found ((ex_intro00 x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (((ex_intro0 (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x6:((f Xx0) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x5:b) (x6:((f Xx0) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))) as proof of (((f Xx0) x5)->((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) % Found (fun (x5:b) (x6:((f Xx0) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))) as proof of (forall (x:b), (((f Xx0) x)->((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))))) % Found (ex_ind00 (fun (x5:b) (x6:((f Xx0) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found ((ex_ind0 ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx0) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (((fun (P:Prop) (x5:(forall (x:b), (((f Xx0) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx0) Xy))) P) x5) x30)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx0) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))) as proof of ((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) % Found (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))) as proof of ((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))))) % Found (and_rect10 (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found ((and_rect1 ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))) as proof of ((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) % Found (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))) as proof of (((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))))) % Found (and_rect00 (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found ((and_rect0 ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6))))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (Xx:a)=> (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))))) as proof of ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) % Found (fun (x0:((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))) (Xx:a)=> (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))))) as proof of (forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) % Found (fun (x:((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))) (x0:((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))) (Xx:a)=> (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))))) as proof of (((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))->(forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))))) % Found (fun (x:((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))) (x0:((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))) (Xx:a)=> (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))))) as proof of (((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))->(((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))->(forall (Xx:a), ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))))) % Got proof (fun (x:((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))) (x0:((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))) (Xx:a)=> (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))))) % Time elapsed = 85.442089s % node=9589 cost=1687.000000 depth=32 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:((and (forall (Xu:a) (Xv:a) (Xw:a), (((and ((cR Xu) Xv)) ((cR Xw) Xv))->((cR Xu) Xw)))) (forall (Xx:a), ((cR Xx) Xx)))) (x0:((and ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))) (Xx:a)=> (((fun (P:Type) (x1:(((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))->((forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))->P)))=> (((((and_rect ((and (forall (Xx:a), ((ex b) (fun (Xy:b)=> ((f Xx) Xy))))) (forall (Xx:a) (Xy1:b) (Xy2:b), (((and ((f Xx) Xy1)) ((f Xx) Xy2))->((cS Xy1) Xy2))))) (forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2)))) P) x1) x0)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x1:((and (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))) (x2:(forall (Xx1:a) (Xx2:a) (Xy:b), (((and ((f Xx1) Xy)) ((f Xx2) Xy))->((cR Xx1) Xx2))))=> (((fun (P:Type) (x3:((forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))->((forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))->P)))=> (((((and_rect (forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2)))) P) x3) x1)) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x3:(forall (Xx0:a), ((ex b) (fun (Xy:b)=> ((f Xx0) Xy))))) (x4:(forall (Xx0:a) (Xy1:b) (Xy2:b), (((and ((f Xx0) Xy1)) ((f Xx0) Xy2))->((cS Xy1) Xy2))))=> (((fun (P:Prop) (x5:(forall (x:b), (((f Xx) x)->P)))=> (((((ex_ind b) (fun (Xy:b)=> ((f Xx) Xy))) P) x5) (x3 Xx))) ((ex b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z))))))) (fun (x5:b) (x6:((f Xx) x5))=> ((((ex_intro b) (fun (Xy:b)=> (forall (Xw:a), ((or ((f Xx) Xy)) ((and (((f Xw) Xy)->False)) ((cR Xx) z)))))) x5) (fun (Xw:a)=> (((or_introl ((f Xx) x5)) ((and (((f Xw) x5)->False)) ((cR Xx) z))) x6)))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------