%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV292^5 : TPTP v6.2.0. Bugfixed v6.2.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n039.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-504.8.1.el6.x86_64 % CPULimit : 300s % DateTime : Tue Apr 21 16:51:41 EDT 2015 % Result : Theorem 1.74s % Output : Proof 1.74s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SEV292^5 : TPTP v6.2.0. Bugfixed v6.2.0. % 0.00/0.03 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.01/1.06 % Computer : n039.star.cs.uiowa.edu % 0.01/1.06 % Model : x86_64 x86_64 % 0.01/1.06 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.01/1.06 % Memory : 32286.75MB % 0.01/1.06 % OS : Linux 2.6.32-504.8.1.el6.x86_64 % 0.01/1.06 % CPULimit : 300 % 0.01/1.06 % DateTime : Thu Apr 16 12:08:37 CDT 2015 % 0.01/1.06 % CPUTime : % 0.01/1.08 Python 2.7.5 % 0.23/1.34 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.23/1.34 FOF formula (<kernel.Constant object at 0xde7ab8>, <kernel.DependentProduct object at 0xde7bd8>) of role type named cP_type % 0.23/1.34 Using role type % 0.23/1.34 Declaring cP:(((fofType->Prop)->Prop)->Prop) % 0.23/1.34 FOF formula (<kernel.Constant object at 0xcb4f38>, <kernel.DependentProduct object at 0xde7b00>) of role type named cONE_type % 0.23/1.34 Using role type % 0.23/1.34 Declaring cONE:((fofType->Prop)->Prop) % 0.23/1.34 FOF formula (<kernel.Constant object at 0xde79e0>, <kernel.DependentProduct object at 0xde77e8>) of role type named cSUCC_type % 0.23/1.34 Using role type % 0.23/1.34 Declaring cSUCC:(((fofType->Prop)->Prop)->((fofType->Prop)->Prop)) % 0.23/1.34 FOF formula (<kernel.Constant object at 0xde77a0>, <kernel.DependentProduct object at 0xde7b00>) of role type named cZERO_type % 0.23/1.34 Using role type % 0.23/1.34 Declaring cZERO:((fofType->Prop)->Prop) % 0.23/1.34 FOF formula (<kernel.Constant object at 0xde7f80>, <kernel.DependentProduct object at 0xde7680>) of role type named c_less__eq__type % 0.23/1.34 Using role type % 0.23/1.34 Declaring c_less__eq_:(((fofType->Prop)->Prop)->(((fofType->Prop)->Prop)->Prop)) % 0.23/1.34 FOF formula (((eq ((fofType->Prop)->Prop)) cZERO) (fun (Xp:(fofType->Prop))=> (((ex fofType) (fun (Xx:fofType)=> (Xp Xx)))->False))) of role definition named cZERO_def % 0.23/1.34 A new definition: (((eq ((fofType->Prop)->Prop)) cZERO) (fun (Xp:(fofType->Prop))=> (((ex fofType) (fun (Xx:fofType)=> (Xp Xx)))->False))) % 0.23/1.34 Defined: cZERO:=(fun (Xp:(fofType->Prop))=> (((ex fofType) (fun (Xx:fofType)=> (Xp Xx)))->False)) % 0.23/1.34 FOF formula (((eq (((fofType->Prop)->Prop)->((fofType->Prop)->Prop))) cSUCC) (fun (Xn:((fofType->Prop)->Prop)) (Xp:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xp Xx)) (Xn (fun (Xt:fofType)=> ((and (not (((eq fofType) Xt) Xx))) (Xp Xt))))))))) of role definition named cSUCC_def % 0.23/1.34 A new definition: (((eq (((fofType->Prop)->Prop)->((fofType->Prop)->Prop))) cSUCC) (fun (Xn:((fofType->Prop)->Prop)) (Xp:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xp Xx)) (Xn (fun (Xt:fofType)=> ((and (not (((eq fofType) Xt) Xx))) (Xp Xt))))))))) % 0.23/1.34 Defined: cSUCC:=(fun (Xn:((fofType->Prop)->Prop)) (Xp:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xp Xx)) (Xn (fun (Xt:fofType)=> ((and (not (((eq fofType) Xt) Xx))) (Xp Xt)))))))) % 0.23/1.34 FOF formula (((eq ((fofType->Prop)->Prop)) cONE) (cSUCC cZERO)) of role definition named cONE_def % 0.23/1.34 A new definition: (((eq ((fofType->Prop)->Prop)) cONE) (cSUCC cZERO)) % 0.23/1.34 Defined: cONE:=(cSUCC cZERO) % 0.23/1.34 FOF formula (((eq (((fofType->Prop)->Prop)->(((fofType->Prop)->Prop)->Prop))) c_less__eq_) (fun (Xx:((fofType->Prop)->Prop)) (Xy:((fofType->Prop)->Prop))=> (forall (Xp:(((fofType->Prop)->Prop)->Prop)), (((and (Xp Xx)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp Xy))))) of role definition named c_less__eq__def % 0.23/1.34 A new definition: (((eq (((fofType->Prop)->Prop)->(((fofType->Prop)->Prop)->Prop))) c_less__eq_) (fun (Xx:((fofType->Prop)->Prop)) (Xy:((fofType->Prop)->Prop))=> (forall (Xp:(((fofType->Prop)->Prop)->Prop)), (((and (Xp Xx)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp Xy))))) % 0.23/1.34 Defined: c_less__eq_:=(fun (Xx:((fofType->Prop)->Prop)) (Xy:((fofType->Prop)->Prop))=> (forall (Xp:(((fofType->Prop)->Prop)->Prop)), (((and (Xp Xx)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp Xy)))) % 0.23/1.34 FOF formula ((cP cONE)->((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx))))) of role conjecture named cBLEDSOE7A % 0.23/1.34 Conjecture to prove = ((cP cONE)->((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx))))):Prop % 0.23/1.34 Parameter fofType_DUMMY:fofType. % 0.23/1.34 We need to prove ['((cP cONE)->((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))))'] % 0.23/1.34 Parameter fofType:Type. % 0.23/1.34 Parameter cP:(((fofType->Prop)->Prop)->Prop). % 0.23/1.34 Definition cONE:=(cSUCC cZERO):((fofType->Prop)->Prop). % 0.23/1.34 Definition cSUCC:=(fun (Xn:((fofType->Prop)->Prop)) (Xp:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xp Xx)) (Xn (fun (Xt:fofType)=> ((and (not (((eq fofType) Xt) Xx))) (Xp Xt)))))))):(((fofType->Prop)->Prop)->((fofType->Prop)->Prop)). % 1.15/2.27 Definition cZERO:=(fun (Xp:(fofType->Prop))=> (((ex fofType) (fun (Xx:fofType)=> (Xp Xx)))->False)):((fofType->Prop)->Prop). % 1.15/2.27 Definition c_less__eq_:=(fun (Xx:((fofType->Prop)->Prop)) (Xy:((fofType->Prop)->Prop))=> (forall (Xp:(((fofType->Prop)->Prop)->Prop)), (((and (Xp Xx)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp Xy)))):(((fofType->Prop)->Prop)->(((fofType->Prop)->Prop)->Prop)). % 1.15/2.27 Trying to prove ((cP cONE)->((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx))))) % 1.15/2.27 Found x:(cP cONE) % 1.15/2.27 Instantiate: x0:=cONE:((fofType->Prop)->Prop) % 1.15/2.27 Found x as proof of (cP x0) % 1.15/2.27 Found x:(cP (cSUCC cZERO)) % 1.15/2.27 Instantiate: x0:=(cSUCC cZERO):((fofType->Prop)->Prop) % 1.15/2.27 Found x as proof of (cP x0) % 1.15/2.27 Found x2:(Xp cZERO) % 1.15/2.27 Instantiate: x0:=cZERO:((fofType->Prop)->Prop) % 1.15/2.27 Found (fun (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of (Xp x0) % 1.15/2.27 Found (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp x0)) % 1.15/2.27 Found (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp x0))) % 1.15/2.27 Found (and_rect00 (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp x0) % 1.15/2.27 Found ((and_rect0 (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp x0) % 1.15/2.27 Found (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp x0) % 1.15/2.27 Found (fun (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (Xp x0) % 1.15/2.27 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp x0)) % 1.15/2.27 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of ((c_less__eq_ cZERO) x0) % 1.15/2.27 Found x2:(Xp x0) % 1.15/2.27 Instantiate: x0:=(fun (Xp0:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xp0 Xx)) (cONE (fun (Xt:fofType)=> ((and (not (((eq fofType) Xt) Xx))) (Xp0 Xt)))))))):((fofType->Prop)->Prop) % 1.15/2.27 Found (fun (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of (Xp (cSUCC cONE)) % 1.15/2.27 Found (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp (cSUCC cONE))) % 1.44/2.53 Found (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp (cSUCC cONE)))) % 1.44/2.53 Found (and_rect00 (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp (cSUCC cONE)) % 1.44/2.53 Found ((and_rect0 (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp (cSUCC cONE)) % 1.44/2.53 Found (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp (cSUCC cONE)) % 1.44/2.53 Found (fun (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (Xp (cSUCC cONE)) % 1.44/2.53 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp (cSUCC cONE))) % 1.44/2.53 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of ((c_less__eq_ x0) (cSUCC cONE)) % 1.44/2.53 Found x2:(Xp cZERO) % 1.44/2.53 Instantiate: x0:=cZERO:((fofType->Prop)->Prop) % 1.44/2.53 Found (fun (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of (Xp x0) % 1.44/2.53 Found (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp x0)) % 1.44/2.53 Found (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp x0))) % 1.44/2.53 Found (and_rect00 (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp x0) % 1.44/2.53 Found ((and_rect0 (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp x0) % 1.44/2.53 Found (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp x0) % 1.44/2.53 Found (fun (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (Xp x0) % 1.54/2.63 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp x0)) % 1.54/2.63 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of ((c_less__eq_ cZERO) x0) % 1.54/2.63 Found x2:(Xp x0) % 1.54/2.63 Instantiate: x0:=(fun (Xp0:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xp0 Xx)) ((cSUCC cZERO) (fun (Xt:fofType)=> ((and (not (((eq fofType) Xt) Xx))) (Xp0 Xt)))))))):((fofType->Prop)->Prop) % 1.54/2.63 Found (fun (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of (Xp (cSUCC (cSUCC cZERO))) % 1.54/2.63 Found (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp (cSUCC (cSUCC cZERO)))) % 1.54/2.63 Found (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2) as proof of ((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp (cSUCC (cSUCC cZERO))))) % 1.54/2.63 Found (and_rect00 (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp (cSUCC (cSUCC cZERO))) % 1.54/2.63 Found ((and_rect0 (Xp (cSUCC (cSUCC cZERO)))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp (cSUCC (cSUCC cZERO))) % 1.54/2.63 Found (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC (cSUCC cZERO)))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2)) as proof of (Xp (cSUCC (cSUCC cZERO))) % 1.54/2.63 Found (fun (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC (cSUCC cZERO)))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (Xp (cSUCC (cSUCC cZERO))) % 1.54/2.63 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC (cSUCC cZERO)))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of (((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp (cSUCC (cSUCC cZERO)))) % 1.54/2.63 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC (cSUCC cZERO)))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> x2))) as proof of ((c_less__eq_ x0) (cSUCC (cSUCC cZERO))) % 1.64/2.74 Found x300:=(x30 x2):(Xp (cSUCC cONE)) % 1.64/2.74 Found (x30 x2) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found ((x3 cONE) x2) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found (fun (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)) as proof of ((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp (cSUCC cONE))) % 1.64/2.74 Found (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)) as proof of ((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp (cSUCC cONE)))) % 1.64/2.74 Found (and_rect00 (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2))) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found ((and_rect0 (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2))) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2))) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found (fun (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))) as proof of (Xp (cSUCC cONE)) % 1.64/2.74 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))) as proof of (((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp (cSUCC cONE))) % 1.64/2.74 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))) as proof of ((c_less__eq_ x0) (cSUCC cONE)) % 1.64/2.74 Found x300:=(x30 x2):(Xp (cSUCC cZERO)) % 1.64/2.74 Found (x30 x2) as proof of (Xp x0) % 1.64/2.74 Found ((x3 cZERO) x2) as proof of (Xp x0) % 1.64/2.74 Found (fun (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2)) as proof of (Xp x0) % 1.64/2.74 Found (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2)) as proof of ((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp x0)) % 1.64/2.74 Found (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2)) as proof of ((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->(Xp x0))) % 1.64/2.74 Found (and_rect00 (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))) as proof of (Xp x0) % 1.64/2.74 Found ((and_rect0 (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))) as proof of (Xp x0) % 1.64/2.76 Found (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))) as proof of (Xp x0) % 1.64/2.76 Found (fun (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2)))) as proof of (Xp x0) % 1.64/2.76 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2)))) as proof of (((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))->(Xp x0)) % 1.64/2.76 Found (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2)))) as proof of ((c_less__eq_ cZERO) x0) % 1.64/2.76 Found ((conj10 (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2))))) as proof of ((and ((c_less__eq_ cZERO) x0)) % ((c_less__eq_ x0) (cSUCC cONE))) % 1.64/2.76 Found (((conj1 ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2))))) as proof of ((and % ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) % 1.64/2.76 Found ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) % x2))))) as proof of ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) % 1.64/2.77 Found ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) % x2))))) as proof of ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) % 1.64/2.77 Found ((conj00 ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 % cONE) x2)))))) x) as proof of ((and ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) % 1.64/2.77 Found (((conj0 (cP x0)) ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC % Xz)))))=> ((x3 cONE) x2)))))) x) as proof of ((and ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) % 1.64/2.79 Found ((((conj ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) % (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x) as proof of ((and ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) % 1.64/2.79 Found ((((conj ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp x0)) % (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x) as proof of ((and ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) % 1.64/2.79 Found (ex_intro000 ((((conj ((and ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE)))) (cP x0)) ((((conj ((c_less__eq_ cZERO) x0)) ((c_less__eq_ x0) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp x0)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp x0)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp x0)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun % (x2:(Xp x0)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x)) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) % 1.64/2.79 Found ((ex_intro00 cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp % (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x)) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) % 1.74/2.81 Found (((ex_intro0 (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC % Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x)) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) % 1.74/2.81 Found ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall (Xz:((fofType->Prop)->Prop)), % ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x)) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) % 1.74/2.81 Found (fun (x:(cP cONE))=> ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall % (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x))) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) % 1.74/2.82 Found (fun (x:(cP cONE))=> ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall % (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x))) as proof of ((cP cONE)->((ex ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx))))) % 1.74/2.82 Got proof (fun (x:(cP cONE))=> ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall % (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x))) % 1.74/2.83 Time elapsed = 1.456651s % 1.74/2.83 node=155 cost=760.000000 depth=24 % 1.74/2.83:::::::::::::::::::::: % 1.74/2.83 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.74/2.83 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.74/2.83 (fun (x:(cP cONE))=> ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xx:((fofType->Prop)->Prop))=> ((and ((and ((c_less__eq_ cZERO) Xx)) ((c_less__eq_ Xx) (cSUCC cONE)))) (cP Xx)))) cONE) ((((conj ((and ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE)))) (cP cONE)) ((((conj ((c_less__eq_ cZERO) cONE)) ((c_less__eq_ cONE) (cSUCC cONE))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cZERO)->((forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cZERO)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp cONE)) (fun (x2:(Xp cZERO)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cZERO) x2))))) (fun (Xp:(((fofType->Prop)->Prop)->Prop)) (x1:((and (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))))=> (((fun (P:Type) (x2:((Xp cONE)->((forall % (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))->P)))=> (((((and_rect (Xp cONE)) (forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz))))) P) x2) x1)) (Xp (cSUCC cONE))) (fun (x2:(Xp cONE)) (x3:(forall (Xz:((fofType->Prop)->Prop)), ((Xp Xz)->(Xp (cSUCC Xz)))))=> ((x3 cONE) x2)))))) x))) % 1.74/2.83 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------