%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV259^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 : n094.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:57 EDT 2014 % Result : Theorem 1.08s % Output : Proof 1.08s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV259^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n094.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:38:46 CDT 2014 % % CPUTime : 1.08 % 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 0x1478e18>, <kernel.Type object at 0x1459560>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (forall (S:((b->Prop)->Prop)), (((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))->(forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))))))) of role conjecture named cCLOSURE_THM0_pme % Conjecture to prove = (forall (S:((b->Prop)->Prop)), (((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))->(forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))))))):Prop % Parameter b_DUMMY:b. % We need to prove ['(forall (S:((b->Prop)->Prop)), (((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))->(forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx)))))))'] % Parameter b:Type. % Trying to prove (forall (S:((b->Prop)->Prop)), (((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))->(forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))))))) % Found x200:=(x20 x0):(S0 Xx) % Found (x20 x0) as proof of (S0 Xx) % Found ((x2 Xx) x0) as proof of (S0 Xx) % Found (fun (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)) as proof of (S0 Xx) % Found (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)) as proof of ((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->(S0 Xx)) % Found (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)) as proof of ((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->(S0 Xx))) % Found (and_rect00 (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0))) as proof of (S0 Xx) % Found ((and_rect0 (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0))) as proof of (S0 Xx) % Found (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0))) as proof of (S0 Xx) % Found (fun (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (S0 Xx) % Found (fun (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx)) % Found (fun (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))) % Found (fun (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx)))) % Found (fun (W:(b->Prop)) (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (forall (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))))) % Found (fun (x:((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))) (W:(b->Prop)) (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))))) % Found (fun (S:((b->Prop)->Prop)) (x:((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))) (W:(b->Prop)) (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))->(forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx)))))) % Found (fun (S:((b->Prop)->Prop)) (x:((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))) (W:(b->Prop)) (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) as proof of (forall (S:((b->Prop)->Prop)), (((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))->(forall (W:(b->Prop)) (Xx:b), ((W Xx)->(forall (S0:(b->Prop)), (((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))->(S0 Xx))))))) % Got proof (fun (S:((b->Prop)->Prop)) (x:((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))) (W:(b->Prop)) (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) % Time elapsed = 0.761788s % node=32 cost=193.000000 depth=15 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (S:((b->Prop)->Prop)) (x:((and ((and ((and (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> False))->(S R)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx:b)=> (False->False)))->(S R))))) (forall (K:((b->Prop)->Prop)) (R:(b->Prop)), (((and (forall (Xx:(b->Prop)), ((K Xx)->(S Xx)))) (((eq (b->Prop)) R) (fun (Xx:b)=> ((ex (b->Prop)) (fun (S0:(b->Prop))=> ((and (K S0)) (S0 Xx)))))))->(S R))))) (forall (Y:(b->Prop)) (Z:(b->Prop)) (S0:(b->Prop)), (((and ((and (S Y)) (S Z))) (((eq (b->Prop)) S0) (fun (Xx:b)=> ((and (Y Xx)) (Z Xx)))))->(S S0))))) (W:(b->Prop)) (Xx:b) (x0:(W Xx)) (S0:(b->Prop)) (x1:((and (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))))=> (((fun (P:Type) (x2:((forall (Xx0:b), ((W Xx0)->(S0 Xx0)))->((forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))->P)))=> (((((and_rect (forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R)))) P) x2) x1)) (S0 Xx)) (fun (x2:(forall (Xx0:b), ((W Xx0)->(S0 Xx0)))) (x3:(forall (R:(b->Prop)), ((((eq (b->Prop)) R) (fun (Xx0:b)=> ((S0 Xx0)->False)))->(S R))))=> ((x2 Xx) x0)))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------