%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV072^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 : n180.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:42 EDT 2014 % Result : Theorem 1.57s % Output : Proof 1.57s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV072^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n180.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 07:55:31 CDT 2014 % % CPUTime : 1.57 % 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 0xf13dd0>, <kernel.Type object at 0xf13518>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (forall (Xr:(a->(a->Prop))) (Xx:a) (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) of role conjecture named cTHM522_pme % Conjecture to prove = (forall (Xr:(a->(a->Prop))) (Xx:a) (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))):Prop % Parameter a_DUMMY:a. % We need to prove ['(forall (Xr:(a->(a->Prop))) (Xx:a) (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))))'] % Parameter a:Type. % Trying to prove (forall (Xr:(a->(a->Prop))) (Xx:a) (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) % Found or_comm_i00:=(or_comm_i0 ((Xr Xy0) Xx0)):(((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))) % Found (or_comm_i0 ((Xr Xy0) Xx0)) as proof of (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))) % Found ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)) as proof of (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))) % Found (fun (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) as proof of (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))) % Found (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) as proof of (forall (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0)))) % Found (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) as proof of (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0)))) % Found or_introl00:=(or_introl0 ((Xr Xy0) Xx0)):(((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) % Found (or_introl0 ((Xr Xy0) Xx0)) as proof of (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) % Found ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)) as proof of (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) % Found (fun (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) as proof of (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) % Found (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) as proof of (forall (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) % Found (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))) as proof of (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) % Found ((conj10 (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) as proof of ((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) % Found (((conj1 (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) as proof of ((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) % Found ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) as proof of ((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) % Found ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) as proof of ((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) % Found (x0 ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) as proof of ((or ((Xr Xx) Xy)) ((Xr Xy) Xx)) % Found ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) as proof of ((or ((Xr Xx) Xy)) ((Xr Xy) Xx)) % Found (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))) as proof of ((or ((Xr Xx) Xy)) ((Xr Xy) Xx)) % Found (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))) as proof of ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) % Found x100:=(x10 Xy):(((Xr Xx) Xy)->((Xp Xx) Xy)) % Found (x10 Xy) as proof of (((Xr Xx) Xy)->((Xp Xx) Xy)) % Found ((x1 Xx) Xy) as proof of (((Xr Xx) Xy)->((Xp Xx) Xy)) % Found ((x1 Xx) Xy) as proof of (((Xr Xx) Xy)->((Xp Xx) Xy)) % Found x100:=(x10 Xx):(((Xr Xy) Xx)->((Xp Xy) Xx)) % Found (x10 Xx) as proof of (((Xr Xy) Xx)->((Xp Xy) Xx)) % Found ((x1 Xy) Xx) as proof of (((Xr Xy) Xx)->((Xp Xy) Xx)) % Found ((x1 Xy) Xx) as proof of (((Xr Xy) Xx)->((Xp Xy) Xx)) % Found x1000:=(x100 x3):((Xp Xy) Xx) % Found (x100 x3) as proof of ((Xp Xy) Xx) % Found ((x10 Xx) x3) as proof of ((Xp Xy) Xx) % Found (((x1 Xy) Xx) x3) as proof of ((Xp Xy) Xx) % Found (((x1 Xy) Xx) x3) as proof of ((Xp Xy) Xx) % Found (x200 (((x1 Xy) Xx) x3)) as proof of ((Xp Xx) Xy) % Found ((x20 Xx) (((x1 Xy) Xx) x3)) as proof of ((Xp Xx) Xy) % Found (((x2 Xy) Xx) (((x1 Xy) Xx) x3)) as proof of ((Xp Xx) Xy) % Found (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))) as proof of ((Xp Xx) Xy) % Found (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))) as proof of (((Xr Xy) Xx)->((Xp Xx) Xy)) % Found ((or_ind00 ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))) as proof of ((Xp Xx) Xy) % Found (((or_ind0 ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))) as proof of ((Xp Xx) Xy) % Found ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))) as proof of ((Xp Xx) Xy) % Found (fun (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))) as proof of ((Xp Xx) Xy) % Found (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))) as proof of ((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->((Xp Xx) Xy)) % Found (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))) as proof of ((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->((Xp Xx) Xy))) % Found (and_rect00 (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))) as proof of ((Xp Xx) Xy) % Found ((and_rect0 ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))) as proof of ((Xp Xx) Xy) % Found (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))) as proof of ((Xp Xx) Xy) % Found (fun (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))))) as proof of ((Xp Xx) Xy) % Found (fun (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))))) as proof of (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)) % Found (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))))) as proof of (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))) % Found (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3))))))) as proof of (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))) % Found ((conj00 (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))))) as proof of ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))) % Found (((conj0 ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))))) as proof of ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))) % Found ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))))) as proof of ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))) % Found (fun (Xy:a)=> ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))))) as proof of ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))) % Found (fun (Xx:a) (Xy:a)=> ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))))) as proof of (forall (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) % Found (fun (Xr:(a->(a->Prop))) (Xx:a) (Xy:a)=> ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))))) as proof of (forall (Xx:a) (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) % Found (fun (Xr:(a->(a->Prop))) (Xx:a) (Xy:a)=> ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))))) as proof of (forall (Xr:(a->(a->Prop))) (Xx:a) (Xy:a), ((iff ((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) % Got proof (fun (Xr:(a->(a->Prop))) (Xx:a) (Xy:a)=> ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))))) % Time elapsed = 1.238243s % node=225 cost=719.000000 depth=28 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (Xr:(a->(a->Prop))) (Xx:a) (Xy:a)=> ((((conj (((or ((Xr Xx) Xy)) ((Xr Xy) Xx))->(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))) ((forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy)))->((or ((Xr Xx) Xy)) ((Xr Xy) Xx)))) (fun (x:((or ((Xr Xx) Xy)) ((Xr Xy) Xx))) (Xp:(a->(a->Prop))) (x0:((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))))=> (((fun (P:Type) (x1:((forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))->((forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))->P)))=> (((((and_rect (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0)))) P) x1) x0)) ((Xp Xx) Xy)) (fun (x1:(forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (x2:(forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))=> ((((fun (P:Prop) (x3:(((Xr Xx) Xy)->P)) (x4:(((Xr Xy) Xx)->P))=> ((((((or_ind ((Xr Xx) Xy)) ((Xr Xy) Xx)) P) x3) x4) x)) ((Xp Xx) Xy)) ((x1 Xx) Xy)) (fun (x3:((Xr Xy) Xx))=> (((x2 Xy) Xx) (((x1 Xy) Xx) x3)))))))) (fun (x:(forall (Xp:(a->(a->Prop))), (((and (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((Xp Xx0) Xy0)))) (forall (Xx0:a) (Xy0:a), (((Xp Xx0) Xy0)->((Xp Xy0) Xx0))))->((Xp Xx) Xy))))=> ((x (fun (x2:a) (x10:a)=> ((or ((Xr x2) x10)) ((Xr x10) x2)))) ((((conj (forall (Xx0:a) (Xy0:a), (((Xr Xx0) Xy0)->((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))))) (forall (Xx0:a) (Xy0:a), (((or ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0))->((or ((Xr Xy0) Xx0)) ((Xr Xx0) Xy0))))) (fun (Xx0:a) (Xy0:a)=> ((or_introl ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))) (fun (Xx0:a) (Xy0:a)=> ((or_comm_i ((Xr Xx0) Xy0)) ((Xr Xy0) Xx0)))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------