%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV062^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 : n101.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:41 EDT 2014 % Result : Theorem 14.29s % Output : Proof 14.29s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV062^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n101.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:51:11 CDT 2014 % % CPUTime : 14.29 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (forall (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))))) of role conjecture named cT146A_pme % Conjecture to prove = (forall (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(forall (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy)))))'] % Parameter fofType:Type. % Trying to prove (forall (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))))) % Found x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found x1 as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found x2:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found x2 as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found x4:((Xr Xx0) Xy0) % Found (fun (x4:((Xr Xx0) Xy0))=> x4) as proof of ((Xr Xx0) Xy0) % Found (fun (Xy0:fofType) (x4:((Xr Xx0) Xy0))=> x4) as proof of (((Xr Xx0) Xy0)->((Xr Xx0) Xy0)) % Found (fun (Xx0:fofType) (Xy0:fofType) (x4:((Xr Xx0) Xy0))=> x4) as proof of (forall (Xy0:fofType), (((Xr Xx0) Xy0)->((Xr Xx0) Xy0))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x4:((Xr Xx0) Xy0))=> x4) as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xr Xx0) Xy0))) % Found x1000:=(x100 x3):((Xp Xx0) Xy0) % Found (x100 x3) as proof of ((Xp Xx0) Xy0) % Found ((x10 Xy0) x3) as proof of ((Xp Xx0) Xy0) % Found (((x1 Xx0) Xy0) x3) as proof of ((Xp Xx0) Xy0) % Found (fun (x20:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x1 Xx0) Xy0) x3)) as proof of ((Xp Xx0) Xy0) % Found (fun (x3:((Xr Xx0) Xy0)) (x20:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x1 Xx0) Xy0) x3)) as proof of ((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)) % Found (fun (Xy0:fofType) (x3:((Xr Xx0) Xy0)) (x20:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x1 Xx0) Xy0) x3)) as proof of (((Xr Xx0) Xy0)->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x3:((Xr Xx0) Xy0)) (x20:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x1 Xx0) Xy0) x3)) as proof of (forall (Xy0:fofType), (((Xr Xx0) Xy0)->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x3:((Xr Xx0) Xy0)) (x20:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x1 Xx0) Xy0) x3)) as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)))) % Found x10000:=(x1000 x2):((Xp Xx0) Xy0) % Found (x1000 x2) as proof of ((Xp Xx0) Xy0) % Found ((x100 Xy0) x2) as proof of ((Xp Xx0) Xy0) % Found (((x10 Xx0) Xy0) x2) as proof of ((Xp Xx0) Xy0) % Found (fun (x200:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x10 Xx0) Xy0) x2)) as proof of ((Xp Xx0) Xy0) % Found (fun (x10:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x200:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x10 Xx0) Xy0) x2)) as proof of ((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)) % Found (fun (x2:((Xr Xx0) Xy0)) (x10:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x200:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x10 Xx0) Xy0) x2)) as proof of ((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0))) % Found (fun (Xy0:fofType) (x2:((Xr Xx0) Xy0)) (x10:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x200:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x10 Xx0) Xy0) x2)) as proof of (((Xr Xx0) Xy0)->((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x2:((Xr Xx0) Xy0)) (x10:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x200:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x10 Xx0) Xy0) x2)) as proof of (forall (Xy0:fofType), (((Xr Xx0) Xy0)->((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0))))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x2:((Xr Xx0) Xy0)) (x10:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x200:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x10 Xx0) Xy0) x2)) as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0))))) % Found x2000:=(x200 x1):((Xp Xx0) Xy0) % Found (x200 x1) as proof of ((Xp Xx0) Xy0) % Found ((x20 Xy0) x1) as proof of ((Xp Xx0) Xy0) % Found (((x2 Xx0) Xy0) x1) as proof of ((Xp Xx0) Xy0) % Found (fun (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)) as proof of ((Xp Xx0) Xy0) % Found (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)) as proof of ((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)) % Found (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)) as proof of ((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0))) % Found (and_rect00 (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1))) as proof of ((Xp Xx0) Xy0) % Found ((and_rect0 ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1))) as proof of ((Xp Xx0) Xy0) % Found (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))) P) x2) x00)) ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1))) as proof of ((Xp Xx0) Xy0) % Found (fun (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))) P) x2) x00)) ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of ((Xp Xx0) Xy0) % Found (fun (x1:((Xr Xx0) Xy0)) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))) P) x2) x00)) ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))->((Xp Xx0) Xy0)) % Found (fun (Xy0:fofType) (x1:((Xr Xx0) Xy0)) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))) P) x2) x00)) ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (((Xr Xx0) Xy0)->(((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))->((Xp Xx0) Xy0))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x1:((Xr Xx0) Xy0)) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))) P) x2) x00)) ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (forall (Xy0:fofType), (((Xr Xx0) Xy0)->(((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))->((Xp Xx0) Xy0)))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x1:((Xr Xx0) Xy0)) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))) P) x2) x00)) ((Xp Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->(((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))->((Xp Xx0) Xy0)))) % Found x2000:=(x200 x1):((Xp0 Xx0) Xy0) % Found (x200 x1) as proof of ((Xp0 Xx0) Xy0) % Found ((x20 Xy0) x1) as proof of ((Xp0 Xx0) Xy0) % Found (((x2 Xx0) Xy0) x1) as proof of ((Xp0 Xx0) Xy0) % Found (fun (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)) as proof of ((Xp0 Xx0) Xy0) % Found (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)) as proof of ((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->((Xp0 Xx0) Xy0)) % Found (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)) as proof of ((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->((Xp0 Xx0) Xy0))) % Found (and_rect00 (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1))) as proof of ((Xp0 Xx0) Xy0) % Found ((and_rect0 ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1))) as proof of ((Xp0 Xx0) Xy0) % Found (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1))) as proof of ((Xp0 Xx0) Xy0) % Found (fun (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of ((Xp0 Xx0) Xy0) % Found (fun (Xp0:(fofType->(fofType->Prop))) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))->((Xp0 Xx0) Xy0)) % Found (fun (x1:((Xr Xx0) Xy0)) (Xp0:(fofType->(fofType->Prop))) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (forall (Xp0:(fofType->(fofType->Prop))), (((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))->((Xp0 Xx0) Xy0))) % Found (fun (Xy0:fofType) (x1:((Xr Xx0) Xy0)) (Xp0:(fofType->(fofType->Prop))) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (((Xr Xx0) Xy0)->(forall (Xp0:(fofType->(fofType->Prop))), (((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))->((Xp0 Xx0) Xy0)))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x1:((Xr Xx0) Xy0)) (Xp0:(fofType->(fofType->Prop))) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (forall (Xy0:fofType), (((Xr Xx0) Xy0)->(forall (Xp0:(fofType->(fofType->Prop))), (((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))->((Xp0 Xx0) Xy0))))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x1:((Xr Xx0) Xy0)) (Xp0:(fofType->(fofType->Prop))) (x00:((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))))=> (((fun (P:Type) (x2:((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))->P)))=> (((((and_rect (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz)))) P) x2) x00)) ((Xp0 Xx0) Xy0)) (fun (x2:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (x3:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))=> (((x2 Xx0) Xy0) x1)))) as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->(forall (Xp0:(fofType->(fofType->Prop))), (((and (forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp0 Xx00) Xy00)))) (forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp0 Xx00) Xy00)) ((Xp0 Xy00) Xz))->((Xp0 Xx00) Xz))))->((Xp0 Xx0) Xy0))))) % Found x3000:=(x300 x2):((Xp Xx0) Xy0) % Found (x300 x2) as proof of ((Xp Xx0) Xy0) % Found ((x30 Xy0) x2) as proof of ((Xp Xx0) Xy0) % Found (((x3 Xx0) Xy0) x2) as proof of ((Xp Xx0) Xy0) % Found (fun (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)) as proof of ((Xp Xx0) Xy0) % Found (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)) as proof of ((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0)) % Found (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)) as proof of ((forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))->((forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz)))->((Xp Xx0) Xy0))) % Found (and_rect00 (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2))) as proof of ((Xp Xx0) Xy0) % Found ((and_rect0 ((Xp Xx0) Xy0)) (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2))) as proof of ((Xp Xx0) Xy0) % Found (((fun (P:Type) (x3:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x3) x0)) ((Xp Xx0) Xy0)) (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2))) as proof of ((Xp Xx0) Xy0) % Found (fun (x2:((Xr Xx0) Xy0))=> (((fun (P:Type) (x3:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x3) x0)) ((Xp Xx0) Xy0)) (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)))) as proof of ((Xp Xx0) Xy0) % Found (fun (Xy0:fofType) (x2:((Xr Xx0) Xy0))=> (((fun (P:Type) (x3:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x3) x0)) ((Xp Xx0) Xy0)) (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)))) as proof of (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)) % Found (fun (Xx0:fofType) (Xy0:fofType) (x2:((Xr Xx0) Xy0))=> (((fun (P:Type) (x3:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x3) x0)) ((Xp Xx0) Xy0)) (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)))) as proof of (forall (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found (fun (Xx0:fofType) (Xy0:fofType) (x2:((Xr Xx0) Xy0))=> (((fun (P:Type) (x3:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x3) x0)) ((Xp Xx0) Xy0)) (fun (x3:(forall (Xx00:fofType) (Xy00:fofType), (((Xr Xx00) Xy00)->((Xp Xx00) Xy00)))) (x4:(forall (Xx00:fofType) (Xy00:fofType) (Xz:fofType), (((and ((Xp Xx00) Xy00)) ((Xp Xy00) Xz))->((Xp Xx00) Xz))))=> (((x3 Xx0) Xy0) x2)))) as proof of (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x10:=(x1 Xx0):(forall (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0))) % Found (x1 Xx0) as proof of (forall (Xy00:fofType), (((Xr Xx0) Xy00)->((Xp Xy0) Xy00))) % Found (x1 Xx0) as proof of (forall (Xy00:fofType), (((Xr Xx0) Xy00)->((Xp Xy0) Xy00))) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x40:=(x4 x20):((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found (x4 x20) as proof of ((Xp Xu) Xy0) % Found (x4 x20) as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x5:((Xp Xu) Xv) % Instantiate: Xy0:=Xv:fofType % Found x5 as proof of ((Xp Xu) Xy0) % Found x1000:=(x100 x6):((Xp Xy0) Xw) % Found (x100 x6) as proof of ((Xp Xy0) Xw) % Found ((x10 Xw) x6) as proof of ((Xp Xy0) Xw) % Found (((x1 Xy0) Xw) x6) as proof of ((Xp Xy0) Xw) % Found (((x1 Xy0) Xw) x6) as proof of ((Xp Xy0) Xw) % Found ((conj10 x5) (((x1 Xy0) Xw) x6)) as proof of ((and ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) % Found (((conj1 ((Xp Xy0) Xw)) x5) (((x1 Xy0) Xw) x6)) as proof of ((and ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) % Found ((((conj ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) x5) (((x1 Xy0) Xw) x6)) as proof of ((and ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) % Found ((((conj ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) x5) (((x1 Xy0) Xw) x6)) as proof of ((and ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) % Found (x2000 ((((conj ((Xp Xu) Xy0)) ((Xp Xy0) Xw)) x5) (((x1 Xy0) Xw) x6))) as proof of ((Xp Xu) Xw) % Found ((x200 Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))) as proof of ((Xp Xu) Xw) % Found (((fun (Xy0:fofType)=> ((x20 Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))) as proof of ((Xp Xu) Xw) % Found (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))) as proof of ((Xp Xu) Xw) % Found (fun (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))) as proof of ((Xp Xu) Xw) % Found (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))) as proof of (((Xr Xv) Xw)->((Xp Xu) Xw)) % Found (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))) as proof of (((Xp Xu) Xv)->(((Xr Xv) Xw)->((Xp Xu) Xw))) % Found (and_rect10 (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))) as proof of ((Xp Xu) Xw) % Found ((and_rect1 ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))) as proof of ((Xp Xu) Xw) % Found (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))) as proof of ((Xp Xu) Xw) % Found (fun (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))) as proof of ((Xp Xu) Xw) % Found (fun (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))) as proof of (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)) % Found (fun (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))) as proof of (forall (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))) % Found (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))) as proof of (forall (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))) % Found (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))) as proof of (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))) % Found ((conj00 x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))) as proof of ((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) % Found (((conj0 (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))) as proof of ((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) % Found ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))) as proof of ((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) % Found ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))) as proof of ((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) % Found (x3 ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))))) as proof of ((Xp Xx) Xy) % Found ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))))) as proof of ((Xp Xx) Xy) % Found (fun (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))) as proof of ((Xp Xx) Xy) % Found (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))) as proof of ((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->((Xp Xx) Xy)) % Found (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))) as proof of ((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->((Xp Xx) Xy))) % Found (and_rect00 (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))))))) as proof of ((Xp Xx) Xy) % Found ((and_rect0 ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))))))) as proof of ((Xp Xx) Xy) % Found (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6)))))))))) as proof of ((Xp Xx) Xy) % Found (fun (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of ((Xp Xx) Xy) % Found (fun (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy)) % Found (fun (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of (forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))) % Found (fun (Xy:fofType) (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy)))) % Found (fun (Xx:fofType) (Xy:fofType) (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of (forall (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))))) % Found (fun (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType) (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of (forall (Xx:fofType) (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))))) % Found (fun (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType) (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) as proof of (forall (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType), ((forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))->(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))->((Xp Xx) Xy))))) % Got proof (fun (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType) (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) % Time elapsed = 13.830762s % node=1915 cost=1415.000000 depth=41 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (Xr:(fofType->(fofType->Prop))) (Xx:fofType) (Xy:fofType) (x:(forall (Xp:(fofType->(fofType->Prop))), (((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw))))->((Xp Xx) Xy)))) (Xp:(fofType->(fofType->Prop))) (x0:((and (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))))=> (((fun (P:Type) (x1:((forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))->P)))=> (((((and_rect (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:fofType) (Xy0:fofType) (Xz:fofType), (((and ((Xp Xx0) Xy0)) ((Xp Xy0) Xz))->((Xp Xx0) Xz))))=> ((x Xp) ((((conj (forall (Xx0:fofType) (Xy0:fofType), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xu:fofType) (Xv:fofType) (Xw:fofType), (((and ((Xp Xu) Xv)) ((Xr Xv) Xw))->((Xp Xu) Xw)))) x1) (fun (Xu:fofType) (Xv:fofType) (Xw:fofType) (x4:((and ((Xp Xu) Xv)) ((Xr Xv) Xw)))=> (((fun (P:Type) (x5:(((Xp Xu) Xv)->(((Xr Xv) Xw)->P)))=> (((((and_rect ((Xp Xu) Xv)) ((Xr Xv) Xw)) P) x5) x4)) ((Xp Xu) Xw)) (fun (x5:((Xp Xu) Xv)) (x6:((Xr Xv) Xw))=> (((fun (Xy0:fofType)=> (((x2 Xu) Xy0) Xw)) Xv) ((((conj ((Xp Xu) Xv)) ((Xp Xv) Xw)) x5) (((x1 Xv) Xw) x6))))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------