%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV186^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 : n105.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:51 EDT 2014 % Result : Theorem 17.80s % Output : Proof 17.80s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV186^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n105.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:24:26 CDT 2014 % % CPUTime : 17.80 % 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 0x1561b48>, <kernel.Type object at 0x1561560>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (forall (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))))) of role conjecture named cTHM565_pme % Conjecture to prove = (forall (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))))):Prop % Parameter b_DUMMY:b. % We need to prove ['(forall (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))))))'] % Parameter b:Type. % Trying to prove (forall (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))))) % Found x2:(S S0) % Found x2 as proof of (S S00) % Found x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) % Instantiate: X0:=X:(b->Prop) % Found x0 as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx0)))))) ((P X0) Y0)) % Found x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) % Instantiate: X0:=X:(b->Prop) % Found x0 as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx0)))))) ((P X0) Y0)) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:(X0 Xx0) % Found x4 as proof of (S0 Xx0) % Found (fun (x4:(X0 Xx0))=> x4) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x4:(X0 Xx0))=> x4) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found x4 as proof of ((P X0) Y) % Found x4:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found x4 as proof of ((P X0) Y) % Found x4:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found x4 as proof of ((P X0) Y) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x5:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found (fun (x5:((P X) Y))=> x5) as proof of ((P X0) Y) % Found (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5) as proof of (((P X) Y)->((P X0) Y)) % Found (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5) as proof of ((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->((P X0) Y))) % Found (and_rect00 (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found ((and_rect0 ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found (((fun (P0:Type) (x4:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x4) x0)) ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found (((fun (P0:Type) (x4:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x4) x0)) ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found x5:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found (fun (x5:((P X) Y))=> x5) as proof of ((P X0) Y) % Found (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5) as proof of (((P X) Y)->((P X0) Y)) % Found (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5) as proof of ((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->((P X0) Y))) % Found (and_rect00 (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found ((and_rect0 ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found (((fun (P0:Type) (x4:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x4) x0)) ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found (((fun (P0:Type) (x4:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x4) x0)) ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found x5:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found (fun (x5:((P X) Y))=> x5) as proof of ((P X0) Y) % Found (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5) as proof of (((P X) Y)->((P X0) Y)) % Found (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5) as proof of ((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->((P X0) Y))) % Found (and_rect00 (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found ((and_rect0 ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found (((fun (P0:Type) (x4:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x4) x0)) ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found (((fun (P0:Type) (x4:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x4) x0)) ((P X0) Y)) (fun (x4:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x5:((P X) Y))=> x5)) as proof of ((P X0) Y) % Found x5:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found x5 as proof of ((P X0) Y) % Found x5:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found x5 as proof of ((P X0) Y) % Found x5:((P X) Y) % Instantiate: X0:=X:(b->Prop) % Found x5 as proof of ((P X0) Y) % Found x6:(X0 Xx0) % Instantiate: X0:=S0:(b->Prop) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Instantiate: X0:=S0:(b->Prop) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Instantiate: X0:=S0:(b->Prop) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x6:(X0 Xx0) % Found x6 as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> x6) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> x6) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x30000:=(x3000 x2):(S0 Xx0) % Found (x3000 x2) as proof of (S0 Xx0) % Found ((x300 S0) x2) as proof of (S0 Xx0) % Found (((x30 x6) S0) x2) as proof of (S0 Xx0) % Found ((((x3 Xx0) x6) S0) x2) as proof of (S0 Xx0) % Found (fun (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2)) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2)) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2)) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found ((conj00 (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) % Found (((conj0 ((P X0) Y)) (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) % Found ((((conj (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) % Found ((((conj (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) % Found (x500000 ((((conj (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)) (fun (Xx0:b) (x6:(X0 Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found ((x50000 X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> (((x5000 X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> ((x500 X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((x50 X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> (((((x5 x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)) as proof of (S0 Xx) % Found (fun (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))) as proof of (S0 Xx) % Found (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))) as proof of (((P X) Y)->(S0 Xx)) % Found (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))) as proof of ((forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))->(((P X) Y)->(S0 Xx))) % Found (and_rect00 (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)))) as proof of (S0 Xx) % Found ((and_rect0 (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)))) as proof of (S0 Xx) % Found (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4)))) as proof of (S0 Xx) % Found (fun (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (S0 Xx) % Found (fun (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of ((S S0)->(S0 Xx)) % Found (fun (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (forall (S0:(b->Prop)), ((S S0)->(S0 Xx))) % Found (fun (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))) % Found (fun (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))) % Found (fun (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) % Found (fun (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (forall (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))) % Found (fun (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))) (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))) % Found (fun (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))) (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))))) % Found (fun (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))) (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (forall (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))))) % Found (fun (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))) (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) as proof of (forall (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))->(forall (Xx:b), ((Y Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx))))))))) % Got proof (fun (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))) (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) % Time elapsed = 17.302542s % node=3030 cost=1296.000000 depth=34 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (P:((b->Prop)->((b->Prop)->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Y:(b->Prop)), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Y))->(forall (Xx0:b), ((Y Xx0)->(Xx Xx0)))))))) (X:(b->Prop)) (Y:(b->Prop)) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y))) (Xx:b) (x1:(Y Xx)) (S0:(b->Prop)) (x2:(S S0))=> (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Y)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Y)) P0) x3) x0)) (S0 Xx)) (fun (x3:(forall (Xx0:b), ((X Xx0)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx0)))))) (x4:((P X) Y))=> (((fun (X0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y)))=> ((((fun (X0:(b->Prop))=> (((fun (X0:(b->Prop)) (Y0:(b->Prop)) (x6:((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Y0)))=> ((((((x S0) x2) X0) Y0) x6) Xx)) X0) Y)) X0) x6) x1)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Y)) (fun (Xx0:b) (x6:(X Xx0))=> ((((x3 Xx0) x6) S0) x2))) x4))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------